KEMEDHOC*: A formally verified quantum-safe key exchange protocol

Thumbnail Image

Files

master_Nguyen_Cuong_2025.pdf (1.7 MB)

URL

Journal Title

Journal ISSN

Volume Title

School of Science | 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

2025-10-30

Department

Major/Subject

Security and Cloud Computing

Mcode

Degree programme

Master's Programme in Computer, Communication and Information Sciences
Master's Programme in Computer, Communication and Information Sciences
Master's Programme in Computer, Communication and Information Sciences

Language

en

Pages

134

Series

Abstract

The advent of quantum computing poses significant threats to classical public-key cryptographic systems such as RSA and Elliptic Curve Cryptography, necessitating quantum-safe migration paths for Internet of Things (IoT) communication. The Ephemeral Diffie-Hellman Over COSE (EDHOC) protocol provides lightweight authenticated key exchange for resource-constrained IoT devices but lacks quantum-safe security and formally verified implementations. This thesis introduces KEMEDHOC, a KEM-based, signature-free, post-quantum variant of EDHOC that achieves mutual authentication through optimized integration of Key Encapsulation Mechanisms (KEMs). Compared to the direct adaptation, KEMEDHOC reduces noticeably message size (by over \textbf{33\%}) and handshake time (by \textbf{15\%}), while maintaining comparable security levels. Formal verification, at design-level, using ProVerif confirms that KEMEDHOC preserve all core EDHOC security properties, including mutual authentication, confidentiality, and forward secrecy. Verified implementations (EDHOC* and KEMEDHOC*) developed in F* and Low* ensure functional correctness, memory safety, and timing constant-time behavior, down to verified C code through KaRaMel compiler. Overall, this thesis delivers the first end-to-end formally verified post-quantum variant of EDHOC, demonstrating that formal assurance and post-quantum security can be obtained efficiently in lightweight key exchange protocols.

Description

Supervisor

Lai, Russell W. F.

Thesis advisor

Sovio, Sampo

Keywords

post-quantum cryptography (PQC), authenticated key exchange, EDHOC, formal verification, ProVerif, F*

Other note

Citation

Permanent link to this item

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

Collections

[dipl] Perustieteiden korkeakoulu / SCI