Type-directed Trace Analysis of Security Protocols in Process Calculus
Guoqiang Li, Bochao Liu, Xin Li, Mizuhito Ogawa · 2008
Abstract. Trace analysis, one of the formal methods to verify security protocols, represents every possible runs of the protocols as traces and analyzes whether any unsafe state is reachable. However, the number of states is infinite because we assume the intruder can generate infinite messages. In this paper, a typed process calculus inspired by the spi calculus is proposed to model the protocol and the security properties. Then based on the the type information, a parametric system with finite states is generated and enjoys sound and complete simulation property of the former system. 1