From dschinazi.ietf@gmail.com Tue Mar 5 18:12:20 2024 Return-Path: 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 D7832C15107A for ; Tue, 5 Mar 2024 18:12:20 -0800 (PST) X-Virus-Scanned: amavisd-new at amsl.com X-Spam-Flag: NO X-Spam-Score: -2.104 X-Spam-Level: X-Spam-Status: No, score=-2.104 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, FREEMAIL_FROM=0.001, HTML_MESSAGE=0.001, RCVD_IN_ZEN_BLOCKED_OPENDNS=0.001, SPF_HELO_NONE=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=gmail.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 zcQFJLCgXqWm for ; Tue, 5 Mar 2024 18:12:18 -0800 (PST) Received: from mail-ej1-x633.google.com (mail-ej1-x633.google.com [IPv6:2a00:1450:4864:20::633]) (using TLSv1.3 with cipher TLS_AES_128_GCM_SHA256 (128/128 bits) key-exchange X25519 server-signature RSA-PSS (2048 bits) server-digest SHA256) (No client certificate requested) by ietfa.amsl.com (Postfix) with ESMTPS id 631FAC14CF0D for ; Tue, 5 Mar 2024 18:12:18 -0800 (PST) Received: by mail-ej1-x633.google.com with SMTP id a640c23a62f3a-a44d084bfe1so492694666b.1 for ; Tue, 05 Mar 2024 18:12:18 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20230601; t=1709691136; x=1710295936; darn=ietf.org; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:from:to:cc:subject:date:message-id:reply-to; bh=4i2K8XsTiP+Mjl4j9S8kEQfEDd2yVxUP3Y+R6r2dGI4=; b=WV+fpobutpN7mz48vcgYx0EHJDzSXm+Md7w3ofSzVRhs9TiUU68DAcpEZ6NavjNGOj D1eY1HtWY6ypH2jd+uY1AwTFgWR0TszlEWMDd46KgLcR5cSPHoXh0Y0yltdmWA4Wrzck TcLBnt1pN21B8D9tsq7bmo4bXI/syp92zFFNWhem5njg7d+g04qcAtZ1Cp5NcJimTJ3g yiXV8G6OKgtx0PMwp4lOXJWYqZ0jWd1x1cDVDbP7YuMiMly9WyeBl8Jf98yoeEJqI4Mh xXMVbi1fnsSWIvoE8mbtfJhNuGBhiwKrShyZSHHRUBUmEbdIFRksKfJ1Umt+EXifSv/0 LGlg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1709691136; x=1710295936; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:x-gm-message-state:from:to:cc:subject:date:message-id :reply-to; bh=4i2K8XsTiP+Mjl4j9S8kEQfEDd2yVxUP3Y+R6r2dGI4=; b=aex5TJWVsxH4Cl+WqTCRK45OZJT7jtLicK8kmOrwU7XuoUclnmySv6IKxjvNy93w9O ZhLXQ1tJzxt+9QUkmE2hAJWirtGtKpJmhI5zpz221wd+7sYQxgA3/d+r8z+sabbVAjuR xb1zrMsJ2Cv1pnwfeuJ66MQMlvJRjijqGlkE8nkVUg1MvIcrn0UxzHYj383PR8nmxH65 sElBdSNdbsX+cuWMuKxOrEKuKUSybKMA2CTBInFpXyd1JghizJBeSJ9Um3XiIkBeJR6U AwmnM4ZSP6YRFaiCCi5gHeiTIzYToep+U+J4F0XJ694NKP9AXtgdmwOqMZzmyM3ezdQS JZlw== X-Gm-Message-State: AOJu0Yw1xNFMZe73qIrvu27u8OwUW1dC7PMZO1ei7mDamvDLZVMh2S6K H8CyvoBXpgBXX9fwauYAFAcoemVwHlf2YVke2/AcB7aVLCc2lsV1nawu2crrcN00Csb4VNMmCby zpbUyhSgV4+06usbUSEAVCTZfds59QiFLFQ4= X-Google-Smtp-Source: AGHT+IFDAp2eTch46z8qAJ77iwWcSYpQqctMAH7QoT5zyQ5/a8QlHWs6pVdO9c1JJkuf9cjAPwdJn07RaG1yb3LgQw8= X-Received: by 2002:a17:906:685:b0:a44:fe70:1b82 with SMTP id u5-20020a170906068500b00a44fe701b82mr6213314ejb.8.1709691136095; Tue, 05 Mar 2024 18:12:16 -0800 (PST) MIME-Version: 1.0 References: In-Reply-To: From: David Schinazi Date: Tue, 5 Mar 2024 18:12:04 -0800 Message-ID: To: Deirdre Connolly Cc: "TLS@ietf.org" Content-Type: multipart/alternative; boundary="000000000000d7bc150612f47c2c" Archived-At: Subject: Re: [TLS] Proposal: a TLS formal analysis triage panel X-BeenThere: tls@ietf.org X-Mailman-Version: 2.1.39 Precedence: list List-Id: "This is the mailing list for the Transport Layer Security working group of the IETF." List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Wed, 06 Mar 2024 02:12:20 -0000 --000000000000d7bc150612f47c2c Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Hi Deirdre, Thanks for this, I think this is a great plan. From the perspective of standards work, more formal analysis is always better, and this seems like a great way to motivate such work. That said, it's unclear to me whether this review would be a hard requirement to pass WGLC. Let's say a document makes it to that stage, and it is sent to the triage panel, but the panel never produces a formal analysis of it. (This could happen for example if the researchers don't find the extension at hand interesting enough, they're volunteering to help so I wouldn't blame them for picking what they want to work on.) In that hypothetical scenario, does the document proceed without formal analysis, or is it blocked? Thanks, David On Tue, Mar 5, 2024 at 5:38=E2=80=AFPM Deirdre Connolly wrote: > A few weeks ago, we ran a WGLC on 8773bis, but it basically came up > blocked because of a lack of formal analysis of the proposed changes. The > working group seems to be in general agreement that any changes to TLS 1.= 3 > should not degrade or violate the existing formal analyses and proven > security properties of the protocol whenever possible. Since we are no > longer in active development of a new version of TLS, we don't necessaril= y > have the same eyes of researchers and experts in formal analysis looking = at > new changes, so we have to adapt. > > I have mentioned these issues to several experts who have analyzed TLS (i= n > total or part) in the past and have gotten tentative buy-in from more tha= n > one for something like a 'formal analysis triage panel': a rotating group > of researchers, formal analysis experts, etc, who have volunteered to giv= e > 1) a preliminary triage of proposed changes to TLS 1.3=C2=B9 and _whether= _ they > could do with an updated or new formal analysis, and 2) an estimate of th= e > scope of work such an analysis would entail. Such details would be brough= t > back to the working group for discussion about whether the proposed chang= es > merit the recommended analysis or not (e.g., a small, nice-to-have change > may actually entail a fundamentally new security model change, whereas a > large change may not deviate significantly from prior analysis and be > 'cheap' to do). If the working group agrees to proceed, the formal analys= is > triage panel consults on farming out the meat of the analysis work (eithe= r > to their teams or to students they supervise, etc.).\ Group membership ca= n > be refreshed on a regular schedule or on an as-needed basis. Hopefully th= e > lure of 'free' research questions will be enticing. > > The goal is to maintain the high degree of cryptographic assurance in TLS > 1.3 as it evolves as one of the world's most-used cryptographic protocols= . > > I would like to hear thoughts on this idea from the group and if we would > like to put it on the agenda for 119. > > Cheers, > Deirdre > > =C2=B9 1.3 has the most robust analysis; we'll see about other versions > > ---------- Forwarded message --------- > From: Joseph Salowey > Date: Tue, Jan 23, 2024 at 10:51=E2=80=AFAM > Subject: [TLS] Completion of Update Call for RFC 8773bis > To: > > > The working group last call for RFC8773bis has completed > (draft-ietf-tls-8773bis). There was general support for moving the docume= nt > forward and upgrading its status. However, several working group > participants raised the concern that formal analysis has not been conduct= ed > on this modification to the TLS protocol. We should at least have consens= us > on whether this document has the required analysis before upgrading it, b= ut > we also need a more general statement on this requirement since the TLS > working group currently does not have a policy for what does and does not > need formal analysis or what constitutes proper formal analysis. > > The chairs are working on a proposal for handling situations like this > that we plan to post to the list in a week or so. > > Thanks, > > Joe, Deirdre, and Sean > _______________________________________________ > TLS mailing list > TLS@ietf.org > https://www.ietf.org/mailman/listinfo/tls > --000000000000d7bc150612f47c2c Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Hi Deirdre,

Thanks for this, I think th= is is a great plan. From the perspective of standards work, more formal ana= lysis is always better, and this seems like a great way to motivate such wo= rk.

That said, it's unclear to me whether this= review would=C2=A0be a hard requirement to pass WGLC. Let's say a docu= ment makes it to that stage, and it is sent to the triage panel, but the pa= nel never produces a formal analysis of it. (This could happen for example = if the researchers don't find the extension at hand interesting enough,= they're volunteering to help so I wouldn't blame them for picking = what they want to work on.) In that hypothetical scenario, does the documen= t proceed without formal analysis, or is it blocked?

Thanks,
David

On Tue, Mar 5, 2024 at 5:38=E2=80=AFPM Deir= dre Connolly <durumcrustulum= @gmail.com> wrote:
A few weeks ago, we ran a WGLC on 8773bis, but = it basically came up blocked because of a lack of formal analysis of the pr= oposed changes. The working group seems to be in general agreement that any= changes to TLS 1.3 should not degrade or violate the existing formal analy= ses and proven security properties of the protocol whenever possible. Since= we are no longer in active development of a new version of TLS, we don'= ;t necessarily have the same eyes of researchers and experts in formal anal= ysis looking at new changes, so we have to adapt.

I have= mentioned these issues to several experts who have analyzed TLS (in total = or part) in the past and have gotten tentative buy-in from more than one fo= r something like a 'formal analysis triage panel': a rotating group= of researchers, formal analysis experts, etc, who have volunteered to give= 1) a preliminary triage of proposed changes to TLS 1.3=C2=B9 and _whether_= they could do with an updated or new formal analysis, and 2) an estimate o= f the scope of work such an analysis would entail. Such details would be br= ought back to the working group for discussion about whether the proposed c= hanges merit the recommended analysis or not (e.g., a small, nice-to-have c= hange may actually entail a fundamentally new security model change, wherea= s a large change may not deviate significantly from prior analysis and be &= #39;cheap' to do). If the working group agrees to proceed, the formal a= nalysis triage panel consults on farming out the meat of the analysis work = (either to their teams or to students they supervise, etc.).\ Group members= hip can be refreshed on a regular schedule or on an as-needed basis. Hopefu= lly the lure of 'free' research questions will be enticing.

The goal is to maintain the high degree of cryptographic = assurance in TLS 1.3 as it evolves as one of the world's most-used cryp= tographic protocols.

I would like to hear thoughts on this id= ea from the group and if we would like to put it on the agenda for 119.=C2= =A0

Cheers,=C2=A0
Deirdre

= =C2=B9 1.3 has the most robust analysis; we'll see about other versions=

---------- Fo= rwarded message ---------
From:=C2=A0Joseph Salowey=C2=A0<joe@salowey.net>Date: Tue, Jan 23, 2024 at 10:51=E2=80=AFAM
Subject: [TLS] Completion = of Update Call for RFC 8773bis
To: <tls@ietf.org> <tls@ietf.org>


The working group last call for RFC8773bis has comp= leted (draft-ietf-tls-8773bis). There was general support for moving the do= cument forward and upgrading its status. However, several working group par= ticipants raised the concern that formal analysis has not been conducted on= this modification to the TLS protocol. We should at least have consensus o= n whether this document has the required analysis before upgrading it, but = we also need a more general statement on this requirement since the TLS wor= king group currently does not have a policy for what does and does not need= formal analysis or what constitutes proper formal analysis.

The chairs are working on a proposal for handling situation= s like this that we plan to post to the list in a week or so.

Thanks,

Joe, Deirdre, and Sean

<= /div>
_______________________________________________
TLS mailing list
TLS@ietf.org
https://www.ietf.org/mailman/listinfo/tls
--000000000000d7bc150612f47c2c--