A Realistic Environment for Crypto-Protocol Analyses by ASMs.
Giampaolo Bella, Elvinia Riccobene · 1998
. The ASM formalism is tailored to develop a general, realistic environment --- a computer network possibly monitored by an active eavesdropper --- on which any crypto-protocols can be faithfully analysed. The well known Needham-Schroeder protocol with public keys is considered as a case study, and is proven to establish secure sessions between honest agents. The eavesdropper model can reproduce Lowe's attack, and Lowe's correction to the protocol is shown to be effective. ASM proofs are based on induction, and can be carried out without automated tools. 1 Introduction Crypto-protocols are well known to be incredibly error prone. Although the use of formal methods to analyse them has become common practice during the current decade, the notion of correctness of a crypto-protocol is still open ground for research. State enumeration tools search for flaws (i.e. breach of security) by the exhaustive visit of all states reachable by the model. Despite the necessity of drastic simplifying...