[TLS] Proposal: a TLS formal analysis triage panel

[Deirdre Connolly]

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

-- Forwarded message -
From: Joseph Salowey 
Date: Tue, Jan 23, 2024 at 10:51 AM
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 document
forward and upgrading its status. However, several working group
participants raised the concern that formal analysis has not been conducted
on this modification to the TLS protocol. We should at least have consensus
on whether this document has the required analysis before upgrading it, but
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

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

[David Schinazi]

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 PM 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
>
> -- Forwarded message -
> From: Joseph Salowey 
> Date: Tue, Jan 23, 2024 at 10:51 AM
> 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 document
> forward and upgrading its status. However, several working group
> participants raised the concern that formal analysis has not been conducted
> on this modification to the TLS protocol. We should at least have consensus
> on whether this document has the required analysis before upgrading it, but
> 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
>
___
TLS mailing list
TLS@ietf.org
https://www.ietf.org/mailman/listinfo/tls

[TLS] ML-KEM key agreement for TLS 1.3

[Deirdre Connolly]

I have uploaded a preliminary version of ML-KEM for TLS 1.3

and have a more fleshed out
 version to be
uploaded when datatracker opens. It is a straightforward new `NamedGroup`
to support key agreement via ML-KEM-768 or ML-KEM-1024, in a very similar
style to -hybrid-design
.

It will be nice to have pure-PQ options (that are FIPS / CNSA 2.0
compatible) ready to go when users are ready to use them.

Cheers,
Deirdre
___
TLS mailing list
TLS@ietf.org
https://www.ietf.org/mailman/listinfo/tls

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

[Deirdre Connolly]

> 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?

Indeed; the interaction with the panel would be in two phases: any changes
that are being proposed by/to the WG would have a preliminary triage of
whether such changes _should_ have formal analysis, and of what scope/type.
This would probably be nicely triggered by an adoption call. Ideally we'd
have a sense from the panel of whether the proposed changes would entail a
significant amount of formal analysis work from the get-go, or not. This
preliminary triage can help inform the adoption call discussion.

If the proposal is adopted, and the working group has received a formal
analysis triage from the panel, and accepts the general scope of work to be
a requirement / blocker before moving to WGLC, then it is. We then work
with the panel to select the researchers/whomever to conduct the analysis,
which may entail rounds of back and forth if the document changes over
time.

There may be changes that, on triage from the panel, are 'easy' and may not
require updated analysis at all, or very little. The WG may agree to adopt
the document and agree to proceed to WGLC _without_ formal analysis, with
the implicit understanding that the adopted document and the one
approaching WGLC will not have significantly diverged from each other. If
we are worried about this, we can implement a sort of 'last chance' review
with the panel to make sure we aren't missing something on such a document
before actually triggering the WGLC.

This is sort of what I had in mind, but am of course welcome to suggestions
or changes. 😁

On Tue, Mar 5, 2024 at 9:12 PM David Schinazi 
wrote:

> 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 PM 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.
>>
>>

Re: [TLS] ML-KEM key agreement for TLS 1.3

[D. J. Bernstein]

The security analysis of post-quantum crypto is far less mature than the
security analysis of ECC was when the Internet moved to ECC:

   * 48% of the 69 round-1 submissions to the NIST post-quantum
 competition in 2017 have been broken by now.

   * 25% of the 48 submissions unbroken during round 1 have been broken
 by now.

   * 36% of the 28 submissions _selected by NIST in 2019 for round 2_
 have been broken by now.

See https://cr.yp.to/papers.html#qrcsp for the data, and slide 11 of
https://cr.yp.to/talks.html#2024.01.11 for a graph showing when the
breaks were published.

We have to try to protect users against quantum computers. This means
rolling out post-quantum crypto asap. But we also need a simple rule of
always using hybrids in case the post-quantum crypto fails. This rule
has been followed by every major post-quantum deployment so far, has
played an important role in _encouraging_ post-quantum deployment, and
meant that the break of SIKE didn't turn into an immediate break of
real user data that Google and Cloudflare had encrypted with CECPQ2.

NSA and GCHQ have been arguing to the contrary. Their arguments don't
hold up to examination; see https://blog.cr.yp.to/20240102-hybrid.html.
But the arguments are still sitting there, and NSA's market influence
cannot be ignored. I would treat non-hybrid drafts in IETF the same way
as "export" options in code: they're security risks. I would encourage
explicit withdrawal of any such drafts.

---D. J. Bernstein

___
TLS mailing list
TLS@ietf.org
https://www.ietf.org/mailman/listinfo/tls

Re: [TLS] ML-KEM key agreement for TLS 1.3

[Andrey Jivsov]

>
> I would treat non-hybrid drafts in IETF the same way
> as "export" options in code: they're security risks. I would encourage
> explicit withdrawal of any such drafts.


Does this point apply in your opinion to hash-based signatures?
___
TLS mailing list
TLS@ietf.org
https://www.ietf.org/mailman/listinfo/tls