摘要： 提出一种基于状态转移系统的安全协议模型，以Dolev-Yao攻击者模型为前提假设，以状态转移系统为框架，用语义编码的方式定义消息和事件，用重写关系定义协议规则，用事件的集合来描述协议的安全属性，并给出安全属性的检验策略。该模型能够对安全协议进行精确的形式化描述，且便于实现自动化分析。

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

Abstract: 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.

Key words: security protocols, formal model, state transition system, rewrite relation, Dolev-Yao intruder model

中图分类号: 

• TP393.08