ITU

Formal Analysis of EDHOC Key Establishment for Constrained IoT Devices

Research output: Book / Anthology / Report / Ph.D. thesisReport

Standard

Formal Analysis of EDHOC Key Establishment for Constrained IoT Devices. / Bruni, Alessandro; Normann, Karl; Sundararajan, Vaishnavi.

2020. 20 p.

Research output: Book / Anthology / Report / Ph.D. thesisReport

Harvard

APA

Vancouver

Author

Bruni, Alessandro ; Normann, Karl ; Sundararajan, Vaishnavi. / Formal Analysis of EDHOC Key Establishment for Constrained IoT Devices. 2020. 20 p.

Bibtex

@book{e8ecb3acf96e469fb990904762a21346,
title = "Formal Analysis of EDHOC Key Establishment for Constrained IoT Devices",
abstract = "The IETF is standardizing an authenticated key establishment (AKE) protocol named EDHOC for constrained IoT devices. In contrast to more powerful devices like web cameras and cars, which receive a lot of media attention, such devices operate under severe energy consumption and message size restrictions. EDHOC was first formally analyzed in 2018 by Bruni et al. Since then, the protocol has been significantly extended and now has three new key establishment methods. In this paper, we formally analyze all methods of EDHOC in a symbolic Dolev-Yao model, using the Tamarin verification tool. We show that the different methods provide sensible, but also rather heterogeneous security properties, and discuss various consequences of this. Our work has also led to improvements in the design and the specification of EDHOC. ",
author = "Alessandro Bruni and Karl Normann and Vaishnavi Sundararajan",
year = "2020",
month = jul,
day = "22",
language = "English",

}

RIS

TY - RPRT

T1 - Formal Analysis of EDHOC Key Establishment for Constrained IoT Devices

AU - Bruni, Alessandro

AU - Normann, Karl

AU - Sundararajan, Vaishnavi

PY - 2020/7/22

Y1 - 2020/7/22

N2 - The IETF is standardizing an authenticated key establishment (AKE) protocol named EDHOC for constrained IoT devices. In contrast to more powerful devices like web cameras and cars, which receive a lot of media attention, such devices operate under severe energy consumption and message size restrictions. EDHOC was first formally analyzed in 2018 by Bruni et al. Since then, the protocol has been significantly extended and now has three new key establishment methods. In this paper, we formally analyze all methods of EDHOC in a symbolic Dolev-Yao model, using the Tamarin verification tool. We show that the different methods provide sensible, but also rather heterogeneous security properties, and discuss various consequences of this. Our work has also led to improvements in the design and the specification of EDHOC.

AB - The IETF is standardizing an authenticated key establishment (AKE) protocol named EDHOC for constrained IoT devices. In contrast to more powerful devices like web cameras and cars, which receive a lot of media attention, such devices operate under severe energy consumption and message size restrictions. EDHOC was first formally analyzed in 2018 by Bruni et al. Since then, the protocol has been significantly extended and now has three new key establishment methods. In this paper, we formally analyze all methods of EDHOC in a symbolic Dolev-Yao model, using the Tamarin verification tool. We show that the different methods provide sensible, but also rather heterogeneous security properties, and discuss various consequences of this. Our work has also led to improvements in the design and the specification of EDHOC.

M3 - Report

BT - Formal Analysis of EDHOC Key Establishment for Constrained IoT Devices

ER -

ID: 85512920