Formal Verification of Ephemeral Diffie-Hellman Over COSE (EDHOC)

Alessandro Bruni, Thorvald Sahl Jørgensen, Theis Grønbech Petersen, Carsten Schürmann

Publikation: Konference artikel i Proceeding eller bog/rapport kapitelKonferencebidrag i proceedingsForskningpeer review


Ephemeral Diffie-Hellman over COSE (EDHOC) [1] is an authentication protocol that aims to replace TLS for resource constrained Internet of Things (IoT) devices using a selection of lightweight ciphers and formats. It is inspired by the newest Internet Draft of TLS 1.3 [2] and includes reduced round-trip modes. Unlike TLS 1.3, EDHOC is designed from scratch, and does not have to support legacy versions of the protocol. As the protocol is neither well-known nor has been used in practice it has not been scrutinized to the extent it should be.
The objective of this paper is to verify security properties of the protocol, including integrity, secrecy, and perfect forward secrecy properties. We use ProVerif [3] to analyze these properties formally. We describe violations of specific security properties for the reduced round-trip modes. The flaws were reported to the authors of the EDHOC protocol.
TitelSecurity Standardisation Research : 4th International Conference
RedaktørerCas Cremers, Anja Lehmann
Antal sider15
UdgivelsesstedDarmstadt, Germany
ISBN (Trykt)978-3-030-04761-0
ISBN (Elektronisk)978-3-030-04762-7
StatusUdgivet - 2018


Dyk ned i forskningsemnerne om 'Formal Verification of Ephemeral Diffie-Hellman Over COSE (EDHOC)'. Sammen danner de et unikt fingeraftryk.