Is Eve nearby? Analysing protocols under the distant-attacker assumption

Reynaldo Gil-Pons; Ross Horne; Sjouke Mauw; Alwen Tiu; Rolando Trujillo-Rasua

doi:10.1109/CSF54842.2022.9919655

Is Eve nearby? Analysing protocols under the distant-attacker assumption

Reynaldo Gil-Pons, Ross Horne, Sjouke Mauw, Alwen Tiu, Rolando Trujillo-Rasua

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution book

2 Citations (Scopus)

Abstract

Various modern protocols tailored to emerging wire-less networks, such as body area networks, rely on the proximity and honesty of devices within the network to achieve their security goals. However, there does not exist a security framework that supports the formal analysis of such protocols, leaving the door open to unexpected flaws. In this article we introduce such a security framework, show how it can be implemented in the protocol verification tool Tamarin, and use it to find previously unknown vulnerabilities on two recent key exchange protocols.

Original language	English
Title of host publication	2022 IEEE 35th Computer Security Foundations Symposium (CSF)
Place of Publication	Piscataway, NJ
Publisher	IEEE
Pages	17-32
Number of pages	16
ISBN (Electronic)	9781665484176
ISBN (Print)	9781665484183
DOIs	https://doi.org/10.1109/CSF54842.2022.9919655
Publication status	Published - 31 Oct 2022
Event	35th IEEE Computer Security Foundations Symposium, CSF 2022 - Haifa, Israel Duration: 7 Aug 2022 → 10 Aug 2022

Publication series

Name	IEEE Computer Security Foundations Symposium
Volume	2022-August
ISSN (Print)	1940-1434

Conference

Conference	35th IEEE Computer Security Foundations Symposium, CSF 2022
Country/Territory	Israel
City	Haifa
Period	7/08/22 → 10/08/22

Funding

This work was supported by the Luxembourg National Research Fund, Luxembourg, under the grant AFR-PhD-14565947.

Keywords

distance bounding
distant attacker
formal verification
key exchange
security protocols

Access to Document

10.1109/CSF54842.2022.9919655

Cite this

@inproceedings{302ea1eb024448fca77ea4aa4f64ab72,

title = "Is Eve nearby? Analysing protocols under the distant-attacker assumption",

abstract = "Various modern protocols tailored to emerging wire-less networks, such as body area networks, rely on the proximity and honesty of devices within the network to achieve their security goals. However, there does not exist a security framework that supports the formal analysis of such protocols, leaving the door open to unexpected flaws. In this article we introduce such a security framework, show how it can be implemented in the protocol verification tool Tamarin, and use it to find previously unknown vulnerabilities on two recent key exchange protocols.",

keywords = "distance bounding, distant attacker, formal verification, key exchange, security protocols",

author = "Reynaldo Gil-Pons and Ross Horne and Sjouke Mauw and Alwen Tiu and Rolando Trujillo-Rasua",

year = "2022",

month = oct,

day = "31",

doi = "10.1109/CSF54842.2022.9919655",

language = "English",

isbn = "9781665484183",

series = "IEEE Computer Security Foundations Symposium",

publisher = "IEEE",

pages = "17--32",

booktitle = "2022 IEEE 35th Computer Security Foundations Symposium (CSF)",

note = "35th IEEE Computer Security Foundations Symposium, CSF 2022 ; Conference date: 07-08-2022 Through 10-08-2022",

}

Gil-Pons, R, Horne, R, Mauw, S, Tiu, A & Trujillo-Rasua, R 2022, Is Eve nearby? Analysing protocols under the distant-attacker assumption. in 2022 IEEE 35th Computer Security Foundations Symposium (CSF). IEEE Computer Security Foundations Symposium, vol. 2022-August, IEEE, Piscataway, NJ, pp. 17-32, 35th IEEE Computer Security Foundations Symposium, CSF 2022, Haifa, Israel, 7/08/22. https://doi.org/10.1109/CSF54842.2022.9919655

Is Eve nearby? Analysing protocols under the distant-attacker assumption. / Gil-Pons, Reynaldo; Horne, Ross; Mauw, Sjouke et al.
2022 IEEE 35th Computer Security Foundations Symposium (CSF). Piscataway, NJ: IEEE, 2022. p. 17-32 (IEEE Computer Security Foundations Symposium; Vol. 2022-August).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution book

TY - GEN

T1 - Is Eve nearby? Analysing protocols under the distant-attacker assumption

AU - Gil-Pons, Reynaldo

AU - Horne, Ross

AU - Mauw, Sjouke

AU - Tiu, Alwen

AU - Trujillo-Rasua, Rolando

PY - 2022/10/31

Y1 - 2022/10/31

N2 - Various modern protocols tailored to emerging wire-less networks, such as body area networks, rely on the proximity and honesty of devices within the network to achieve their security goals. However, there does not exist a security framework that supports the formal analysis of such protocols, leaving the door open to unexpected flaws. In this article we introduce such a security framework, show how it can be implemented in the protocol verification tool Tamarin, and use it to find previously unknown vulnerabilities on two recent key exchange protocols.

AB - Various modern protocols tailored to emerging wire-less networks, such as body area networks, rely on the proximity and honesty of devices within the network to achieve their security goals. However, there does not exist a security framework that supports the formal analysis of such protocols, leaving the door open to unexpected flaws. In this article we introduce such a security framework, show how it can be implemented in the protocol verification tool Tamarin, and use it to find previously unknown vulnerabilities on two recent key exchange protocols.

KW - distance bounding

KW - distant attacker

KW - formal verification

KW - key exchange

KW - security protocols

U2 - 10.1109/CSF54842.2022.9919655

DO - 10.1109/CSF54842.2022.9919655

M3 - Conference contribution book

AN - SCOPUS:85141869811

SN - 9781665484183

T3 - IEEE Computer Security Foundations Symposium

SP - 17

EP - 32

BT - 2022 IEEE 35th Computer Security Foundations Symposium (CSF)

PB - IEEE

CY - Piscataway, NJ

T2 - 35th IEEE Computer Security Foundations Symposium, CSF 2022

Y2 - 7 August 2022 through 10 August 2022

ER -

Is Eve nearby? Analysing protocols under the distant-attacker assumption

Abstract

Publication series

Conference

Funding

Keywords

Access to Document

Fingerprint

Cite this