基于状态转移系统的安全协议形式模型  

Formal Model for Security Protocols Based on State Transition System

作　　者：毛中全[1] 刘楠[1] 顾纯祥[1] 祝跃飞[1] 

机构地区：[1]信息工程大学信息工程学院,郑州450002

出　　处：《计算机工程》2008年第13期149-151,共3页Computer Engineering

基　　金：国家自然科学基金资助项目(60473021)

摘　　要：提出一种基于状态转移系统的安全协议模型,以Dolev-Yao攻击者模型为前提假设,以状态转移系统为框架,用语义编码的方式定义消息和事件,用重写关系定义协议规则,用事件的集合来描述协议的安全属性,并给出安全属性的检验策略。该模型能够对安全协议进行精确的形式化描述,且便于实现自动化分析。This paper proposes a formal model based on state transition system. Dolev-Yao intruder model are assumed, and based on state transition system, message and event are semantically encoded, protocol rule are defined by rewrite relation, and security properties are descripted by event set. It proposes inspection strategy for security properties. The model can give accurate formal specifications for security protocols, and is easy to realize automatic analysis.

关 键 词：安全协议 形式模型 状态转移系统 重写关系 Dolev-Yao攻击者模型 

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