Formal Verification and Standardization of Security Protocols

Thumbnail Image

Files

isbn9789526413341.pdf (869.6 KB)

URL

Journal Title

Journal ISSN

Volume Title

School of Science | Doctoral thesis (article-based) | Defence date: 2023-08-08
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

2023

Department

Tietotekniikan laitos
Department of Computer Science

Major/Subject

Mcode

Degree programme

Language

en

Pages

58 + app. 110

Series

Aalto University publication series DOCTORAL THESES, 101/2023

Abstract

Secure communication over open networks is fundamental to many modern information systems. Previously centralized architectures now depend on distributed computing and inter-system communication over the Internet. Consequently, the need for secure, reliable, and efficient cryptographic protocols has grown significantly. The demand is further amplified by the emergence of new technologies, such as the Internet of Things, that require previously autonomous devices to interact or connect to remote servers. Numerous security breaches have shown that design flaws in these increasingly complex systems can be challenging to detect and sometimes go unnoticed for years. This thesis demonstrates how formal verification can be used during the development and standardization process of cryptographic protocols to avoid critical security flaws and to detect issues. Formal verification methods provide a way of analyzing the security of a protocol even before it has been implemented or deployed. These methods can be used to ensure that, at the very least, common vulnerabilities and design flaws are avoided. This is particularly important for standards organizations since revising an already standardized protocol is slow and complicated. This thesis evaluates the security of widely deployed protocols and work-in-progress drafts presented to organizations such as the Internet Engineering Task Force (IETF) and the 3rd Generation Partnership Project (3GPP). Specifically, we use two state-of-the-art verification tools, ProVerif and Tamarin prover, to model cryptographic protocols and verify their intended security goals. We identify an identity misbinding attack in device pairing and bootstrapping protocols. Our case study discovers multiple variations of the attack in Bluetooth, Device Provisioning Protocol (DPP), Wi-Fi Direct, and Nimble Out-of-Band Authentication for EAP (EAP-NOOB). Furthermore, we argue that the same attacks are possible for all protocols in this category since they do not require pre-distributed credentials and instead rely on physical access for authentication. We also comprehensively analyze the security of two protocols designed for mobile networks: the consumer Remote SIM Provisioning (RSP) protocol and 5G handover. Finally, we present a case study of a recently standardized device bootstrapping protocol, EAP-NOOB, and explain howformal verification was used throughout the standardization process to understand the security goals and identify potential weaknesses in the design.

Suojattu viestintä avoimissa verkoissa on olennaista monille nykyaikaisille tietojärjestelmille. Aiemmin keskitetyt arkkitehtuurit ovat entistä riippuvaisempia hajautetuista järjestelmistä ja niiden välisestä tiedonsiirrosta Internetin välityksellä. Tämän seurauksena turvallisten, luotettavien ja tehokkaiden salausprotokollien tarve on kasvanut merkittävästi. Kysyntää lisää entisestään uusien teknologioiden, kuten esineiden internetin, ilmaantuminen. Aiemmin itsenäisten laitteiden vaaditaan nyt toimivan vuorovaikutuksessa keskenään tai muodostavan yhteyden etäpalvelimiin. Lukuisat tietoturvahyökkäykset ovat osoittaneet, että yhä monimutkaisempien järjestelmien tietoturvariskien havaitseminen on vaikeaa ja ne voivat jäädä huomaamatta jopa vuosien ajan. Tämä väitöskirja osoittaa, kuinka formaalia verifiointia voidaan käyttää kryptografisten protokollien kehitys- ja standardointiprosessin aikana kriittisten haavoittuvuuksien välttämiseen ja ongelmien havaitsemiseen. Formaalit verifiointimenetelmät mahdollistavat protokollien tietoturvan analysoinnin jo ennen niiden käyttöönottoa. Näillä menetelmillä voidaan varmistaa, että ainakin yleiset haavoittuvuudet ja suunnitteluvirheet vältetään. Tämä on erityisen tärkeää standardointiorganisaatioille, kuten Internet Engineering Task Force (IETF) ja 3rd Generation Partnership Project (3GPP), koska jo standardoidun protokollan päivittäminen on hidasta ja monimutkaista. Tässä väitöskirjassa arvioidaan sekä laajalti käytettyjen protokollien että työn alla olevien luonnosten turvallisuutta. Käytämme kahta viimeisintä tekniikkaa edustavaa verifiointityökalua, ProVerif ja Tamarin prover, mallintamaan kryptografisia protokollia ja analysoimaan niiden tietoturvaa. Identifioimme identiteettien väärinsitomisen mahdollistavan hyökkäyksen laitteiden yhdistämiseen käytettävissä protokollissa. Tapaustutkimuksemme esittelee useita muunnelmia hyökkäyksestä protokollissa, kuten Bluetooth, Device Provisioning Protocol (DPP), Wi-Fi Direct ja Nimble Out-of-Band Authentication for EAP (EAP-NOOB). Lisäksi osoitamme, että samat hyökkäykset ovat mahdollisia kaikissa vastaavissa protokollissa, jotka käyttävät fyysistä hallintaa identiteettien todennusta varten. Analysoimmemyös kattavasti kahden mobiiliverkoissa käytettyjen protokollien (Remote SIM Provisioning ja 5G handover) turvallisuutta. Lopuksi esittelemme äskettäin standardoidun EAP-NOOB protokollan ja kerromme, kuinka formaalia verifiointia käytettiin sen standardointiprosessin ajan tietoturvatavoitteiden ymmärtämiseen ja mahdollisten haavoittuvuuksien tunnistamiseen.

Description

Supervising professor

Aura, Tuomas, Prof., Aalto University, Department of Computer Science, Finland

Thesis advisor

Sethi, Mohit, Dr., Aalto University, Department of Computer Science, Finland

Keywords

formal verification, cryptographic protocols, device bootstrapping, standardization, formaali verifiointi, salausprotokollat, standardointi

Other note

Parts

  • [Publication 1]: Mohit Sethi, Aleksi Peltonen, and Tuomas Aura. Misbinding Attacks on Secure Device Pairing and Bootstrapping. In Proceedings of the 2019 ACM Asia Conference on Computer and Communications Security (Asia CCS ’19), pages 453–464, July 2019.
    Full text in Acris/Aaltodoc: http://urn.fi/URN:NBN:fi:aalto-201909205369
    DOI: 10.1145/3321705.3329813 View at publisher
  • [Publication 2]: Aleksi Peltonen, Mohit Sethi, and Tuomas Aura. Formal verification of misbinding attacks on secure device pairing and bootstrapping. Journal of Information Security and Applications (JISA), 51, February 2020.
    Full text in Acris/Aaltodoc: http://urn.fi/URN:NBN:fi:aalto-202004282923
    DOI: 10.1016/j.jisa.2020.102461 View at publisher
  • [Publication 3]: Abu Shohel Ahmed, Aleksi Peltonen, Mohit Sethi, and Tuomas Aura. Security Analysis of the Consumer Remote SIM Provisioning Protocol. Submitted for publication, November 2022.
  • [Publication 4]: Aleksi Peltonen, Ralf Sasse, and David Basin. A Comprehensive Formal Analysis of 5G Handover. In Proceedings of the 14th ACM Conference on Security and Privacy in Wireless and Mobile Networks (WiSec ’21), pages 1–12, June 2021.
    Full text in Acris/Aaltodoc: http://urn.fi/URN:NBN:fi:aalto-202108048172
    DOI: 10.1145/3448300.3467823 View at publisher
  • [Publication 5]: Aleksi Peltonen, Eduardo Ingles, Sampsa Latvala, Dan Garcia-Carrillo, Mohit Sethi, and Tuomas Aura. Enterprise Security for the Internet of Things (IoT): Lightweight Bootstrapping with EAP-NOOB. Sensors, 20(21), October 2020.
    Full text in Acris/Aaltodoc: http://urn.fi/URN:NBN:fi:aalto-2020113020501
    DOI: 10.3390/s20216101 View at publisher

Citation

Permanent link to this item

https://urn.fi/URN:ISBN:978-952-64-1334-1

Collections

[diss] Perustieteiden korkeakoulu / SCI