[{"author": "Tirumaleswar Reddy.K", "text": "

Hi all

", "time": "2026-03-17T08:01:36.000Z"}, {"author": "Nathanael Ritz", "text": "

Hello!

", "time": "2026-03-17T08:02:54.000Z"}, {"author": "Hannes Tschofenig", "text": "

A change in the order of the agenda

", "time": "2026-03-17T08:03:55.000Z"}, {"author": "Muhammad Usama Sardar", "text": "

No, not strong at all

", "time": "2026-03-17T08:04:11.000Z"}, {"author": "Muhammad Usama Sardar", "text": "

Sincere apologies, had to get consensus at GA4GH.

", "time": "2026-03-17T08:05:08.000Z"}, {"author": "Paul Wouters", "text": "

didnt we have the linksage of webpki and attestation certificates via SAN ?

", "time": "2026-03-17T08:17:39.000Z"}, {"author": "Jonathan Hoyland", "text": "

@Tirumaleswar that's not true

", "time": "2026-03-17T08:24:35.000Z"}, {"author": "Markus Rudy", "text": "

Think of DHE as a counter-example to \"if private keys are leaked, everything is lost\".

", "time": "2026-03-17T08:24:48.000Z"}, {"author": "Jonathan Hoyland", "text": "

You can prove that a compromised key is used honestly if you have other uncompromised keys.

", "time": "2026-03-17T08:25:07.000Z"}, {"author": "Yaron Sheffer", "text": "

I'm amazed by this rhetorical question, now for the second time, \"any other intra-HS method\" when there are 2 ones on the charter.

", "time": "2026-03-17T08:29:39.000Z"}, {"author": "Yaron Sheffer", "text": "

-> on the agenda

", "time": "2026-03-17T08:30:08.000Z"}, {"author": "Ionu\u021b Mihalcea", "text": "

Right, but it might just leak the other key and not priv_EK, why only look at the case where priv_EK is leaked

", "time": "2026-03-17T08:32:34.000Z"}, {"author": "Jonathan Hoyland", "text": "

You could do pre-handshake attestation securely if you establish some symmetric key material during the attestation, and then sign that symmetric key during the handshake.

", "time": "2026-03-17T08:32:38.000Z"}, {"author": "Markus Rudy", "text": "

An interesting property of the protocols that don't break down on leaked priv EKs is that we could go from EKs to long-term keys that don't need to be confidential.

", "time": "2026-03-17T08:32:56.000Z"}, {"author": "Muhammad Usama Sardar", "text": "

Yaron Sheffer said:

\n
\n

I'm amazed by this rhetorical question, now for the second time, \"any other intra-HS method\" when there are 2 ones on the charter.

\n
\n

I was asking for implementations. Are you aware of any implementation of both drafts?

", "time": "2026-03-17T08:33:30.000Z"}, {"author": "Ionu\u021b Mihalcea", "text": "

Looking forward to a TEE that guarantees that only private keys can be leaked, no other part of the TEE memory , though!

", "time": "2026-03-17T08:33:58.000Z"}, {"author": "Thomas Fossati", "text": "

Ionut: +1. There is only one memory space. If you leak one location, you are essentially leaking them all.

", "time": "2026-03-17T08:34:15.000Z"}, {"author": "Muhammad Usama Sardar", "text": "

Yaron Sheffer said:

\n
\n

-> on the agenda

\n
\n

I see no implementation mentioned in the slides on the agenda.

", "time": "2026-03-17T08:34:54.000Z"}, {"author": "Muhammad Usama Sardar", "text": "

Ionu\u021b Mihalcea said:

\n
\n

Right, but it might just leak the other key and not priv_EK, why only look at the case where priv_EK is leaked

\n
\n

Sure, that's where we have the attack. We are not denying that the other case is not possible.

", "time": "2026-03-17T08:35:42.000Z"}, {"author": "Hannes Tschofenig", "text": "

I believe that there is always a change to a state machine afterall we are adding new messages

", "time": "2026-03-17T08:36:07.000Z"}, {"author": "Muhammad Usama Sardar", "text": "

Ionu\u021b Mihalcea said:

\n
\n

Looking forward to a TEE that guarantees that only private keys can be leaked, no other part of the TEE memory , though!

\n
\n

Transient key leakage is possible too. If provisioned at runtime, the problem could be in provisioning protocol. So there are several possibilities.

", "time": "2026-03-17T08:37:33.000Z"}, {"author": "Muhammad Usama Sardar", "text": "

Thomas Fossati said:

\n
\n

Ionut: +1. There is only one memory space. If you leak one location, you are essentially leaking them all.

\n
\n

See #seat > ietf-125 @ \ud83d\udcac

", "time": "2026-03-17T08:38:20.000Z"}, {"author": "Hannes Tschofenig", "text": "

Maybe the use case draft should also talk a bit about our attacker assumptions. I have been puzzeled also in the TLS group with regards to key attestation about what people assume attackers can and cannot do.

", "time": "2026-03-17T08:39:02.000Z"}, {"author": "Muhammad Usama Sardar", "text": "

Nathanael, thank you for using our models. This is one answer to Jun's question that the whole IETF/IRTF community can actually use these Apache License 2.0 models to gain confidence.

", "time": "2026-03-17T08:39:32.000Z"}, {"author": "Paul Wouters", "text": "

knowing of current implementations bolted onto core TLS does not seem very relevant to planning a new method that cannot currently be deployed because we havent specified things yet

", "time": "2026-03-17T08:40:15.000Z"}, {"author": "Hannes Tschofenig", "text": "

Agree!

", "time": "2026-03-17T08:40:46.000Z"}, {"author": "Muhammad Usama Sardar", "text": "

Jonathan Hoyland said:

\n
\n

You could do pre-handshake attestation securely if you establish some symmetric key material during the attestation, and then sign that symmetric key during the handshake.

\n
\n

Jonathan, would it not have replay attacks, as in code can change at runtime. Could you please elaborate?

", "time": "2026-03-17T08:42:04.000Z"}, {"author": "Paul Wouters", "text": "

hannes: agreed on the user cases and attack explanations. also knowing real world limitations of things like tees deployed with identical keys and other expected deployment characteristics

", "time": "2026-03-17T08:42:20.000Z"}, {"author": "Muhammad Usama Sardar", "text": "

Paul Wouters said:

\n
\n

knowing of current implementations bolted onto core TLS does not seem very relevant to planning a new method that cannot currently be deployed because we havent specified things yet

\n
\n

Paul, we did our best. Now that we have more drafts, we can start their analysis. If you have more ideas, please let us know.

", "time": "2026-03-17T08:43:10.000Z"}, {"author": "Jonathan Hoyland", "text": "

@Usama, it would only have replay attacks if your prehandshake attestation doesn't establish freshness / injectivity.

", "time": "2026-03-17T08:43:46.000Z"}, {"author": "Ionu\u021b Mihalcea", "text": "

Hannes, Paul: ack about attacker capabilities for the use-cases draft.

", "time": "2026-03-17T08:44:40.000Z"}, {"author": "Paul Wouters", "text": "

the reason for use cases doc is that we want to know what we need to support before making solutions. Instead, SEAT seems focused on formal verifications of solutions of which we dont know what or if they solve the problems we are trying to solve. I really wish the WG would park all formal verifications and work on defining our problem before we verify our solution candidates

", "time": "2026-03-17T08:45:02.000Z"}, {"author": "Muhammad Usama Sardar", "text": "

Paul, AI agent is one of the use cases https://datatracker.ietf.org/doc/draft-jiang-seat-dynamic-attestation/
\nOne probably cannot verify incomplete specifications. Starting with existing ones seemed like the most reasonable thing to us.

", "time": "2026-03-17T08:45:54.000Z"}, {"author": "Hannes Tschofenig", "text": "

Thanks for the presentation Nathanael and for all the work

", "time": "2026-03-17T08:48:27.000Z"}, {"author": "Nancy Cam-Winget", "text": "

Thank you Nathanaael!

", "time": "2026-03-17T08:52:23.000Z"}, {"author": "Ionu\u021b Mihalcea", "text": "

Thank you, Nathanael!

", "time": "2026-03-17T08:53:05.000Z"}, {"author": "Tirumaleswar Reddy.K", "text": "

Thanks, Nathanael.

", "time": "2026-03-17T08:53:18.000Z"}, {"author": "Nathanael Ritz", "text": "

:D

", "time": "2026-03-17T08:53:37.000Z"}, {"author": "zhang jun", "text": "

Void formal (input)
\n{
\n Blabla x 1000 line of codes

\n

If(formal(input)
\n Return true;
\n else
\n Return false;

\n

}

\n

run (formal(formal))

", "time": "2026-03-17T08:53:47.000Z"}, {"author": "Hannes Tschofenig", "text": "

Paul, we are engineers. We care about solutions - not problems :-)

", "time": "2026-03-17T08:55:13.000Z"}, {"author": "Yaron Sheffer", "text": "

@Jun, cynicism aside, people have found vulnerabilities using formal methods.

", "time": "2026-03-17T08:55:13.000Z"}, {"author": "Paul Wouters", "text": "

\"required to coordinate with\" is a bit misleading when a charter mentions \"coordinating\"

", "time": "2026-03-17T08:55:43.000Z"}, {"author": "Hannes Tschofenig", "text": "

Formal methods are not perfect but they certainly help. If nothing else, they help you look at the solution from a different angle.

", "time": "2026-03-17T08:55:51.000Z"}, {"author": "Paul Wouters", "text": "

as in the WG has no actin item - it just hopes members will reach out to those other groups for cooperation.

", "time": "2026-03-17T08:56:35.000Z"}, {"author": "Muhammad Usama Sardar", "text": "

Paul Wouters said:

\n
\n

\"required to coordinate with\" is a bit misleading when a charter mentions \"coordinating\"

\n
\n

Isn't it the intention? There were several concerns who needs it; who will implement it, etc.

\n
\n\n
", "time": "2026-03-17T08:57:25.000Z"}, {"author": "zhang jun", "text": "

sure, it is one case of G\u00f6del's incompleteness theorems.

", "time": "2026-03-17T08:58:03.000Z"}, {"author": "Muhammad Usama Sardar", "text": "

I have repeated my position multiple times. Formal methods are helpful but not perfect.

", "time": "2026-03-17T08:58:33.000Z"}, {"author": "Hannes Tschofenig", "text": "

Jonathan, can you put your statement here in the chat for the minutes?

", "time": "2026-03-17T09:00:50.000Z"}, {"author": "Paul Wouters", "text": "

@usama: the intension is not an action item - it's more a \"the chairs might might look a draft reaching WGLC has been conveyed to such other groups (by any WG member). It's not a blocking action of any kind.

", "time": "2026-03-17T09:01:31.000Z"}, {"author": "Paul Wouters", "text": "

WGs have no formal duties to reach out to other SDOs for mandatory feedback.

", "time": "2026-03-17T09:02:28.000Z"}, {"author": "Muhammad Usama Sardar", "text": "

Formal methods are complementary and not a replacement of other methods.

", "time": "2026-03-17T09:03:01.000Z"}, {"author": "zhang jun", "text": "

I think one interesting problem to consider is that when the code of formal anaylisis scale up, how to enure that it covers all the aspects that may happen in the real cases.

", "time": "2026-03-17T09:03:18.000Z"}, {"author": "zhang jun", "text": "

That it to say, the code is correct but not complete.

", "time": "2026-03-17T09:03:55.000Z"}, {"author": "Hannes Tschofenig", "text": "

What do you mean by \" code of formal anaylisis scale up\"?

", "time": "2026-03-17T09:07:54.000Z"}, {"author": "Nathanael Ritz", "text": "

@jun, formal analysis isn't \"code\" per-se. It doesn't compile into an app. It's more like a cryptographic puzzlebox with mathematical soundness proofs that back the outcomes. So, I'm not sure \"scaling\" isn't quite the right phrase.

", "time": "2026-03-17T09:07:56.000Z"}, {"author": "Hannes Tschofenig", "text": "

With F* you can also compile code

", "time": "2026-03-17T09:08:32.000Z"}, {"author": "Jonathan Hoyland", "text": "

@Nathanael It actually kind of is. The TLS 1.3 model was something like 700,000 lines

", "time": "2026-03-17T09:09:08.000Z"}, {"author": "zhang jun", "text": "

For me, any sequence of words is code.

", "time": "2026-03-17T09:09:20.000Z"}, {"author": "Jens-Rene Giesen", "text": "

Possibly there is some confusion about formal methods wrt protocol anlaysis (i.e., Tamarin) vs. for program analysis?

", "time": "2026-03-17T09:09:25.000Z"}, {"author": "Yaron Sheffer", "text": "

Anecdote: the TLS 1.3 formal proof was found to contain errors (it wasn't progressed as the I-D progressed to RFC). Credit to Usama for that.

", "time": "2026-03-17T09:10:17.000Z"}, {"author": "Nathanael Ritz", "text": "

Sure, in terms of complexity. My brain jumped to number of concurrent connections like a deployed binary lol.

", "time": "2026-03-17T09:10:18.000Z"}, {"author": "Thomas Fossati", "text": "

I believe that before asking adoption we should clarify what the scope of expat is: see https://github.com/tls-attestation/exported-attestation/issues/56

", "time": "2026-03-17T09:10:28.000Z"}, {"author": "zhang jun", "text": "

Like DNA sequences, poems, they are codes as well.

", "time": "2026-03-17T09:10:53.000Z"}, {"author": "Paul Wouters", "text": "

without having a much more developed use cases draft, it seems we are not in a good position to adopt solution douments ?

", "time": "2026-03-17T09:11:13.000Z"}, {"author": "Yaron Sheffer", "text": "

More clarity on Thomas's point: expat at the moment is a protocol framework (or sketch), not a complete protocol.

", "time": "2026-03-17T09:11:37.000Z"}, {"author": "Ionu\u021b Mihalcea", "text": "

Jonathan: +1. I think I raised this question at IETF-124. See: https://github.com/tls-attestation/exported-attestation/issues/41

", "time": "2026-03-17T09:12:41.000Z"}, {"author": "Deirdre Connolly", "text": "

Formal analysis is broad collection of techniques applicable to 'formalizable' schemes, protocols, etc, including cryptographic ones; techniques include different approaches of pen-and-paper proofs, game based or otherwise; formal methods techniques such as the symbolic models in Tamarin and ProVerif, or computational models such as EasyCrypt; or 'other', like Squirrel, that try to straddle those two worlds; other techniques include formal verification of executable programs that they correctly implement a reference model/spec of an algorithm

", "time": "2026-03-17T09:13:26.000Z"}, {"author": "Tirumaleswar Reddy.K", "text": "

Audio is clear.

", "time": "2026-03-17T09:14:22.000Z"}, {"author": "Muhammad Usama Sardar", "text": "

Yaron is breaking a lot for me

", "time": "2026-03-17T09:14:26.000Z"}, {"author": "Jens-Rene Giesen", "text": "

@Deirdre, exactly, there's a lot of formal X terminology that gets mixed easily.

", "time": "2026-03-17T09:14:29.000Z"}, {"author": "Tirumaleswar Reddy.K", "text": "

audio is good now.

", "time": "2026-03-17T09:15:04.000Z"}, {"author": "Ionu\u021b Mihalcea", "text": "

Usama: for clarity, it's just the use of key derivation, they're not deriving from the keys in the key schedule.

", "time": "2026-03-17T09:16:59.000Z"}, {"author": "Tirumaleswar Reddy.K", "text": "

+1

", "time": "2026-03-17T09:17:28.000Z"}, {"author": "Jonathan Hoyland", "text": "

@Deidre I have been trying to get people to use terms consistently for ages, but I can't even get myself to do it :sweat_smile:

", "time": "2026-03-17T09:18:42.000Z"}, {"author": "Muhammad Usama Sardar", "text": "

Ionu\u021b Mihalcea said:

\n
\n

Usama: for clarity, it's just the use of key derivation, they're not deriving from the keys in the key schedule.

\n
\n

Sure, but the usage of key derivations generates keys, no?

", "time": "2026-03-17T09:18:44.000Z"}, {"author": "Markus Rudy", "text": "

It does not change the keys used by TLS itself, though?

", "time": "2026-03-17T09:19:34.000Z"}, {"author": "Ionu\u021b Mihalcea", "text": "

I'll let TLS folks answer that, and whether those keys are part of the TLS key schedule.

", "time": "2026-03-17T09:20:08.000Z"}, {"author": "Muhammad Usama Sardar", "text": "

Thomas Fossati said:

\n
\n

I believe that before asking adoption we should clarify what the scope of expat is: see https://github.com/tls-attestation/exported-attestation/issues/56

\n
\n

This is an implementation detail. We will see how the discussions go as more developers implement it. In CCC Attestation SIG, as you know, there is clear interest in SHIM layer.

", "time": "2026-03-17T09:20:14.000Z"}, {"author": "Muhammad Usama Sardar", "text": "

Jens-Rene Giesen said:

\n
\n

Possibly there is some confusion about formal methods wrt protocol anlaysis (i.e., Tamarin) vs. for program analysis?

\n
\n

So in UFMRG, we distinguish formal analysis vs. formal verification to distinguish the two.

", "time": "2026-03-17T09:21:18.000Z"}, {"author": "Nathanael Ritz", "text": "

@Usama, I think if we were to be pedantic, it generates a psuedorandom number (PRF)

", "time": "2026-03-17T09:21:27.000Z"}, {"author": "Jonathan Hoyland", "text": "

Pseudorandom bitstring, surely

", "time": "2026-03-17T09:21:49.000Z"}, {"author": "Hannes Tschofenig", "text": "

Extended Key Update is pretty far along!

", "time": "2026-03-17T09:22:13.000Z"}, {"author": "Nathanael Ritz", "text": "

a jumble of bytes, like Yaron's voice unfortunately

", "time": "2026-03-17T09:22:19.000Z"}, {"author": "Hannes Tschofenig", "text": "

Maybe Tiru should continue

", "time": "2026-03-17T09:22:40.000Z"}, {"author": "Jonathan Hoyland", "text": "

It sounds choppy like we're getting lots of packet drops.

", "time": "2026-03-17T09:22:51.000Z"}, {"author": "Deb Cooley", "text": "

I wonder where he is - physically....

", "time": "2026-03-17T09:23:14.000Z"}, {"author": "Paul Wouters", "text": "

extended key update needs to accommodate extensions that can be used by things like attestation extensions. did that get updated yet in the draft?

", "time": "2026-03-17T09:23:31.000Z"}, {"author": "Nathanael Ritz", "text": "

The moon. tiptop wg is doing work

", "time": "2026-03-17T09:23:34.000Z"}, {"author": "Muhammad Usama Sardar", "text": "

Option c does not cover server as Attester. Option b requires reconnections.

", "time": "2026-03-17T09:23:42.000Z"}, {"author": "Tirumaleswar Reddy.K", "text": "

Yes, extended key update allows extensions.

", "time": "2026-03-17T09:23:54.000Z"}, {"author": "Muhammad Usama Sardar", "text": "

Option a: EKU has lots of problems with the threat model.

", "time": "2026-03-17T09:24:04.000Z"}, {"author": "Deb Cooley", "text": "

@Nathanael he may be in a bomb shelter

", "time": "2026-03-17T09:24:08.000Z"}, {"author": "Paul Wouters", "text": "

@tiru: ok good. I will have to read the latest draft :)

", "time": "2026-03-17T09:24:27.000Z"}, {"author": "Jonathan Hoyland", "text": "

0 and PSK, no?

", "time": "2026-03-17T09:24:48.000Z"}, {"author": "Deirdre Connolly", "text": "

Jonathan Hoyland said:

\n
\n

@Deidre I have been trying to get people to use terms consistently for ages, but I can't even get myself to do it :sweat_smile:

\n
\n

it's so hard

", "time": "2026-03-17T09:26:28.000Z"}, {"author": "Thomas Fossati", "text": "

Muhammad Usama Sardar said:

\n
\n

Thomas Fossati said:

\n
\n

I believe that before asking adoption we should clarify what the scope of expat is: see https://github.com/tls-attestation/exported-attestation/issues/56

\n
\n

This is an implementation detail. We will see how the discussions go as more developers implement it. In CCC Attestation SIG, as you know, there is clear interest in SHIM layer.

\n
\n

It is not an implementation detail; it is a question about the scope of the specification.

", "time": "2026-03-17T09:26:49.000Z"}, {"author": "Muhammad Usama Sardar", "text": "

Jonathan Hoyland said:

\n
\n

0 and PSK, no?

\n
\n

Initially the PSK is 0, right? (without resumption)

", "time": "2026-03-17T09:27:32.000Z"}, {"author": "Jonathan Hoyland", "text": "

It could also be an out-of-band PSK

", "time": "2026-03-17T09:27:54.000Z"}, {"author": "Muhammad Usama Sardar", "text": "

and no external PSK

", "time": "2026-03-17T09:28:00.000Z"}, {"author": "Muhammad Usama Sardar", "text": "

sorry was just typing. Let's there are not both of them. It's still a key in key schedule, right?

", "time": "2026-03-17T09:28:37.000Z"}, {"author": "Jonathan Hoyland", "text": "

Not one that I'd rely on though :joy:

", "time": "2026-03-17T09:29:19.000Z"}, {"author": "Muhammad Usama Sardar", "text": "

not about dependency, point is: it is a key in key schedule.

", "time": "2026-03-17T09:30:08.000Z"}, {"author": "Muhammad Usama Sardar", "text": "

My point was: Key can be constant.

", "time": "2026-03-17T09:30:26.000Z"}, {"author": "Ionu\u021b Mihalcea", "text": "

Thank you, everyone!

", "time": "2026-03-17T09:30:26.000Z"}, {"author": "Yaron Sheffer", "text": "

Thank you!

", "time": "2026-03-17T09:30:36.000Z"}, {"author": "Henk Birkholz", "text": "

Thanks all!

", "time": "2026-03-17T09:30:37.000Z"}, {"author": "Hannes Tschofenig", "text": "

Thank you all

", "time": "2026-03-17T09:30:41.000Z"}, {"author": "Muhammad Usama Sardar", "text": "

Thank you all. Welcome feedback and discussion on list.

", "time": "2026-03-17T09:30:50.000Z"}]