Analyzing DTLS security in Tamarin
Authors
Møller, Tobias ; Rusbjerg, Signe Kirstine
Term
4. term
Education
Publication year
2025
Submitted on
2025-06-12
Pages
63
Abstract
Denne kandidatafhandling undersøger sikkerheden i DTLS 1.3 med udgangspunkt i IoT-brug og den begrænsede offentlige udbredelse af versionen sammenlignet med TLS 1.3. Målet er at verificere, om protokollen opfylder sine specificerede sikkerhedsgarantier, og at belyse, hvordan tilgængelighed bedst kan analyseres. Vi udvikler tre formelle modeller i Tamarin Prover: et fuldt handshake med cookie-udveksling til førstegangskommunikation, et PSK-baseret handshake til genforbindelse, og recordlaget som står for kryptering og integritetsbeskyttelse af meddelelser. Modellerne er baseret på RFC 9147 (DTLS 1.3) og RFC 8446 (TLS 1.3), som DTLS-specifikationen refererer til, og de følges op af modelvalidering og formulering af sikkerhedsegenskaber. Vi adresserer de tre CIAA-kategorier fortrolighed, integritet og autenticitet i Tamarin, hvor flere sikkerhedsaspekter valideres og verificeres, mens tilgængelighed ikke var praktisk mulig at analysere i Tamarin. For at supplere analysen skitserer vi derfor en generel metode til at oversætte Tamarin-modeller til UPPAAL, et værktøj bedre egnet til at undersøge tilgængelighed (og som tidligere er anvendt af gruppen). Arbejdet bidrager med en DTLS 1.3-model for håndtryk og recordlag, en formel verifikationsramme og et forslag til værktøjsoversættelse, der kan understøtte fremtidig evaluering af tilgængelighed.
This master’s thesis examines the security of DTLS 1.3 in the context of IoT use and its limited public uptake compared to TLS 1.3. The goal is to verify whether the protocol meets its specified security guarantees and to clarify how availability can be effectively analyzed. We develop three formal models in the Tamarin Prover: a full handshake with cookie exchange for first-time communication, a PSK-based handshake for resumption, and the record layer that provides message encryption and integrity protection. The models are grounded in RFC 9147 (DTLS 1.3) and RFC 8446 (TLS 1.3), to which the DTLS specification refers, and are accompanied by model validation and explicit security properties. We address the CIAA categories of confidentiality, integrity, and authenticity in Tamarin, where several security aspects are validated and verified, while availability was not practical to assess in Tamarin. To complement the analysis, we outline a general method to translate Tamarin models to UPPAAL, a tool better suited to study availability (and previously used by the group). The work contributes a DTLS 1.3 model of handshakes and the record layer, a formal verification setup, and a translation proposal to support future availability evaluation.
[This abstract was generated with the help of AI]
Documents