Formalna verifikacija post-kvantnog protokola pomoću alata Tamarin

diplomski rad

• Naslov (engleski): Formal verification of a post-quantum protocol using the Tamarin tool
• Autor: Ivan Futivić
• Mentor: Ante Đerek (mentor)
• Član povjerenstva: Ante Đerek (predsjednik povjerenstva)
• Član povjerenstva: Marin Golub (član povjerenstva)
• Član povjerenstva: Adrian Satja Kurdija (član povjerenstva)
• Ustanova koja je dodijelila akademski / stručni stupanj: Sveučilište u Zagrebu; Fakultet elektrotehnike i računarstva; Zagreb
• Datum i država obrane: 2024-07-02, Hrvatska

Sažetak

Ovaj diplomski rad bavi se sigurnosnom analizom PQXDH protokola, post-kvantne modifikacije X3DH protokola razvijenog za aplikaciju Signal. Cilj rada bio je analizirati sigurnosna svojstva protokola koristeći alat za formalnu verifikaciju Tamarin. Provedena je analiza sigurnosnih svojstava poput autentičnosti, integriteta i unaprijedne povjerljivosti. Rezultati su pokazali da PQXDH protokol zadovoljava sva ključna sigurnosna svojstva. Formalna verifikacija također je omogućila identifikaciju kritičnih dijelova protokola, potvrđujući njihovu neophodnost u osiguravanju navedenih svojstava i cjelokupne sigurnosti protokola. Ovaj rad također potvrđuje važnost formalne verifikacije u razvoju sigurnih kriptografskih protokola otpornih na napade kvantnim računalima.

Sažetak (engleski)

This thesis describes a security analysis of the PQXDH protocol, a post-quantum modification of the X3DH protocol developed by Signal. The goal of the thesis is to analyze the security properties of the protocol using a formal verification tool called Tamarin. These properties include authenticity, integrity, and forward secrecy. The results show that the PQXDH protocol meets all key security properties. Formal verification also enabled the identification of some critical parts of the protocol, confirming their necessity in ensuring these properties and the overall security of the protocol. This paper also underscores the importance of formal verification in the development of secure cryptographic protocols resistant to attacks by quantum computers.

• Ključne riječi: Tamarin; X3DH; PQXDH; formalna verifikacija; post-kvantna kriptografija
• Ključne riječi (engleski): Tamarin; X3DH; PQXDH; formal verification; post-quantum cryptography
• Jezik: hrvatski
• URN:NBN: urn:nbn:hr:168:404428
• Studijski program: Naziv: Računarstvo; Vrsta studija: sveučilišni; Stupanj studija: diplomski; Akademski / stručni naziv: magistar/magistra inženjer/inženjerka računarstva (mag.ing.comp.)
• Vrsta resursa: Tekst
• Način izrade datoteke: Izvorno digitalna
• Prava pristupa: Zatvoreni pristup
• Datum i vrijeme pohrane: 2024-10-12 20:35:38