Describing and verifying cryptographic protocal using PI-calculus
Zhang Xiao-pei, Luo Wen-Jun, Xiang Li · 2008
Using formal method is an effective methodology for modeling and verifying software system. Describing and verifying cryptographic protocol by formal method is an important research. Pi-calculus is a kind of mobile process algebra which can be used to model concurrent and dynamic system. Mobility Workbench (MWB) is an automatic tool for pi-calculus and can be used for analyzing and verifying mobile concurrent system described by pi-calculus. In this paper we analyze Aziz-Diffie wireless communication security protocol using formal method based pi-calculus and verifying the attack of this protocol by MWB.