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