A Simple Process Calculus for the analysis of Security Protocols
Yonggen Gu, Yuxi Fu · 2005
The spi calculus has been proved useful for reasoning about security protocols. It is however difficult to mechanize the equivalence checking in that framework due to the complexity caused by name passing communications. The paper proposes a calculus for the analysis of the security protocols (SPC for short) as a simplification of the spi calculus. SPC can explicitly express environment knowledge, protocol participants and their knowledge. We present its syntax and semantics, and specify some security properties in terms of equivalence relations. Finally two examples of formal verification is given.