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

Petri net method in cryptographic protocol verification

作　　者：郭祥法 程震[2] 

机构地区：[1]青岛朗讯公司,山东青岛266061 [2]山东理工大学计算机科学与技术学院,山东淄博255049

出　　处：《计算机工程与设计》2007年第6期1317-1319,共3页Computer Engineering and Design

摘　　要：如何验证密码协议的安全性是一个复杂的问题,只有形式化的验证方法才能证明密码协议的绝对正确。利用Petri网给出了一种用于密码协议验证的形式化方法。在合理假设的基础上,区分合法用户与攻击者在执行协议时的前提条件,列出执行协议后的结果,在此基础上建立了攻击者的Petri网模型。最后,用这种方法对NSPK协议进行了验证,证明了最初的NSPK协议中存在一个安全问题,而改进的NSPK协议则消除了这个问题。证明了这种方法的有效性。It is a complex problem that how to verify whether a cryptographic protocol is secure. Only formal methods prove a cryptographic protocol is accurate absolutely. A formal method in cryptographic protocol verification is proposed using Petri net. Based on proper assumptions, preconditions between legal user＇s execution and attacker＇s execution of cryptographic protocols are differentiated, and result of execution is given. Then model of attacker is established using Petri net. At last, NSPK is verified with this method. It is proved that a security problem exists in original NSPK, but it is removed in mended NSPK. The efficiency of this method is proved.

关 键 词：密码协议 验证 PETRI网 形式化方法 攻击 

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