基于PCL的改进型Helsinki协议的形式化分析  

Formal analysis of improved Helsinki protocol through PCL

作　　者：鲁来凤[1,2] 吴振强[3] 马建峰[1] 

机构地区：[1]西安电子科技大学计算机网络与信息安全教育部重点实验室,陕西西安710071 [2]陕西师范大学数学与信息科学学院,陕西西安710062 [3]陕西师范大学计算机科学学院,陕西西安710062

出　　处：《华中科技大学学报（自然科学版）》2011年第4期53-55,共3页Journal of Huazhong University of Science and Technology(Natural Science Edition)

基　　金：国家自然科学基金重点资助项目(60633020);国家自然科学基金资助项目(60573036,60671063);国家高技术研究发展计划资助项目(2007AA01Z429,2007AA01Z405);陕西省自然科学基金资助项目(2009JM8002)

摘　　要：针对改进型的Helsinki协议安全性问题,利用协议组合逻辑PCL对协议进行形式化分析.首先使用基于'Cords演算'的程序描述语言对协议本身进行形式化描述,然后通过协议逻辑描述协议的安全属性,最后给出性质和定理,并通过逻辑推理证明改进型Helsinki协议满足其安全要求,该协议是安全的.【Abstract】 From the security of the improved Helsinki protocol, a formal analysis based on the formal method, protocol composition logic （PCL） was developed. First, the protocol itself was presented formally by program description language which was based on “Cords calculus”. Then, the security property of the improved Helsinki protocol was shown by PCL logic syntax. Finally, the detailed prove was developed by PCL logic reasoning. The result shows that the improved Helsinki protocol is secure and PCL is effectual

关 键 词：协议分析 安全协议 形式化方法 协议组合逻辑 Helsinki协议 形式化描述 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]