[Lake] Formal Verification of EDHOC-PSK with Ephemeral KEM
Clement Papon <clement.papon@unilim.fr> Fri, 24 April 2026 15:18 UTC
Return-Path: <clement.papon@unilim.fr>
X-Original-To: lake@mail2.ietf.org
Delivered-To: lake@mail2.ietf.org
Received: from localhost (localhost [127.0.0.1]) by mail2.ietf.org (Postfix) with ESMTP id A0C30E27354B for <lake@mail2.ietf.org>; Fri, 24 Apr 2026 08:18:09 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=ietf.org; s=ietf1; t=1777043889; bh=Y7Yf0MkkU3i+F9E+kLkR2+vWnCS5bPxhv8wJE+SZ+SU=; h=Date:From:To:Subject; b=oN5SgtOmF2mUZ0aXhpIajMvZNiRPYBjbybHRyc3KtkAbWVSPLHwsg9MVqooCfDMXV lclKE/Wla7ysGxUM3jCGSNxiINq2wk5qVYNCpRiJac39yZWf5J+AN/gEwAfN5W5gt3 G1BqUFVlDHk1C4I0LtDmXVq4dcLCCViuTrpOBgiI=
X-Virus-Scanned: amavisd-new at ietf.org
X-Spam-Flag: NO
X-Spam-Score: -4.397
X-Spam-Level:
X-Spam-Status: No, score=-4.397 tagged_above=-999 required=5 tests=[BAYES_00=-1.9, DKIM_SIGNED=0.1, DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, HTML_MESSAGE=0.001, RCVD_IN_DNSWL_MED=-2.3, RCVD_IN_VALIDITY_CERTIFIED_BLOCKED=0.001, RCVD_IN_VALIDITY_RPBL_BLOCKED=0.001, SPF_HELO_NONE=0.001, SPF_PASS=-0.001] autolearn=ham autolearn_force=no
Authentication-Results: mail2.ietf.org (amavisd-new); dkim=pass (2048-bit key) header.d=unilim.fr
Received: from mail2.ietf.org ([166.84.6.31]) by localhost (mail2.ietf.org [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id OOVwSGagOH1E for <lake@mail2.ietf.org>; Fri, 24 Apr 2026 08:18:08 -0700 (PDT)
Received: from smtp.unilim.fr (smtp.unilim.fr [164.81.1.32]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange ECDHE (P-256) server-signature ECDSA (P-256) server-digest SHA256) (No client certificate requested) by mail2.ietf.org (Postfix) with ESMTPS id 079C5E27332D for <lake@ietf.org>; Fri, 24 Apr 2026 08:16:25 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; q=dns/txt; c=relaxed/relaxed; d=unilim.fr; s=smtp; h=Content-Type:MIME-Version:Subject:Message-ID:To:From:Date:Sender: Reply-To:Cc:Content-Transfer-Encoding:Content-ID:Content-Description: Resent-Date:Resent-From:Resent-Sender:Resent-To:Resent-Cc:Resent-Message-ID: In-Reply-To:References:List-Id:List-Help:List-Unsubscribe:List-Subscribe: List-Post:List-Owner:List-Archive; bh=Y7Yf0MkkU3i+F9E+kLkR2+vWnCS5bPxhv8wJE+SZ+SU=; b=UiMRbtdT6lXaq8RKW5+xWiBQDb BsKwaUT4kclzJWONG5XT3Vp/GInQ1mW7oco5kvdRtTz1hWRAhTIfh8Nf6UG35IpRJoO0cA6fb37ZL SRjy1swIirl3wDUd519F5iDut0Qkjryaj411IVVPlI3Jw8tFJ4YyqDslPakB+Q1rBxRmsp7pDy46Y w10BtL94RQWwZSxJA/5bnwyjGOIFuCSgpOnD26Bb+Cl/lpVgOJaebntvxIDHUhkisfcI6DkE/T6ql rHAWgvkHm0cNtX4wytq3FisCsVps7Htr17dIVCsYPLvEoG7pvkoCYsjJ/6WWZ9ITnQfleXIormzAj xlv1ltHQ==;
Received: from crb-mta04.unilim.fr ([164.81.1.92]) by smtp.unilim.fr with esmtps (TLS1.3) tls TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384 (Exim 4.94.2) (envelope-from <clement.papon@unilim.fr>) id 1wGIGO-00BnTP-6Z for lake@ietf.org; Fri, 24 Apr 2026 17:16:16 +0200
Received: from crb-mta04.unilim.fr (localhost [127.0.0.1]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange x25519 server-signature RSA-PSS (2048 bits) server-digest SHA256) (No client certificate requested) by crb-mta04.unilim.fr (Postfix) with ESMTPS id E7BA5C0102A5 for <lake@ietf.org>; Fri, 24 Apr 2026 17:16:15 +0200 (CEST)
Received: from crb-mta04.unilim.fr (localhost [127.0.0.1]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange x25519 server-signature RSA-PSS (2048 bits) server-digest SHA256) (No client certificate requested) by crb-mta04.unilim.fr (Postfix) with ESMTPS id DA024C0102A8 for <lake@ietf.org>; Fri, 24 Apr 2026 17:16:15 +0200 (CEST)
Received: from crb-mailstore01.unilim.fr (crb-mailstore01.unilim.fr [164.81.20.5]) by crb-mta04.unilim.fr (Postfix) with ESMTP id D55B2C0102A5 for <lake@ietf.org>; Fri, 24 Apr 2026 17:16:15 +0200 (CEST)
Date: Fri, 24 Apr 2026 17:16:15 +0200
From: Clement Papon <clement.papon@unilim.fr>
To: lake <lake@ietf.org>
Message-ID: <906896129.93295774.1777043775771.JavaMail.zextras@unilim.fr>
MIME-Version: 1.0
Content-Type: multipart/alternative; boundary="=_6bc6c03a-8b10-4b91-883a-f48cb9f6de1f"
X-Originating-IP: [164.81.41.51]
X-Mailer: Carbonio 25.9.0_ZEXTRAS_202509 (CarbonioWebClient - Safari 26.4 (Mac OS)/25.9.0_ZEXTRAS_202509 carbonio 20250902-1300 FOSS)
Thread-Index: WCTJzherHrnU9GR5zPB2pzoOfXeGDA==
Thread-Topic: Formal Verification of EDHOC-PSK with Ephemeral KEM
X-Univ-Limoges-MailScanner-Information: Serveur Anti-virus Please contact postmaster@unilim.fr for more information
X-Univ-Limoges-MailScanner-ID: 1wGIGO-00BnTP-6Z
X-Univ-Limoges-MailScanner: Found to be clean
X-Univ-Limoges-MailScanner-Envelope-From: clement.papon@unilim.fr
Message-ID-Hash: Q2XTIVGXIKRDLRJNJOLHQ3JJXAE6V4X2
X-Message-ID-Hash: Q2XTIVGXIKRDLRJNJOLHQ3JJXAE6V4X2
X-MailFrom: clement.papon@unilim.fr
X-Mailman-Rule-Misses: dmarc-mitigation; no-senders; approved; emergency; loop; banned-address; member-moderation; nonmember-moderation; administrivia; implicit-dest; max-recipients; max-size; news-moderation; no-subject; digests; suspicious-header
X-Mailman-Version: 3.3.9rc6
Precedence: list
Subject: [Lake] Formal Verification of EDHOC-PSK with Ephemeral KEM
List-Id: Lightweight Authenticated Key Exchange <lake.ietf.org>
Archived-At: <https://mailarchive.ietf.org/arch/msg/lake/2XGOI9OCwylJUfSCasvvwM2FXmw>
List-Archive: <https://mailarchive.ietf.org/arch/browse/lake>
List-Help: <mailto:lake-request@ietf.org?subject=help>
List-Owner: <mailto:lake-owner@ietf.org>
List-Post: <mailto:lake@ietf.org>
List-Subscribe: <mailto:lake-join@ietf.org>
List-Unsubscribe: <mailto:lake-leave@ietf.org>
Hi all, Following Dhekra's presentation at the last IETF meeting and her suggestions (Formal Verification of EDHOC-PSK: A Symbolic Approach with SAPIC+), as well as what is discussed in draft-spm-lake-pqsuites, I have carried out a formal modeling and verification of EDHOC-PSK using an Ephemeral KEM, covering different variants in the KEM modeling. The analysis confirms the expected security properties in the classical model - consistent with the results presented by Dhekra - and additionally provides complementary approach for the Identity Protection property modeling. This work is currently being written up for journal submission, and I hope to share more details with the group in July. Best, Clément Papon
- [Lake] Formal Verification of EDHOC-PSK with Ephe… Clement Papon
- [Lake] Re: Formal Verification of EDHOC-PSK with … Muhammad Usama Sardar