Formal Verification and Standardization of Security Protocols

Aleksi Peltonen

Formal Verification and Standardization of Security Protocols

Julkaisun otsikon käännös: Salausprotokollien formaali verifiointi ja standardointi

Aleksi Peltonen

Tutkimustuotos: Doctoral Thesis › Collection of Articles

Abstrakti

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.

Julkaisun otsikon käännös	Salausprotokollien formaali verifiointi ja standardointi
Alkuperäiskieli	Englanti
Pätevyys	Tohtorintutkinto
Myöntävä instituutio	Aalto-yliopisto
Valvoja/neuvonantaja	Aura, Tuomas, Vastuuprofessori Sethi, Mohit, Ohjaaja
Kustantaja	Aalto University
Painoksen ISBN	978-952-64-1333-4
Sähköinen ISBN	978-952-64-1334-1
Tila	Julkaistu - 2023
OKM-julkaisutyyppi	G5 Artikkeliväitöskirja

Tutkimusalat

formaali verifiointi
salausprotokollat
standardointi

Pääsy asiakirjaan

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

Siteeraa tätä

@phdthesis{5273e6530c60477d918d9a6163be9874,

title = "Formal Verification and Standardization of Security Protocols",

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

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

author = "Aleksi Peltonen",

year = "2023",

language = "English",

isbn = "978-952-64-1333-4",

series = "Aalto University publication series DOCTORAL THESES",

publisher = "Aalto University",

number = "101",

address = "Finland",

school = "Aalto University",

}

TY - BOOK

T1 - Formal Verification and Standardization of Security Protocols

AU - Peltonen, Aleksi

PY - 2023

Y1 - 2023

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

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

KW - formal verification

KW - cryptographic protocols

KW - device bootstrapping

KW - standardization

KW - formaali verifiointi

KW - salausprotokollat

KW - standardointi

KW - formal verification

KW - cryptographic protocols

KW - device bootstrapping

KW - standardization

M3 - Doctoral Thesis

SN - 978-952-64-1333-4

T3 - Aalto University publication series DOCTORAL THESES

PB - Aalto University

ER -

Formal Verification and Standardization of Security Protocols

Abstrakti

Tutkimusalat

Pääsy asiakirjaan

Sormenjälki

Siteeraa tätä