摘要
运用形式化方法分析密码协议的安全性已成为网络信息安全领域的研究热点之一。提出一种新的扩展Petri网——LPetri网。并且利用LPetri网对TMN密码协议进行建模,采用模型检测工具Maria分析LPetri网模型的可达性,说明利用LPetri网对安全协议建模的有效性。
Using formal method to analyze the cipher protocol has been one of the hot spots in the domain of network information security. Proposes a new extended Petri Net named LPetri Net. Establishes the TMN cipher protocol model with LPetri Net and then uses the model checking tool Maria to analyze the reachability of the LPetri Net. The efficiency of using LPetri Net to model security protocol has been proved.
