Automatic Security Analysis of Lightweight Authentication and Key Exchange Protocols

Thumbnail Image

Files

master_Kabra_Adhirath_2022.pdf (1.6 MB)

URL

Journal Title

Journal ISSN

Volume Title

Perustieteiden korkeakoulu | Master's thesis
Unless otherwise stated, all rights belong to the author. You may download, display and print this publication for Your own personal use. Commercial use is prohibited.

Authors

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

Permanent link to this item

https://urn.fi/URN:NBN:fi:aalto-202208285061

Collections

[dipl] Perustieteiden korkeakoulu / SCI