Automatic Security Analysis of Lightweight Authentication and Key Exchange Protocols

Abstract

Perfect Forward Secrecy (PFS) is vital in contemporary authenticated key exchange (AKE) protocols. Typically attained using public key cryptography, achieving forward secrecy is infeasible for communication in resource-constrained environment. Consequently, lightweight AKE protocols that offer PFS with only symmetric primitives are recently proposed. Formal analysis of these protocols can help in providing credibility prior to their deployment, and also reliably serve as a universally understood proof for the corresponding security properties.

To this end, we perform the formal verification of the SAKE protocol using an automatic verification tool Tamarin. In addition to proving the claimed security properties of session key secrecy, authentication and forward security, through Tamarin analysis, we also illustrate an attack that breaks the synchronization robustness of the protocol, resulting in de-synchronization of the internal states of the communicating parties. Furthermore, we have cogently presented a comprehensive guide to using Tamarin as a verification tool, detailing its key features, software usage and the foundational logic behind its analysis.