Re: [TLS] Proposal: a TLS formal analysis triage panel

[Muhammad Usama Sardar <[e-mail]>]

Hi Deirdre,

Just in case I miss the meeting (which is unfortunately after midnight 
for me), I would like to mention that this is great idea and I would be 
happy to contribute to this.

In our recent research on integrating attestation in Inria's ProVerif 
artifacts [1] for TLS 1.3, we faced several challenges, such as:

  * There are very few comments in the code. Main processes (such as
    Client12, Server12, Client13, Server13, appData, channelBindingQuery
    and secrecyQuery) have literally no comments at all.
  * The latest version of the artifacts (modeling draft 20 of TLS 1.3)
    has incorrectly modeled the key schedule [2,3]. The same incorrect
    model has been used in a number of TLS extensions, including the
    recent LURK [4].
  * WG seems to have no understanding of why some of the decisions were
    taken in TLS 1.3. In a discussion over mailing list [5] as well as
    with other experts, nobody has been able to justify the intuition of
    Derive-Secret for Master Secret, and whether there is any practical
    attack if that Derive-Secret is missing.

So I believe one initial useful thing that the 'formal analysis triage 
panel' could do is to create RFC8446-consistent baseline artifacts, 
which are well-commented, thoroughly validated and reviewed by a few 
experts (both TLS as well as formal methods). Then these artifacts can 
be used for any TLS extension for which formal analysis is required.

Regards,

Usama

[1] https://github.com/Inria-Prosecco/reftls/tree/master/pv

[2] https://github.com/Inria-Prosecco/reftls/issues/6

[3] https://github.com/Inria-Prosecco/reftls/issues/7

[4] https://github.com/lurk-t/proverif

[5] https://mailarchive.ietf.org/arch/msg/tls/ZGmyHwTYh2iPwPrirj_rkSTYhDo/

On 06.03.24 02:37, 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 
> necessarily 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 
> (in total or part) in the past and have gotten tentative buy-in from 
> more than one for 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¹ and _whether_ they could do with an updated or new formal 
> analysis, and 2) an estimate of the scope of work such an analysis 
> would entail. Such details would be brought back to the working group 
> for discussion about whether the proposed changes 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 
> analysis triage panel consults on farming out the meat of the analysis 
> work (either to their teams or to students they supervise, etc.).\ 
> Group membership can be refreshed on a regular schedule or on an 
> as-needed basis. Hopefully 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 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
>
> ¹ 1.3 has the most robust analysis; we'll see about other versions
>