[TLS] Formal analysis of draft-ietf-tls-pake
Muhammad Usama Sardar <muhammad_usama.sardar@tu-dresden.de> Sun, 16 November 2025 09:20 UTC
Return-Path: <muhammad_usama.sardar@tu-dresden.de>
X-Original-To: tls@mail2.ietf.org
Delivered-To: tls@mail2.ietf.org
Received: from localhost (localhost [127.0.0.1]) by mail2.ietf.org (Postfix) with ESMTP id E4ADD8A6278E for <tls@mail2.ietf.org>; Sun, 16 Nov 2025 01:20:14 -0800 (PST)
X-Virus-Scanned: amavisd-new at ietf.org
X-Spam-Flag: NO
X-Spam-Score: -4.398
X-Spam-Level:
X-Spam-Status: No, score=-4.398 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, RCVD_IN_DNSWL_MED=-2.3, RCVD_IN_VALIDITY_RPBL_BLOCKED=0.001, RCVD_IN_VALIDITY_SAFE_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=tu-dresden.de
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 dt1w4kTWiVzt for <tls@mail2.ietf.org>; Sun, 16 Nov 2025 01:20:14 -0800 (PST)
Received: from mailout4.zih.tu-dresden.de (mailout4.zih.tu-dresden.de [141.30.67.75]) (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 03AE48A62778 for <tls@ietf.org>; Sun, 16 Nov 2025 01:20:13 -0800 (PST)
DKIM-Signature: v=1; a=rsa-sha256; q=dns/txt; c=relaxed/relaxed; d=tu-dresden.de; s=dkim2022; h=Content-Type:Subject:From:To:MIME-Version:Date :Message-ID: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=3GJrgHYBp5Bk+obOloJKRMzsCh9k3+ui2YctdyKLnis=; b=ydEC9yzH49y7wOVii6Eg8Ok82L g225haQbuhvxjBTmZguy5E1iVhVCBSNdvPdADexuPQOZpjmNICrhTESRXk4PJv0lMMN1qKfnsOqKB K7ZHq0UuwIxRilezks2mrBdd8SA544c3SDENX0NYPMXU2+vWD7I1uhx8ApXDtyzb5AunbW0UD6u8S +QMhPXT1k6UH+ULdyn2LixGIm87TSAYwOSLnWs0bcYwdKf7WuXiWm0MLn81e6g2gXf6n04z4FBmUB A+DF61W4eAsuZ4Kqp5xNsj80KGsmw2Le2eB/yMYV1cnQ7mt0I9Bhsq85hdarwgf5jjmQpzeawGXGu jWKpG1vw==;
Received: from msx-t422.msx.ad.zih.tu-dresden.de ([172.26.35.139] helo=msx.tu-dresden.de) by mailout4.zih.tu-dresden.de with esmtps (TLS1.2) tls TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384 (Exim 4.94.2) (envelope-from <muhammad_usama.sardar@tu-dresden.de>) id 1vKYvc-001zNe-N4 for tls@ietf.org; Sun, 16 Nov 2025 10:20:12 +0100
Received: from [10.12.5.228] (141.76.13.149) by msx-t422.msx.ad.zih.tu-dresden.de (172.26.35.139) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.2.2562.29; Sun, 16 Nov 2025 10:20:04 +0100
Message-ID: <727371d5-4a06-489c-acfa-5392242a1b9b@tu-dresden.de>
Date: Sun, 16 Nov 2025 10:20:03 +0100
MIME-Version: 1.0
User-Agent: Mozilla Thunderbird
Content-Language: en-US
To: "TLS@ietf.org" <tls@ietf.org>
From: Muhammad Usama Sardar <muhammad_usama.sardar@tu-dresden.de>
Content-Type: multipart/signed; protocol="application/pkcs7-signature"; micalg="sha-512"; boundary="------------ms030504070407020103080907"
X-ClientProxiedBy: MSX-L420.msx.ad.zih.tu-dresden.de (172.26.34.140) To msx-t422.msx.ad.zih.tu-dresden.de (172.26.35.139)
X-TUD-Virus-Scanned: mailout4.zih.tu-dresden.de
Message-ID-Hash: ZXJSSAQ7C4HVT3R2M6AT6FUMBLQY64MQ
X-Message-ID-Hash: ZXJSSAQ7C4HVT3R2M6AT6FUMBLQY64MQ
X-MailFrom: muhammad_usama.sardar@tu-dresden.de
X-Mailman-Rule-Misses: dmarc-mitigation; no-senders; approved; emergency; loop; banned-address; member-moderation; header-match-tls.ietf.org-0; 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: [TLS] Formal analysis of draft-ietf-tls-pake
List-Id: "This is the mailing list for the Transport Layer Security working group of the IETF." <tls.ietf.org>
Archived-At: <https://mailarchive.ietf.org/arch/msg/tls/SRH9bcgGZ8MpSx3uwRfDcT7vhQE>
List-Archive: <https://mailarchive.ietf.org/arch/browse/tls>
List-Help: <mailto:tls-request@ietf.org?subject=help>
List-Owner: <mailto:tls-owner@ietf.org>
List-Post: <mailto:tls@ietf.org>
List-Subscribe: <mailto:tls-join@ietf.org>
List-Unsubscribe: <mailto:tls-leave@ietf.org>
If I understood correctly in the meeting, the authors have some ongoing formal analysis but I could not find anything in the repo [0]. Could you please point me to the repo where the formal analysis is being done? From the formal analysis perspective, is there something specific other than the open issue mentioned in section 8.4 that you need help with? -Usama [0] https://github.com/tlswg/tls-pake
- [TLS] Formal analysis of draft-ietf-tls-pake Muhammad Usama Sardar
- [TLS] Re: Formal analysis of draft-ietf-tls-pake Muhammad Usama Sardar