摘要
提出一种基于状态转移系统的安全协议模型,以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.
出处
《计算机工程》
CAS
CSCD
北大核心
2008年第13期149-151,共3页
Computer Engineering
基金
国家自然科学基金资助项目(60473021)
