Automatic Security Analysis of Lightweight Authentication and Key Exchange Protocols

Loading...
Thumbnail Image
Journal Title
Journal ISSN
Volume Title
Perustieteiden korkeakoulu | Master's thesis
Date
2022-08-22
Department
Major/Subject
Security and Cloud Computing
Mcode
SCI3113
Degree programme
Master’s Programme in Security and Cloud Computing (SECCLO)
Language
en
Pages
55
Series
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.
Description
Supervisor
Brzuska, Chris
Thesis advisor
Millerjord, Lise
Keywords
perfect forward secrecy, authenticated key exchange, public key cryptography, formal analysis, Tamarin, synchronization robustness
Other note
Citation