AnB2Murphi: A translator for converting Alice&Bob specifications to murphi

As an important part of Internet of Things and 5G network technology, security protocols play a critical role in ensuring communication security. Formal analysis of security protocol has been successfully applied to find design flaws in recent years. Many formal verification tools have been used to verify the security protocols, including Murphi model checker. However, security protocols are often expressed in so-called Alice&Bob notation to describe the messages exchanged between honest principals. And security protocols defined by the A&B specifications can not be applied to the formal verification tool directly. Therefore, there is a gap between Alice&Bob specifications and the modeling languages of the formal tools. In this paper, we propose AnB2Murphi, a novel and general translator which compiles the Alice&Bob specifications of security protocols into the input language of Murphi to bridge the gap. First, we specify the Alice&Bob specifications of the security protocol. Then we take the strand space as the intermediate form between A&B specifications and Murphi formal model. Finally, we use the Murphi model checker to verify the generated model of security protocol. The case studies of security protocols like Needham-Schroeder public key protocol and 5G EAP-TLS authentication protocol demonstrate the efficiency of our translator.