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
