[TLS] Re: Consensus call for RFC8773bis Formal Analysis Requirement
Russ Housley <housley@vigilsec.com> Mon, 23 September 2024 22:54 UTC
Return-Path: <housley@vigilsec.com>
X-Original-To: tls@ietfa.amsl.com
Delivered-To: tls@ietfa.amsl.com
Received: from localhost (localhost [127.0.0.1]) by ietfa.amsl.com (Postfix) with ESMTP id 43BB0C14F60E for <tls@ietfa.amsl.com>; Mon, 23 Sep 2024 15:54:49 -0700 (PDT)
X-Virus-Scanned: amavisd-new at amsl.com
X-Spam-Flag: NO
X-Spam-Score: -7.106
X-Spam-Level:
X-Spam-Status: No, score=-7.106 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_HI=-5, RCVD_IN_ZEN_BLOCKED_OPENDNS=0.001, SPF_PASS=-0.001, T_SCC_BODY_TEXT_LINE=-0.01, URIBL_BLOCKED=0.001, URIBL_DBL_BLOCKED_OPENDNS=0.001, URIBL_ZEN_BLOCKED_OPENDNS=0.001] autolearn=ham autolearn_force=no
Authentication-Results: ietfa.amsl.com (amavisd-new); dkim=pass (2048-bit key) header.d=vigilsec.com
Received: from mail.ietf.org ([50.223.129.194]) by localhost (ietfa.amsl.com [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id NL4n4yynwfLz for <tls@ietfa.amsl.com>; Mon, 23 Sep 2024 15:54:44 -0700 (PDT)
Received: from mail3.g24.pair.com (mail3.g24.pair.com [66.39.134.11]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature ECDSA (P-256) server-digest SHA256) (No client certificate requested) by ietfa.amsl.com (Postfix) with ESMTPS id 852CAC14F602 for <tls@ietf.org>; Mon, 23 Sep 2024 15:54:44 -0700 (PDT)
Received: from mail3.g24.pair.com (localhost [127.0.0.1]) by mail3.g24.pair.com (Postfix) with ESMTP id DE355F7DA5; Mon, 23 Sep 2024 18:54:43 -0400 (EDT)
Received: from smtpclient.apple (pfs.iad.rg.net [198.180.150.6]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by mail3.g24.pair.com (Postfix) with ESMTPSA id C23A7150807; Mon, 23 Sep 2024 18:54:43 -0400 (EDT)
From: Russ Housley <housley@vigilsec.com>
Message-Id: <0BAA3B8C-BAC0-47E1-A202-2BC4B001C48B@vigilsec.com>
Content-Type: multipart/alternative; boundary="Apple-Mail=_9D1F8E87-8268-4F28-AC38-3F8888B74620"
Mime-Version: 1.0 (Mac OS X Mail 16.0 \(3731.700.6.1.2\))
Date: Mon, 23 Sep 2024 18:54:33 -0400
In-Reply-To: <CAOgPGoCLnLHbO9mTbaqjERbpFtoGyJeVk=mjDvxkJYe8nySTvw@mail.gmail.com>
To: Joe Salowey <joe@salowey.net>
References: <CAOgPGoBxoEhVkzb=WYFvNEhN0sKLDLir0qPVSqx_a=Co7dkXgA@mail.gmail.com> <CAOgPGoCLnLHbO9mTbaqjERbpFtoGyJeVk=mjDvxkJYe8nySTvw@mail.gmail.com>
X-Mailer: Apple Mail (2.3731.700.6.1.2)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=vigilsec.com; h=from:message-id:content-type:mime-version:subject:date:in-reply-to:cc:to:references; s=pair-202402141609; bh=lPWWwRDZd4w22EYl/v65BHyJx+jt8XDBt9UQ0uu4ct8=; b=FA61JMqppUJig86WvtReY2g20OArODorft06twVixC4ERGnWirPh/kBdNOFVxMccLwcIvLuFCMBC6124goNU/hfFH/Q60CfBw40Ye6oOVkMFl+97LopMgrF05opYxSUDi5IUaLH7UUKjSWFZkPfVl47dOnMPejsUrmutNr7HkCG+Cb0X+1VlNabAd9iYSX8/NvYQo+k5nldEDGe62ajRoS7fAyyKeKIB5ZyObWHd04rHbb7/vK+8wr+iwOBzhimerEOsAYj56GTJq2MKxuINU96BXJvozQMcjLbsrEBlMuC+OQBbOpp8Wvhqk0dprOpi1GUGfGgosc3jDeLSYBj14A==
X-Scanned-By: mailmunge 3.11 on 66.39.134.11
Message-ID-Hash: BUKX6FRZUPP4Z3WHQVF2IJLQPZPPOASE
X-Message-ID-Hash: BUKX6FRZUPP4Z3WHQVF2IJLQPZPPOASE
X-MailFrom: housley@vigilsec.com
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
CC: IETF TLS <tls@ietf.org>
X-Mailman-Version: 3.3.9rc4
Precedence: list
Subject: [TLS] Re: Consensus call for RFC8773bis Formal Analysis Requirement
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/nGieq7hUsd3iiHzJq1FyepetZrI>
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>
I agree, and I think the Security Considerations already cover this point: If the external PSK is known to any party other than the client and the server, then the external PSK MUST NOT be the sole basis for authentication. The reasoning is explained in Section 4.2 of [K2016]. When this extension is used, authentication is based on certificates, not the external PSK. Russ > On Sep 23, 2024, at 4:49 PM, Joseph Salowey <joe@salowey.net> wrote: > > There is rough consensus that the document should have additional formal analysis before publication. Ekr proposed the following for the authentication property, which seems like a reasonable clarification > > "I think the right analysis is one in which the attacker knows the PSK. For instance, say we have a company where everyone shares a PSK (as some kind of post-quantum protection) and you want to make sure employee A cannot impersonate employee B." > > At this point it is up to the authors and working group to address the request for additional symbolic analysis in order to move the document forward. > > The consensus call also indicated that there is a need to continue to work out the process for formal analysis triage which we are working on as a separate topic. See interim scheduling poll from Sean. > > On Fri, Aug 23, 2024 at 10:30 AM Joseph Salowey <joe@salowey.net <mailto:joe@salowey.net>> wrote: >> In regard to moving RFC 8773 to standards track the formal analysis triage group has provided input on the need for formal analysis which was posted to the list [1]. The authors have published a revision of the draft [2] to address some of this feedback, however the general sentiment of the triage panel was that there should be some additional symbolic analysis done to verify the security properties of the draft and to verify there is no negative impact on TLS 1.3 security properties. >> >> The formal analysis is to verify the following properties of the proposal in the draft: >> >> - The properties of the handshake defined in Appendix E.1 of RFC8446 [3] remain intact if either the external PSK is not compromised or (EC)DH is unbroken. >> - The public key certificate authentication works as in TLS 1.3, and this extension adds the condition that the party has possession of the external PSK. The details of external PSK distribution are outside the scope of this extension. >> >> This is a consensus call for the working group to determine how to proceed between these two options: >> >> 1. Require formal analysis in the symbolic model to verify that the proposal in the document does not negatively impact the security properties of base TLS 1.3 and that the additional security properties cited above are met >> 2. Proceed with publishing the document without additional formal verification >> >> Please respond to the list with a brief reason why you think the document requires formal analysis or not. This call will end on September 16, 2024. >> >> Thanks >> >> Joe, Deirdre, and Sean >> >> [1] https://mailarchive.ietf.org/arch/msg/tls/vK2N0vr83W6YlBQMIaVr9TeHzu4/ >> [2] https://author-tools.ietf.org/iddiff?url1=draft-ietf-tls-8773bis-00&url2=draft-ietf-tls-8773bis-02&difftype=--html >> [3] https://www.rfc-editor.org/rfc/rfc8446.html#appendix-E.1 > _______________________________________________ > TLS mailing list -- tls@ietf.org > To unsubscribe send an email to tls-leave@ietf.org
- [TLS]Consensus call for RFC8773bis Formal Analysi… Joseph Salowey
- [TLS]Re: Consensus call for RFC8773bis Formal Ana… Ben Smyth
- [TLS]Re: Consensus call for RFC8773bis Formal Ana… Salz, Rich
- [TLS]Re: Consensus call for RFC8773bis Formal Ana… Eric Rescorla
- [TLS]Re: Consensus call for RFC8773bis Formal Ana… Bob Beck
- [TLS]Re: Consensus call for RFC8773bis Formal Ana… Deirdre Connolly
- [TLS]Re: Consensus call for RFC8773bis Formal Ana… Deirdre Connolly
- [TLS]Re: Consensus call for RFC8773bis Formal Ana… Salz, Rich
- [TLS]Re: Consensus call for RFC8773bis Formal Ana… Deirdre Connolly
- [TLS]Re: Consensus call for RFC8773bis Formal Ana… Salz, Rich
- [TLS]Re: Consensus call for RFC8773bis Formal Ana… Muhammad Usama Sardar
- [TLS]Re: Consensus call for RFC8773bis Formal Ana… Stephen Farrell
- [TLS]Re: Consensus call for RFC8773bis Formal Ana… Christopher Patton
- [TLS] FATT Process Joseph Salowey
- [TLS]Re: Consensus call for RFC8773bis Formal Ana… Eric Rescorla
- [TLS] Re: FATT Process Stephen Farrell
- [TLS] Re: FATT Process Joseph Salowey
- [TLS] Re: FATT Process Salz, Rich
- [TLS] Re: FATT Process Stephen Farrell
- [TLS] Re: FATT Process Watson Ladd
- [TLS] Re: FATT Process Salz, Rich
- [TLS]Re: Consensus call for RFC8773bis Formal Ana… Salz, Rich
- [TLS] Re: Consensus call for RFC8773bis Formal An… Joseph Salowey
- [TLS] Re: Consensus call for RFC8773bis Formal An… Russ Housley
- [TLS] Re: Consensus call for RFC8773bis Formal An… Eric Rescorla
- [TLS] Re: Consensus call for RFC8773bis Formal An… John Mattsson
- [TLS] Re: Consensus call for RFC8773bis Formal An… John Mattsson