Automated analysis of key exchange protocols using the Tamarin prover tool

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.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