NSSK协议的SPIN模型检测

黄鹏

摘要：安全协议是以密码学为基础的消息交换协议。针对传统的改进NSSK安全协议，通过使用Promela语言对协议进行建模，并使用SPIN模型检测工具进行验证，发现仍然存在安全漏洞，攻击者可以冒充合法者进行通信。針对上述缺陷，提出了一种有效的改进方案，主要是在协议中增加了自身产生的随机数和发送者的身份标识，该改进方案提高了协议安全性。

关键词：安全协议； 安全漏洞；NSSK；SPIN；模型检测

DOIDOI：10.11907/rjdk.171239

中图分类号：TP309文献标识码：A文章编号：16727800（2017）010018504

0引言

如今，随着信息逐渐成为重要的战略资源，信息化水平已成为衡量一个国家现代化水平和综合国力的重要标志。同时，信息安全问题也成为人们重点关注的一个问题。安全协议是以密码学为基础的消息交换协议，其目的是在网络环境下提供各种安全服务。安全协议可以分为密钥交换协议、认证协议、电子商务协议、安全多方计算协议等多种类型。简单安全协议虽然只是简单消息的传递，但消息之间存在微妙、复杂的关系。NSSK协议[12]是一个经典的认证密码协议，不少学者在NSSK协议研究中提出了一些NSSK认证方案，但这些方案也不是完全安全的，仍然存在风险。2014年Hu等主要根据GSMR系统现有的安全威胁和必须采取的安全措施，采用一种改进的NSSK安全协议来保障车载设备与RBC之间的安全通信。通过分析发现，其存在着一些安全缺陷，因此提出了改进方案。

本文使用SPIN模型检测工具对NSSK协议的改进方案进行验证和分析，发现存在着攻击。因此，针对该攻击提出一种改进方案，以提高协议安全性。

1模型检测及工具SPIN

系统的设计和验证需要SPIN模型检测器的支持，首先形式化描述整个系统模型，对模型进行分析，发现语法错误，如果没有发现语法错误，则需要对系统进行交互模拟运行，直到系统设计达到预期为止。然后，SPIN会生成一个优化的onthefly验证程序，该程序将被编译后执行，如果在执行过程中发现了任何违背正确性的反例，则会返回交互模拟执行状态，继续进行检测诊断，以确定产生反例的原因。因此，它的建模方法是：定义进程模板，将每个进程模板的行为视为一种行为规范，实际系统可以被看作一个或多个异步进程模板实例的组合。SPIN是一种基于计算机科学的形式化方法，它将先进的理论验证方法应用于大型软件系统的验证中，目前在工业界和学术界得到了广泛应用。

SPIN的基本结构如图1所示，其描述了整个检测过程。

2协议介绍

2.1NSSK协议原理及存在的问题

NSSK协议是一个经典的认证密码协议。协议先通过对两个主体的身份进行认证，通信主体需要经过5个阶段的通信过程，才能获得安全通信过程的会话密钥。

协议符号说明：A表示用户A的身份标识；B表示用户B的身份标识；S表示服务器；Nb表示用户B产生的随机数；Na表示用户A产生的随机数；Kbs表示用户B与S之间的共享密钥；Kas表示用户A与S之间的共享密钥；Kab表示用户A和用户B的会话密钥。

协议的步骤如下：

（1）A→S：A，B，Na

（2）S→A：{Na，B，Kab，{Kab，A}Kbs}Kas

（3）A→B：{Kab，A}Kbs

（4）B→A：{Nb}Kab

（5）A→B：{Nb-1}Kab

在此协议中，用户A和用户B进行秘密通信，用户A会向服务器S请求分配一个会话密钥来保证通信内容的秘密性。协议前3个消息主要是服务器分配会话密钥给合法用户，后两个消息主要是合法用户之间的相互验证。

具体过程为：①协议开始时，合法用户A将用户A的身份标识、用户B的身份标识以及用户A产生的随机数Na组成消息1，发送给服务器S，告诉服务器它将与用户B进行通信；②服务器S在接收到消息1时，随机产生一个Kab，这是为双方分配的会话密钥，同时将A的身份标识和Kab用B的密钥Kbs加密生成一个证书，然后将证书、用户A在消息1发送的Na、用户B的身份标识和会话密钥Kab用A的密钥Kas加密组成消息2发送给A；③用户A接收到消息2时，用密钥Kas解密消息得到会话密钥Kab和证书{Kab，A}Kbs，然后再将证书组成消息3发送给用户B；④用户B接收到消息3时，用密钥Kbs解密得到会话密钥Kab，再用Kab加密自身产生的随机数Nb组成消息4，发送给用户A；⑤用户A接收到消息4后，用会话密钥Kab解密得到Nb，再将Nb与1进行运算后，将得到的结果用Kab进行加密组成消息5发送给用户B。这里的Nb-1可以用Nb来代替，只是用来区别消息4，而消息4和消息5是为了防止中间人攻击。

在此协议中，在消息4中用户A是通过Nb来确认用户B的身份，在消息5中用户B是通过Nb-1来确认用户A的身份。这里的Kab表示用户A和用户B之间的会话密钥，只有用户A和用户B可以对其解密。

该协议比较简单，实现起来也较为容易，但在文献[8]中，Denning和Sacco在1981年发现了一个攻击，发现此协议不能抵抗“新鲜性”攻击，如果一个攻击者拥有过期的会话密钥，能够冒充用户A，通过重放消息3，来实施以下攻击：

（1）A→S：A，B，Na

（2）S→A：{Na，B，Kab，{Kab，A}Kbs}Kas

（3）I（A）→B：{ K′ab，A}Kbs

（4）B→I（A）：{N′b}K′ab

（5）I（A）→B：{N′b-1}K′ab

其中，I（X）表示攻击者可以冒充合法用户X接收和发送消息。通过上面的攻击过程，使合法用户B相信自己得到的会话密钥K′ab是执行当前协议回合的结果。因此，该攻击是有效的。endprint

在2001年，王贵林、卿斯汉等在文献[12]又提出攻击者可以冒充合法用户B实施以下攻击：

（1）A→S：A，B，Na

（2）S→A：{Na，B，Kab，{Kab，A}Kbs}Kas

（3）A→I（B）：{Kab，A}Kbs

（4）I（B）→A：NI

（5）A→I（B）：{{NI}K-1ab-1}Kab

其中，NI和{Nb}Kab格式相同，攻击者冒充用户B发送消息给用户A，用户A收到消息4，然后对其进行所谓的解密，并将得到的结果与1进行运算后，将运算后的结果用Kab加密发给用户B。用户A以为用户B知道了会话密钥，但实际上，B根本没有参加整个协议的执行过程，甚至可能还是离线的。因此，该攻击是有效的。

2.2协议改进方案

文献[7]分析了NSSK协议后，提出一种改进方案，该方案采用的符号与原协议相同，而且消息形式与原协议相似，修改后的完整协议简单描述如下：

（1）A→S：A，B，Na。用户A通过发送消息1给服务器S，它将与用户B进行通信，主要将用户A的身份标识、用户B的身份标识和用户A产生的随机数Na组成消息1提供给服务器S。

（2）S→B：A。当服务器S接收到消息1后，随即发送A的用户标识给用户B。S通过发送消息告诉用户B，用户A要与其进行通信。

（3）B→S：{ Nb} Kbs。当用户B接收到消息2后，知道用户A将与它通信，然后将自身产生的随机数Nb用密钥Kbs进行加密组成消息3，将其发送给服务器S。

（4）S→A：{ Na ，B，Kab} Kas。当服务器S收到消息3后，将用户A产生的随机数Na、用户B的身份标识、用户A与用户B之间的密钥Kab用A的密钥Kas进行加密，组成消息4发送给用户A，告诉用户A，用户B已经准备好与之通信。

（5）S→B：{ Nb ，A，Kab} Kbs。服务器S收到消息3后，解密消息3得到Nb，然后再将用户B的随机数Nb、用户A的身份标识、用户A与用户B之间的密钥Kab用B的密钥Kbs进行加密，组成消息5发送给用户B，通知用户B，用户A已经准备好与之通信。

（6）B→A：{N′b}Kab。当用户B接收到消息5后，将自己产生的随机数N′b用会话密鑰Kab加密组成消息6，再发送给用户A。

（7）A→B：{N′b-1}Kab。当用户A接收到消息6后，用会话密钥Kab解密消息6，得到N′b，然后将N′b与1计算后得到N′b-1，用会话密钥Kab加密N′b-1组成消息7，再发送给用户B。

此改进协议也是用户A通过N′b来确认用户B的身份。同样，用户B通过N′b-1来确认用户A的身份。

3改进协议Promela建模及分析

3.1攻击者建模

攻击者[11]可以根据自身的知识能力对网络和信息采取敌意的行为，其可以具备如下知识能力：①在合法主体通信过程中，对其进行截获或者转发任何消息；②可以冒充合法用户或服务器参与协议运行；③可以对协议里的任何消息进行解密和加密；④可以对协议里的任何消息进行重构，通过重构消息来试图欺骗用户和服务器。

3.2协议系统属性

NSSK协议及其改进方案都是在秘密状态下，用户与用户之间身份的相互鉴别，同时协商了会话密钥，所以该协议必须满足认证性和秘密性。认证性的含义为：A与B如果成功运行了一次协议，那么用户A要相信通信对方就是用户B，同时用户B相信通信对方就是用户A，即通信双方的真实身份要相互鉴别。用LTL公式表示如下：

[]（（statusA==ok&&partnerA==responserID）？（statusB=ok&&partnerB==askerID））

其中&&表示逻辑与，←→表示逻辑等价，[]表示always。

秘密性的含义为：要确保需要加密的协议消息内容在传送过程中不被攻击者非法窃取。根据协议特点，从消息3到消息7都有密钥进行加密，攻击者无法获得其随机数N′b，也无法冒充用户或服务器进行攻击。因此，只要成功运行了一次协议，LTL公式则能保证其秘密性。

3.3验证结果分析

通过模型检测工具Xspin检测改进后的协议可发现漏洞，并得到入侵者的攻击路径。入侵者利用获得的消息，重构消息冒充B与A通信，最终使A误认为它与B通信，其实是I与之进行通信，成功地对其进行了攻击。

其中askerID代表A的身份标识，responserID代表B的身份标识，nonceA、nonceI分别代表A、I产生的随机数，nonceB1和nonceB2分别代表B在协议消息1和消息6产生的随机数，keyAB代表A与B之间的会话密钥，keyBS代表B的密钥，keyAS代表A的密钥，key代表I产生的密钥，temp代表空值。为了简化建模过程，最后一步验证消息没有减1。攻击路径如图2所示。

图2协议改进受攻击轨迹

由图2得知入侵者攻击时序如下：

（1）A→S：A，B，Na

（2）S→B：A

（3）B→S：{ Nb} Kbs

（4）S→A：{ Na，B，Kab} Kas

（5）S→I（B）：{ Nb，A，Kab} Kbs

（6）I（B）→A：NI

（7）A→I（B）：{{NI}K-1ab-1}Kab

攻击过程描述如下：攻击过程的前4个消息都是A、S、B接收消息或转发消息，攻击过程主要是在后面3个消息中：先是入侵者I冒充用户B发送NI给A，其中NI与{N′b}Kab格式相同，A接收到消息6后对其进行所谓的解密，得到结果后，将结果与1运算后用Kab加密后组成消息7发送给B，I将其截获。endprint

通过上述分析，在文献[7]的改进协议中，前5个消息是分配会话密钥，在消息4和消息5分别加上了随机数，从而可以抵抗文献[8]提出的新鲜性攻击。但发现的攻击与王贵林、卿斯汉等在文献[12]发现的攻击类似，B在消息4之后就没有收到消息，一直在等待消息，但A不知B在等待消息，以为它还在与B进行通信，其实I在与A进行通信，攻击有效，所以说其无法抵抗该攻击。

3.4NSSK协议改进

NSSK协议受攻击的原因是，文献[7]改进的协议消息6太过简单，容易被重构骗过合法的参与者。

针对上述攻击，对协议的改进如下：

（1）A→S：A，B，Na

（2）S→B：A

（3）B→S：{ Nb} Kbs

（4）S→A：{ Na ，Nb，B，Kab} Kas

（5）S→B：{ Na，Nb，A，Kab} Kbs

（6）B→A：{Nb，Na，B}Kab

（7）A→B：{Nb-1，Nb，A}Kab

对其改进的协议进行建模，改进的协议和文献[7]改进协议格式相同，只是传递的消息内容有所差别，建模过程和上文的建模过程相似，用模型检测工具Xspin对上述改进后的协议进行验证，验证结果如图3所示。

图3对改进NSSK协议的验证结果

通过验证结果发现，结果显示错误为0，则新改进的协议没有发现漏洞，说明新改进的协议是安全的。

3.5改进方案安全性分析

定理1改进方案能加强双向认证。

证明在協议的后两条消息中分别加上了自己之前产生的随机数，在消息6中，当合法用户A解密消息得到自己的随机数和B的身份标识，才会相信是用户B发来的消息，在消息7中原理相同。因此，该协议能够加强双向认证。

定理2改进方案能抵抗中间人攻击。

证明对于文献[7]的改进协议，主要是消息6容易被攻击者篡改，伪装攻击欺骗合法用户，所以在消息6和消息7中分别增加前面产生的随机数和身份标识，如果解密消息不是自己产生的随机数和身份标识，用户会拒绝该消息，攻击者则无法重构信息来欺骗合法用户。因此，改进方案能抵抗中间人攻击。

定理3改进方案能够抵抗重放攻击。

证明对于文献[7]的改进协议，攻击者截取到消息6后，会重放该消息来骗过合法用户，所以在消息6加上合法用户前面产生的随机数和身份标识，如果解密消息得不到期望的消息，用户会拒绝该消息，使攻击者无法通过重放消息6来欺骗合法用户。因此，改进方案能抵抗重放攻击。

4结语

本文使用Promela语言对NSSK协议[7]的改进方案进行建模，根据协议必须满足的安全性质描述（LTL公式、断言）进行验证，用模型检测工具Xspin进行检测，成功地找出了反例。通过分析攻击序列产生的原因，给出了一种修改方案。通过验证和分析发现，改进后的协议可以满足安全协议要求。SPIN模型检测技术是分析安全协议的有效工具，下一步工作可以使用SPIN工具检测和改进其它安全协议。

参考文献参考文献：

[1]LIAO J， ZHU B， YONG H. Security analysis of NSSK protocol and its improvement[C].Eighth IEEE International Conference on Dependable， Autonomic and Secure Computing， Dasc 2009， Chengdu， China， DBLP， 2009：115118.

[2]CHEN L， WANG W. An improved NSSK protocol and its security analysis based on logic approach[C]. International Conference on Communications， Circuits and Systems. IEEE， 2008：772775.

[3]TINGYUAN L， XIAODONG L， ZHIGUANG Q， et al. An improved security protocol formal analysis with BAN logic[C].International Conference on Electronic Commerce and Business Intelligence. IEEE Xplore， 2009：102105.

[4]WANG X， YUAN C W. Formal analysis method of security protocol[J]. Computer Engineering， 2010， 36（7）：8284.

[5]CHEN H，CLARK J A，JOCOB J L.A searchbased approach to the automated design of security protocols，YCS 376[R].New York：University of York，Department of Computer Science，2004.

[6]LERDA F， SISTO R. Distributedmemory model checking with SPIN[C]. SpringerVerlag， 1999：2239.

[7]胡晓辉，陈慧丽，石广田，等.CTCT4级安全通信协议的形式化建模与验证[J]. 计算机工程与应用， 2014，50（4）：8185.

[8]DENNING D E， SACCO G M. Timestamps in key distribution protocols[J]. Communications of the Acm， 1981，24（8）：533536.

[9]王巧丽.SPIN模型检测的研究与应用[D].贵阳：贵州大学，2006.

[10]杨霓霏，刘晓斌，卢佩玲，等.CTCS3级列控系统车地无线通信消息认证和加密技术的研究[J].铁道通信信号，2010，46 （10）：15.

[11]尤启房，杨晋吉.SIP协议的SPIN模型检测[J].计算机工程与应用，2014，50（13）：8789.

[12]王贵林，卿斯汉，周展飞.认证协议的一些新攻击方法[J].软件学报，2001，12（6）：907913.

[13]万子龙.基于模型检测的SET协议形式化验证与改进[D].南昌：南昌大学，2014.

[14]李翠翠.基于SPIN模型检测的电子商务协议分析与验证[D].上海：华东理工大学，2012.

责任编辑（责任编辑：黄健）endprint