The security of whole communication network is affected by session key. The forward security is a special proper-ty of key exchange protocols which ensures the security of session key. The applied PI calculus is extended.The stage process syntax is added to describe the forward security of protocol. An automatic analysis method of the forward security based on first-order theorem prover ProVerif is proposed,with which the forward security of two typical key exchange protocols(STS protocol and MTI protocol)were analyzed. The analysis results show that this method has the advantages of simplicity and reliability.%会话密钥的安全影响了整个通信网络的安全,前向安全性是密钥交换协议中保证会话密钥安全的一种特殊的安全属性.首先扩展了应用PI演算,增加了阶段进程语法描述协议的前向安全性;然后提出了一个基于一阶定理证明器ProVerif的前向安全性自动化分析方法;最后运用这种方法分析了两种典型的密钥交换协议,STS协议和MTI协议的前向安全性,分析结果表明该方法简单可靠.
展开▼
