SPI演算规范的建模、实现验证研究

摘要：

针对安全协议安全属性是否满足,缺乏有效性能评价方法的现状,大都使用SPI演算或相近的进程代数方法进行建模.利用这种方法不仅能够有效地形式化描述安全协议,并且能够对安全协议进行多方面的系统评价,但基本上没有说明怎么样寻找设计合适的验证工具,验证其安全属性实现的正确性.本文引入基于SPI演算的验证工具SPRITE来保证建模过程正确性,并设计给出实现映射的具体方法.本方法通过对典型的WOO-LAM单向认证协议予以说明,最后SPRITE产生的具体JAVA代码,给出了安全协议的安全属性,使形式化描述的协议的安全属性是否满足更接近于人的理解而不仅只是机器的解释.

关键词：形式化方法、进程代数、安全协议、SPI演算、应用程序接口(API)

所属期刊栏目：34

分类号：TP3(计算技术、计算机技术)

资助基金：国家自然科学基金60473098;国家高技术研究发展计划863计划2004AA112040

在线出版日期：2007-12-10（万方平台首次上网日期，不代表论文的发表时间）

页数：共4页

页码：80-83