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

I do think a 'reference' Tamarin model would be useful. It would of course
only model part of TLS (1.3, for example) and only through a particular
symbolic model/tool. And would require maintenance by...someone.

For the triage panel, I do think the preliminary triage is key: we'd ask a
group of experts /if/ formal analysis (new or updated) is warranted /at
all/, and if warranted, of what kind, what scope, if it needs novel
modeling work, if it can build on existing work, or even if pen and paper
analysis would suffice. I do not think there are any prerequisites to
standing such a triage panel up.

On Mon, Mar 18, 2024, 10:34 AM Muhammad Usama Sardar <
muhammad_usama.sardar@tu-dresden.de> wrote:

> 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
>
> _______________________________________________
> TLS mailing list
> TLS@ietf.org
> https://www.ietf.org/mailman/listinfo/tls
>