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

• 作者: 侯迪 徐东红 齐勇
• 来源期刊: 计算机科学
• 学科: 工学
• 关键词: 形式化方法 进程代数 安全协议 SPI演算 应用程序接口(API)
• 年，卷（期）: 2007,（10）
• 所属期刊栏目: 计算机网络与信息技术
• 页码范围: 80-83
• 页数: 4页
• 分类号: TP3
• 字数: 4852字
• 语种: 中文
• DOI: 10.3969/j.issn.1002-137X.2007.10.018

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	侯迪	西安交通大学电子与信息工程学院	45	532	12.0	22.0
2	齐勇	西安交通大学电子与信息工程学院	80	870	16.0	27.0
3	徐东红	西安交通大学电子与信息工程学院	2	4	2.0	2.0