Session Date/Time: 16 Mar 2026 06:00
Mališa Vučinić: Okay. So welcome everyone. Uh this is the LAKE meeting at IETF 125. Hello to all the remote presenters from Shenzhen. My name is Mališa and my co-chair is Renzo. Uh since we are the Monday of the IETF week, it uh meant we should take a moment to take care of the Note Well. Note Well covers the IETF contributions and uh all the contributions that you make with respect to this meeting are uh are considered contributions to the IETF standardization process. Please be respectful to each other and behave in a professional manner. Uh if you are aware of any patents, uh you are required to disclose them following the uh the Note Well. This meeting is recorded, uh so uh we are and we are taking notes. I believe we already have at least two note takers, Marco and Giosuè, and I would like to thank them at this occasion for their availability. Uh so onsite attendance, please sign uh sign in using the Meetecho uh onsite tool by scanning the QR code such that your presence is logged. Remote participants, please make sure your audio and video are off unless you're chairing or presenting during a session.
Mališa Vučinić: So here are a couple of resources for today's meeting. We have a packed agenda. So uh we uh I will be going through this in a moment. Uh we uh I took I took a moment to recap a little bit because we have a couple of newcomers in the in the meeting. So to recap what the working group is about. So uh LAKE working group has standardized uh the EDHOC protocol, RFC 9528, uh a lightweight authenticated key exchange protocol. It was standardized, I believe, two years ago as an RFC in RFC 9528 and RFC 9529. The EDHOC protocol targets constrained IoT use cases such as BLE, 6TiSCH, IEEE 802.15.4, LoRaWAN, and other applicable use cases. It was developed in synchronization with the formal methods community uh by launching different formal analysis calls in parallel with the standardization process in the IETF. Uh we will see that how that process works in action during this meeting as we will be hearing multiple presentations on formal analysis related to the ongoing drafts of the LAKE working group.
Mališa Vučinić: Uh EDHOC is deployed. I provide here a pointer to a blog post uh that uh that we wrote on EDHOC and some deployments that we are aware of. More information, implementation, formal analysis pointers, etc. are available at lake-wg.org. It's a confluence page that we as chairs try to maintain to the to the extent possible. Of course, if you see anything outdated on that page, please let us chairs know and we can update the page or you can update it directly by clicking by anonymously uh editing the page. Current work in the in the LAKE working group considers rekeying and pre-shared key-based authentication, remote attestation, third-party authorization, implementation consideration documents, etc. and we will be seeing more of these during the meeting today.
Mališa Vučinić: So that would be it for the recap. Right now on the status, uh so all the six of the active adopted documents got recent updates for this IETF, so I thank the editors and the draft authors for uh for their reactivity. Today five of them will be presented and uh so the documents will be presented as well as formal analysis presentations for two of them because we recently launched the formal analysis for the pre-shared key-based authentication draft uh in uh during the last IETF meeting after the last IETF meeting in Canada sometime in November 2025. Uh apart from the adopted documents, we have four individual drafts that will be discussed at this meeting and uh I would like to take this occasion to thank Paul for serving as our AD uh and for doing uh the the bulk of the work on the rechartering uh of the LAKE. As a reminder, the new LAKE recharter allows us to uh standardize new EDHOC methods that includes KEM authenticated uh KEM authenticated EDHOC methods as well as to perform maintenance on the protocol to include to standardize new cipher suites, which includes the work on reducing transport overhead. One document that is not discussed in today's meeting is the GREASE document that is led by Christian. Uh he kindly provided the hackathon report in the form of a GitHub issue which you can consult at this page and in consultation with Christian, we will be launching a working group last call uh after this uh after this meeting on the GREASE document. Uh we expect multiple working group last calls to be launched at this meeting, so for note takers it would be it would be appropriate to to maybe make a section in the notes on the working group last calls and we we would need to agree on the order in which we will in which we will launch working group last calls as this is the best practice of the working group so far such that we do not overlap the documents uh and we give enough time for reviewers to review individual documents uh during the working group last call.
Mališa Vučinić: So I'm already a little bit over time and we have a packed agenda. So this is what the agenda looks like. Do we have any agenda bashing on this agenda here? Uh so I hear none, so I suppose uh we'll be going on with this agenda. Okay, thank you. Uh so uh so this will be for any other business. For with that, I propose we get a get going with the first slot, which is the formal analysis of draft-ietf-lake-edhoc-psk-06 by Dekra. Dekra, can you hear us?
Dekra Mahmoud: Yes, I do.
Mališa Vučinić: Okay, let me just share the slides. I'll just give to Dekra I think.
Mališa Vučinić: Okay, perfect. I couldn't find her in the participants list, that's perfect. So Dekra, you have 20 minutes. Uh please go ahead.
Dekra Mahmoud: Okay, thank you Mališa. Uh so I am Dekra Mahmoud, I'm a postdoc researcher from a lab called LIMOS in France and I basically work fully on the formal analysis of security protocols. Um okay, so as Mališa mentioned, so the EDHOC-PSK is currently under standardization and uh the LAKE working group called for formal analysis and here we are.
Slide 01-Mahmoud-Formal Analysis of EDHOC-PSK
Dekra Mahmoud: Um okay, so before going through the formal analysis, let me just give you a quick reminder regarding the EDHOC-PSK protocol. Uh so it involves an initiator and a responder, they both share a symmetric secret key beforehand and in the first message, the initiator is going to create his own ephemeral Diffie-Hellman key which is here uh g to the power of x and the responder uh is going to uh process the message and send and create his first his also ephemeral Diffie-Hellman key g to the power of y. In the third message, uh the initiator is going to use his PSK uh in uh in the message, so uh upon receiving this message, the responder is going to authenticate I and uh the initiator waits to the last message from the responder in order to authenticate him, right? And after actually this exchange, so uh a session key called PRK is going to be created, right? Uh so here you only need to recall that um it's based on pre-shared key and uh both of them needs an identifier for the pre-shared key called ID_CRED_PSK. I will go again to this ID_CRED_PSK maybe later.
Dekra Mahmoud: Okay, great. Um now regarding the formal analysis in the symbolic model. So in this particular approach, we consider that cryptographic primitives are perfect, meaning that uh there is no cryptanalysis attacks, there is no uh side-channel attacks, uh meaning that we need only um the the secret key in order to decrypt, I mean the only way to decrypt is with the secret key, right? So uh the protocols also needs to be encoded in a formal language, right? It depends on um the tool or it depends on um what formal language that we choose. The attacker is considered the full network and generally speaking, we consider the worst case, I mean it's an active attacker who can intercept, play, replay messages, delete or block messages and also inject messages of his own. Uh we can also add some particular compromise capabilities for the attacker. In this uh work, we added um the compromise of the PSK, we added the compromise of the Diffie-Hellman secret keys x and y. We added also the possibility for the attacker to compromise the session key and we also added a capability at infinity of the attacker, which is um a discrete logarithm oracle. So why here at infinity? Because we considered in our formal analysis unbounded number of sessions and unbounded number of participants, that mean infinite number of sessions, so the oracle only need to be deployed, I mean at the very end or after um the protocol executions. Um the security protocols also should be expressed formally either as reachability or derivability properties or trace properties or equivalence properties. So in order to have a model and when we I mean talk about a model in the symbolic in formal analysis, so we talk about a model of the protocol, model of the primitives, model of the attacker, and a model of the security property. And the modeler actually has yeah—
Mališa Vučinić: So we have some in the queue, would you like to take questions now or at the end of your presentation?
Dekra Mahmoud: Maybe at the end because I'm going back to to all of them. No.
Mališa Vučinić: Okay.
Dekra Mahmoud: Okay. Uh so yes and the model actually has the freedom over all those properties. So for for those who consider that designing security protocols is actually hard, I mean also verifying security protocols is actually hard because if there is some details missing in one of those features, then we may have different results. Um okay, so I think maybe all of you have heard of the mainstream protocol verifiers Tamarin and Proverif. Also the choice of the tool is important because I mean they may give different results. So um in 2022, um we have um this paper called Sapic+, Protocol Verifier of the World Unite, where they introduced a new framework uh from which we can, I mean from one model of Sapic+, we can generate two models, one for Tamarin and one for Proverif, and we have some the soundness over the protocol model. Not over the primitives, not over the security properties, but over the protocol model in order to be able to work on it with both tools. Uh so here maybe my my table is not fair for Proverif, it seems like Tamarin checks all the all the marks, but this is not true. Proverif generally speaking is more efficient and is very fast compared to Tamarin. But Tamarin is more precise.
Dekra Mahmoud: Um okay, so now let's see the claimed uh and formalized security properties for the EDHOC protocol. Uh so there is confidentiality of the session key and we formalized it differently. So we formalized secrecy of session key from the initiator point of view and the responder point of view since they may not agree on the same session key. We formalized also um secrecy upon agreement and forward secrecy. Also mutual authentication and explicit key confirmation was claimed, so we formalized the authentication of the initiator to the responder uh upon receiving message three and the authentication of R and I uh upon yeah upon the receiving of message four. Uh so regarding the properties that we formalized as equivalence properties, so we can see that uh it's called identity protection. We formalized two flavors of identity protection, namely anonymity and unlinkability. Anonymity of a participant just means that the attacker won't be able to uh extract or to know the identity of uh either the initiator or the responder uh when the protocol has been executed. And unlinkability means that even though the attacker doesn't know the identity, can the attacker actually link sessions to the same identity?
Dekra Mahmoud: Okay, now let's see the table of the results using Tamarin and Proverif with trace properties. So here I put the uh minimal compromise scenarios that are needed to break the security properties and this table can be, I mean we can read it as the following: For example, the PRK secrecy upon agreement can be broken either uh in the active case, either if the attacker has a PSK or x, which is the ephemeral key, or PSK and the other ephemeral key, or simply if the attacker compromises the PRK. Uh we can see here that PSK is basically everywhere, that means that it uh it acts like a defense mechanism to um all the properties, uh but we can see that um the forward secrecy is not achieve- achieved if we consider um discrete logarithm oracle. Uh okay, so the minimal compromise scenarios for the identity-hiding properties, so we can see that the unlinkability of the initiator in the passive case can be broken either if the attacker knows one of the ephemeral keys, but if the attacker has an access to a discrete logarithm oracle, then there is no unlinkability of the initiator and also there is no unlinkability um for the responder considering a passive attacker. And in this particular case, Proverif actually output um a counter-example for the unlinkability of the responder considering um a passive attacker which is actually very, let's say, obvious. If we have um one responder uh executing the protocol with maybe multiple initiators, and on the other hand, this execution should be indistinguishable from having many responders. And if the initiator actually just broadcast um messages, then at some point in the case of we have many initiators, uh many responders, so the protocol would fail uh at many points since the authentication of the responder only happens in the last message. However, if we have only one responder, we are always having message four, message four everywhere, so um the protocol would never fail and the attacker would be able to compare uh those scenarios.
Dekra Mahmoud: Okay, so before taking the questions, uh I'm going to say that are we done with the formal analysis? I would say no because uh we can add many features to our models. So here I put um what we can integrate immediately. For example, more precise model of the XOR, uh also add more algebraic properties of the Diffie-Hellman exponentiation in Proverif. And more importantly, so for me, we need to replace the Diffie-Hellman with a standard KEM model to see whether if the KEM actually uh I mean behaves exactly like the Diffie-Hellman or not. Um also we need to, I mean there is those security properties which is called unknown key-share attacks that we need maybe to model such as bilateral and unilateral case. Uh for the next next steps but not immediate, those are more complicated features. So I put here uh some ideas, so for those who want to collaborate or for those who want to make their models, so it would be, I mean, great to add those features. Thank you so much.
Mališa Vučinić: Thank you Dekra. So we can take questions now. So we have Usama in the queue. Usama, do you want to go ahead?
Usama Sardar: Yeah, sure. Thanks very much. It was very interesting and great to see that the working group is going into more and more formal analysis. That's really nice to see. Uh if you go back to fourth slide, I just a clarification question. So replay, delete, inject, that all is fine. So I just want to understand intercept that so at the top you are saying the network as the worst case, so intercept would just be a passive listener, it wouldn't be active one, right?
Dekra Mahmoud: Yes, exactly.
Usama Sardar: Okay, thanks. Okay, and in the next slide I have I work a lot with Proverif, I do have concern about this. I think it's a not not a fair comparison as you also kind of agreed. Yeah, I mean saying maybe is not enough because your slides are there and people can misinterpret it. The thing is that it can be useful in many cases where Tamarin will get stuck and so on and you need to move to some tool where you can still get some results with some approximations maybe. Um but anyway. So in the next I think six or seven slide you had minimal—
Dekra Mahmoud: Yeah yeah, wait, but I mean what I put in here actually is is correct, this is not not correct. I mean the only thing that Proverif maybe can, I don't know, can be better uh toward Tamarin is just the efficiency and not regarding the precision.
Usama Sardar: That's what I mean. I mean there has to be one row which should kind of show that it's more efficient so I didn't mean to say that this table is wrong, I was just saying that there is a row missing kind of. Okay, so I see Jonathan is in the queue, so I will stop here and let other people ask and then uh I was trying to understand here minimal compromise scenarios, what does that mean, but I will come back to it later. Thanks.
Dekra Mahmoud: You're welcome.
Jonathan Hoyland: Yes, Jonathan. Uh hi, this is Jonathan Hoyland. Um I just you you mentioned something very briefly and I didn't really understand how it worked. Um I'm it is gone 6 o'clock in the morning for me so I'm a little bit slow today. Um how is the PSK ID bound to the PSK?
Dekra Mahmoud: Yeah, okay. So that's actually because I wanted to go back to this um okay, so to be honest with you, so this is something I mean I was dealing with uh and was asking question regarding the ID_CRED_PSK to the designers. And what I understood is that um the ID_CRED_PSK is just an identifier, either it I mean it is locally it locally binds I mean in the memory the um the PSK on the initiator side and or and on the responder side, or it's actually a different uh ID and which I mean locally different and it should bind uh the PSK and the participants to uh the same PSK. But I believe that it should be sent or known uh beforehand uh in the moment where the PSK is shared with the initiator and the responder. Or maybe Elsa or someone in the working group can explain this further.
Jonathan Hoyland: So because I remember when we were looking at Tamarin, uh one of the things sorry, TLS, one of the things that was found, one of the attacks that was found was if you end up in a misconfigured state where the client, the initiator sorry, thinks ID_CRED_PSK corresponds to key one but the responder thinks it corresponds to key two, they could both complete the protocol with the attacker and think it had all gone fine. Um yeah, so yeah, I think to me this is something that should be um specified more in the draft because uh for instance I can ask many I mean I have many questions regarding the ID_CRED_PSK, for in- for example, is the ID_CRED_PSK as I mentioned locally the same for from the both points of views or it's not locally the same? And also is the ID_CRED_PSK the same when um the participants switch roles? I mean uh do we have even here the same PSK or not? So so I don't know. So the way we modeled this is that uh it is known to both participants beforehand and it's actually the same uh and it's just an identifier.
Jonathan Hoyland: So if I was doing this modeling this in Tamarin, I would say that you should that I would model it as the attacker chooses uh like you literally just the attacker says to the client use this ID_CRED_PSK and the responder use that ID_CRED_PSK. Um because unless it's actually bound to the PSK, so like if your ID is the hash of the the pre-shared key or something.
Dekra Mahmoud: Okay.
Jonathan Hoyland: Then then it's actually bound to the key, but otherwise I'd just say let the attacker choose it.
Dekra Mahmoud: Okay. So I think you are talking about two different things. It's the way you model you model it or uh how it is in real life. So the way we modeled is we apply only a function symbol on uh the PSK and the both identities cred_I and cred_R. So it's actually bound to the I mean binds to the both uh participants. But in real life I don't really know how it should be implemented or uh maybe John—
Jonathan Hoyland: So so for my like if you want to model this so that your model is going to capture attacks that might happen in real life, you you shouldn't say oh we assume that it's perfect, you should model it saying we assume that it's broken and then increase the requirements of the protocol until it fixes it.
Dekra Mahmoud: Yes yes. Yeah.
Jonathan Hoyland: Just some thoughts.
Dekra Mahmoud: Yeah, thank you.
John Mattsson: Yeah, uh just in in the draft it's not the identity. What the draft says currently is not it does not force that identity is bound to the PSK in a cryptographic way. It says that the receiver can find the PSK using the ID_CRED and then it assumes that it's provisioned in in a secure way. Um so I think any additional requirements would have to come for the formal analysis. And theoretically you can add a lot of things and if you have some unconstrained protocol like TLS it's not a problem, but here every byte counts, so like any any change that would add additional bytes on the wire uh would have to be discussed then it becomes a tradeoff.
Mališa Vučinić: Okay, thank you John. So uh I there is Meiling in the queue.
Meiling: Hello, sorry to interrupt. Is it still possible to change the agenda? It's just because I'm the last item, I just need three—
Mališa Vučinić: I'm sorry, we are in the middle of a slot on formal analysis. Can we take that question after the after this slot?
Meiling: Okay.
Mališa Vučinić: Yeah.
Dekra Mahmoud: Yeah okay, so I'm just going to add uh I put in here to add um to the remark of the last um I don't know what's his name, sorry, I forgot your name regarding the PSK and ID_CRED_PSK. So here ideally yeah we should uh have a model of stateful protocol where we have really a I mean a table and uh a database where we can actually store the ID_CRED_PSK and the PSK etc. and uh give the attacker the possibility to choose the ID_CRED_PSK. Yeah just some some thoughts. Thank you.
Mališa Vučinić: Okay, so we have one more person in the queue. I will lock the queue after because we are out of time. Usama, do you want to go ahead?
Usama Sardar: Yeah, maybe very quick one. So coming back on this minimal compromise scenarios, maybe you can give one example of how did you find these minimal ones because adding these ORs it seems to me that there are multiple combinations possible. So maybe you can give a quick example of PRK secrecy upon agreement, how do you how did you find that or how how do you claim that to be the minimal and how what was your kind of strategy in finding that minimal? Thanks.
Dekra Mahmoud: Yeah, okay. So uh to me because okay, how we found it um so maybe so we can start first with just uh an attacker who is just active, so without compromise scenarios, and then we start uh by one by one, I mean PSK alone, x alone, y alone, PRK alone, right? And then if it's if we find an attack then we validate it. For example, here we found uh that it's not the property's not verified with PRK, so we put PRK uh at the moment here, and then we start uh to look at the combination of twos, right? For instance PSK and x or PSK and y and uh etc. and if something if a combination is actually validated, then we move to the others until we have no other uh combination, and that's how we can find the minimal. And and here actually it's if and only if, I mean secrecy upon agreement if and only if we have this combination. That's what minimal means.
Mališa Vučinić: Okay, thank you Dekra. So the time is over, so I would uh thank you for presenting. So uh what I hear is some additional clarifications that might need be needed for the draft, so I would kindly ask the draft authors to work with this formal analysis team that responded to the analysis in order to clarify uh the the ID_CRED_PSK considerations in the draft.
Dekra Mahmoud: Thank you so much Mališa.
Mališa Vučinić: Thank you Dekra for presenting and thank you for responding to this call for formal analysis.
Elsa Lopez: Uh hello, can you hear me?
Mališa Vučinić: Yes, we hear you Elsa.
Elsa Lopez: Okay. Um so I'll I'll try to be fast since we're a bit out of time. Um so I will be presenting the updates on the EDHOC with pre-shared key authentication uh corresponding to draft uh version seven. Um sorry. Um so yeah, the status of the presentation. Um we did some corrections on the test vectors uh after the latest um updates on the draft. We also update the security properties after the formal analysis that was just presented. And we're working on the integration of EDHOC-PSK into the Laker's Rust implementation of EDHOC. Uh so regarding the test vectors, uh little recap after the last IETF, uh there was some changes regarding PRK for E3M, TH transcript hash for and uh the external AAD ciphertexts 3b. And those changes included the addition of the PSK or the cred_I and cred_R in these computations. Uh these were not included into the computation of the test vectors, so we implemented we did a new run of interoperability test using two implementations, one in Rust and one in C, and uh the test vectors were verified and updated in the draft. Uh regarding the updates after formal analysis, so as Dekra mentioned, uh there was some properties that were not verified uh in terms of the identity protection. And so in fact in the um security properties we updated a possible attack regarding the unlinkability of the initiator. So the assumption is that we have an active attacker uh which is a man-in-the-middle between the initiator and responder. So when the initiator sends uh message three, um which contains the encrypted identity of ID_CRED_PSK, the attacker is going to intercept and modify this ciphertext uh to modify the ID_CRED_PSK to one of his choices. Uh this modified message three is going to be forwarded to the responder and the responder is going to attempt to decrypt and verify the message. Now, because the ciphertext is modified, the AAD verification will fail. However, uh depending on the behavior of the responder, the observable behavior of the responder, um the attacker may obtain some information. So for example, if there are different error types, whether it is an unknown credential versus an authentication failure, or timing differences during the credential lookup. Uh and this allows the attacker to test candidate identities and observe how the responder fails. So this is very related with um yeah how the protocol is implemented. Um then I also mentioned that we're working on the integration of EDHOC-PSK into the Lakers' implementation of EDHOC uh in Rust. And as for next steps, uh well after the presentation of formal analysis, I believe we need to clarify the ID_CRED_PSK uh thing. Uh and then I believe we might be ready to call for last call, but um yeah. So that's all for me. Thank you.
Slide 02-Lopez-EDHOC Authenticated with Pre-Shared Keys
Mališa Vučinić: Okay, thank you Elsa. So I will wait for the green light from the author team on the working group last call when I have that we can start when we have the new version of the draft we can start the working group last call.
Elsa Lopez: Yeah.
Mališa Vučinić: Okay, thank you.
Mališa Vučinić: Uh so the next item in the agenda is uh okay so just. Also Elsa I'm trying to give Elsa I changed the deck giving you the I think you have control. Uh so we are doing a little context switch so let me introduce this. So we are this is a work on uh remote attestation that is happening. Uh Elsa performed a formal analysis on this draft even though it wasn't formally called in the working group and requested for a slot to present this. And we have additional presentation by Usama on the formal analysis after this as well as followed by Yuxuan's updates to the draft as the result of formal analysis. As a reminder, this is draft-ietf-lake-ra uh on remote attestation. Usama, yes, do you want to comment something quickly?
Usama Sardar: Yeah, so very very quick comment. So I would like to request the chairs since there is already two parallel works on formal analysis going on, it helps us as researchers if you launch an official call for example in the paper we can cite that hey there was a call although we are uh already past that so we would like to request the chairs if they can have an official call since both are already working on it. Thanks.
Mališa Vučinić: Are you requesting the draft to be frozen or just a call on the on the list because typically the work—
Usama Sardar: No no. No no, not frozen, so just a request for like officially that the call for formal analysis is required, that would be great help for us to justify this work and uh not by any means on frozen.
Mališa Vučinić: Okay, that's fine. Okay, sounds good. Sounds good, we can do that.
Elsa Lopez: Uh should I go?
Mališa Vučinić: Yes, please.
Elsa Lopez: Okay. So me again, I will be presenting the formal analysis of draft-ietf-lake-ra-03 using Sapic+.
Slide 03-Lopez-Formal Analysis of Remote attestation over EDHOC
Elsa Lopez: So outline of the presentation, I'll be presenting the a little summary recap of what remote attestation over EDHOC is, and in particular I'll be focusing on the studied models which include the background check model, the passport model, and mutual attestation. I will then describe the claimed security properties, uh which we divided in three uh categories: remote attestation properties, EDHOC properties, and combined properties. Uh I will then define the symbolic analysis model that we used and in particular the verification framework, Sapic+, and how we modeled the properties, and I will end up with the results that we found and the mitigations uh to these results.
Elsa Lopez: So um the models that we studied, um we in the draft there are two versions uh two models uh described which are the background check and the passport model. Uh so we will be focusing on what we called unilateral attestation case one and four, so those that are in green, in which in the background check model we have the initiator acting as attester and the responder as the relying party, and in the passport model the roles are inverted. So we have the responder acting as a tester and the initiator as a relying party. Um we also studied mutual attestation in which we have basically unilateral case one and four combined, so that both initiator and responder undergo attestation.
Elsa Lopez: So as for the case unilateral attestation case one, this corresponds to the background check model in which we have the initiator, so the IoT device, working as an attester. Then we have the network service working as acting as a relying party and then a trusted web service server, sorry, that uh is the verifier. The EDHOC session therefore is established between the attester and the relying party uh and we see that uh the attestation information in EDHOC is going to be carried on the external authorization data, so the EAD items.
Elsa Lopez: Um then as for the unilateral case four, this corresponds to the passport model and in this case we have uh now the attester is the responder and the relying party is the initiator, so the IoT device, and we see that in this passport model we actually need a fourth message, an EDHOC fourth message, to transport the attestation result in the EAD4.
Elsa Lopez: Um and then for mutual attestation as I mentioned, um so in this case both the IoT device and the network service undergo attestation. So the network service attestation is going to employ the passport model, so what we called unilateral case four, and the IoT device uh attestation is going to employ the background check model, so the unilateral case number one. And similarly we have the EDHOC session established between the attester and the relying party.
Elsa Lopez: So for the claimed properties, uh we based uh our definition and uh division of claim properties on Usama's paper uh that I cite below. Um so we divided them in three groups, the first one being the remote attestation properties. Um and we can highlight four properties here which are freshness of both the evidence and the attestation result and integrity similarly of the evidence and the attestation result. So the freshness is going to ensure that the uh evidence or the attestation result reflect the current state uh of the attester uh or the relying party, therefore uh avoiding replayed or outdated uh values, and this can be achieved by means of a nonce, a random nonce. Uh as for the integrity of the evidence and the attestation result, it's going to ensure that the evidence or the attestation result have not been altered in an authorized authorized manner, and this can be achieved by using a signature with the corresponding private key then then the other party can verify using the corresponding uh public key, um yeah.
Elsa Lopez: As for the mutual uh EDHOC properties, we have the mutual authentication which is going to ensure that both parties verify each other's identity, preventing therefore impersonation and man-in-the-middle attacks. And then we have what it is called combined properties which uh mix authentication and attestation. So we have the channel binding, which is going to ensure that the attestation is cryptographically bound to the authentication. And we also have agreement of parameters, which is going to ensure that the responder's view of attestation and authentication parameters at the end of the protocol matches those of the initiator's point of view. So this property is going to ensure both authentication and attestation correctness.
Elsa Lopez: As for the formal verification, we did this under a symbolic analysis symbolic analysis model. Uh this has already been presented by Dekra before, so I'll be brief. Uh so we have the DY attacker that has full control over of the communication and the most important thing is that we have the perfect cryptography assumption in which the cryptographic primitives are not breakable. Uh therefore the security failures must arise from the protocol design and not from breaking cryptography. Uh and then we have the security properties that are going to be formally expressed as reachability or equivalences. Uh for Sapic+, uh as Dekra mentioned, uh this uh framework allows us to use multiple uh like one input for multiple verifiers. Um and we um we defined a more advanced threat model um to increase the capabilities of the attacker, and in this case we included the compromise of the long-term keys, uh the leak share, which is the leakage of the ephemeral uh keys, uh leakage of session key, and uh the leakage of uh attestation key.
Elsa Lopez: Regarding the modeling of the properties, uh so here are some snippets of how we model the properties uh for the mutual attestation case. So regarding the freshness, uh for the freshness of the evidence and well the result would be in a similar way. This is captured by requiring that if we have two verification events referring to the same honest nonce, then this must correspond to the same protocol execution. As for the integrity, um we express this as a correspondence property, therefore successful verification will by the responder uh implies that this attestation was generated by the initiator with the same parameters, otherwise there was a compromise scenario. Then we have the combined properties uh which are the channel binding and uh agreement of parameters. Um so for the channel binding, um we state that uh successful attestation acceptance by the responder, so if the event attestation accept R happened, then this means that there was a previous event, it was previously sent by an initiator authenticated in that EDHOC session unless a compromise event occurred. And for the agreement of parameters, um this property will ensure that whenever a party finishes, which we see with the finish R, then there exists a unique peer execution that agrees on the same authentication and attestation parameters, therefore finish I with the same parameters uh as the previous event unless there was a compromise event.
Elsa Lopez: Um so the results, um well these are the minimal compromise scenarios again. Um so for the evidence freshness and attestation result freshness, uh the results were verified. Uh so the nonce is indeed going to guarantee that we have freshness in both. As for the integrity, uh we see that the compromise scenarios include the leakage of the attestation key and the long-term key whereas it's the PSK or the static Diffie-Hellman key. We see that channel binding was not verified, and agreement of parameters, similarly those were the minimal compromise scenarios. So what we saw regarding channel binding in fact, we we verified the properties in all four authentication methods, so the standard zero to three authentication methods that are defined in the RFC plus the fourth authentication method that is being standardized in PSK. Um and we see that channel binding did not hold. Uh and this is because there was we found an attack due to the lack of cryptographic binding between um the attestation evidence and the authentication session. And in fact this attack can happen without a leakage of the attestation key. Uh so the description of the attack is as follows. Um if there was a compromise of the authentication keys, then we can have a man-in-the-middle uh attacker that establishes sessions with both endpoints and is going to obtain a valid attestation evidence from an honest attester. So the attacker will present the evidence within a different session as if it were produced by that for that authentication channel. And if the evidence is not somehow bound to the session, then the verification is going to succeed. So what we proposed as a fix uh or as a mitigation was to include the hash of the first two messages in the digitally signed attestation evidence. And this is because the hash contains information that is linked to the authentication session, um including uh the ephemeral shared secret uh of that session that is unique to the session. Uh therefore we are sure that an attacker cannot replay evidences from different sessions. And as for next steps, um it would be interesting to because we only checked the case one and four, but uh maybe it would be interesting to have uh formal verification of the other um cases, uh so with the roles inverted for each of the models. And that's it. Thank you.
Mališa Vučinić: Okay, thank you Elsa. So we have Jonathan in the queue and then Dekra.
Jonathan Hoyland: Hi, Jonathan again. Could you possibly go back to slide 17? Um yeah, I'm I'm surprised that that channel binding would work um because usually you would want the you want to also have the uh hash of some secret for the channel binding to uh be uh for the channel binding to be correct.
Elsa Lopez: Um but so when we include the when we include the hash, in fact the hash as I said contains this ephemeral shared secret. So and this shared secret is unique to the session, so by including the hash we are implicitly including this shared secret as well, which is bound to the session.
Jonathan Hoyland: I I don't that I don't is that correct? You the do you send the uh ephemeral shared secret on the wire?
Elsa Lopez: Uh no, but it's the transcript hash too for instance contains the gy, so we would be including this uh this public key into the hash.
Jonathan Hoyland: Mhm. Um interesting. I I'd have to look at exactly how it's written, but I I would be very surprised if that works without including some shared secret into the hash derivation. Uh yeah, I'll have to read through the draft.
Elsa Lopez: Okay.
Dekra Mahmoud: Uh hello Elsa. Can you please go again to the to the freshness lemma, the way you formalized freshness? Yeah. Okay, so um is it I mean do you here you don't have um conditions regarding the PKI and PKR, so they should be different or they should be the same, I don't understand.
Elsa Lopez: Uh so here we are saying that if we were to have they could be different they could be the same but if the nonce is in fact the same then this means that these events must actually be the same because we cannot have a nonce that is repeated amongst different sessions because it's freshly generated.
Dekra Mahmoud: Yeah, but if they need to be the same, okay so yeah I do because you know some some of this I mean security properties are not conventional security properties so that's why I was curious on how you formalized them. Okay, I will have to look at this again. Thank you.
Elsa Lopez: Okay.
Usama Sardar: Yeah, so following up on what I understood from Jonathan, I think there is uh um one thing more missing, which is that the identity of the endpoints itself is not yet established at the time you generate that evidence. That's my core concern, but I will talk about it in my talk, so I just wanted to know uh how that property that you have if you go back to the channel binding property that you state, uh so I am a bit curious about—so the one where you show that was fixed. So I'm very skeptical about that being fixed because of the reason that the time at which you generate that evidence it's not yet authenticated. So I will talk about it in the my talk as well so I just wanted to raise this issue.
Elsa Lopez: Okay.
Mališa Vučinić: Okay, we had to lock the queue at this point because we are we have a packed agenda and we are over time. Uh but thank you everyone for your comments. It is great to see that these models uh are open-source and published, and I would invite all the uh interested folks to look at the models and to provide feedback to the working group uh concretely on the properties uh how they were defined in the models as they were defined.
Mališa Vučinić: So Usama, you have five minutes. I believe this uh this refers to the same version of the draft LAKE-RA-03.
Usama Sardar: Yes, that's correct. Yeah. Okay. Thanks very much. Yeah, um this is joint work with Viatcheslav and Jan Mehri and thanks to Yuxuan, Marco, and Göran who helped us in this work. And uh specifically I want to describe the motivation why we already started even before the call for formal analysis was there, our brand new charter basically says that the we will borrow as far as possible from RATS and TLS working group and this work was basically religiously following the draft-fosati-tls-attestation to which I have been contributing and formal analysis as per charter was welcome not specifically for this uh draft as I said the call, but overall it is welcome, so we already started the work since since we had done the work for attested TLS. So we believe that it's a subtle addition, it does need formal analysis since we have found many attacks in formal analysis of attested TLS, that's why we started already and the kind of the thing is that from attested TLS what we have noticed is that the devil is in the details as the kind of a clumsy picture here.
Slide 04-Sardar-From formal analysis of attested TLS to attested EDHOC
Usama Sardar: So I have three levels, which is the one at 1b level one, level two, and level three, which is um level one is the shared gxy, level two is the uh application sorry the handshake traffic secret of the client and I'm taking from the client perspective, it can be also from the server perspective because here the server is the attester so client is the one who going to send the secret, and level three at the bottom 2d is the application traffic secret of the client. And I want to make specifically two arguments here: Number one is that um what Ekr actually raised at the time of the chartering of the TLS working group and he said that the look this this handshake traffic secret is independent of the security claim, it's irrelevant and we checked that we removed all of this encryption which you see in the brown color, KSH and KCH, these are the keys derived from the handshake traffic secret of the client and used for encryption of these messages. So removing this encryption makes no difference on the security properties, it's important for privacy, not for security. Second argument here is that HTSC, which is handshake traffic secret of the client, is derived at the point in time where number two of authentication has not even started. So if we generate that evidence which is to be put into the certificate message in TLS, we don't actually get that guarantee. And moving on to from attested TLS to attested EDHOC, what we did was the approach overall as I posted in the one of the uh threads was we used modularity, that is to say both from model and the um properties perspective. Properties already uh was presented in one of the talks. So from the protocol perspective, what we did was this is the key exchange part, the first part, and then the authentication part that remains the same. We applied some abstractions which we don't currently have a proof that they are completely sound but that looks reasonable to us at the symbolic level and that's what we use currently. We are refining it further and we will also share the paper that we have uh ongoing on that. And analogies basically here mean that which key represents which uh which key from TLS represents which key in EDHOC, so that's the kind of analogies that we did here. And based on that, what we have is the results for correlation properties which we presented in UFMRG in last meeting apply as is to this protocol version three. There is no binding as Elsa already pointed out, so there is no binding from the evidence to that specific connection which is established, and with that root cause all of the three bindings, that is to the gxy, um the shared secrets, handshake traffic secret, and the application traffic secret corresponding to the TLS properties still apply in this case. And the post fix specifically for this is to use post-handshake attestation because of the server authentication not being there and in this case the responder one not being there. So that's pretty much it. I see Yuxuan in the queue, yes please.
Yuxuan: Okay hi, I'm Yuxuan. So um after your slide was uploaded, I have sent an email in the working group to ask like if you have any links that can provide to tell us like how you got these results for the draft-attested-edhoc because um from all your public results, I think these are all for the results um for the formal analysis of attested TLS. And I agree that attested EDHOC somehow follows the attestation TLS attestation in the attestation part, but still they are two different drafts. So um and also from your reply I didn't see that you provide links for the model that you have for the draft-attested-edhoc, so um I do not agree that here in the table of the results you put the draft-lake-ra here because you at least from we know you do not have a real model that is only for attested EDHOC and you I don't think it's correct to just copy the results for attested TLS and then put it here in the table for the attested EDHOC, so um yeah that that's what I think.
Usama Sardar: Okay, so I want to recall you that we had a meeting between you, Elsa, and Mališa in December 22 around of that time. So we had a long discussion about that where I explained you all these attacks, and uh you're right, we don't have the model as Elsa has. We have modularity and analogies and abstractions which I explained and we will make that all public once we have that paper accepted. So I will explain you again uh how all that works, but I completely disagree with you that the attacks do not apply. We have there might be soundness reasoning that hey this doesn't the abstraction is not sound, that's fine, but the attacks do apply and I can share with you the attack traces. That's something I can share with you.
Yuxuan: Um yeah and actually the reason I asked this question is because I completely understand what you explained to me because what you explained to me is the attacks that you found in attested TLS. And as you said, Elsa also had the formal analysis because and she also shared the public source code for the formal analysis and here I think you are just copy the results you have for the attested TLS, so I don't think it makes sense.
Usama Sardar: Yeah, it might not make sense to you, it makes perfect sense to me because it's just following the same protocol and the same analogy. So you might disagree but the attack traces are—
Mališa Vučinić: Yeah, so TLS and EDHOC are two different protocols with two different key schedules, so it would it would be useful to the working group I agree to have the models published. So as soon as you have the paper, the publication pending or whatever published, it would be good to to send this to the working group so that we can examine closely.
Usama Sardar: Sure, yeah. I already pointed out that we will share it and that will be under Apache 2 license so everybody can have a look and satisfy themselves and I believe that this feedback is already sufficient for the editor to move forward.
Mališa Vučinić: Okay. Thank you Usama. Thank you for for doing this work. Uh so we have Zhang in the in the queue.
Speaker 1: So I have the comments after your proposed the fix, it's Jun Zhang from Huawei. So security is important, but the security is not everything. So this morning everyone have noticed that there's a crash of the internet connection, right, for the for the everything is cut off. This is because if you have very serious, important consideration of the security, you do not have a good usability. So in this case for the attested EDHOC, sometimes we need very small delays so that if you have the post-handshake, you will violate the the requirement of the application in the attested EDHOC. So I have some draft submitted to the SEED but due to the time delay I have not successfully submitted, but I will share the my consideration in the SEED working group and so welcome for the feedback. Thank you.
Usama Sardar: So your your concern is about attested TLS or attested EDHOC, which one?
Speaker 1: For the general case, so that the security is not everything, you need to consider the tradeoff.
Usama Sardar: That's fine to have both solutions, I mean I'm not advocating to have post-handshake only if you want, so if there is some genuine concern that you have or a genuine case, I would really love to have a look at the use case that you are mentioning if that's worth it that we still live with the attacks which are possible. Thanks.
Mališa Vučinić: Thank you, moving on.
Mališa Vučinić: Thank you. Yes, we we need to move on. So the next slot is the draft-ietf-lake-ra-04 presented by Yuxuan. So this will present in my understanding the updates to the draft that as they have been done after following Elsa's presentation.
Slide 05-Song-Remote Attestation over EDHOC
Yuxuan: Yeah yeah, so hi I'm Yuxuan and this is for the updates for the draft remote attestation over EDHOC. Next slide please. Um yeah, a quick recap is that this draft specifies how to perform the attestation by using the EDHOC EAD fields, and the figure here is an example for the mutual attestation which is defined in the draft. So for the updates we have, um the first one is based on the formal verification results uh from Elsa who just presented. So the results showed the attestation evidence is not bound to the authentication session. Uh so when the authentication key leaks, it may have a potential relay attack that the attester, the party who generates the evidence, is not guaranteed to be the initiator who authenticates. So the figure here is also like quite similar to what Elsa had in her slide. So uh when the attacker can impersonate when he can impersonate the EDHOC roles and has two different sessions, then the evidence that is generated in session A by the initiator A will be received by the attacker and then be related to the session B, and since the evidence is not bound to the authentication session, so here the evidence uh which is generated in the session A will also be accepted by the session B by the responder B. So this is uh some thing that we found the channel binding does not hold in the version three in our draft.
Yuxuan: So then we uh have the mitigation as an attestation binder, so this was added in the current version. Uh and also like followed by the suggestion from the verification results from Elsa. So uh when we have the attester as initiator, we have the evidence that is sent in EAD3 which is in EDHOC message 3. And here we uh have the attestation binder which is defined as the hash of the first two messages, and the uh hash algorithm is the cipher suit that uh in EDHOC. And then uh because of the implementation considerations and also to be aligned with the draft-ietf-lake-authz, we decided to change in the next version uh to let the attestation binder be the hash of the hash of message 1 comma message 2. And also this attestation binder must be included in the evidence and then signed by the attestation key. So as you see here, um when we have the evidence that contains the attestation binder which is the hash of the first two messages, uh and this hash of the first two messages is somehow session unique. So in this way we can we can say like the evidence is cryptographically bound to the authentication session, so when the responder receives this uh evidence, he will check if the attestation binder is the correct one because the responder responder itself will also generate the attestation binder by calculating the hash value. So if it's the same then it's correct, otherwise uh it would not continue the following operation.
Yuxuan: And then we also have the case that the attester is the responder, so this happens when evidence is sent in message four in EAD4. Um so as in EDHOC, we know that after three messages we have the final session key derived. So here we define the attestation binder that is derived by the EDHOC exporter, so if you know EDHOC you will know that EDHOC exporter is derived by the final session key. Uh so in this way we can bind the uh evidence with the authentication session. And of course the same this attestation binder must be included in the evidence and signed by the attestation key.
Yuxuan: And then for the next issue which I remember was raised by Carsten, uh we this time fixed the CDDL syntax errors throughout the draft. Uh and I think it was also mentioned by Carsten that we are thinking uh if it's possible to validate the CDDL syntax as part of the continuous integration. Uh I don't know if Carsten is here today but if uh he's still willing to help or give any guidance, it will be very appreciated.
Yuxuan: Uh and then um we have some issues for the clarifications and editorails. So we uh explain the difference between the background check model and the passport model, and then we add RATS part in the privacy consideration as well, and then uh we added the requirement of the ability to generate random nonces because when the relying party is the one who needs to generate the nonces to guarantee the freshness of the attestation result, we need to make sure that this uh relying party when it's a constrained device has the ability to generate a real random nonce. Okay, that's it. Thank you.
Mališa Vučinić: Thank you Yuxuan. So we have two people in the queue: Usama and Zhang. So Usama, you want to go?
Usama Sardar: Yeah, yeah, so I will put your question back to you. So uh why do you think that the attacks do not apply in your specific case? And I want to follow up also on Mališa's point specifically here, so at the symbolic level if we talk about the symbolic security analysis, basically if you see that the functions are assumed to be ideal, so that doesn't matter whether it's TLS key schedule or it's EDHOC key schedule, that's how the proof is derived. But I want you to explain me why do you believe that the hashes that you have used are sufficient, and number two why do you believe that the attacks are not possible.
Mališa Vučinić: So I will I will cut it here Usama, please. Uh I mean so there is a point of disagreement in the group on this, so uh I think we all agree on that. Uh one group uh has published their models, you have not and you have not provided the attack traces. As soon as you do that, we will be able to discuss in details uh this matter further. So I would postpone this discussion to that point once you can publish the the models. Thank you.
Yuxuan: Yeah and also uh I've sent you Usama I've sent you the email to say that we can have the meeting but I didn't receive the response so if you are available we can also have a meeting to discuss this deeper.
Mališa Vučinić: Let's please take that offline. Uh so we have another comment.
Speaker 1: So just two comments. So for your operation after you will take the the hash of the message one, so what do you think that if you use the XOR instead, it will be better or it's another alternative for for that message one with XOR certain certain value. So for a lightweight operation. So this is the first comments. And for the second one is that so you see that in sometimes with the relying party generate nonce, so when it is do not have the ability to generate very strong random number, uh you can look at the the recent IETF epoch mark uh one so that epoch mark will generate a strong strong epoch ID. So says that you can have the concatenate of the the random number generated by the relay with the one from the epoch marker. So that will generate a more a stronger random number. So you can have a look at that. Thank you.
Yuxuan: Okay. Thank you, yeah.
John Mattsson: Yeah, I'm just confused by the discussion, seems like Usama claims that the TLS attacks apply to 03 and probably also the 04, and then Elsa has formally verified 04. I don't know, it seems to be seems like some simple misunderstanding. Probably an offline meeting would solve that.
Mališa Vučinić: Agreed, agreed. So yeah, uh I would propose to the to the authors and the involved parties to have a an offlist meeting and then to feedback to the working group based on the discussions during that meeting.
Mališa Vučinić: Okay, thank you. Thank you Yuxuan.
Mališa Vučinić: So with that we can move on, the next item in the agenda is draft-ietf-lake-authz-07 presented by Giosuè.
Slide 06-Fedrecheski-Lightweight Authorization using Ephemeral Diffie-Hellman Over COSE
Giosuè Fedrecheski: All right. Yes, works, thank you. All right, so Giosuè here, and I'm presenting updates on version 07 of Lightweight Authorization using EDHOC. So um big reorganization of the draft. We found a vulnerability where uh the device, the initiator U, can uh impersonate be impersonated to W. So to give context, so U can ask for a voucher uh via a a domain authenticator V, which will forward this request to W and which will upon authorizing this request, reply with a voucher which is then sent back to the device U. Uh yes, and this voucher it can be it can mean a binary decision authorized or not authorized or it can contain some opaque information uh detailing whether what kind of capabilities the device is allowed to do in the network. For example, uh to trust more or less or do different capabilities related to the network that it's joining or the type of domain it's enrolling. So this is the context. And then uh what we found is that if E impersonates U when doing this request to W, then W will still issue a valid voucher for U. So what happens is if E learns the IDU, the identity information of the device which is not secret uh from a legitimate U, it can construct a valid voucher info which contains that identity information and will be read by W and if that is in the authorization policies then W will generate a valid voucher which is sent back to E and then uh E can decrypt that voucher and so it can learn whether or not U is authorized. Even after and after E can just uh not continue with the with the protocol and give up uh or if it continues then uh V will realize that uh E does not have the right CredU transmitted in message 3 uh and then the protocol will fail but at that point E already learned uh something about. So that's the consequence, so that there's an information leak where E learns uh what U can do in the system. So as I said, in the more simple cases it is a binary authorized or not authorized information leak, in the most complicated case it uh U E can keep learning uh about what devices can do in the network.
Giosuè Fedrecheski: So the solution is actually a major protocol upgrade update, so where we moved uh the request we before it was happening to use the EAD fields from EDHOC message 1 and 2, we moved it to message 3 and 4. Because with that we give the chance to V to first check if the device the initiator it's actually if it it actually contains a valid credential before doing the authorization. And this actually aligns with doing first authentication and then after doing authorization. And before we're authorizing something before checking the real identity of the device. So that's the overview. And now I'll go into the details of several changes that are were done as a consequence of this change. So one of them is that uh because now we start the protocol in message 3 instead of starting it in message 1, uh so then we don't use an additional identity for U anymore because message 3 already carry carries ID_CRED_I, so we just rely on that ID_CRED_I and then we forward it to the uh V will forward ID_CRED_I to W on the voucher request. So that means that the voucher info which is carried in message 3 also does not carry IDU because that would be redundant. This has an implication that because normally ID_CRED_I is supposed to be understood only between U and V but in this particular case ID_CRED_I must also be understood by W, so we have a restriction on the namespace of ID_CRED_I such that it should be unambiguous also to W, which makes sense because this is a use case a very particular use case where W is also involved. Uh the second implication is that uh we modified the external AAD of generating the voucher because before we are we were binding it to the session using the hash of the handshake and the credential of V and now uh we don't have the the identity of U in the hash of the handshake anymore, so uh we actually decouple it, so we have the hash of message 2 and 1, ID_CRED_I and CredV to bind to the EDHOC session also to U and to V. And this also has the advantage of working the same structure works for both the forward flow and the reverse flow of the draft. Uh another implication is that in this new protocol approach, uh the two roundtime uh join with in conjunction with Constrained Join Protocol is no longer applicable because we don't have really a way to carry the last message uh together with message 4, so then we removed that appendix.
Giosuè Fedrecheski: Some other changes still part of this this PR of this update where is that uh now V can be more flexible on when it can ask for when it can decide to fetch or actually verify the credential of U. So we leave to V the decision of whether to process the EAD field 3 of LAKE-AUTHZ as a uh pre-verification EAD item or a post-verification EAD item, and this aligns with the implementation consideration drafts. So uh in case V wants to do a consider the EAD field as a post-verification EAD item, it can also rely try to rely on W to obtain a credential the CredU, credential of U, so then it can indicate to W using the field fetchCredU that it wants to obtain the credential of U. And W if it has this credential it will return uh on the on the voucher response. We have been questioned why uh W is not always sending it back and the reason is that the responsibility of fetching CredU is on V and W may help if it's available but it's not the responsibility of W, so that's why the returning of CredU is optional.
Giosuè Fedrecheski: And with this uh in this same PR we also made EAD4 optional, so this was discussed in a previous version of the document but then we we got a comment by Christian and so we make the whole EAD4 optional instead of only the voucher. So this also makes processing the protocol more clean. Uh this change also makes the protocol now compatible with LAKE-EDHOC application profiles, so that message 1 and message 2 are now free to be used to advertise ELA support, so that uh U and V can advertise that they implement this protocol, and this was a subject of discussion in previous versions, so now this is one clear solution and we added an example in appendix a.1.
Giosuè Fedrecheski: We also addressed the issue of support EDHOC with post-quantum security cipher suites, so we added an extra field uh called ephemeral_keys_ciphertext, so depending on the EDHOC uh key exchange algorithm that is selected on the cipher suite, then this field will mean a Diffie-Hellman public key or a KEM encapsulation key. Uh we had an an open issue of allowing for the keys of V and W to be the same, uh but this was the main use case was to perform a sort of encrypted client hello but since now we are moving to message 3 to start the protocol so that use case is not applicable so we close the issue. Finally, uh we have an open PR with a discussion uh about clarifying that fetchCredU is best effort, um in which cases if V fails to obtain the credential the session is aborted. And uh a recent PR developed during the hackathon here at this IETF 125 uh with the review by Marco, so thank you Marco, several clarifications uh on the use together with LAKE application profiles, not reusing uh the ephemeral key of EDHOC uh in the new version, and determining uh we also discussed that um it makes sense that V always use the same credential with U and W uh because there was a particular use case a situation if V uses more than one credential we want that the credential used with U is the same that is used with W. That simplifies uh when W needs to compute the the voucher which credential to use to do the binding with the identity of V. We updated the interoperability section where uh we defined that V must support both flows so that we can have a default interoperable case. Some adjustments on the REST error codes and some editorial fixes. So this was a very good review. And also synced with LAKE remote attestation to to rename and adjust the order of the fields so that we define uh the EDHOC session binding uh that is used in generating the voucher to use the same order of fields, so we have the hash of hash of message 1 and message 2. This is also good for the implementation because uh on message 1 we also we already save the the hash of message 1 after processing it because we need it after. And next steps, uh first of course is resolving the last uh open PRs but uh we believe that this the document is uh solved several of the points that were open and hopefully it's ready for open working group last call. Thank you Giosuè.
Mališa Vučinić: So Christian has a comment.
Christian Amsüss: Um yeah, thanks thanks for all that work. Um I think that um moving everything down from messages 1, 2 to messages 3, 4 is premature because I think that there are better mitigations for the leaked information of uh for the attack that you found. Um I'm working on on writing that all up we've already been discussing, so um I really appreciate that we could with the older version do COJP much better and that a lot of the a lot of the exchange can be done with really really small and short messages and I hope that we can preserve this uh without moving everything down uh down message.
Giosuè Fedrecheski: Okay. So I believe we can have a discussion internally about this but uh one of the questions is that uh when we did this this modification we also simplified a lot the protocol so we rely less on uh specific new cryptographic elements, so it's also uh in a way uh cryptographically safe to it's it's a more thin layer on top of EDHOC to what we can achieve.
Mališa Vučinić: Okay, so we have Zhang.
Speaker 1: So uh can you go back to the slides that you mentioned that in this version you has go back to use the I ID_CRED_I? I'm thinking that whether there's a problem of the privacy. So in your case do you need to consider the privacy or not, depends on the use cases.
Giosuè Fedrecheski: Yes, so in the previous version of the draft, we were protecting the identity of the device but that at the cost of doing authorization without checking the real without really authenticating the device. So that's the tradeoff we did.
Speaker 1: Yeah, so so depends, that's you can have a look at it to see that whether you need to have some some way to protect that the privacy or not.
Giosuè Fedrecheski: Correct. Okay.
Mališa Vučinić: Okay, thank you Giosuè. So uh what I hear is that Christian would like to discuss this a little bit further, so I propose that we have an offlist meeting uh between you guys and then that you come back to the working group with the conclusion of that meeting whether we can proceed as is merged now I understand or we uh we revert back to the to the old flow. Okay, so we are quite a bit over time.
Mališa Vučinić: So Marco, if you could trim off a little bit some minutes on your two presentations, that would be highly appreciated to give speakers at the end of the agenda opportunity to present.
Marco Tiloca: I'll try. Thanks. Hi everyone, this is an update on the implementation considerations draft.
Slide 07-Tiloca-Implementation Considerations for Ephemeral Diffie-Hellman Over COSE (EDHOC)
Marco Tiloca: Yeah, this has been always about providing consideration for implementers of EDHOC to not reinvent the wheel or rethink about old-fashioned problems. It's the same set of topics covered almost from the beginning of this document as a working group document. and other than than touching on these points, in general um two other documents have been considered as case in point beyond the basic EDHOC protocol, meaning the draft-ietf-lake-app-profiles in this working group uh and the ELA document that Giosuè has just presented.
Marco Tiloca: Uh so since uh two versions ago actually other than editorial improvements, most of the updates have been related to the work that was going on uh on ELA that Giosuè presented. That inspired first of all, some additional general contents of which ELA is a particular example. If one of the EDHOC peers learn a new credential on the fly and that credential is valid it might be that in some cases that credential has to be treated during the EDHOC session just as provisionally trusted because some confirmation of that has to come later in the execution of EDHOC, for example the voucher in ELA. So that was discussed in general terms as a concept in section 3 and then in the particular ELA-related section 3.3.2. And then in general again on the processing of an incoming message with particular reference to message 2 and 3 as those were the credentials uh come. so if anything is going to change again in the ELA document I think the general concept is still good to have and found out and worst case it's about well changing the ELA specific session to something else to reflect the latest version of the ELA document.
Marco Tiloca: And also related to ELA when it comes to its specific session, well here I just tried to uh write things in the spirit of this document aligned with the new regular flow that was updated in ELA while the reverse one um got unchanged as far as I understood. Thinking from the point of view of the considerations given in this document, if a peer learns on credential on the fly, well it really accepts it if the learning policy is just call learning so the very generous one if it's no learning is still fine if you have compelling exceptions enabling that and in the case of ELA the exceptions would be well for the initiator explicitly opting in to to run the ELA procedure with the expectation to request and obtain the voucher and for the reverse message flow, it's even more explicit the initiator who have been receiving the voucher.
Marco Tiloca: More updates somehow still related to ELA again were inspired by Christian in an open issue that was crossing this document and the ELA document where in its previous version in case the voucher was not issued there was the EAD item included but with no value. ELA changed that uh I'm happy to see that also well in that case the EAD item is not included altogether which is better actually and that triggered the talk about the implementation of an EDHOC peer as a peer receiving an incoming message is supposed to be absolutely able to detect the absence of an EAD item especially if it's an expected one that was kind of requested for like in ELA again expecting a requested voucher. So in this document taking again ELA as a case in point and a relevant example, there's also general discussion about this expectation on implementations. They they have to be able to track expected EAD items and to detect their absence, and if something really expected is absent, well that may be a reason depending on the procedure in question to terminate the session.
Marco Tiloca: Yeah, it's becoming more and more expected in the near future it will be formally expected I believe to include operational considerations in document according to an OPSAWG draft right now. I tried here, I believe this draft doesn't really have anything special to say from that side and if so, well you are still supposed to include the section with a well-known boilerplate just giving a reason why, and that's literally what you find in the very short section I added on this topic in the document. I believe at least that to be the case. So I believe everything I could think about was poured out here and I could benefit of somehow other people experience mostly Christian and Giosuè largely related to to ELA and also covering the other Ace document taking another angle. This is just again a summary of this update. I believe this should be ready for working group last call now.
Mališa Vučinić: Great news Marco, thank you. So let's write this draft in the queue for working group last calls to launch after this meeting. So I believe the first one is GREASE that we agreed on and the second one is this draft. And with that I guess we can proceed to the next presentation.
Marco Tiloca: Thank you. This is an update on the other draft on the app profiles. And to recap, this document started to provide a number of means or a toolbox if you want to help EDHOC peers coordinating about what they support in terms of EDHOC features and capabilities or so-called EDHOC application profile profiles. This can be expressed in two different flavors, à la carte just spelling out the features or as a compact menu, meaning the profile identified by an integer abbreviation. And there are different ways or venues where you can express this preferences or advertised supports. They have been quite stable for a while now. They are during the EDHOC session in itself or or out of it typically in advance.
Marco Tiloca: Yeah, since the previous version other than editorial touches there was a little qualification to give that was identified during the presentation in Vancouver in November. Peers have to be vigilant that if they learn about something prescriptive that they really has to happen during an EDHOC session and then there's a violation about that by the other peer, that evaluation does have to happen upon receiving a message but not only it has to continue throughout the execution of the session of course, otherwise the session has to be aborted. It was just about those four red words to add.
Marco Tiloca: Yeah, I revised the CDDL grammar, there there was a mistake in one grammar now fixed. I defined the CDDL grammar for two of the parameters defined in this document in the same namespace otherwise mainly defined in the Ace document creating the overall data structure and registry. After submission I just noticed a typo in the bottom right grammar there, it's correct in the slide, it's wrong in the draft I'll fix that in the next revision. It should really say exporter-out-length like in the slide.
Marco Tiloca: Yeah, I also consider issues from Christian especially number one. Thank you, it was basically an invitation to revisit the set of parameters that were floating around as if really necessary or instead possible to remove. Yes, four were definitely possible to remove considering the experience we now have more about EDHOC compared to the time of its standardization. The actual removal of the parameter definition happened in the document where they went defined, the Ace document. In this document of course we removed their use or or discussion and we also removed the definition of the corresponding link target attributes that could be used when using web link as an advertisement means. That also resulted in the removal of some corresponding new IANA registries that we were defining.
Marco Tiloca: Um about this, it refers to the new EAD item that we are defining in order to to advertise the peer's capabilities during the execution of EDHOC itself. This slide refers specifically to the use of the EAD item in message 1 where the initiator can optionally include one boolean flag at the beginning of the EAD item value. I renamed that from reply-flag to advertise-flag cause this new name fits better for the new possible use that comes in the next slide. But this slide focuses on the original use in the EAD item, the semantics is still the same if included the flag can be true or false. True is an invitation to the responder to talk about itself in the following EDHOC message. False means don't bother telling me. I clarify how it is possible to still use that for the initiator in case the initiator does want to ask the responder to talk about itself but the initiator also doesn't have anything to say about itself in message 1. That is still indeed possible by setting the flag followed by essentially no information about itself. I think it was worth spelling this out.
Marco Tiloca: But on the new use I anticipated, that was also suggested by Christian in another issue. Thanks thanks again. This same data point would also be useful when advertising the EDHOC capabilities of a server in SVCB record, resource records returned when doing DNS resolution for that server. I had to re-engineer a bit the the semantic of the wire format of the SVC key related to this information about the server. The final effect is basically that the information that could be provided before now can also be optionally prepended by that boolean flag, if present has as only possible value true and the server is indirectly saying to whatever other peer finds it through DNS discovery that well, the other peer that has found the server is very encouraged to tell about itself to this server when running EDHOC just for the sake of disclosing its EDHOC supports.
Marco Tiloca: Yeah, I added a lot of examples that I promised in Vancouver. One is about the use of core-link format with a particular use of some target attributes related to the supported trust anchors that was missing and I think worth doing. All other examples are in CBOR diagnostic notation when using essentially the different means of advertisement, so the EAD item in message 1 or 2, the EDHOC error message with the new error code, and the wire format for the two new introduced SVC parameter keys when using the SVCB resource records.
Marco Tiloca: Yeah, I also visited finally the security considerations other than obvious inherited ones. I tried to emphasize that some approaches for this advertisement are unavoidably non-protected, for example when relying on EAD1 in EDHOC message 1, on discovery from well-known core that is not protected. If you acquire this information through an unprotected channel you really need to bear that in mind and treat them as a hint. Worst case an adversary may induce you to have wrong expectations of the other peer's capabilities, but this shouldn't really have any impact of the security of the EDHOC protocol in itself that eventually is performed according to to what the two peers really agree to do in the first two messages, for example out of the cipher suite negotiation.
Marco Tiloca: And like mentioned in the previous presentations, since this is a raising expectations, I also added a section on operational considerations, here there was quite something to say actually. I think that fundamentally what this draft proposes is also in the interest of operational considerations to have the network run in in a smoother way since it facilitates EDHOC peers to agree on how to run EDHOC and to discover each other's capabilities. And as long as this advertisement happens in some non-protected ways and there are a few like I mentioned before, operators may even take advantage of that and understand most preferred ways or most supported ways to run EDHOC and in turn build on that information to do some fine-tuning of the network setups or to learn what are the most popular, favored, whatever EDHOC application profiles that maybe deserve more attention in terms of maintenance and implementation. And on the other end, on the peer side, I'm trying to encourage peers to remember what they have learned about other peers just to not rediscover the same things over and over with possible additional network traffic that can be avoided. And if an EDHOC session fails in spite advertised capabilities of other peers were followed by the book, well that should be reported and it's possibly the starting point to detect anomalies and misbehaviors and peers to to remove from the network.
Marco Tiloca: Yeah, I also think this draft is complete from an author team point of view in terms of content, there's no open issues or points as far as I know and content-wise it should also be ready for working group last call. I just wanted to point out it has two drafts as normative references, one should be fine because it's in IESG evaluation now, the C509 certificate. The other one is the EDHOC-ACE application profile in ACE, the working group is still working on it. So even though again I believe this should be ready in itself for working group last call, maybe time-wise that dependency can be factored in to have the working group last call later. But I leave that consideration to chairs and AD. Thank you.
Mališa Vučinić: Thanks Marco. So I would suggest we proceed with the working group last call and then the second draft can wait on we can wait in the IESG queue like once the other draft aligns with us essentially.
Marco Tiloca: Fantastic. Thank you.
Mališa Vučinić: Yeah, so the action item same as for the previous draft, add this draft to the queue of working group last call items to launch after this meeting. Thanks Marco, and thank you for being concise.
Mališa Vučinić: So we have 18 minutes to go in the meeting and I believe we have four three presentations and one time permitting, so if everyone could shim off like couple of minutes of their allocated time that would be highly appreciated.
Lydia Pocero: Well, I am Lydia Pocero from the Industrial Systems Institute and I will present the last updates in our drafts regarding KEM-based authentication.
Slide 09-10-Pocero-Updates on KEM-based Authentication methods for EDHOC
MališaVučinić: Let me just interrupt you for a second, I forgot to introduce that we are now skipping to the individual drafts. So Marco's presentation concluded the adopted drafts of the working group and we are now passing to the individual drafts and these mostly consider quantum-resistant EDHOC methods.
Lydia Pocero: Well, let me just summarize the current post-quantum support in EDHOC, I mean that from the EDHOC RFC, they already introduced that the use of ephemeral KEMs will be make it with the method 0 and also is there the draft-spm for the cipher suite quantum-resistant that in a way complete the post-quantum signature-based EDHOC and also the pre-shared key method using corresponding quantum-resistant ephemeral KEM will also be quantum-resistant. Then, let's say, both approach have some limitation because the pre-shared key-based approach requires this pre-shared knowledge and on the other way the post-quantum-based signature-based EDHOC introduced significant overhead when we are speaking about NIST standardized signature schemes that have longer key size, high processing time, and high memory overhead, and that bring us to the motivation of our draft that is to complete this post-quantum EDHOC portfolio with the KEM-based authentication method that provide signature-free authentication for one or both parties. We first address the post-quantum equivalent of method 3 where both parties use static KEM keypairs for authentication, and starting from the version 1 of the draft, we extend this work to also support post-quantum versions of EDHOC method 1 and 2 by allowing hybrid authentication combinations.
Lydia Pocero: Well, in the method 4 we have this in which both parties have the signature-free authentication, an ephemeral KEM is used for the key exchange and a KEM mechanism authentication for both the initiator and the responder are used. Unlike of the DH authentication requires now receiving an encapsulation of its static key first, which add a key confirmation step resulting in this five-message handshake. The method 5 provides signature-free authentication for the initiator, then the initiator use KEM and MAC and the responder use a signature to authenticate itself, and just make the reference that in a different approach in which we would like to authenticate early, instead of put the signature in message 4, we could bring the signature to message 2, that as just the method 2 of EDHOC make it, but in a way we will stop to have the same scheme for all the KEM-based EDHOC. When we speak about the method 6 is now the responder who is only signature-free, and now the message 4 is half a MAC and message 5 have the signature. Again, this signature could come to message 3 that we will reduce the message size because we don't need the message 5 anymore, but again the methods between them will not keep the same structure for KEM-based. And this is the key schedule that we have already speak about, we don't have time, let's go directly to what changes come in the last version. The first one is just we identified was an issue with the order in which we computed the transcription hash of PRK, and we solved it. We then add a transport consideration section because the post-quantum KEMs and signature produce much larger message. EDHOC message may exceed the MTU limits in constrained network and in this case fragmentation at the transport layer may be required, and we refer mechanisms such as CoAP block-wise transfer that can come as possible solutions. Notice that with these larger messages and fragmentation require acknowledgement, the key goal in the design should focus on reducing the overall handshake size rather than the number of messages.
Lydia Pocero: There has been some questions regarding responder identity protection against active attacks, because it's important to try to have the same property security property that the original EDHOC, let me tell one more that the initiator credentials are encrypted in message 3 using AEAD with a key derived from the ephemeral shared secret and the responder static shared secret. Then only the legitimate responder who owns the corresponding private key can derive the key, decrypt the message, and retrieve the initiator credential. Then to also prevent the initiator from revealing its identity to untrusted responders and to stay aligned with the original EDHOC, we add a requirement that the responder credential must be authenticated and validated by the application before the initiator sends its own credentials. And the last change, wait, sorry, I passed two times, yes. The last update we also add a new section that is the KEM security consideration section because prior research showed that IND-CCA2 security alone is not always sufficient for KEM-based key exchange protocols because they may still be vulnerable to re-encapsulation attacks, which can lead to unknown-key-share situation where two parties derive the same secret but associated with different identities. For this, we clarified that the KEM used in this protocol must be IND-CCA2 secure and ensure that the derived shared secret is cryptographically bound to the recipient's public key. These two things are guaranteed for schemes such as ML-KEM.
Lydia Pocero: We also are collaborating with Vishnavi from IIT Delhi to try to formal verify the protocol, since we have used firstly the Tamarin tool and we are focusing the method 4, and since the KEM encapsulation output both ciphertext and shared secret, we introduced two functions, KEM_ENC and KEM_ENC_SS to adopt it. We also defined the KEM_PK to derive the public key from a secret key and add some necessary equations in Tamarin. But just because we don't have time, just to fast tell you what we have achieved until now, that is work in progress, we have not finished, but first we have proved the secrecy of the final session key, meaning that once the protocol completes only the initiator and the responder know this key. Second, we have injective agreement for the initiator, which ensures that if the initiator finished session believing it's in communication with a specific responder, then that responder must have participated in exactly one matching session with him, and also the injective agreement for the responder. And we managed also to verify other properties, secrecy of intermediate key materials and perfect forward secrecy. And our next step is to work in this formal verify this of the identity protection of credentials that we have to move for this to the Proverif tool, and we expect to have this finished before the next meeting. Just for the last for the second draft, just I wanted to to tell little things that the goal of this is to reduce the handshake to three message, targeting scenarios where the initiator already knows the responder credential. And one of the main updates in this version 2 is we highlighted the derivation principle of this protocol, which follows the NOISE framework. In this design, each new shared secret is immediately incorporated into the key schedule, improving the protection of subsequent messages. For this reason, the key schedule is adapted to incorporate all shared secrets that are already available after message 1 for the responder and after message 2 for the initiator, and in this way we prioritize maintaining the design principle of the framework rather than keeping the key schedule identical to the original EDHOC. There are the summary of the last change that we make and because we don't have a lot of time, yes, thank you a lot.
Mališa Vučinić: Thank you Lydia. So we have Dekra in the queue.
Dekra Mahmoud: Yeah, thank you for the presentation. So you said that you worked with Tamarin, right, and for the formal analysis and as far as I know the standard way to model KEM in Tamarin is that you use just asymmetric encryption. Did you use asymmetric encryption to model the KEM or is it another one?
Lydia Pocero: Well, to this question maybe will be better to speak directly with Vishnavi that today couldn't be here, but what the model that we used was similar to the model that used KEM-TLS done with her in one of their papers. They have their model open in GitHub and we used the same approach. But for more details again, be free to mail Vishnavi that is more expert in this, but today couldn't join us to explain it better.
Dekra Mahmoud: Yeah, okay. So just one simple remark regarding that because the standard way is just to use asymmetric encryption so the message is the shared secret in the KEM, so that the shared secret won't be I mean bound to the static key. So that's my only concern regarding that, so maybe you can use a library in Tamarin which is I mean more sophisticated into bindings the static keys, etc. And also just a small remark so the binding properties that in the KEM do not just specific are not just specific to the static keys so that we have many bindings properties, for example for the ciphertext, etc. So maybe you should investigate this further. Thank you.
Lydia Pocero: Okay. For sure, for sure. Thank you very much.
Mališa Vučinić: Okay. Thank you, so we lock the queue here. Thank you Lydia for presenting and we have one more presentation on the 00 version of a new draft that was submitted by Clément. Clément, can you? So you have a little let's say you have five minutes because we would like to conclude the meeting at the end. Thank you.
Clément Papu: Do you hear me well?
Mališa Vučinić: Yes, we hear you Clément.
Clément Papu: Okay. Hello, so I'm Clément Papu, PhD student at XLIM in Limoges in France. I'm working on cryptography. So today I would like to present you some proposal for post-quantum secure extension for EDHOC. So there's five protocol proposal I will just review two of them today. So the first one is a variant of what Lydia proposed, when the initiator already knows the responder, I will try to propose a flexible way where the initiator can authenticate using a post-quantum signature. So here it goes. So in green we retrieve the ephemeral KEM as already explained and the initiator already is knowing the responder identity can send send the ciphertext of the responder in the first message but we do no more have here an encryption and it authenticates itself with a MAC in the second message, and in this case the responder sorry the initiator can authenticate with in the EDHOC classical way with a signature in the third message and so here we only have three mandatory message. That's a first proposal to make it more suitable with the traditional EDHOC protocol. A second proposal in a more classical case is when the responder already knows. So we return to a more classical case and this time we suggest authentication for the responder with a KEM and a signature. So in fact here in the second message highlighted in orange the responders provide a signature of a message that the initiator can retrieve locally on its side and so at the end of when we receive the second message he can already authenticate the responder and send him in the third message the associated ciphertext and also in red its authentication. So in this case we do no more have a fourth mandatory message, we only have three mandatory message and the the only fact here is that we have one more signature in the second message but we do no more we do no more need to compute a MAC on each side, so it only heavier a little bit the second message with this signature but it lightens not the computational part on each side. So we have variant, in fact the four the three other protocol that we propose in the draft are some variant of that one protocol, I mean by using signature and KEM combined at the same time. So I will not describe all of them that was an example, maybe going on a security consideration. So at the end of each handshake of course we have both endpoint are assured that they have securely compute the same session key and they are securely authenticate. The the combination of a KEM and a signature also simplify the authentication delay and increase the session key security in case where, for example, a participant becomes compromised in a post post-compromise security situation for example. As for the traditional EDHOC we have forward secrecy, downgrade protection and transcript hash binding. One point I would be I would suggest it's about the identity protection property, something that I read on the Coti and Poncheval analysis about the security property modeled. It's that it would not always fit correctly or be able to adapt to this new post-quantum version of EDHOC and also in the draft that were presently previous by Lydia. So maybe we can suggest a more global approach based on PPK. And just for a comparison quickly about the byte analysis, I just added that, it's not in the draft but it's to have it in mind that based on what was done of EDHOC, I will take the same structure, we have this global comparison of the proposal we done on the byte of each messages. So the size of each messages is really increased only by the post-quantum cipher suites consider not the message structure themselves.
Clément Papu: Thank you.
Mališa Vučinić: Thank you Clément, maybe very quick question from John. We are already at the end of the meeting.
John Mattsson: Yeah, it's a high level question on both of these last drafts. Now we have a new recharter, how do we progress with the PQC work? I think Lydia gave a quite nice overview of the different options. I think the ephemeral key exchange is quite straightforward for when you have signature and PSK authentication. What needs more work seems to be the KEM authentication, there's many solutions and many design options. How do we progress with that? Could we have some design team or some interim meeting offline since it seems we should progress what we want to do?
Mališa Vučinić: Yes, yeah, so that's a good point. So we have a new charter which allows us to work on quantum-resistant EDHOC methods. So I would propose an interim meeting before Vienna that is specifically dedicated to quantum-resistant EDHOC that we can use as an opportunity to discuss exactly how do we proceed on this issue because we are on top of the hour and we are out of time today. But what I do see is that as you were saying John, key exchange seems to be straightforward, we have an individual draft on that, so it would make sense to to progress this fast and then we need to decide what exactly gets standardized in terms of KEM-based authentication for for EDHOC. So I propose that we schedule a meeting before Vienna, sometime in May and we discuss these these issues further there. Do we have any any other opinions on this subject? The queue is locked, so I will unlock it in case somebody wants to comment. So I hear no opinions, so I would take that as that as if we agree on the proposed way forward with the interim meeting. In parallel to that I would propose to form a design team meeting of on quantum-resistant EDHOC and perhaps we can start with that immediately and have the the presentations of the design team in the interim meeting in May, such that we use the time wisely between now and May between now and the interim meeting in order to progress through these issues and form consensus in the working group on what exactly it needs to be standardized. Does that work for everyone?
Clément Papu: Yes, for me.
Mališa Vučinić: Okay, so we are three minutes late. So we had one more agenda item that is Meiling's draft but I don't see her in the room and we are late anyway, so we can perhaps take this presentation either for Vienna or for for the interim depending on on the interest of the audience. We will as chairs we will consult on that and we'll come back to the working group. So I would like to thank everyone for attending the today's meeting and for the productive discussions. So there are several action items, I believe they are captured in the minutes and we will be publishing these minutes and the recording will be published on the list following the meeting. Thank you all. Final note, I would just like to to thank Paul for serving as the AD in in his two terms and to welcome to welcome Christopher. Paul thank you very much and Christian welcome.
Paul Wouters: Thank you very much.
Christian Amsüss: Thanks for having me.