Formal Model for Security Protocols Based on State Transition System
Yuefei Zhu · Jisuanji gongcheng · 2008
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.