CAJ | 학술논문

会话密钥的安全影响了整个通信网络的安全,前向安全性是密钥交换协议中保证会话密钥安全的一种特殊的安全属性.首先扩展了应用PI演算,增加了阶段进程语法描述协议的前向安全性;然后提出了一个基于一阶定理证明器ProVerif的前向安全性自动化分析方法;最后运用这种方法分析了两种典型的密钥交换协议,STS协议和MTI协议的前向安全性,分析结果表明该方法简单可靠.
회화밀약적안전영향료정개통신망락적안전,전향안전성시밀약교환협의중보증회화밀약안전적일충특수적안전속성.수선확전료응용PI연산,증가료계단진정어법묘술협의적전향안전성;연후제출료일개기우일계정리증명기ProVerif적전향안전성자동화분석방법;최후운용저충방법분석료량충전형적밀약교환협의,STS협의화MTI협의적전향안전성,분석결과표명해방법간단가고.
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.