密码协议验证中的Petri网方法

作     者：郭祥法 程震 GUO Xiang-fa;CHENG Zhen

作者机构：青岛朗讯公司山东青岛266061 山东理工大学计算机科学与技术学院山东淄博255049 

出 版 物：《计算机工程与设计》 (Computer Engineering and Design)

年 卷 期：2007年第28卷第6期

页      码：1317-1319页

摘      要：如何验证密码协议的安全性是一个复杂的问题,只有形式化的验证方法才能证明密码协议的绝对正确。利用Petri网给出了一种用于密码协议验证的形式化方法。在合理假设的基础上,区分合法用户与攻击者在执行协议时的前提条件,列出执行协议后的结果,在此基础上建立了攻击者的Petri网模型。最后,用这种方法对NSPK协议进行了验证,证明了最初的NSPK协议中存在一个安全问题,而改进的NSPK协议则消除了这个问题。证明了这种方法的有效性。

主 题 词：密码协议 验证 Petri网 形式化方法 攻击 

学科分类：08[工学] 0839[0839] 081201[081201] 0812[工学-测绘类] 

D　O　I：10.3969/j.issn.1000-7024.2007.06.024

馆 藏 号：203347639...