Automatizirana analiza protokola za razmjenu ključeva pomoću alata Tamarin prover

undergraduate thesis

• Title (english): Automated analysis of key exchange protocols using the Tamarin prover tool
• Author: Ivan Inkret
• Mentor: Ante Đerek (mentor)
• Committee member: Ante Đerek (predsjednik povjerenstva)
• Committee member: Petar Paradžik (član povjerenstva)
• Committee member: Laura Majer (član povjerenstva)
• Granter: University of Zagreb; Faculty of Electrical Engineering and Computing; Zagreb
• Defense date and country: 2023-07-04, Croatia
• Scientific / art field, discipline and subdiscipline: TECHNICAL SCIENCES; Computing

Abstract

Komunikacija zahtijeva sigurnosne protokole kao način zaštite podataka i identiteta. Ovi protokoli moraju zadovoljavati određena sigurnosna svojstva kao što su tajnost, autentifikacija i integritet. U tu svrhu protokole je potrebno verificirati, tj. provjeriti da su njihova sigurnosna svojstva zadovoljena. Ovo nije jednostavan posao, pogotovo za kompleksne moderne protokole. Razvijeni su automatizirani sistemi koji mogu verificirati svojstva sigurnosnih protokola, a dva glavna pristupa u koje spadaju su simbolički i računarski. Alat tamarin prover spada pod simbolički pristup i njime sam provjerio svojstva protokola za internet stvari koji je razvijen kako bi se zadovoljili specifični zahtjevi u takvom okruženju.

Abstract (english)

Communication requires security protocols as a way to protect data and identity. These protocols must satisfy certain security properties such as secrecy, authentication and integrity. For this purpose, it is necessary to verify the protocols, i.e. check that their security properties are satisfied. This is not a simple task, especially for complex modern protocols. Automated systems have been developed that can verify the properties of security protocols, and the two main approaches they fall into are symbolic and computational approach. The tamarin prover tool belongs to the symbolic approach and I used it to verify the properties of an Internet of Things protocol that was developed to meet the specific requirements in such an environment.

• Keywords: Sigurnosni protokoli; tamarin; sigurnosna svojstva; IoT
• Keywords (english): Security protocols; tamarin; security properties; IoT
• Language: croatian
• URN:NBN: urn:nbn:hr:168:999136
• Study programme: Title: Computing; Study programme type: university; Study level: undergraduate; Academic / professional title: sveučilišni/a prvostupnik/ prvostupnica (baccalaureus/baccalaurea) inženjer/inženjerka računarstva (sveučilišni/a prvostupnik/ prvostupnica (baccalaureus/baccalaurea) inženjer/inženjerka računarstva)
• Type of resource: Text
• File origin: Born digital
• Access conditions: Closed access
• Created on: 2023-10-11 09:05:03