Analyzing security protocols by a bisimulation method based on environmental knowledge

The bisimulation method is the kernel of process calculi; it is usually used to reason about reactive systems. When it comes to the spi calculus (an extension of the π-calculus), we must take into account the knowledge of the environment with which a protocol interacts. Framed bisimulation is such a kind of environmental knowledge sensitive bisimulation relation. The paper tries it on checking the soundness of the Kerberos protocol. Rigorous proofs on its two security properties reveal that the authenticity property holds while its secrecy property is threatened by a possible attack.