密钥交换协议前向安全性的自动化分析

顾香++潘进++王小明

摘 要： 会话密钥的安全影响了整个通信网络的安全，前向安全性是密钥交换协议中保证会话密钥安全的一种特殊的安全属性。首先扩展了应用PI演算，增加了阶段进程语法描述协议的前向安全性；然后提出了一个基于一阶定理证明器ProVerif的前向安全性自动化分析方法；最后运用这种方法分析了两种典型的密钥交换协议，STS协议和MTI协议的前向安全性，分析结果表明该方法简单可靠。

关键词： 应用PI演算； 前向安全性； ProVerif； 自动化分析； STS协议； MTI协议

中图分类号： TN958?34； TP309 文献标识码： A 文章编号： 1004?373X（2015）22?0021?04

随着信息时代的来临，网络已成为人类文明飞速发展的主要载体[1]。与此同时，网络安全问题也日益突出，这是信息时代无法回避的关键问题。而安全协议能够为网络提供有效的安全保障，它可以保证秘密性、认证性、完整性、匿名性、公平性等多种安全属性。根据协议安全目的的不同，通常将安全协议分为认证协议、密钥交换协议、认证及密钥交换协议和电子商务协议。其中密钥交换协议主要用于建立会话密钥，在信息系统安全中是极为重要的。

在实际应用中，为了实现某个具体目标，密钥交换协议往往要求达到某些特殊的安全属性：已知会话密钥安全性，前向安全性，不能使用泄露的身份信息冒充其他合法用户，未知会话密钥共享，密钥控制，密钥的新鲜性[2]。其中前向安全性是一种比较重要的安全属性，它能够保证在协议参与方长期私钥泄露的情况下不会泄露之前建立的会话密钥。但是目前，对于前向安全性的分析都仅仅局限于人脑逻辑证明的非形式化分析方法[3?7]，即通过假设攻击者在获取协议参与方的长期私钥时，证明其是否能够获取已建的会话密钥。文献[6]非形式化地分析了WTLS握手协议的前向安全性，并提出两种改进的具有前向安全性的协议方案。而文献[7]对这两种方案的前向安全性进行分析，提出其中一种方案并不满足前向安全性。由此可见，非形式化分析方法极易出错。基于应用PI演算对协议进行建模，并用ProVerif、SPVT等工具自动化分析协议，是一种简单可靠的协议分析方法。目前，这种方法能够自动化分析协议的秘密性、认证性、强秘密性、公平性[8]和抗拒绝服务攻击性[9]。由于标准的应用PI演算语法不能描述协议的前向安全性，本文首先对应用PI演算进行扩展，主要是扩展了一个阶段进程语法，然后提出一个基于定理证明器ProVerif的前向安全性自动化分析方法，最后应用这种方法来分析验证两种典型密钥交换协议的前向安全性。

1 扩展的应用PI演算

应用PI演算[10]是一种进程演算，是对PI演算的扩展，是SPI演算的一般化形式。应用PI演算在PI演算的语法上增加了函数和等式，使其能够描述各种密码操作及精确描述协议的交互过程。但是现有语法并不足以分析协议的前向安全性，针对这一缺陷，在应用PI演算的现有语法上进行扩展，扩展后的语法如表1所示。

表1 扩展的应用PI演算语法

表1中，元组项[M1，M2，…，Mn]、进程宏[R（M1，M2，…，Mn）]和阶段进程[phase t.P]是在应用PI演算基础上扩展的新语法。 元组[M1，M2，…，Mn]本质上也是一个项，它是具有两个以上参数的项，能够表示复杂的消息及操作。进程宏[R（M1，M2，…，Mn）]用来表示参与协议各个主体的进程，其中[M1，M2，…，Mn]表示协议主体拥有的原始项。进程宏的扩展可以使协议的主进程用几个分进程来描述。阶段进程[phase t.P]表示在t阶段执行进程P，t代表一个全局时钟，并且进程[phase t.P]只在t阶段是活跃的。带有阶段的进程被执行如下：首先，执行0阶段下的所有指令，即不在[i≥1]阶段的所有指令；然后，在0阶段到1阶段的过渡阶段，所有没有达到[i≥1]阶段的所有进程被丢弃；然后进程执行1阶段的指令，但不是[i≥2]阶段的指令。更一般地，当从n阶段到n+1阶段转换时，所有没有达到n+1阶段的进程都被丢弃，同时执行n+1阶段而不是[i≥n+2]阶段的指令。

从上述描述可知，在阶段转换之前执行一个特定阶段的所有指令是没有必要的。此外，只有在相同阶段的进程才能进行通信。本文增加阶段进程用来描述协议的前向安全性。

2 前向安全性的自动化分析方法

2.1 自动化分析工具ProVerif

Blanchet等人在2002年开发了自动化分析工具ProVerif[11]，它由3部分组成：协议输入部分、系统处理部分和结果输出部分，具体结构如图1所示。其中系统输入部分可以是Horn逻辑或应用pi演算描述的协议，既要描述协议的交互过程也要描述所要验证的安全属性；系统处理部分是基于一阶逻辑规则对安全属性进行推导，该工具能够解决状态空间爆炸问题；结果输出部分在协议不满足某安全属性时能够给出相应的攻击序列，这是一个很实用、可靠的自动化分析工具。目前，该工具已经成功分析了很多复杂协议，如网络投票协议、JFK协议、电子商务协议等。

2.2 前向安全性的自动化分析

根据前向安全性的定义[4]，如果协议参与方中一方的长期私钥泄露，并不会泄露他们以前建立的会话密钥，则称协议具有前向安全性。如果协议所有参与方的长期私钥都泄露，也不会影响之前建立的会话密钥，则称协议具有完美前向安全性。由上述定义可知，协议具有前向安全性必须满足两个条件：第一阶段，运行协议，协议能够保证会话密钥不被攻击者获取，即保证会话密钥的秘密性；第二阶段，协议运行结束后，攻击者获取协议参与方的长期私钥，但是根据协议运行时攻击者获取的知识无法计算出之前建立的会话密钥。根据扩展的阶段进程语法[phase t.P]，可以进行这两个阶段的描述。

基于一阶定理证明器ProVerif，协议的秘密性自动化分析方法[12]如定义1。

定义1 秘密性

如果M为协议的一个基本项，输入查询语句：query attacker（M），其输出结果为not attacker（M） is true，则称协议保证项M的秘密性。

其中attacker（M）表示攻击者能够获取项M，证明可达性是ProVerif的最基本功能。工具允许研究查询攻击者能够获得哪些项，如果攻击者不能获取项M，即not attacker（M），那么协议就保证了项M的秘密性。

根据前向安全性的定义，基于扩展的应用pi演算阶段进程语法及ProVerif工具，定义协议的前向安全性如下。

定义2 前向安全性

[R1（M1，M2，…，Mn）]、[R2（M1，M2，…，Mk）]为协议参与方的进程宏，k为协议所建立的会话密钥。如果运行协议进程[！R1（M1，M2，…，Mn）！R2（M1，M2，…，Mn）！phase1；outc，sk]，并输入查询语句：query attacker（k）phase 0和query attacker（k）phase 1，其两个输出结果都为not attacker（k） is true，则称协议满足前向安全性。

其中[phase1；outc，sk]表示1阶段在公共信道c上输出私钥sk（协议参与方任意一方的长期私钥）。ProVerif所有进程都默认在phase 0下执行。由阶段进程的语法可知，ProVerif会首先执行0阶段下的所有指令，即[！R1（M1，M2，…，Mn）！R2（M1，M2，…，Mn）！]，这时就能建立一个会话密钥k。然后，在0阶段到1阶段的过渡阶段，所有没有达到1阶段的进程被丢弃，并且进程执行1阶段的指令[outc，sk]，这样攻击者就可以获取协议参与方的私钥。查询会话密钥k在0阶段和1阶段是否被泄露，即query attacker（k），就能验证协议的前向安全性。与秘密性一样，如果攻击者不能获取会话密钥k，即not attacker（k） is true，则称协议具有前向安全性。

引理：[R1（M1，M2，…，Mn）]，[R2（M1，M2，…，Mk）]为协议参与方的进程宏，k为协议所建立的会话密钥，s为用会话密钥k加密传输的保密信息。如果运行进程[！R1（M1，M2，…，Mn）！R2（M1，M2，…，Mn）！phase1；outc，sk]，并输入查询语句：query attacker（s）phase 0和query attacker（s）phase 1，其输出结果都为not attacker（s）is true，则称协议满足前向安全性。

如果s是一条保密的信息，用会话密钥k加密后传输，若攻击者不能获取信息s，那么攻击者必然不知道会话密钥k，即若输出结果为not attacker（s）is true，则协议满足前向安全性。

3 两种典型密钥协商协议前向安全性分析

Diffie?Hellman协议是最基本的密钥协商协议，它容易遭受中间人攻击，泄露会话密钥。STS（端?端）和MTI密钥协商协议是DH协议的改进，能够抵抗中间人攻击，建立安全的会话密钥。

3.1 STS密钥协商协议

STS密钥协商协议[13]由3条消息组成。其中，公开群[G，?]和一个阶为[n]的元素[g∈G]，[ski]和[pki]为用户[I]的签名密钥及其对应的公钥。

[MSG1 A→B： ga，Cert A]

[MSG2 B→A： gb，Cert B，Signb（IDbgbga）]

[MSG3 B→A：Signa（IDagagb）]

协议消息交互如下：用户A选取一个随机数[a]，[0≤a≤n-1]，计算[ga]，将[ga]和[Cert A]发送给用户B；用户B随机选取[b]，[0≤b≤n-1]，计算[gb]和会话密钥[k=gab]，并用自己的私钥[skb]进行签名[Signb（IDbgbga）]，再将[gb]，[Cert B]和[Signb（IDbgbga）]发送给用户A；A验证证书及签名，验证成功后计算会话密钥[k=gba]，再用私钥[ska]进行签名[Signb（IDbgagb）]，并发送给B；B验证签名，成功后则完成会话密钥的协商。

基于提出的前向安全性自动化分析方法，用扩展的应用pi演算对STS协议进行建模，然后用ProVerif工具进行前向安全性分析。由于篇幅限制，只给出了ProVerif的分析结果，如图2所示。

根据图2可知，在0阶段的查询结果为true，表明STS协议能够保证会话密钥的秘密性；在1阶段的查询结果也为true，表明在用户A和B的长期私钥都泄露的情况下，协议能够保证之前建立的会话密钥不被泄露出去，STS协议具有完美前向安全性。

3.2 MTI密钥协商协议

MTI密钥协商协议[13]由两条消息组成。其中，公开群[G，?]和一个阶为[n]的元素[g∈G]。每个用户[I]拥有一个私钥[ski]，其中[0≤xi≤n-1]，对应的公钥为[pki=gski]，被包含在用户的证书[Cert I]中，且被TA签名。

[MSG1 A→B：ga，Cert A]

[MSG2 B→A：gb，Cert B]

协议消息交互如下：用户A随机选取[a]，[0≤a≤n-1]，计算[ga]，将[ga]和[Cert A]发送给用户B；用户B随机选取[b]，[0≤b≤n-1]，计算[gb]，将[gb]和[Cert B]发送给用户A。B通过[Cert A]认证A，并获取A的公钥[pka]，计算会话密钥[k=gabpkaskb]；A通过[Cert B]认证B，并获取B的公钥[Pb]，计算会话密钥[k=gbapkbska]。由于[gabPaxb=gabgskaskb=gbapkbska]，用户A，B计算的会话密钥相等。

同样，基于提出的方法对MTI协议进行建模及前向安全性分析，分析结果如图3和图4所示。

图3为只有用户A的长期私钥被泄露时的分析结果（只泄露用户B私钥时的分析结果相同）。由图3可知，两个阶段的查询结果都为true，表明MTI协议满足前向安全性。图4为用户A和B的私钥都泄露时的分析结果，由图4可知，1阶段的分析结果为false，表明攻击者在获取A和B私钥时，能计算他们之前建立的会话密钥，则MTI 协议并不满足完美前向安全性。

4 结 语

密钥交换协议主要是用来建立会话密钥的，它的前向安全性能够保证在协议参与方长期私钥泄露的情况下不会泄露会话密钥。形式化分析方法是一种有效的协议分析方法。本文扩展了应用PI演算的阶段进程语法，并在此基础上提出了一种基于定理证明器ProVerif的前向安全性自动化分析方法。与人脑逻辑证明分析方法相比，这种能够实现自动化分析，更简单。这是一种形式化分析方法，不需要依靠人的逻辑思维，更加可靠。但是由于本文考虑的是分析密钥交换协议中的前向安全性，这种方法还不足以分析组密钥协商协议的前向安全性，下一步的研究还要继续。未来研究工作中，将对应用PI演算语法及一阶定理证明器ProVerif做进一步扩展及改进，使其能够分析大型复杂协议的多种安全属性。

参考文献

[1] 薛锐，雷新锋.安全协议：信息安全保障的灵魂：安全协议分析研究现状与发展[J].信息安全，2011，26（3）：287?296.

[2] 冯登国.安全协议：理论与实践[M].北京：清华大学出版社，2011.

[3] 项顺伯，彭志平，柯文德.一种可证安全的两方口令认证密钥交换协议[J].计算机工程，2013，39（1）：164?167.

[4] 李强，冯登国，张立武，等.标准模型下增强的基于属性的认证密钥协商协议[J].计算机学报，2013，36（10）：2156?2167.

[5] 陈家琪，冯俊，郝妍.基于无证书密码学的可认证三方密钥协商协议[J].计算机应用研究，2010，27（5）：1902?1904.

[6] KWAK D J， HA J， LEE H J C， et al. A WTLS handshake protocol with user anonymity and forward secrecy [J]. Lecture Notes in Computer Science， 2003， 2524： 219?230.

[7] 崔媛媛，周永彬，丁金扣，等.一种具有用户匿名性和前向安全性的WTLS握手协议的安全性分析及其改进[J].高技术通讯，2005，15（4）：6?10.

[8] 郭云川，丁丽，周渊，等.基于ProVerif的电子商务协议分析[J].通信学报，2009，30（3）：125?129.

[9] 孟博，黄伟，王德军，等.协议抗拒绝服务攻击性自动化证明[J].通信学报，2012，33（3）：112?121.

[10] RYAN M D， SMYTH B. Applied Pi calaulus [M]. [S.l.]： IOS Press， 2011.

[11] BLANCHET B. An efficient cryptographic protocol verifier based on prolog rules [C]// Proceedings of 14th IEEE Computer Security Foundations Workshop. Nova Scotia， Canada： IEEE， 2002： 82?96.

[12] BLANCHET B， SMYTH B， CHEVAL V. ProVerif 1.88： automatic cryptographic protocol verifier， user manual and tutorial [M]. [S.l.]： [s.n.]， 2013.

[13] 斯延森.密码学原理与实践[M].冯登国，译.3版.北京：电子工业出版社，2009.