基于时延Petri网的密码协议分析及性能评估

摘要

形式化分析方法由于其精炼、简洁和无二义性逐步成为分析密码协议的一条可靠和准确的途径,但是密码协议的形式化分析研究目前还不够深入,针对这一现状,该文提出用时延Petri网来表示和分析密码协议.该模型不但能够反映协议的静态和动态的特性,而且能够对密码协议进行时间、空间上的性能评估.作为实例,文章对MSR无线协议作了详细的形式分析和性能评估.最后,与其它形式化分析密码协议的方法作了比较.