Formal verification of the Lowe modified BAN concrete Andrew Secure RPC protocol

The Andrew Secure RPC (ASRPC) is a protocol that allows two entities, already shared a secret key, to establish a new cryptographic key. It must guarantee the authenticity of the new sharing session key in every session. Since the original protocol, several revised versions have been made in order to make the protocol more secure. In this paper we present a formal development to prove the correctness of the newly modified version, we use the formal method Event-B and the Rodin tool to model the protocol and to verify that the desired security properties hold. We show that the protocol is indeed more secure than the previous versions.