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

Research on Model and Implementation Authentication of SPI Calculus Specifications

作　　者：徐东红[1] 齐勇[1] 侯迪[1] 

机构地区：[1]西安交通大学电子与信息工程学院,西安710049

出　　处：《计算机科学》2007年第10期80-83,共4页Computer Science

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

摘　　要：针对安全协议安全属性是否满足,缺乏有效性能评价方法的现状,大都使用SPI演算或相近的进程代数方法进行建模。利用这种方法不仅能够有效地形式化描述安全协议,并且能够对安全协议进行多方面的系统评价,但基本上没有说明怎么样寻找设计合适的验证工具,验证其安全属性实现的正确性。本文引入基于SPI演算的验证工具SPRITE来保证建模过程正确性,并设计给出实现映射的具体方法。本方法通过对典型的WOO-LAM单向认证协议予以说明,最后SPRITE产生的具体JAVA代码,给出了安全协议的安全属性,使形式化描述的协议的安全属性是否满足更接近于人的理解而不仅只是机器的解释。Under the situations of effective approach being lack to evaluate the security properties of security protocols, an approach is proposed to construct the security protocol based on SPI calculus or similar process algebra in this paper. Applying this approach, the formal description of security protocol can be described effectively, furthermore, the SPI calculus can be implemented. However, there is no any traces to illustrate how to find or design an adapted tool to authenticate the correction of the security properties of the security protocol. In this paper we introduce SPRITE, SPRITE is a tool based on SPI calculus that can guarantee whether is the model and process describing right or not, and design the concrete ways to implement the reflection from abstract SPI calculus to concrete Java code. The approach is illustrated by a typed one way authentication protocol WOO-LAM security protocol. The authentication tool SPRITE generate concrete Java code that can be simple and concrete to describe the security property. It is more adapt to mankind＇s understand not just to adapt computer interpretation.

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

分 类 号：TP393.08[自动化与计算机技术—计算机应用技术]