摘要
如何验证密码协议的安全性是一个复杂的问题,只有形式化的验证方法才能证明密码协议的绝对正确。利用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.
出处
《计算机工程与设计》
CSCD
北大核心
2007年第6期1317-1319,共3页
Computer Engineering and Design
