运用SPIN对云环境双向认证协议Nayak的安全性验证

肖美华 梅映天 李 伟

(华东交通大学软件学院 江西 南昌 330013)

运用SPIN对云环境双向认证协议Nayak的安全性验证

肖美华 梅映天 李 伟

(华东交通大学软件学院 江西 南昌 330013)

随着云计算的发展，由欺诈行为驱动的窃取云资源和云服务的行为日趋严重，导致云资源提供商与用户间出现信任危机。Nayak协议是一种改进的云环境双向认证协议，用于保障用户安全登录云服务器，防止第三方恶意窃取用户信息。采用对称密钥密码体系对Nayak协议进行加密，基于Dolev-Yao攻击者模型，提出四通道并行建模法描述攻击者能力。该建模方法解决了Nayak协议并行运行过程中的模型检测问题以及安全隐患，优化了模型复杂度与存储状态数。运用SPIN模型验证工具分析表明采用对称密钥密码体系对Nayak协议加密不安全。此方法可运用于类似复杂协议形式化分析与验证。

Nayak协议 模型检测 四通道并行建模 对称密钥加密

0 引 言

认证属于云安全领域中最需要重视的安全问题之一，其中云认证安全协议涉及到对用户与服务器的双向认证、建立双方的会话密钥等相关技术，保证信息沟通的机密性、完整性、匿名性以及有效性，保证信息不泄露给任何未被授权的用户，保证信息的完整、不被丢失与篡改等，还能保证传输信息的实时有效性。

形式化方法[1]主要包括模型检测[2]与定理证明[3]两个分支，模型检测能够自动验证系统是否满足刻画的性质并且验证速度快、效率高，若不满足性质要求，会提供攻击序列图。SPIN(Simple Promela Interpreter)[4-5]是一种著名的模型验证工具，具有语意清晰、通俗易懂、高效率等特点。1989年SPIN的第一版本问世，主要验证ω-regular属性，1995年引入线性事态逻辑和偏序规约，2001年推出的SPIN4.0支持C语言植入，改善了SPIN的使用局限性，2003年推出的SPIN4.1采用深度优先搜索算法，进一步优化了模型检测的效率。

Nayak等提出一种改进的云环境下双向认证协议方案[6]，成功完成双向认证后协商好了会话密钥;詹丽[7]用BAN逻辑对Nayak协议进行了验证，并发现其中漏洞，但BAN逻辑从方法上看，由于其限制性很大程度上阻碍其分析范围，学者们进行了一系列改进，得到了AT逻辑、GNY[8]逻辑等类逻辑，而文献[7]依旧使用BAN逻辑验证协议安全性，准确度低，代表性弱；从结果来看，使用BAN逻辑对Nayak协议的验证，只能通过逻辑推理证明协议的不安全，不能完全直观地反映协议的运行过程，实际操作性弱。

Maggi等[9]以Needham-Schroeder为例，基于Dolev等攻击者模型[10]，提出一种安全协议模型检测的建模方法。本文针对Nayak协议，对Maggi方法做出改进，以四通道并行建模方式对协议进行建模，并验证Nayak协议是否满足身份认证性质。

1 模型检测技术

模型检测是一种基于有限状态模型并检验该模型的期望特性的技术，为确定检验的系统模型是否某些性质需搜索模型状态空间，若验证性质未满足时，搜索过程将被终止并给出反例。检测结果所得的数据信息对系统设计者排错有极大帮助。目前模型检测技术以其简洁明了、自动化程度高以及实用性强等特性已经在计算机芯片设计、软件可靠性、通信可靠性、通信协议、控制系统等领域得到广泛应用。基本原理如图1所示。

图1 模型检测基本原理图

对于表示系统性质某种时态逻辑公式或者一类有穷状态并发系统，模型检测技术的关键在于是否能找到算法判定系统类中的任一给定系统是否满足公式类中任意给定的一个时态逻辑公式。如图1所示，其算法的输入分别是待验证系统模型M和系统属性φ，若模型M满足性质φ，则给出true结果，否则给出false以及反例详细说明。

模型验证工具SPIN是一个对并发系统进行形式化验证的模型检测工具。它支持promela规约语言并用于验证并发系统进程的正确性。SPIN在仿真模式下可很好地捕捉模型中变量的变化过程，也能方便地可视化仿真过程。对与违法模型性质的反例，在验证模式下会有详细数据说明，在仿真模式下会给出错误轨迹图。2002年，Holzmann(SPIN的设计者)得到了ACM颁发的软件系统开发奖。仿真与验证结构流程见图2。

图2 SPIN仿真与验证结构流程

2 Nayak协议

该协议的主要思想是用户需要注册初始化，然后用户通过双向认证进行授权访问，并且在双向认证过程中通过确认随机数来实现认证。注册阶段抽象协议流程如图3所示。

(1) 当用户需要访问云资源时，需要一个有效的邮箱账号(Email_id)。 用户选择一个合法的用户账号(User_id)，服务器检验该账号是否有效。

(2) 用户输入有效的邮箱账号，服务器通过该账号发送动态口令(Token)给用户，用户输入动态口令。

(3) 服务器检测动态口令以及密码(Pwd),如有效则成功。

(4) 通过单向哈希函数生成的B发送给用户。

图3 注册抽象协议流程

登录与验证抽象协议流程如图4所示。

(1) 用户生成一个随机数Nc，然后通过AES(Advanced Encryption Standard)加密技术生成密钥K得到消息(M_client)，将其发送给服务器。

(2) 服务器收到消息后，对其解密，将解密获得的Nc与随机生成的Ns加密成M_server发送给用户。

(3) 用户收到M_server后解密，检测获得的Nc与拥有的Nc是否相等，相等则认为服务器可信。

(4) 用户将解密获取的Ns用密钥K′加密成消息(M)发送给服务器。

(5) 服务器计算出K′,得到Ns，将其与拥有的Ns进行比对，相等则认为用户和服务器都可信。

图4 登录与验证抽象协议流程

本文将对登录与验证阶段进行研究与分析，由于协议使用对称密钥加密解密，我们可将步骤(1)使用的加密技术得到的密钥K，看成是用户与服务器的共享密钥，步骤(4)使用的加密技术得到的K′，看成用户与服务器的新共享密钥，得到的Nayak协议如下：

(1) client→server:{Nc}Kcs

(2) server→client:{Nc,Ns}Kcs

(3) client→server:{Ns}K_cs

其中Kcs表示用户与服务器的共享密钥， 表示用户与服务器的新共享密钥。

3 Nayak协议建模

本文要验证的协议共有两个合法主体和一个非法主体，分别是Client、Server和Intruder。为了方便，简写成C、S、I。

3.1 四通道并行建模

攻击者模型遵循Dolev-Yao模型,Dolev-Yao规定攻击者可以窃取合法主体发送的所有消息，并能对所窃取的消息进行删除、转发、篡改等。然而，在模型检测中，对攻击者能力的描述可能会出现大量重复子消息项以及忽略多轮协议并行的情况，造成进程间交叉运行所产生的状态迁移量增大，甚至可能发生状态爆炸[11-12]问题。本文以四通道并行建模方式来描述攻击者能力。

模型定义了四个通道：发起者与攻击者两个通道；响应者与攻击者两个通道。

两个合法主体之间是没有通道相连的，因为两个合法主体在进行消息交换时，攻击者总是能窃听或窃取到合法主体发送的所有消息，合法主体所接收的消息总是攻击者发送的。并行建模是指合法主体C、S既扮演了发起者，也扮演了响应者，例如C在发送消息的同时，可能会收到S发送的消息。示意图如图5所示。

图5 四通道并行建模

3.2 诚实主体建模

首先对协议数据项名称进行简化命名，主体名：C、S、I，挑战数：Nc(C作为发起者所用的随机数)、N_c(C作为响应者所用的随机数)、Ns(S作为响应者所用的随机数)、N_s(S作为发起者所用的随机数)，共享密钥：CS、C_S(新共享密钥)。

Nayak协议的诚实主体为Client发起者与Server响应者，proctype PC()、proctype PS()为其对应的进程。四个通道分别是发起者PC的消息通道为ch1与ch2，响应者PS的消息通道为ch3与ch4。

由于协议中传输的消息数不同，发起者PC的通道定义如下：

chan ch1=[0] of {mtype, mtype, mtype};

chan ch2=[0] of {mtype, mtype, mtype,mtype};

同理，响应者PS的通道定义如下：

chan ch3=[0] of {mtype, mtype, mtype};

chan ch4=[0] of {mtype, mtype, mtype,mtype};

其中[0]表示通道中传递数据和接收数据同步。

对本文所用的消息类型做枚举说明：

mtype = {C,S,Nc,Ns,N_c,N_s,R,gD,CS,C_S,,x};

这里符号表示：R为不可识别的主体，x代表任意诚实主体，gD为泛型数据量符号化。

对Client的描述，具体实现代码如下：

{

mtype g1;

mtype g2;

atomic {

IniRunning(self, party);

ch1!self,nonce, CS;

}

atomic {

After investigation, your obedient servants find that on the 25th of the first month of the 36th year of Qianlong, Lifan Yuan presented this memorial:

ch2?g2,eval(nonce), g1, eval(CS);

IniCommit(self, party);

ch1! self,g1,C_S;}}

在PC发起者进程中，self与party分别表示消息发起者与接收者，g1、g2表示泛型变量，发起者一共完成了两次发送操作和一次接收操作。其中发送消息语句ch1？self,nonce,CS的含义是：self(发送者C)发送自己的随机数，用C与S的共享密钥加密。atomic表示promela语言定义的原子序列语法规则，运用该语法规则可使进程交叉运行次数减少，把接收操作与下一次发送操作放在一个atomic中同时完成，能有效地减少状态空间。原子谓词表示协议的性质，原子谓词变量的值由模型的宏定义来更新记录，IniRunning、IniCommit和ResRunning、ResCommit为模型程序中定义的四个宏，其中IniRunning表示发起者与响应者会话，IniCommit表示发起者提交了与响应者的会话，宏定义如下：

#define IniRunning(x,y) if

::((x==C)&&(y==S))->IniRunningCS=1

::((x==S)&&(y==C))->IniRunningSC=1

:: else skip

fi

#define IniCommit(x,y) if

::((x==C)&&(y==S))->IniCommitCS=1

::((x==S)&&(y==C))->IniRunningSC=1

:: else skip

fi

#define ResRunning(x,y) if

::((x==C)&&(y==S))->ResRunningCS=1

::((x==S)&&(y==C))->ResRunningSC=1

:: else skip

fi

#define ResCommit(x,y) if

::((x==C)&&(y==S))->ResCommitCS=1

::((x==S)&&(y==C))->ResCommitSC=1

:: else skip

fi

3.3 运用LTL公式刻画Nayak协议安全性质

LTL线性时态逻辑[13-14]被运用于描述协议所需要满足的属性，通过判断所建立的模型是否满足所描述的属性公式来验证协议的安全性。

模型的每一条性质都需要用一个promela全局变量表示，初始化操作如下所示：

bit IniRunningCS = 0;bit IniCommitCS = 0;

bit ResRunningCS = 0;bit ResCommitCS = 0;

bit IniRunningSC = 0;bit IniCommitSC = 0;

bit ResRunningSC = 0;bit ResCommitSC = 0;

其中IniRunningCS表示client发起与server的会话，初始值为0表示client没有发起与server的会话，IniCommitCS表示client提交与server的会话，初始值为0表示client没有提交与server的会话，其他与之类似。

根据3.2节给出的所有属性描述函数的定义与属性变量的初始化，用户与服务器间的身份认证属性具体描述如下：

C必须在S发起会话后才能提交与S的对话或者S从来没有发起与C的会话，LTL(线性时态逻辑)刻画如下：

([](([]!IniCommitCS)||(!IniCommitCS U

ResRunningCS)))

S必须在C发起会话后才能提交与C的对话或者C从来没有发起与S的会话，LTL(线性时态逻辑)刻画如下：

([](([]!IniCommitSC)||(!IniCommitSC U

ResRunningSC)))

将这两个LTL公式运用逻辑符连接后得到完整LTL属性描述：

([](([]!IniCommitCS)||(!IniCommitCS U

ResRunningCS)))&&([](([]!IniCommitSC)||

(!IniCommitSC U ResRunningSC)))

3.4 攻击者建模

攻击者建模通常是模型检测中最重要的一部分，攻击者能力的强弱也会直接影响模型检测的效果以及效率。根据Dolev-Yao模型构建攻击者知识库函数，把攻击者获取的知识提取出来，建立单独的知识库存储攻击者知识，攻击者根据这些知识伪造、转发消息。构建攻击者知识库函数需要找到攻击者需要表示的知识，而攻击者可以学会的知识集合A与攻击者需要学会的知识集合B的交集即攻击者需要表示的知识，具体如下：

攻击者可以学会的知识：由诚实主体的发生语句所得。

ch1!self,nonce, CS;

ch1! self,g1,C_S;

ch4!self,g1, nonce, CS;

利用静态分析法缩减随机变量的取值范围，降低搜索状态数，例如client将随机变量g1用新共享密钥C_S加密发送给server，对于client来说，它不确定g1是不是server的随机数，因此变量g1取值范围为{Nc,N_c,Ns,N_s}，nonce的取值范围为{Nc，N_s},响应者进程中变量g1取值范围为{Nc,N_c,Ns,N_s},具体如表1。

表1 攻击者可以学会的知识

攻击者需要学会的知识:由诚实主体的接收语句所得。

ch2?g2,eval(nonce), g1, eval(CS);

ch3 ?g2,g1, eval(CS);

ch3?g3,eval(nonce),eval(C_S);

利用静态分析法分析得出，发起者进程中nonce取值范围为{Nc,N_s}，变量g1取值范围为{Nc,N_c,Ns,N_s}，响应者进程中变量g1取值范围为{Nc_,Ns}，具体如表2。

表2 攻击者需要学会的知识

表1与表2的交集即攻击者需要表示的知识项:

{Nc}Kcs,{N_s}Kcs,{N_c}K_cs,{Ns}K_cs,{Nc,Ns}Kcs,{Nc,N_c}Kcs,{N_s,Ns}Kcs,{N_s,N_c}Kcs

根据以上分析，攻击者模型的代码框架如下：

proctype PI() {

bit k_Nc_CS=0;

…

bit k_N_s_N_c_CS=0;

/*需要表示的知识初始化*/

mtype x1;mtype x2;mtype x3;

do

::ch2!x,Nc,Ns,(k_Nc_Ns_CS->CS:R)

::ch4!x,Nc,Ns,(k_Nc_Ns_CS->CS:R)

::ch2!x,Nc,N_c,(k_Nc_N_c_CS->CS:R)

::ch4!x,Nc,N_c,(k_Nc_N_c_CS->CS:R)

::ch2!x,Ns,Ns,(k_N_s_Ns_CS->CS:R)

::ch4!x,N_s,Ns,(k_N_s_Ns_CS->CS:R)

::ch2!x,N_s_,N_c,(k_N_s_N_c_CS->CS:R)

::ch4!x,N_s_,N_c,(k_N_s_N_c_CS->CS:R)

::ch3!x,Nc,(k_Nc_CS->CS:R)

::ch1!x,Nc,(k_Nc_CS->CS:R)

::ch3!x,N_s_,(k_N_s_CS->CS:R)

::ch1!x,N_s_,(k_N_s_CS->CS:R)

::ch3!x,N_c_,(k_N_c_C_S->C_S:R)

::ch1!x,N_c_,(k_N_c_C_S->C_S:R)

::ch3!x,Ns,(k_Ns_C_S->C_S:R)

::ch1!x,Ns,(k_Ns_C_S->C_S:R)

::d_step { ch2? _,x1,x2,x3->k2(x1,x2,x3);

x1 = 0;x2 = 0;x3 = 0; }

::d_step { ch4? _,x1,x2,x3->k2(x1,x2,x3);

x1 = 0;x2 = 0;x3 = 0; }

:: d_step { ch1 ? _,x1,x2->k1(x1,x2);

x1 = 0;x2 = 0; }

:: d_step { ch3 ? _,x1,x2->k1(x1,x2);

x1 = 0;x2 = 0;}

od}

4 实验结果与分析

使用SPIN验证工具对上述模型进行验证，发生了属性违反，自动生成了并行攻击路径，攻击序列图如图6所示。

图6 攻击序列图

得到如下攻击序列：

C→I:{Nc}Kcs I→C:{Nc}Kcs

C→I:{Nc,N_c}Kcs I→C:{Nc,N_c}Kcs

C→I:{N_c}K_cs I→C:{N_c}K_cs

协议开始运行时，发起者C将Nc(C作为发起者所用的随机数)以CS共享密钥加密发送给攻击者，这样攻击者I就掌握了相关信息，随后发起者C又将N_c(C作为响应者所用的随机数)以CS共享密钥加密发送给攻击者，攻击者I冒充了响应者S与发起者C进行了三次会话。然而，响应者S与发起者C却并不知情，这就表明该协议充满危险性。

如图7所示，ResCommitCS,ResRunningCS，IniCommitSC,IniRunningSC为0，IniCommitCS，IniRunningCS,ResCommitSC,ResRunningSC为1，表示在整个协议运行中，发起者(响应者)C开始并提交与响应者(发起者)S的会话，但响应者(发起者)S没有参与或提交一次会话。

图7 性质违反信息

图8描述单个全局系统状态需要64字节的内存，检测后状态树的高度达到27层，并且检测到1项错误。transitions和states-stored的数量越少表示状态迁移量越少，系统存储的状态量越少，验证效率越高，且不易引起状态爆炸。state-vector和depth-reached属性表示状态矢量数和深度优先搜索的深度，数量越少表明模型越优秀，检测效率越高。并且，从图8可知，本文构建的模型并未出现状态爆炸等情况。

图8 模型验证结果信息

5 结 语

随着信息网络的快速发展，云服务走进人们的视野。与此同时，因云环境的开放性等特点给云计算的安全带来极大的挑战。因此，云安全协议为了能够有更多功能和更强大的安全性，也需更为复杂。本文以Nayak协议为例，采用对称密钥密码体系对Nayak协议进行加密，提出四通道并行建模法对协议建模，该建模方法适用于多协议或多主体并行运行的环境，有效缓解了状态爆炸问题。最后运用SPIN模型检测工具找到一条攻击路径，发现协议中存在的安全漏洞。下一步研究将尝试对Nayak协议进行改进，并对其安全性进行验证。

[1] Xiao M,Jiang Y,Liu Q.On formal analysis of cryptographic protocols and supporting tool[J].Chinese Journal of Electronics,2010,19(2):223-228.

[2] Clarke E M.Model checking[M].Cambridge,MA:MIT Press,1999.

[3] Xiao M,Ma C,Deng C,et al.A Novel Approach to Automatic Security Protocol Analysis Based on Authentication Event Logic[J].Chinese Journal of Electronics,2015,24(1):187-192.

[4] Holzmann G J.The model checker SPIN[J].IEEE Transactions on software engineering,1997,23(5):279-295.

[5] Xiao Meihua,Wan Zilong,Liu Hongling.The Formal Verification and Improvement of Simplified SET Protocol[J].Journal of Software,2014,9(9):2302-2308.

[6] Nayak S K,Mohapatra S,Majhi B.An Improved Mutual Authentication Framework for Cloud Computing[J].International Journal of Computer Applications,2012,52(5):36-41.

[7] 詹丽.云计算中基于Smartcard的双向认证安全协议的研究与形式化分析[D].广州:暨南大学,2014.

[8] 马成林,肖美华,邓春艳,等.基于改进GNY逻辑的Kerberos*协议安全性分析[J].计算机与数字工程,2014(10):1758-1762,1882.

[9] Maggi P,Sisto R.Using SPIN to verify security properties of cryptographic protocols[M]//Model Checking Software.Springer Berlin Heidelberg,2002:187-204.

[10] Dolev D,Yao A C.On the security of public key protocols[J].Information Theory,IEEE Transactions on,1983,29(2):198-208.

[11] 侯刚,周宽久,勇嘉伟,等.模型检测中状态爆炸问题研究综述[J].计算机科学,2013,40(6A):77-86,111.

[12] Groote J F,Kouters T W D M,Osaiweran A.Specification guidelines to avoid the state space explosion problem[J].Software Testing,Verification and Reliability,2015,25(1):4-33.

[13] Barnat J,Cerná I.Distributed breadth-first search LTL model checking[J].Formal Methods in System Design,2006,29(2):117-134.

[14] Xiao M,Bickford M.Logic of Events for Proving Security Properties of Protocols[C]//International Conference on Web Information Systems and Mining.IEEE Computer Society,2009:519-523.

SECURITYVERIFICATIONOFMUTUALAUTHENTICATIONPROTOCOLNAYAKINCLOUDENVIRONMENTWITHSPIN

Xiao Meihua Mei Yingtian Li Wei

(SchoolofSoftware,EastChinaJiaotongUniversity,Nanchang330013,Jiangxi,China)

With the development of cloud computing, the behavior of cloud resources and cloud services driven by fraud is becoming more and more serious, leading to cloud trust crisis between resource providers and users. Nayak protocol is an improved mutual authentication protocol in cloud environment, it used to protect the user’s security login cloud server and prevent the third-party malicious theft of user information. We use the symmetric key cryptosystem to encrypt the Nayak protocol. On the basis of Dolev-Yao attacker model, we propose a four-channel parallel modeling method to describe the attacker’s ability. The modeling method solved the problem of model detection and security hidden trouble while Nayak protocol run in parallel, and optimized the model complexity and storage state. We introduced the SPIN model validation tools in this paper. The validation tool analysis shows that the symmetric key cryptography is not secure for Nayak protocol encryption. This method can be applied to formal analysis and verification of similar complex protocols.

Nayak protocol Model checking Four-channel parallel modeling method Symmetric-key cryptography

TP309

A

10.3969/j.issn.1000-386x.2017.10.053

2016-11-17。国家自然科学基金项目(61163005，61562026)；计算机软件新技术国家重点实验室开放课题项目(KFKT2012B18)；江西省自然科学基金项目(2013BAB201033)；江西省高校科技落地计划项目(KJLD13038)；江西省对外科技合作技术项目(20151BDH80005)；华东交通大学研究生创新计划项目(YC2014-X007)。肖美华，教授，主研领域：信息安全，软件形式化方法。梅映天，硕士生。李伟，硕士生。