[Lake] EDHOC is ready for formal analysis

Mališa Vučinić <malisa.vucinic@inria.fr> Tue, 23 November 2021 16:00 UTC

Return-Path: <malisa.vucinic@inria.fr>
X-Original-To: lake@ietfa.amsl.com
Delivered-To: lake@ietfa.amsl.com
Received: from localhost (localhost [127.0.0.1]) by ietfa.amsl.com (Postfix) with ESMTP id B1BE83A094E for <lake@ietfa.amsl.com>; Tue, 23 Nov 2021 08:00:08 -0800 (PST)
X-Virus-Scanned: amavisd-new at amsl.com
X-Spam-Flag: NO
X-Spam-Score: -1.897
X-Spam-Level:
X-Spam-Status: No, score=-1.897 tagged_above=-999 required=5 tests=[BAYES_00=-1.9, HTML_MESSAGE=0.001, RCVD_IN_MSPIKE_H3=0.001, RCVD_IN_MSPIKE_WL=0.001, SPF_HELO_NONE=0.001, SPF_PASS=-0.001] autolearn=ham autolearn_force=no
Received: from mail.ietf.org ([4.31.198.44]) by localhost (ietfa.amsl.com [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id 6z7JjNBu8KYf for <lake@ietfa.amsl.com>; Tue, 23 Nov 2021 08:00:04 -0800 (PST)
Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by ietfa.amsl.com (Postfix) with ESMTPS id E7B433A0940 for <lake@ietf.org>; Tue, 23 Nov 2021 08:00:03 -0800 (PST)
IronPort-HdrOrdr: A9a23:csFr8ql68VR9LHGPbARIutDRDlvpDfKX3DAbv31ZSRFFG/FwWfrOoB19726TtN9xYgBGpTnkAsO9qBznmKKdjbN8AV7mZniEhINHRLsSkbcKgAeQZhEXz4ZmpNhdmtFFeaPN5DpB7foSkTPId+rIm+P3iZxA7N22pxxQpENRGsNdBmFCZTpzeXcGITWua6BWKHO03Ls3mxOQPVoWc+WmDT0/U+DYodqjruOdXTc2QzAm9SiThneS5LT7ChiV2Qp2aUI1/Z4StUbEji3k7eGZv/u60x/R0HKWx5lag9f60LJ4dbyxo/lQBDXwqxqiIL5sXLCPp1kO0ZmS1Go=
X-IronPort-AV: E=Sophos;i="5.84,326,1620684000"; d="scan'208,217";a="400146864"
Received: from cep85-1_migr-78-203-210-80.fbx.proxad.net (HELO smtpclient.apple) ([78.203.210.80]) by mail3-relais-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 23 Nov 2021 17:00:00 +0100
From: Mališa Vučinić <malisa.vucinic@inria.fr>
Content-Type: multipart/alternative; boundary="Apple-Mail=_6BAAB60A-B718-4DCA-B4A4-7843ECBC68C8"
Mime-Version: 1.0 (Mac OS X Mail 15.0 \(3693.20.0.1.32\))
Date: Tue, 23 Nov 2021 17:00:00 +0100
Message-Id: <AD3896D1-11C7-4AD6-B78C-E31D2C0D7129@inria.fr>
To: lake@ietf.org
X-Mailer: Apple Mail (2.3693.20.0.1.32)
Archived-At: <https://mailarchive.ietf.org/arch/msg/lake/dtEkPlVR4nMlNbQTy0kAjsf5Lx4>
Subject: [Lake] EDHOC is ready for formal analysis
X-BeenThere: lake@ietf.org
X-Mailman-Version: 2.1.29
Precedence: list
List-Id: Lightweight Authenticated Key Exchange <lake.ietf.org>
List-Unsubscribe: <https://www.ietf.org/mailman/options/lake>, <mailto:lake-request@ietf.org?subject=unsubscribe>
List-Archive: <https://mailarchive.ietf.org/arch/browse/lake/>
List-Post: <mailto:lake@ietf.org>
List-Help: <mailto:lake-request@ietf.org?subject=help>
List-Subscribe: <https://www.ietf.org/mailman/listinfo/lake>, <mailto:lake-request@ietf.org?subject=subscribe>
X-List-Received-Date: Tue, 23 Nov 2021 16:00:09 -0000

Dear all,

(At IETF 112, we discussed kicking off a process that we hope will produce security analyses of EDHOC over the coming months. This mail describes that in a form suitable for people less familiar with the details of the working group.)

Back in October 2019, the IETF LAKE working group was chartered to work on a lightweight authenticated key exchange protocol for constrained Internet of Things environments. A deliverable of this standardization process, the EDHOC specification, underwent multiple revisions as an official IETF working group document. Different versions of the specification were implemented through 7 independent and interop-tested implementations, including those that specifically target low-end microcontrollers.

The EDHOC protocol is based on a well-studied SIGMA-I core. However, the additional static Diffie-Hellman authentication methods depart from the original SIGMA design. Based on the study in the symbolic model on an early version of the specification, we have good reason to believe that these additional methods are still secure. But before publishing a document as an Internet Standard, it is important to further raise the confidence of the community on its formal security aspects, which also includes the proofs in the computational model. Based on the discussion during the IETF 112 meeting, we believe that the version -12 of the specification is “ready for formal analysis” and we are launching a call to the teams and individuals outside of the working group to formally study the specification. In that sense, we are now “freezing” the specification at -12 and requesting the authors to withhold from publishing new versions of the draft until further notice.

In order to facilitate this process, Mališa has worked with the authors on an EDHOC primer published in the form of a preprint [1], which summarizes EDHOC and its expected security properties. The document also outlines the research questions we would like to have answers to. While the document is formally not a working group document, we would be happy to incorporate any feedback you might have in the next version.

Mališa and Stephen

[1] https://hal.inria.fr/hal-03434293/document <https://hal.inria.fr/hal-03434293/document>