智能化电视网络安全协议的验证方法综述

张 兴，韩 冬，马晓光

(1.辽宁工业大学 电子与信息工程学院，辽宁 锦州 121001;2.北京歌华有线电视网络股份有限公司，北京100000)

随着互联网产业的发展，电视技术的双向化、智能化趋势逐步凸显。当前我国智能化电视的普及率已达到23.2%，根据格兰研究数据，截至到2013 年三季度末，我国有线电视双向网络覆盖用户为8 914.3 万户，有线电视双向网络渗透用户为2 641.1 万户。预计2015 年全国县级以上城市有线广播电视网络80%以上基本实现双向化。用户可以实现在双向电视机顶盒端生活缴费、网上购物、网银管理等一系列家庭事务，极大地方便了用户的生活，然而也正是由于双向交互式机顶盒、智能电视的功能越来越丰富，各种信息也越来越多地被收集到数字电视网络中，如果缺乏有效的协议安全性意味着数字电视网络中的信息将存在着巨大的安全隐患。2013年11 月LG 智能电视被曝会强制收集用户的浏览记录、观看历史等个人信息，并通过HTTP 流量加密传输到GB.smartshare.legtvsdp.com，被制造商用来投放广告。2014 年5 月哥伦比亚大学有关专家公布红色按钮攻击漏洞，利用该漏洞可以攻击采用HbbTV 标准的智能电视。2014 年8 月温州地区部分电视用户机顶盒遭黑客攻击，电视画面遭到非法入侵，严重地影响了用户的正常生活［1－2］。这种情形的出现无疑是电视网络的通信安全机制不够完善所导致的合法用户的现实生活受到影响。通信协议的验证机制是确保电视网络安全的主要手段之一，通过安全协议的验证法［3－4］选择安全性更高的通信协议就显得极为重要。通常安全协议主要由消息交换规则和加密手段两部分组成。由于在安全协议的设计过程中存在着安全目标的微妙性、运行环境的复杂性、攻击者的不定性以及协议本身的高并发性等因素，使得协议本身存在着一些缺陷。因而，正确的选择一种适合的验证方法来验证安全协议的的可用性、正确性、安全性是很必要的。安全协议的形式化分析思想最早是在1978 年由Needham 和Schroeder 两人共同提出，但真正意义上的协议验证思想是由Dolev 和Yao 二人提出的Dolev－Yao 模型［5］。当Dolev－Yao 模型提出后，一部分研究者对其进行了进一步研究和扩展，相关的协议分析工具也被研发出来，如Interrogator［6］、NRL 协议分析器［7］等。1989 年，Burrows、Abadi 和Needham 三人提出了BAN 逻辑［8］，BAN 逻辑具有简单直观、推理思路清晰等特点。使安全协议形式化分析领域的可操作性变得简洁，推动了协议验证的进一步发展。然而BAN 逻辑的缺陷也是不容忽视的，如抽象假设过度、不能对新鲜性建模等。对于BAN 逻辑的缺陷研究者们对其作了改进，提出了GNY 逻辑［9］、AT 逻辑［10］、SVO 逻辑［11］等BAN 逻辑的改进形式。20 世纪90 年代中期，当Lowe 利用通信顺序进程对协议进行分析时，得出了更清晰的验证结果。CSP 验证模型便广泛地应用于协议验证分析领域。到90 年代末期，由Fabrega、Herzog 和Guttma 提出的串空间模型［12］及Paulson 归纳法［13］，引领了应用定理归纳证明法对安全协议验证分析的新局面。

随着安全协议验证领域的不断发展，近五年提出的一些衍生类协议验证方法正在引领着协议验证分析领域的新潮流，如绑定项证明法［14］、软件模拟法［15］、SPVT 验证工具［16］、理性安全协议推理系统［17］、改进的BAN 逻辑［18］、改进型有色Petri 网的协议验证法［19］、基于Horn 扩展逻辑的非否认建模与验证方法［20］、基于SAT 的安全协议惰性形式化分析方法［21］、串空间的改进方法IVAP［22］、含时间因素的安全协议形式化分析方法［23］、混合的安全协议分析法［24］、新的协议验证逻辑［25］等。这些安全协议着重于对经典的协议验证方法的改进、扩展或提出了新的通信协议验证方法。但在安全协议形式化分析领域，每一类验证方法都存在着相应的缺陷或不足。因此，对于这些改进或新提出的安全协议进行总结、分析，并在此基础上指出新的研究方向显得十分必要。

下面，本文就以下几类安全协议验证方法做详细介绍。

1 逻辑推理分析法

逻辑推理分析法指的是在协议的验证过程中，通过将协议描述为对应验证规则的语法，对相应变量进行假设，在符合假设和约定规则的前提下，进行逻辑推导验证协议是否达到了预期目的的验证方法，逻辑推理分析法的对比如表1 所示。

表1 逻辑推理分析法的对比表

1)BAN 逻辑是由Michael Burrows，Martin Abadi 等提出的，它是协议形式化分析的工具之一。BAN 逻辑是一种基于主体信念来从已知的信念中推出新的信念的逻辑规则。通过应用BAN 逻辑来验证协议从信息传递过程中是否可以推出最终运行的结果。BAN 逻辑的应用过程:将协议的条件进行合理的假设，通过假设来构造BAN 逻辑中的公式，然后将这些公式应用BAN 逻辑的语法进行推理，最终得出验证结果。

2)GNY 逻辑于1990 年由Gong，Needham 和Yahalom 提出。属于类BAN 逻辑的扩展，相较于BAN 逻辑对逻辑分析能力、可识别概念、判断规则等方面进行了改进。GNY 逻辑总共44 条规则，推导过程较为复杂。

3)AT 逻辑是由Abadi M 和Tuttle M R 提出的。AT 逻辑较BAN 逻辑而言，重新形式化了BAN 逻辑，采用将信仰作为源绑定形式和可作废的知识对待，具备了更好的自然逻辑语义模型和合理的计算模型。

4)SVO 逻辑是由Syverson 和Van Oorschot 提出，SVO 逻辑吸取BAN、GNY、AT 等逻辑的优势，建立自己简洁合理的推理模型，在形式化语义方面，SVO 逻辑取消了AT 逻辑中的部分限制，重新定义了部分概念。当前SVO 逻辑被主要用于电子商务中相关协议的研究。

5)Kailar 逻辑［26］的提出主要是为了电子商务协议的可追究性，以解决主体向第三方证明另一方执行的责任行为。然而它缺乏对签名密文的分析能力，证明协议时不够严格。

6)CS 逻辑［27］由Coffey 和Saidha 提出，它结合了谓词逻辑和模态逻辑的特点，也是一种将时间和逻辑结构相结合的逻辑。但CS 逻辑对环境因素考虑不足，在某些特定环境下不能对协议进行有效验证。

7)KG 逻辑［28］由Kailar 和Gligor 提出的，来验证双方的最终信仰，即验证双方互相发送和接收报文能否从最初的信仰发展成协议要达到的最终目的。通过验证协议运行中的信仰变换来检测协议中是否存在着缺陷。

2 模型模拟检测法

模型模拟检测法指的是采用模拟工具或构建模型的方式，将初始状态下的协议进行检测，通过对协议运行开始到运行结束的路径进行检测，判断是否协议存在缺陷的验证方法。模型模拟检测法具有高度自动化的特点，模型模拟检测法则对比见表2。

表2 模型模拟检测法的对比表

1)有限状态机FSM［29］是一种应用于系统动态行为的建模，借助状态图进行可视化表示。通过对有限状态机的不断的研究，可以被用于更多更复杂行为的建模。但FSM 的实现也存在着复用性差，维护困难等问题。

2)Dolev－Yao 模型是由Dolev 和Yao 最早提出，经过后来研究者T Genet 和F Klay［30］等的进一步扩展。Dolev－Yao 模型首先对安全协议进行层次划分，将安全算法和协议本身区分研究，然后对协议的正确性、安全性等进行研究。提出了重视攻击者知识和能力的原则。

3)CSP 方法［31］即通信顺序进程方法，由C.A.R.Hoare提出。他将输入、输出作为程序语言的基本要素，将实现顺序进程间通信的并行组合。对安全协议进行验证时首先从协议说明中建立模型，再结合FDR 工具(故障偏差精炼检测器)［32］检测协议是否存在问题。

4)Spin 模拟检测方法［33］是由贝尔实验室的形式化小组研发的协议检测模型，使用Promela 语言建模，整个系统可以看作是扩展的有限状态机。主要用于对于线性时态逻辑的正确性检测。

5)murφ 模型检测法［34］由J.C. Mitchell，M.Mitchell 和Stern 最早应用于对协议预期性质的建模，通过加入入侵者模型，在应用状态枚举法来检测系统状态都符合规范。

6)Interrogator 由Millen 等人提出的，基于状态机技术的协议分析器。Interrogator 对协议分析时采取前向搜索，从初始状态直到最终状态存在不安全路径。

7)NRL 模型检测工具由Meadows 等人研发，它是Dolev－Yao 模型的扩充版本。NRL 工具采取后向搜索方式，从协议执行的最终状态出发搜寻是否存在到达初始状态的路径。

3 定理归纳证明法

定理归纳证明法是通过将协议形式化的模型和规则进行验证，在协议的模型中是否满足了初始的规则。定理归纳证明法相较模型模拟检测法是从协议的正方向验证，直接对协议的规约进行证明。定理归纳证明法对比如表3 所示。

表3 定理归纳证明法的对比表

1)串空间模型(strand space model)由Thayer 和Herzog 等人提出的形式化方法。主要用于安全协议的认证性和私密性的验证。卿斯汉等针对此方法的不足进行了扩展，并提出了扩展后的通用串空间模型。随着对串空间方法的不断研究，串空间与信任管理相结合，使得串空间模型更好地应用于多种安全协议的验证。

2)Paulson 归纳法由L C Paulson 提出，这种方法通过将协议归纳定义为所有时间可能路径的集合。一条路径即为一个包含多轮协议的通信事件序列。可以模拟所有攻击及密钥丢失事，通过对路径归纳来证明属性安全。

3)重写逼近法(Rewriting Approximation Method)［35］由Boichut Y 等人提出。此方法的验证目标是验证协议中不存在任何攻击。在实际协议验证中，重写逼近法对协议的安全属性进行正面验证，较其他测试方法而言具有更好的可靠性。

4 其他衍生验证法

其他衍生验证法指的是通过研究一些经典协议的验证方法，对这些协议验证方法进行扩展，或者选取新的验证角度，构建出全新的协议验证模型。

1)绑定项证明法指的是由微观角度通过形式化理论来判定协议的绑定项(即加密项)的完备性。验证过程中若存在绑定项不符合规则，可认定协议存在缺陷，快速准确地给予判定协议结果。

2)软件模拟法是指利用软件模型模拟出协议运行环境，从而对安全协议进行验证。针对RFID 安全协议而言，利用Linux 系统、gcc 编译器、Mysql 数据库相结合模拟出RFID 系统，在将协议导入模拟系统中运行，最终得出验证结果。

3)SPVT 验证工具是基于Objective Caml 开发的协议验证工具。利用类π 演算来描述安全协议。SPVT 验证工具根据逻辑程序的不动点计算验证安全性质，来验证出不满足安全性质的缺陷。

4)理性安全协议推理系统是基于博弈逻辑ATL 和ATEL的扩展研究，针对理性环境下，在传统博弈逻辑的基础下，提出了新的推理系统rA－TEL－A。在此推理系统中，将协议进行形式化描述，并对协议进行模拟验证。

5)改进的BAN 逻辑是根据BAN 逻辑在对协议验证过程中存在的一些缺陷，而对其进行改进的协议验证逻辑。在使用BAN 逻辑验证协议的过程中，BAN 逻辑的初始假设、消息形式化描述转换、逻辑语义、推理规则及探测协议存在的攻击等几方面存在不足。通过对这方面分析及改进，改进的BAN逻辑又从消息形式化描述、消息含义推理规则、先行判断规则这三个角度对改进的BAN 逻辑进行了验证，提高了BAN 逻辑验证的安全可靠性。

6)改进型有色Petri 网的协议验证法通过对传统有色Petri 的分析改进而提出的。运用传统有色Petri 网安全协议分析法对协议进行验证，主要通过倒推的方法即在检测前确定出可能的不安全状态，验证此不安全状态可达，从而分析协议可能的缺陷，但对于未知的不安全状态无法进行检测。另外，对于验证入侵者的协议时，构造协议模型时由于对入侵者的攻击步骤不了解，使其状态规模快速增长，导致空间爆炸的问题。然而改进型有色Petri 网在对协议进行分析验证时，不必了解未知的安全状态，只需要了解一个攻击成功的目标。改进型有色Petri 网对攻击成功的知识集与可以获取的知识集进行整合，将其融入到传统的有色Petri 网中缩小入侵攻击步骤的范围，缓解了传统有色Petri 网在验证协议时所引起的空间爆炸问题。

7)基于Horn 扩展逻辑的非否认建模与验证方法是基于Horn 逻辑扩展模型验证非否认协议的验证方法。本方法主要强调验证非否认协议的非否认性和公平性，并对协议的非否认性和公平性建模。在对协议的建模过程中还需要对协议的诚实主体、恶意主体、仲裁进行建模，提出了适用于非否认协议的验证算法。基于Horn 逻辑扩展的模型可应用于无穷会话交叠运行的情况，提高了对协议保密性的验证效率。

8)基于SAT 的安全协议惰性形式化分析方法是一种基于SAT 问题的协议分析方法。加入惰性思想优化初始状态和转换规则，根据协议的复杂度自动调用命题公式的范式形式，提升了模型的验证效率。其次根据在消息类型上定义的偏序关系，本方法可以检测到更多类型的缺陷攻击。

9)串空间的改进方法IVAP 是一种以串空间为理论基础，根据认证协议的一致性属性及测试分量唯一性属性而建立的安全性验证算法。本方法证明了安全协议的安全性，而且能运用改进协议生成算法为有漏洞的协议生成安全的改进协议。但本方法不能实现对无线认证协议的安全属性验证。

10)含时间因素的安全协议形式化分析方法是一种针对包含时间因素的有色Petri 网形式化分析法。本方法利用有色Petri 网中内置的全局自动时钟标记，并通过仿真和生成状态图的方式对时间相关性质进行验证。由于利用系统的内置自动时钟，在建模及验证过程中，系统提供时钟支持方法，因此对于一些复杂的包时间因素的安全协议，此方法依然可以清晰的描述验证。

11)混合的安全协议分析法是以SPALL 逻辑为基础，结合了可证安全的思想，提出概率推导的分析方法。本方法将形式化证明中的模态逻辑分析法和可证明安全法两者相结合，将逻辑假设的成立概率结合到协议的推导过程中，形成一种概率推导方法。根据概率的条件，来判别协议假设安全与否，从而确定协议整体的安全性。此方法克服了两种方法的各自缺陷，具有简单易用、分析全面的特点。

12)新的协议验证逻辑是一种可以验证安全协议的认证性、非否认性、公平性等特性的逻辑方法。本方法提出了新的逻辑构件、推理规则及公理。通过增加Hash 函数的密码原语相关的逻辑谓词、推理规则和公理，实现了对基于对称密钥体制、公钥密码体制和Hash 函数密码体制协议的分析验证能力。并通过串空间语义对新逻辑进行验证，证明了此逻辑方法具备了逻辑验证的正确性。

13)基于SPIN 的安全自适应协议栈的形式化验证法［36］属于一种自动化的模型检测方法。本方法将相邻搜索机制和路由协议作为切入点，对安全协议进行自动检测、分析并指出存在缺陷。因此本验证法具备自动化程度高、缺陷自动检测等优点，但是在对协议建模的过程中需要采集各方面的约定规则、抽象假设，导致在构建协议的premola 描述模型时较为复杂。

14)变异性监测(Veriability)验证法［37］是一种针对密码协议进行自动化验证的方法。本方法主要应用于电子选举协议，可以对匿名认证用户的加密信息进行检测，同时对于部署广泛的加密协议可以自动评估检测，发现其不安全的漏洞。本验证法具备部分自动化、验证安全属性较为全面，但由于仅仅针对电子投票协议的验证，所以此方法存在验证的局限性。

15)一种自动化的模型检测方法［38］是集合了模型提取和代码生成于一体的验证方法。本方法通过代买编写、模型抽取的方式来自动构建协议的验证模型，同时尽可能编译出真实的协议环境，达到更精确的验证。本方法具有自动化程度高、验证精确度高等优点，然而对于代码的编译过程较为复杂，构建出的模型具有针对性，所以验证角度有限。

16)协议代码模块化验证方法［39］是一种基于声明和执行不变论密码学的应用方法，本方法开发了加密嵌入逻辑模型的库结构，并提出了一个验证理论，证明了模块化代码验证的合理性。同时本方法具备验证结果精确度高、可扩展性强的优点，但对于验证角度而言仅针对协议中的加密代码模块进行验证。

17)基于拍处理的自动化验证方法［40］属于自动化模型检测的验证法。本方法应用了关于概率的时间演算的加密算法，以此更好地对协议的实时性、概率性、加密性等几方面进行验证。本方法具备自动化程度高、验证精确性高的优点，但其验证存在局限性，而且不能对外部攻击者进行追踪检测。

5 协议验证法的比较

针对以上的安全协议验证方法，分析对比各类验证方法的优缺点，如表4 所示。对各类验证方法的特点进行比较，总结出每类验证方法适合验证的安全协议。逻辑推理分析法虽然简单直观、可视化，但其由于过度抽象化等原因只适用于验证规模较小、特定的小系统的安全协议;模型模拟检测法具备自动化程度高、协议自动校正等优势，但不能很好地克服空间控制及主题数目限制的问题，根据其这些特点适用于模型适中、较大系统的安全协议;定理归纳证明法虽然自动化程度不高、部分证明复杂，但由于其语义清晰、分析直观、避免了空间控制问题等特点，所以其适用于不受模型限制、大型系统的安全协议;其他衍生验证法是前几类安全协议验证法的延伸，通过对一些经典的的验证方法进行了改进及扩展，并加以创新，推动了安全协议验证领域不断发展，这一类安全协议验证方法适用于验证更为广泛的安全协议。

6 总结与展望

当前，随着有线电视网络承载的应用量越来越多，其安全性必须得到保障。因此，验证电视网络通信协议的验证方法的研究就显得极为重要。协议验证法是从确定协议系统与其运行环境的界面、协议行为的描述、协议特性的定义及证明协议符合规定语义等角度对协议的安全性进行分析验证。然而以上的协议验证方法虽然经过不断的研究扩展具备了各自的特点，但每类协议验证法都或多或少存在着一些不足。为了研究出一种更加简洁、通用、自动化程度高的协议验证方法，还需要做进一步的努力。针对当前的安全协议验证领域提出如下的研究方向:

表4 各类安全协议验证方法对比表

1)对于逻辑角度证明，降低形式化抽象的“完美假设”。对于应用逻辑推理法来对安全协议进行验证时，首先要对安全协议的运行环境、理论条件作出假设，然而这些假设或多或少存在着缺陷，如过度理想化、条件完整化等。这些过于完美的初始假设已然使协议的精确验证出现了部分偏差，因此在对安全协议进行初始假设的过程中，尽量将抽象假设的理想程度降低，以此提高对协议验证的准确性。

2)将自动化验证理念进一步扩展，以适应更广泛的安全协议。对于安全协议验证领域而言，若验证工具可以自动的对安全协议进行查找漏洞、缺陷修复、构建修正协议，那么将极大地提高安全协议的验证效率。在安全协议验证领域中，模型模拟检测法在自动化验证方面较其他协议验证方法具有着很大的优势，但此方法也存在着不容忽视的缺陷。因此如何改进模型模拟检测法的缺陷或者提高其他验证方法的自动化程度将值得对此进行进一步研究。

3)尝试将几类协议验证法进行结合，优势互补，推出一种验证性能优越的协议验证法。安全协议验证方法的类型如上文所述，每一种安全协议验证方法都有着自己的优势和不足。若用某一类验证方法对安全协议进行验证，那么得出的验证结果并不能完全确定所验证协议是否是安全的、正确的、可行的。因此如何将几类安全协议验证法进行结合，使得结合后的验证方法具备了这几种验证法的优势，同时弥补这几种验证法的不足，最终得出的协议验证方法可以对安全协议进行更加可靠、更加全面的验证。这种将验证法相结合的研究方向势必成为通信协议验证领域研究的新趋势。

［1］蔡盛勇，吴静.基于SSL 协议的智能电视安全支付方案［J］.电视技术，2013，37(24):49－51.

［2］《电视技术》编辑部.信息安全:风高浪急［J］.电视技术，2014，38(20):1.

［3］冯登国，范红.安全协议形式化分析理论与方法研究综述［J］.中国科学院研究生院学报，2003，20(4):389–406.

［4］高尚等. 安全协议形式化分析研究［J］.密码学报.2014，1(5):504－512.

［5］DOLEV D，YAO A.On the security of public key protocols［J］.IEEE Trans.Information Theory，1983，29(2):98－208.

［6］MILLEN J K，CLARK S C，FREEDAM S B.The interrogator:protocol security analysis［J］.TSE，1987，13(2):274－288.

［7］MEADOWS C.The NRL protocol analyzer:anoverview［J］.Journal of k c Progranarning，1996，26(2):113－131.

［8］BURROES M，ABADI M，NEEDHAM R. A logic of authentication［J］.ACM Transaction in Computer Systems，1990，8(1):18－36.

［9］GONG L，NEEDHAM R，YAHALOM R.Reasoning about belief in cryptographic protocols［C］//Proc.1990 IEEE Symp. Security and Privacy.［S.l.］:IEEE Press，1990:234－248.

［10］ABADI M，TUTTLE M R.A semantics for a logic of authentication［C］//Proc.10th Annual ACM Symposium on Principles of Distributed Computing.［S.l.］:ACM Press，1991:201－216.

［11］SYVERSON P F，OORSCHOT P C.A unified cryptographic protocol logic［R］.Washington D.C:Naval research lab，1996.

［12］THAYER F J，HERZOG J C，GUTTMAN J D.Strand spaces:why is a security protocol correct［C］//Proc.1998 IEEE Symposium on Security and Privacy.［S.l.］:IEEE Press，1998:160－171.

［13］PAULSON L C.Proving properties of security protocols［C］//Proc.IEEE Computer Security Foundations Workshop X.［S.l.］:IEEE Press，1997:70－83.

［14］薛海峰，荆立夏.认证协议的必要条件证明［J］.计算机工程，2011，37(11):144－145.

［15］郭艾侠，李峰，熊俊涛.RFID 认证协议的研究及仿真［J］.实验室研究与探索，2010，29(3):61－65.

［16］李梦君，李舟军，陈火旺.SPVT:一个有效的安全协议验证工具［J］.软件学报，2006(4):898－906.

［17］刘海，彭长根，任祉静.一种理性安全协议形式化分析方法及应用［J］.贵州大学学报:自然科学版，2014，31(6):77－84.

［18］王正才，许道云，王晓峰，等. BAN 逻辑的可靠性分析与改进［J］.计算机工程，2012，38(17):110－115.

［19］张卉，李续武，赵媛莉，等.改进型有色Petri 网的安全协议分析［J］.计算机工程与科学，2013(7):60－63.

［20］徐畅，李舟军，郭华，等. 基于Horn 扩展逻辑的非否认协议建模与验证［J］.清华大学学报，2012，52(10):1488－1495.

［21］顾纯祥，王焕孝，郑永辉，等.基于SAT 的安全协议惰性形式化分析方法［J］.通信学报，2014，35(11):117－125.

［22］张孝红，李谢华.基于串空间的安全协议自动化验证算法［J］.计算机工程，2011，37(5):131－133.

［23］范玉涛，苏桂平.一种含时间因素的安全协议形式化分析方法［J］.计算机应用与软件，2013，30(1):315－318.

［24］霍腾飞，李益发，邓帆.一种混合的安全协议分析方法［J］.计算机应用与软件，2011，28(3):289－292.

［25］陈莉.一种新的安全协议验证逻辑及其串空间语义［J］.计算机工程，2011，37(1):145－148.

［26］DUTERTRE B，SCHNEIDER S. Using a PVS embedding of CSP to verify authentication rotocols［M］.［S.l.］:Springer Berlin Heidelberg，1997.

［27］COFFEY T，SAIDHA P.Logic for verifying public－key cryptographic protocols［J］.IEEE Proc. Computers and Digital Techniques，1997，144(1):28－32.

［28］BOLDYREVA A.KUMAR V.Extended abstract provab le－security analysis of authenticated encryption in kerberos［C］//Proc. IEEE Symmposium on Security and Privacy.New York:IEEE Press，2007:92－100.

［29］JAMES R，IVAR J，GRADY B.The Unified modeling language reference manual［M］.Boston:Addison Wesley，1999.

［30］GENET T，KLAY F.Rewriting for cryptographic protocol verification［C］//Proc.17th International Conference on Automated Deduction.Pittsburgh:IEEE Press，2000:9－9.

［31］HOARE C A R.Communicating sequential processes［J］.Prentice－Hall International，1985，31(1):413－443.

［32］LOWE G.Breaking and fixing the needham－schroeder public－key protocol using FDR［C］//Tools and Algorithms for the Construction and Analysis of Systems. Heidelberg:Springer Berlin，1996:147－166.

［33］GNESI S，LENZINI G，LATELLA D，et al. An automatic SPIN validation of a safety critical railway control system［C］//Proc.2000 IEEE Intemational Conference on Dependable Systems and Networks.Piscataway:IEEE Press，2000:119－124.

［34］MITCHELL J C，MITCHELL M，STERN U.Automated analysis of crypto－graphic protocols using mur［C］//Proc.1997 IEEE Symposium on Security and Privacy. New York:IEEE Press，1997:141－151.

［35］BOICHUT Y，GENET T，JENSEN T，et al. Rewriting approximations for fast prototyping of static analyzers［M］.［S.l.］:Springer Berlin Heidelberg，2007:48–62.

［36］RIPON S，Mahbub S，INTIAZ－UD－DIN K M［J］.International Journal of Engineering and Technology，2013:254－256.

［37］SMYTH B.Formal verification of cryptographic protocols with automated reasoning［D］.Birmingham:University of Birmingham，2011.

［38］AVALLE M，PIRONTI A，RICCARDO S. Formal verification of security protocol implementations:a survey［J］.Formal Aspects of Computing，2014，26(1):99－123.

［39］Gordon. Modular verification of security protocol code by typing［J］.Acm Sigplan Notices，2010，45(1):445－456.

［40］TA V，BUTTYáN L，DVIR A. On formal and automatic security verification of WSN transport protocols［EB/OL］.［2014－12－31］.http://www.hindawi.com/journals/isrn/2014/891467/.