基于SPIN的安全协议形式化验证方法

1引言

随着计算机技术的发展，人类进入了信息时代，信息技术已经渗透到了人们日常生活的方方面面，然而信息在开放的网络环境中传输会遭到各种各样的攻击，如偷听攻击、截取攻击、伪造攻击、篡改攻击等。这些攻击的存在在不同程度上损害了网络用户的利益。因此为了确保信息安全，人们设计出了安全协议来保证通信过程的安全可靠。安全协议是一个分布式算法，它规定了两个或两个以上的协议主体在一次通信过程中必须要执行的一系列步骤。利用安全协议人们来实现在开发网络中的安全通信。可以说安全协议是信息安全的基础，其自身的安全问题已成为安全研究的重要内容。目前，在安全协议验证领域存在多种验证方法如模拟、形式化等，模拟的方法存在不能100%覆盖的缺陷，而形式化能够达到覆盖率100%而且具有严密的数学基础，因而越来越受到业内人士的信赖。形式化验证主要有两种验证方法定理证明和模型检测两种方法。定理证明的基本思想是将安全协议描述为公理系统，安全协议的安全目标则表示成需要证明的定理，安全协议是否符合安全目标则对应于公理系统中的目标定理是否成立。定理证明的最大优势是协议运行期间不会出现状态爆炸的问题。缺点是，对使用者的技术要求较高，需专业人士才能驾驭，而且自动化程度不高，需要人工干预。模型检测的基本思想是，把安全协议看成一个分布式系统，单个协议实体涉及的协议执行部分为局部状态，所有局部状态构成了分布式系统的全局状态。在安全协议的全局状态上定义安全属性，安全协议是否满足安全属性等价于系统可达的每个全局状态上安全属性都能够得到满足。模型检测可实现全自动的执行，人的干预较少操作简单易实行，但模型检测会出现状态空间爆炸的情况，这种情况制约了模型检测技术的发展。SPIN这种模型检测工具利用on-the-fly技术可以有效的缓解状态空间爆炸问题，SPIN模型检测工具的基本思想是将协议表示成一自动机的形式，并且将待验证属性表示为另一自动机，然后求这两个自动机的同步积。通过遍历求同步积后产生的新的状态机的整个状态空间，检查协议是否满足我们期望的性质描述。如果不满足则返回错误并提供导致错误的状态迁移路径，我们将通过错误路径来定位错误。本文详细介绍了模型检测工具SPIN的工作原理，并给出了一个基于SPIN模型检测工具的简单安全协议的形式化描述和分析。

2SPIN的工作原理

SPIN作为一种验证反应式并发系统逻辑一致性的工具，已广泛应用到航空、核电、网络信息安全等众多领域中。它首先把用Promela建模语言，通过进程、变量和消息通道等描述的待验证系统，以及以LTL或断言描述的待验证属性，作为输入，然后把Promela描述的待验证系统中每个进程转化为一个有限自动机并对这些有限自动机进行异步积运算得到优先自动机A，同时把LTL表达式取反并转换为一个自动机B，最后对自动机A和自动机B进行同步积运算得到自动机C。SPIN通过内嵌的搜索算法对自动机C进行穷尽搜索，在搜索的过程中SPIN通过on-the-fly技术以及偏序简化技术对状态空间进行简化，当搜索完毕显示自动机C所能接受的语言为空，表示待验证系统满足LTL表达的属性，反之则不满足。若在检测过程中，发现了违背待验证属性的反例，返回到交互模拟执行状态再继续仔细诊断，定位错误原因。

2.1待验证属性的描述

对于待验证属性的描述一般使用LTL公式。LTL就在命题逻辑的基础上加入了时序操作符：G：表示永远为真。F：表示最终为真。X：表示下一个时刻为真。U：表示直到某刻前一直为真。R：表示到了某刻才为真。时序逻辑只在乎事件发生的先后顺序，不在乎事件发生的时间间隔。每一个LTL公式都可以表达为一个buchi自动机，在SPIN中用neverclaim来描述buchi自动机。时序逻辑提高了对于系统在时间顺序上的行为的公式化描述，有了这些操作符，我们就可以方便地描述系统的时态性质了。断言也可以作为一种描述待验证属性的方法，如可以验证在某个状态下某个性质是否成立，是否存在无意义的空转等。

2.2Promela(PROcessMetaLanguage)建模语言

Promela语言不是一种设计语言，它是一种系统描述语言。它是用来对有限状态系统进行建模的形式描述语言．由于Promela提供对数据结构与c代码嵌入方面的支持，可以很好地形式化描述协议．一个Promela(processmetalanguage)模型由类型(type)、通道(channe1)、变量(variable)与进程(process)构成。Promela允许动态创建并行的进程，并且可以在进程之间通过消息通道进行同步或异步通信．同步使用会面点(rendezvousport)进行通信，而异步使用缓冲(bufers)进行通信．由此可以看出它是一种面向反应式系统的描述语言,而安全协议属于典型的反应式系统，因此用Promela语言来描述协议系统是可行的、方便的。对于待验证属性我们可行使用LTL、never以及断言等来描述。

3用SPIN验证协议的过程

基于SPIN的安全协议验证，我们首先依据Dolev-Yao模型构造协议主体及攻击者模型然后对它们进行交叉复合来构造整个模型。协议的一次运行包括所有协议主体所有动作的交叉序列。主要步骤:(1)用Promela语言描述各个协议主体，定义协议的各个元素的数据类型，定义协议主体的行为动作。由于各个协议主体具有并发性，因而使用进程来描述各个协议主体。在进程内部通过协议的各个元素及协议主体的行为动作对协议主体进行描述，进程与进程间通过信道进行交互。(2)以进程的形式为系统增加工具者。根据Dolev-Yao模型假设攻击者能够监听和截取网络中的每一条消息而且能够向其他协议主体发送新的消息。依据攻击者假设通过协议的各个元素及攻击者的行为动作对攻击者进行Promela描述(3)用LTL公式描述协议需要验证的数据机密性属性要求。(4)运行SPIN进行语法检查。(5)运行SPIN验证器进行属性验证(6)观察协议的运行结果，发现协议的问题。SPIN可以产生一个错误跟踪文件，我们能够根据这个文件通过SPIN提供的模拟功能还原协议执行时产生的问题。

4实例分析

4.1协议的简化的描述

在用户Alice和Bob不知道对方私钥的情况下，用户Alice希望采用公钥密码技术向Bob发送一条秘密消息，协议使用RSA公钥加密算法。该协议利用了RSA算法加密和解密是互反而且可交换的性质。协议流程如下：（1）Message1:Alice-Bob:{X}pk_Alice（2）Message2:Bob-Alice:{{X}pk_Alice)pk_Bob（3）Message3:Alice-Bob:{X}pk_Bob其中Alice,Bob是协议的通信个体，其中Alice为协议的发起者，Bob为协议的响应者。X为发送的消息。pk_Alice,pk_Bob分别是Alice和Bob的公钥，用于加密消息。协议流程如下：首先，发起者Alice将消息X用自己的公钥加密后发送给Bob,然后当Bob接收Alice发来的秘文消息后，由于它没有Alice的私钥，所以不能解读收到的消息，它用自己的公钥将接收到的密文消息再次加密后发送给Alice。Alice根据RSA算法的交换性质解除自己的加密后得到{X}pk_Bob，并将该消息发送给用户Bob，用户Bob接收到该消息后，利用自己的私钥解密，从而得到消息X。表面上看，通过该协议用户Alice和Bob可以进行安全通信；然而事实上是攻击者Eve可以通过截获Alice和Bob之间的消息，并插入一些自己的消息来达到获取机密信息甚至是破坏的目的。

4.2协议的系统模型以及Promela描述

以Dolev-Yao模型为依据对协议系统进行建模。假设协议主体在拥有了正确的秘钥时才可以解码，并且产生的密文必须拥有相应的明文和秘钥，攻击者无法破译密码，但是他可以在任意时刻对任意信道截获密文，也可以再任意时刻对任意信道发送密文。这样可以看出系统中应有三个进程，消息发起者进程，消息响应者进程，攻击者进程。进程之间通过信道来通信。定义Promela程序的数据类型:chanch1=[1]of{byte,byte,byte,byte};chanch2=[1]of{byte,byte,byte,byte};typedefMsg{bytecode1,code2,code3,message};Msgsrc_Alice,rev_Alice,src_Bob,rev_Bob,src_Eve,rev_Eve;byteOK;其中，ch1,ch2为通信主体接收、发送数据通道。Msg为信息格式，code1、code2、code3分别Alice,Bob,Eve的加密区，即当code1为1表示消息被加密Alice，其他情况以此类推。src_Alice为Alice发送区，rev_Alice为Alice接收区，src_Bob为Bob发送区，rev_Bob为Bob接收区,src_Eve为Eve发送区，rev_Eve为Eve接收区，OK表示入侵者成功获取了其他通信主体的非加密信息。协议发起者Bob、协议入侵者Eve的代码和Alice差不多只是在消息的发送和接收方面有一些差异。

4.3协议安全属性的描述

即：！[]（OK==0）表示入侵者不会永远获取不到其他通信主体的非加密信息。我们要验证系统的转移过程中不会出现人侵者Eve能够成功获取其他通信主体的非加密信息，从而证明各个协议主体在通信过程其发送的数据具有机密性。我们通过SPIN中“neverclaim”来描述待验证属性，验证协议系统模型是否满足要传输数据机密性要求。

4.4模型验证的结果分析

SPIN验证的结果：SPIN验证出存在Eve成功获取其他通信主体非加密信息的情况，通过SPIN自带的模拟工具我们可以看出Eve获取其他通信主体非加密信息的路径为：可以看出Eve通过冒充Alice的身份接收或发送消息。攻击者截获Bob发送给Alice的消息，并用自己的公钥加密，并将两次加密的消息发送给Bob，而Bob无法识别该消息是不是他所期望的从Alice发出的，因为每条随机信息看起来都很相似，根据协议，他会立即解除自己的加密，并将结果发送给Alice，此时攻击者再次将消息截获，解除自己的加密，那么他就得到了Bob发送给Alice的非加密的消息。

5结束语

通过应用SPIN模型检测工具对安全协议进行分析，我们可以发现形式化验证可以发现一些深层次的问题，这些问题靠人工审查和分析是很难发现的，这是形式化验证的巨大优势，然而我们也可以看到随着协议主体的增加状态空间大小呈指数级增长，无可避免的会出现状态空间爆炸问题，状态空间的大小与我们待验证系统的抽象是紧密相关的，因而如何合理抽象是我们以后的研究方向。

本文作者：刘虹工作单位：河北省张家口市阳原县华原市政工程有限公司