Formal analysis of robust email protocol based on authentication tests  

基于认证测试的鲁棒电子邮件协议形式化分析(英文)

作　　者：蒋睿 胡爱群[1] 

机构地区：[1]东南大学信息科学与工程学院,南京210096

出　　处：《Journal of Southeast University(English Edition)》2009年第2期147-151,共5页东南大学学报（英文版）

基　　金：The Natural Science Foundation of Jiangsu Province(No.BK2006108)

摘　　要：Based on the authentication tests and the strand space model, the robust email protocol with perfect forward secrecy is formally analyzed, and the security shortcomings of the protocol is pointed out. Meanwhile, the man-in-the-middle attack to the protocol is given, where the attacker forges the messages in the receiving phase to cheat the two communication parties and makes them share the wrong session keys with him. Therefore, the protocol is not ensured to provide perfect forward secrecy. In order to overcome the above security shortcomings, an advanced email protocol is proposed, where the corresponding signatures in the receiving phase of the protocol are added to overcome the man-in-the-middle attack and ensure to provide perfect forward secrecy. Finally, the proposed advanced email protocol is formally analyzed with the authentication tests and the strand space model, and it is proved to be secure in authentication of the email sender, the recipient and the server. Therefore, the proposed advanced email protocol can really provide perfect forward secrecy.基于认证测试方法及strand space模型,形式化分析了具有完美前向机密性的鲁棒电子邮件协议,指出该协议存在安全缺陷.同时给出了针对该协议的中间人攻击方法,即攻击者在协议的接收阶段通过伪造消息即可欺骗通信双方,使通信双方与其共享错误的会话密钥,由此使得协议的完美前向机密性得不到保证.针对协议的上述缺陷,提出一种改进方案,即通过在协议的接收阶段加入相应的签名信息,以保证改进协议能够克服中间人攻击并且提供完美前向机密性.最后,基于认证测试方法及strand space模型,形式化证明了改进协议在发起者、接收者及服务器之间的安全认证,确保了改进协议具备真正的完美前向机密性.

关 键 词：email protocol authentication tests formal method perfect forward secrecy strand space model 

分 类 号：TP393[自动化与计算机技术—计算机应用技术]