基于时间Petri网的密码协议分析
形式化分析方法由于其精炼、简洁和无二义性逐步成为分析密码协议的一条可靠和准确的途径,但是密码协议的形式化分析研究目前还不够深入.在文中首先对四类常见的密码协议形式化分析方法作了一些比较,阐述了各自的特点,然后用时间Petri网来表示和分析密码协议.该方法不但能够反映协议的静态和动态的特性,而且能够对密码协议进行时间、空间上的性能评估.作为实例,对Aziz-Diffie无线协议作了详细的形式分析和性能评估,验证了已知的、存在的漏洞,并且给出了该协议的改进方案.
密码协议 时间Petri网 BAN逻辑 认证协议
张广胜 吴哲辉 逄玉叶
山东科技大学信息学院(山东泰安) 山东大学信息科学与工程学院(山东济南)
国内会议
杭州
中文
11-16
2003-09-01（万方平台首次上网日期，不代表论文的发表时间）