Session Date/Time: 26 May 2026 16:00
Mališa Vučinić: Hello everyone, this is the LAKE interim meeting. As any IETF meeting, by participating in this meeting, you agree to follow certain IETF processes and policies captured in the Note Well, and you are requested to be familiar with the Note Well. Please note that the meeting is being recorded, and the presence is logged. And for any advice regarding Note Well, please talk to Working Group chairs or our Area Director.
So I hear we noted a small typo left over from the Shenzhen meeting in the title, but the links otherwise should be good. We give a couple of links towards the agenda, the MeetEcho, and the minutes. So we already have two note-takers, Marco and Juwan, which we greatly acknowledge. And anyone who is willing to help with note-taking in addition to Marco and Juwan is very welcome too as well.
So I will start off with the status slide on the current status of the Working Group. So since the Shenzhen meeting and the action items that we as chairs have took during that meeting, we have issued three Working Group Last Calls. First Working Group Last Call on ad-hoc-grease document was issued on 30 March 2026. After some pings, we received enough feedback to be able to continue with this document, and we are we are now waiting for Christian to incorporate the feedback and present the resolutions of these issues to the Working Group. And Christian has notified us that he will be able to do so during the Vienna meeting.
Similarly, for implementation considerations and the application profiles, the documents that are led by Marco, we have launched the Working Group Last Call on 4th of May and 19th of May respectively. And we are currently pending the Working Group Last Call on the PSK document, which is conditioned on the green light from the authors, as it was discussed in Shenzhen. So all of these documents are to be discussed in Vienna. In the meantime, we have worked on forming the Post-Quantum ad-hoc Design Team. We will be hearing more about it in this meeting, as well as we will have updates on remote attestation and the draft-ietf-lake-authz in the first half of today's meeting.
So the agenda, we give priority to the Working Group items, but it's quite packed anyways. So we will start with the remote attestation items, Yuxuan, and then wrapping up the call for formal analysis that happened since the Shenzhen meeting. We will proceed with draft-ietf-lake-authz led by Geovane, and then we will pass on to non-Working Group items. Meiling will give us an update on her individual submission, and then we will go to the Post-Quantum Design Team and its main findings. At the end, Lidia requested a presentation of her draft, lake-authkem-edhoc, which we will devote the last 10 minutes of today's meeting for discussion. So this is the agenda. Does anyone want to bash this agenda?
I hear no objections to this agenda, so I propose we kick off the meeting. The first item on the agenda is draft-ietf-lake-ra, draft on remote attestation over ad-hoc, led by Yuxuan Song. So, Yuxuan, I will pass you the control over the slides.
Yuxuan Song: Uh, not yet.
Mališa Vučinić: I will pass you the control over the slides.
Yuxuan Song: Uh, yeah, now I think it's good.
Mališa Vučinić: Okay, so Yuxuan, you have, I forgot the time.
Renzo Navas: Five total. So if you want questions, four. Yeah.
Mališa Vučinić: Yeah, five minutes.
Yuxuan Song: Okay, so hi, I'm Yuxuan, and this is for the updates of the draft, Remote Attestation over EDHOC.
Um, so basically, we solved some issues, and one of the biggest issues is to complete the four examples in Section 6. So Section 6 is the instantiation of Remote Attestation Protocol. And before, we had only two examples: one is the initiator as attester in the background check model, and the second one is the responder as attester in the passport model. So in the latest version, firstly we deleted the third dimension, the forward or reverse message flow, because the draft actually does not require necessarily to run ad-hoc in CoAP. So what we try to say is just like, if that is the case, then we support both forward and reverse message flow. So now in Section 6, we have listed all the possible four examples. And the 6.1 and 6.2 are the previous examples, and then we have two new subsections.
So, the Section 6.3 is the case when responder as attester in the background check model. So just be aware of the difference between the 6.1, when the initiator is the attester in the background check model. Um, so this example in Section 6.3 is post-handshake attestation, while the example in 6.1 is the intra-handshake attestation. So here the evidence is sent in message 4, when the ad-hoc handshake is finished. And then in Section 6.4, we have the case when the initiator is the attester and perform attestation in the passport model. Um, so more details can be found in the draft, and I will not, I'll just go to the next slide.
Um, okay, so the next issue is to combine Appendix A with Figure 1, because we think the Appendix A is quite redundant and only Figure 1 is actually clear enough to illustrate the contents sent between the ad-hoc session and also the materials sent to and from the verifier.
And then the next one is to, is that we improved the attestation binder. So in the last version, the binder was defined based on the formal analysis result by Elsa, and in the latest version we also improved the attestation binder with a more, with a better structure, and also we gave different names. So, attestation binder M3 is to use when evidence is sent in message 3, and it is derived by the key derivation function and also contains the attestation-related information and also the hash of the first two messages. And then we also have another binder named attestation binder M4, which is used to, when the evidence is sent in message 4, and this is derived by the ad-hoc exporter.
Uh, we also have another new subsection, reuse of ad-hoc, so this is just to collect all the reused ad-hoc variables like EAD, the ID-CRED-I, and so on.
Uh, and then at last, many thanks to Marco, who helped do the sanity check on the draft. We have also addressed all of his comments. So I think now the draft is much more clear than before. So I think that's all. Yeah, thank you.
Mališa Vučinić: Thank you Yuxuan, do we have any comments on this draft? On the status update?
I hear no comments. I guess we will have time for discussion during the next items. So as a reminder, in Shenzhen we agreed to launch the call for formal analysis on this draft, and Elsa will be presenting the findings of the symbolic verification of this draft in the next slot.
Elsa, do you want to share slides?
Elsa Lopez-Perez: Yeah, great.
Mališa Vučinić: So, on the agenda...
Renzo Navas: Elsa, you should have control.
Elsa Lopez-Perez: Yeah.
Renzo Navas: You have 15 minutes, okay.
Elsa Lopez-Perez: Okay. Okay. Um, so hello everyone. Uh, my name is Elsa, and I will be presenting the results of the formal analysis of the remote attestation draft, the latest version, so 05, using Sapic+.
So the outline of the presentation: I will do a little recap of the findings on IETF 119, what were the results and what were the proposed mitigations, attacks, etc. Um, then Yuxuan already mentioned what was the update from draft 03 to draft 05, so what has changed since we did our first formal analysis. I will then present the different models of remote attestation over ad-hoc and what exactly are we studying in this formal analysis. This includes the background check model, the passport model, and the mutual attestation model, which is a combination of both previous ones. Um, then I will define what are the claimed security properties, which we organize in remote attestation properties, ad-hoc properties, and the combined properties. I will then give some information about what is the symbolic analysis and the verification framework that we use, which in this case is Sapic+. And I will finish by presenting the results of the formal analysis.
So in IETF 119, we presented the formal analysis of draft version 03. The formal analysis was conducted on all four authentication methods, so this includes the three asymmetric authentication methods of RFC 9528 and the PSK authentication method. And what we found was that the channel binding property did not hold in any of the authentication methods. In fact, we found an attack because of the lack of cryptographic binding between the attestation evidence and the authentication session. So, we proposed a mitigation as a result of the formal analysis, which was to include the hash of the first two messages in the digitally signed attestation evidence. The reason behind is that this hash contains information which is linked to the authentication session, and that is session-unique, such as, for example, the ephemeral shared secret.
The authors of the draft updated the draft to the latest version, and as Yuxuan presented shortly, the solution depends on whether the evidence is sent in message 3 or message 4. So whenever the evidence is sent in EAD3, in message 3, then the attestation binder is defined by using the HKDF expand function, and the attestation info includes the hash of messages 1 and 2, which is following the line of the proposal after the IETF meeting. However, when the evidence is sent in message 4, so in EAD4, then the attestation binder is defined as the ad-hoc exporter, since this already contains information that is session-unique because it depends, it's derived from the PRK_out that is derived at the end of the handshake.
So regarding the models that we studied, previously we included the background check and the passport, which were, we provided the results and they were published in the following paper that is cited, in IEEE Transactions on Computers. And we also included the mutual attestation, which was a combination of both. However, we didn't include the other two models, which are RBG and IPP, so the responder in background check model and the initiator in passport model, plus the mutual attestation that results as a combination of those two. So in this case, we added all of these models, and we extended them with the attestation binders that were included.
So, a little recap on what has changed from the previous analysis. In the background check model, so the IBG, which corresponds to the intra-handshake attestation, we have the initiator acting as the attester, and it's also the constrained device. And note that here we update the EAD3 to contain the attestation binder that we defined before, which includes the hash of the messages 1 and 2.
Then we have the RBG, which is the responder in background check model, and it's the responder the one that's being, it's the one that is the attester, and also the constrained device. And here, because we need the four messages, we are sending the evidence in EAD4, and therefore we use the attestation binder M4. And this is an example of a post-handshake attestation, as Yuxuan mentioned before.
And then we have the passport model, so we have both the IPP, in which the initiator is the attester, and the responder, which is the relying party, is the constrained device. In this case, we only need three messages. And then we have the RPP, in which we have the responder as attester, initiator as relying party, and we need the four messages. Note that here, there were no changes included, because in fact, the evidence is generated by a third party, so in this case, the verifier, and the ad-hoc session only carries the attestation result. Therefore, we do not need to bind the evidence, which is generated by a different party, to the ad-hoc session.
And then we have the mutual attestation, in which both the ad-hoc initiator and ad-hoc responder undergo attestation. So this can be done by either merging the IBG and RPP, or the IPP and RBG.
So, as for the claimed properties, following the same approach as before, we divide them in remote attestation properties, ad-hoc properties, and the combination of attestation and authentication. As for remote attestation, we have freshness and integrity. So for the evidence freshness and attestation result freshness, this property ensures that these values reflect the current state of the attester, and therefore we prevent replay or outdated values. And this is achieved by means of a nonce, which is freshly generated, and it's also unique for each session. And then we have the integrity of the evidence and the attestation result, and this allows us to show that the evidence or the attestation result has not been altered in an unauthorized manner since it was created and transmitted. And this we achieve by using a signature.
Then we have the ad-hoc properties, and here we define mutual authentication. So we are ensuring that both parties verify each other's identity, therefore preventing impersonation and man-in-the-middle attacks.
And finally, we have the combined properties. So here we're focusing on channel binding and agreement of parameters. Channel binding is the property that was falsified in the previous formal analysis, and it basically ensures that the attestation is cryptographically bound to authentication, so that the same party that authenticates is the party that is generating the attestation. And then we have agreement of parameters, which can be seen as a combination of mutual authentication and attestation, and it ensures that the responder's view of both attestation and authentication matches the initiator's view of attestation and authentication as well.
A few notes on the symbolic analysis. We did again a symbolic analysis, therefore we're using the DY attacker model, in which the attacker has full control of the communication. This means that it can intercept and eavesdrop messages, modify them, replay, interact with honest parties, and even act as one of the peers. An important assumption is the perfect cryptography assumption, in which cryptographic primitives are not breakable, and this means that security failures arise from protocol design and not from breaking cryptographic elements. And then we can define the security properties as either reachability or equivalence properties.
So the framework that we are using, we extended the model that we had before, using Sapic+. Sapic+ is a framework, a platform, that allows us to use different verifiers. So for instance, we are using ProVerif and Tamarin. This comes with the advantage that we can exploit the strengths of the different tools. And the particularity of Sapic+ is that we are defining the protocols using the applied pi-calculus, which is the syntax of ProVerif, and the properties defined using first-order logic, which is that of Tamarin. And then we are defining an advanced threat model in which we are giving the attacker more capabilities of the DY model. So for instance, we define the compromise of long-term keys, this can be the static Diffie-Hellman keys or the pre-shared key. We also define a leakage of ephemeral keys, a leakage of the session key, and finally a leakage of the attestation key.
So here are the results. We basically verified that now the channel binding property holds. Note that here, we are showing the minimal compromise scenarios, which means that these properties hold unless the attacker is given these capabilities. So in the case of the channel binding that was before falsified, now it holds unless the attacker has knowledge of the attestation key and therefore can generate its own evidence. And the rest of the properties remain unchanged with respect to the results that we had and that we present in the IETF in Shenzhen. And this is it. Thank you. So if there are any questions.
Muhammad Usama Sardar: Yes.
Mališa Vučinić: Thank you Elsa. If there is any question, please join the queue. Yes.
Muhammad Usama Sardar: Yeah, thank you, thank you chairs. I would like to actually refer back to the results that we have listed many times on the list, and in specifically we talked about attested TLS, we mentioned two solutions: intra-handshake and post-handshake. And these were, like, using these exporters, designed exporters, channel binders, like, I've put the link in the chat as well, there are several list discussions on that. So coming to my question, specifically in short, my question is: what did you learn from all of that compared to attested TLS? Where does your result differ from our results? Can you, can you briefly comment on that point?
Elsa Lopez-Perez: Yeah, so I think that the main difference is that we are talking about different protocols. Um, so, yeah, like, here we are doing a formal analysis on ad-hoc, which is not TLS. Um, yeah, so I think that even if there's an attack that might, that might happen in both protocols, we're still talking about different protocols. Uh, so I think that we need separate models for that, and yeah.
Mališa Vučinić: Okay, so Göran?
Göran Selander: Yes, Göran. Thanks for the presentation. So, a question for you here: this presentation, as far as I understand, it basically shows the security properties of ad-hoc with remote attestation in these different models. Um, so the interesting question from the point of view of LAKE is that these security property holds, and not whether this is new or not. So, I have, in my point of view, it doesn't matter if there is something proven before on this. This is not academic discussion, this is about whether the security properties of these protocols holds. And as far as I understand, there is no contention about this, as far as I hear. So that's good.
And I also repeat that ad-hoc is not identical to TLS, and I think the burden of proof to state that TLS is identical to ad-hoc on this point is on the person that makes the claim. It's not, it's not your problem, I think. So that's, that's also clear.
And in particular, I want to emphasize that there are different methods, ad-hoc is using different methods which does not exist in TLS, and it seems that you have taken into account all three, all four asymmetric and also the symmetric method. And some of these method doesn't exist in TLS. I think this is, is very good that you have covered all that and this is very, very good results. Thank you.
Elsa Lopez-Perez: Thank you.
Mališa Vučinić: Thank you. I will take over the chairing. Thank you Elsa, thank you for the questions and answers. We will move on to the next item is Vaishnavi. Vaishnavi, I will give you the slides. But before I give you the slide, a small intro from my side. I mean, some context to the audience. We launch the formal call for analysis of remote attestation on the list. Initially, Elsa and Usama respond, and they were working on that. Elsa just present. And then Vaishnavi asked, "What can I do?" And we asked you personally to look about both works and to give us, like, a trusted third party, so Vaishnavi will introduce your results. I will give you control. Please, if you can stay in four minutes so we have at least one minute for question. Floor is yours.
Vaishnavi Sundararajan: Um, yeah, hi everyone, my name is Vaishnavi Sundararajan, and I was asked to be an expert evaluator for the two different formal verification efforts that were happening in parallel for Remote Attestation over EDHOC. So, yeah. Just a quick introduction about me. Okay, there's a lag. Okay, there we go. So, um, I did a PhD in the formal verification of security protocols, I got my degree in 2018. Then, I did a postdoc at Inria in the CNRS lab where I was working on identifying a class of security protocols for which reachability and equivalence properties are decidable. In general, these properties are undecidable, and we would like some nicely behaved protocols for which they are decidable without extra restrictions, which is what we were working on there. From 2019 to 2020, I was at Ericsson Research. I worked on helping with the formal verification effort for the original EDHOC protocol along with Karl Norrman and Alessandro Bruni, who is at TU Denmark. And we wrote a couple of papers out of that. I believe the draft that we were verifying was version 5, but I could be wrong. Um, and after that, I did a postdoc at the University of California, Santa Cruz, where I was working on protocols involving authentication and authorization. And from 2023 onwards, I've been assistant professor at IIT Delhi. And I've been part of the IETF mostly involved in other formal verification efforts involving EDHOC. Most recently, this has been the EDHOC PSK work, along with Elsa and a lot of other people. And EDHOC-AKA, which is work with Lidia. So that's about me.
And this is a high-level overview of what the FV efforts were like. There was one strand of work that was happening, which was being headed by Yuxuan and Elsa. That basically built on top of the model that was used for analyzing the original EDHOC protocol, which came out in 2023. And there also the code was written in the Sapic+ platform, so they've basically been extending that model. And their work is available at the GitHub link that's in the slide. There is another effort by Usama and some other people. Apparently, this is for version 3 of the EDHOC-RA protocol. It is in ProVerif, I'm told. Unfortunately, the code is not open access. So we did not get to actually look at the code or check what it does or get a sense of the kind of properties it verifies or, you know, the kind of model that it utilizes. It is a symbolic effort, and Usama tells us that they basically add more properties on top of attested TLS and apply code transformations to convert attested TLS to EDHOC. And that they believe that neither the key schedule nor the EAD field makes any difference at the symbolic level. So this is what Usama told the chairs and me when we sent an email asking to review this, this code. And he tells us that the code is not open access because there is a paper under publication and the code is part of that, and therefore they cannot open access to the code just yet. So the only code that I managed to review was the one by Elsa and Yuxuan.
Right. So the highlights, I think, are going to be a summary of the two presentations that you've already heard. Essentially, the first effort dealt with version 3, but newer branches have been added to bring it up to date with version 5. So they do have formal verification efforts for all four combinations of the initiator-responder and the passport and the background check models, and they also have mutual attestation models for each participant playing the background check model and the passport model and combinations. They apparently found an attack on the V03 version, which was fixed by including this binder. The binder has been changed between V04 and V05, so the newer code involves the new definition of the binder that you heard earlier, regarding HKDF extract, etc. There is a short, a small departure from the standard, which is that they include an extra test to see if the credentials of the initiator and the responder are the same. From what I can tell, this will avoid unrealistic attacks being found by the tool where the same person is talking to themselves and asking for an attestation, which is just not going to happen in the, in the real world.
So there are this list of properties that's been verified. We've heard a lot about these in any case. So I'm just going to quickly go through them. So you have the freshness of the evidence, the freshness of the result, the integrity of the evidence, the integrity of the result. You also have the mutual authentication, so we are ensuring that both parties verify each other's identity, therefore preventing impersonation and man-in-the-middle attacks. And finally, you have the combined properties. So here we're focusing on channel binding, which is the property that was falsified in the previous formal analysis and then fixed in the later one, and agreement on parameters.
And that's basically it. I'm open for questions, thank you.
Mališa Vučinić: Thank you. We can have, yeah, one-minute questions. Please, yes. Usama.
Muhammad Usama Sardar: Yeah, thank you, and thank you chairs. I just want to, kind of highlight here that we couldn't manage to work further on the version 3 model that we had. I want to confirm that we had the version 3 where we had the attack, and then we couldn't manage to get over the version 5, although we, kind of agreed that we will try to do our best but there were like post-quantum and other important things, and also our paper was in submission. But the important thing here I want to highlight here is that we fully disagree with the property that they have for the channel binding. The follow-up attacks that we have found, and that's my, that was why I was asking Elsa that what is new that they have found. Because if they accept our attack from attested TLS applies to attested EDHOC, they should also accept that the attack that we have from the follow-up work that should also apply here. So that's my only comment that we, we disagree with the proposition that this work is done. So it is, it is still vulnerable, the intra-handshake one. Thanks.
Vaishnavi Sundararajan: So Usama, two things. One thing is that if you have a different formulation of the property, Elsa and Yuxuan's work says nothing about that. I am only talking about the formulation of the property that they have as part of their work, and that has shown that there is a need for a channel binder as far as version 3 is concerned. Right? So that's one thing.
The other thing is that since you have verified, or, or well-found counterexamples, as it were, to some behavior of attested TLS, again, that does not imply anything about EDHOC with remote attestation, because the very structure of the messages is different. So even in a symbolic world, you are working at the structure level of the messages rather than the cryptographic, computational level of the messages. And at the structural level, the messages that are sent as part of EDHOC, as Göran mentioned as well, are very different from the messages that are sent as part of TLS, even discounting the fact that there are different methods and, you know, different combinations at play here. The very fact that the messages are different does not allow you to port the results from TLS to EDHOC, just ab initio. I realize that you say that you are doing some code translation, and that needs to be examined further before we can say anything about, you know, accepting results for one and sort of porting them to the other. That doesn't seem to me how you could possibly get security.
Mališa Vučinić: I will, sorry, I will, I think we can go on for long, we are already over time. I don't know if this helps. Maybe if you want to talk more, bring it on the list publicly. I mean, if you want maybe one more, but I don't think we will solve the issue here. I think we are working as transparently as possible. So we, yeah, I mean, we do the best we can, what we have in front of our eyes. So yes, I hope, Usama, that you can share the code with us soon. And I don't know, we have to move on. In any case, we cannot be dependent on a paper acceptance in any case, and we, the experts should see, or everybody should see what's what's claimed, right?
I propose we move on to the next meeting. We are already over time. Geovane, you have five minutes for lake-authz.
Geovane Fedrecheski: Perfect. Thank you. So hello everyone. My name is Geovane, and I am presenting today the updates on Lightweight Authorization using ad-hoc. So as a quick recap, on the last IETF 119 in Shenzhen, we presented, so, the last updates from the draft. So now the draft is compatible with both elliptic curve keys and also KEMs, and in a recent refactor that was presented in Shenzhen, the flow was changed from message 1 and message 2 to message 3 and message 4. And this was part of fixing the issue of spoofing ID_U vulnerability that was documented and discussed in the issue tracker and also during last meeting. This simplified the cryptography and relied on, because now it relies on ad-hoc already on protection of message 3 and message 4, which already has a formal analysis done for this flow of the protocol. On top of that, the user identity, the device identity is also protected within message 3. And this also in turns allows using ad-hoc app profiles to advertise the capability to use ELA by a client.
And what is new? It's only a few editorial fixes, in particular a IANA registration table and some minor improvements on editorial on the draft. So it's stable. And one issue that was still open is trying to save the flow of message 1, message 2, where a proposal by Christian was to pad the voucher and always send it, and encrypt the voucher for the private key of U instead of the ephemeral key, and then V, the domain authenticator, would defer authorization until it can verify message 3. However, the main limitation of this approach is that then it requires a key to be able to do a key exchange, so the key needs to be a Diffie-Hellman or KEM and it will not work with signature keys. So that's the main blocker for that approach. So then we need to close this issue.
And that's it essentially. So looking forward to comments from the Working Group, if any. And in particular, we think this draft is stable, and we are looking forward to Working Group Last Call.
Mališa Vučinić: Thank you Geovane. Is there any question, please join the queue. Yes. Well, we will consider and yeah, the, the Last Call. Shall we do a show of hands, Malisa, or we decide offline to to launch the Last Call?
Mališa Vučinić: Uh, we could do the show of hands, yes.
Renzo Navas: Okay, so we have two minutes for this, so I guess it makes sense, yeah.
Mališa Vučinić: Okay, so where is this show of hands, yeah, I found it, so. Okay, the question that we are asking is, shall we launch the Working Group Last Call? Is draft-ietf-lake-authz ready for Working Group Last Call? Yes, Elsa, you can talk while the people vote. You want, yeah. Ah, okay, it was, sorry, I was not sure how to vote. Ah, okay, there is a button on top, yeah. No opinion, uh. Okay. Yeah, uh, if if you are hearing me, at least vote for no opinion. Okay. So Malisa, Juwan, Malisa, can you know this? We have eight, eight yes, zero no, ah, nine no opinion. I guess we should launch because there is no strong opposition to no. 10 no opinion. Okay.
Mališa Vučinić: Yeah, I guess it's converging, I guess that's the results that we get, so we will, yeah, we will launch Working Group Last Call. Then the people with no, yeah.
Renzo Navas: Okay, thank you Geovane, let's move on, we are already behind schedule. Next item is Meiling. Meiling, I will give you the slides. But before I give you the slide, a small intro from my side. I mean, some context to the audience. We launch the formal call for analysis of remote attestation on the list. Initially, Elsa and Usama respond, and they were working on that. Elsa just present. And then Vaishnavi asked, "What can I do?" And we asked you personally to look about both works and to give us, like, a trusted third party, so Vaishnavi will introduce your results. I will give you control. Please, if you can stay in four minutes so we have at least one minute for question. Floor is yours.
Meiling Chen: Okay, I got, I think I have got the control, yeah. So I have update a newer version here for ad-hoc-aka. For the last version, I have some feedback from the open comments, they think ad-hoc PSK can be better to do the ad-hoc-aka, and I can use the EAD items to carry the aka vector and also reuse ad-hoc PSK verification results to slow the effort, and I also know that ad-hoc PSK have complete the implementation, so I decided to redesign the ad-hoc-aka as a new profile of ad-hoc PSK. So I will leverage the ad-hoc PSK framework to better implementation.
And I have been asked, why I do the ad-hoc-aka here is that, from my side, I think, in the massive satellite IoT use cases, they will do better things is because there are thousands of sensors with battery-powered sensors in remote areas with no terrestrial coverage, it means that no base station in there. So, relying on satellite connections, characterized by high latency and low bandwidth. So I am looking for a new protocol that can do this with low cost here. So in this use case, I made the sensor the initiator and the, like, just for example, the cloud-based agriculture data analytic server as the responder, and mobile network operator as the authorization authority to do the authentication, because the mobile network operation, they have the SIM card and also they support 3GPP aka flows. So, I think the key value here is that ad-hoc-aka can do the lightweight and efficient and also a forward security key exchange here. And the most important thing is that I want to leverage the mature SIM card or 3GPP aka mechanism here for the identity and key management.
And how it works, that's the core mechanism here that I use EAD fields to carry the RAND and AUTN that used in the 3GPP aka authentication, and also message 3, the EAD3 that carry the response back, but message 4 is option for that, they can carry a final authentication result, for example, success or failed. So with that, they can build a successful connection with initiator and responder. But here is that we are different from the ad-hoc PSK is that the session key, the session key will be used for the key generation, it means that I will use the aka key generation that from long-term key to CK and IK and then do the next key derivation, then K_AK will be used as the PSK to complete the ad-hoc PSK flow.
And another question, I another comment I have received is that, does the RAND and AUTN value changed with each access? Yes, if the network allows proper encryption, they will change for each session. But it's only a basic solution is support, maybe it will unchanged, there will be the same with ad-hoc PSK.
And also, they want to know the relationship with 5G is that, in 5G, they will, the 5G network functions will respond for the low responder, so act as the network side front end for authentication. It is analogous to AUSF or SEAF in the 5G control plane, so I think is also the two-party protocol, not three-party. And also, aka vector retrieval is fetches from the home network via standard service-based interfaces, have standardized in 3GPP. So, I have to say that is transparent to UE, and they also very good in security and privacy.
Another, another comment is that, why combine aka with ad-hoc? The first reason is that it will enhance the forward protection, because the each session, it will be, will be changed the key. So, combine the ephemeral Diffie-Hellman keys and even the long-term key is compromised, will be also forward protection be got. And also, the second advantage is the fewer round trips, and another is the very tight cryptical bindings, is because all final session keys are cryptobound to the ephemeral public keys, prevent misbinding and substitution attacks.
Okay, is another benefits of ad-hoc-aka is using COSE/CBOR method, so, it will be very compact in the message format, so, that's the, that's the advantage of COSE/CBOR encoding to avoid EAP frame overhead, keeping message smaller for NB-IoT and smaller networks.
So, the deployment scenarios I list here is for NTN, non-terrestrial network, and also for NB-IoT, and also can do for the private networks and industrial IoTs, if they have the SIM card.
So, the key is takeaway that ad-hoc-aka I have redesigned for, as a file profile of ad-hoc PSK here.
And I also want some feedbacks on, like, how well this draft go, I would like to know whether this document is better merged into ad-hoc PSK or just exist as an independent document. Thank you.
Renzo Navas: Thank you Meiling. So yes, Göran, please.
Göran Selander: Hi Meiling.
Meiling Chen: Hi Göran.
Göran Selander: Thanks for your presentation. I realized I have a camera as well, hello. So, could you please flip back to slide 8? Slide 7, sorry.
Meiling Chen: Slide 7.
Göran Selander: That one, exactly. Yeah, I was looking, no, slide 7, you passed it, that's good.
I was a little bit, this was my question actually. Why not just use ad-hoc-aka? I mean, that's an Emu draft, which is essentially done. And your argument here, could you just repeat what, you're saying you embed the challenge-response in ad-hoc 1, one round-trip flow, okay, so you have, because you are essentially, you're still using the same AKA secret in both cases, but, but you're running it in ad-hoc instead of in AKA. And this is okay, simpler implementation, built-in confidentiality, I don't see that, I mean, ad-hoc-aka also has the confidentiality of these AKA parameters, right? That, at least that part I didn't understand. And then the compact message format, yes, I mean, ad-hoc framing, EAP framing, sorry, adds overhead to some extent. Okay, so this was basically my question. Thank you for taking, I had some time to read more on this, on this slide. Indeed.
Mališa Vučinić: Meiling, you should try to engage people on the mailing list to make them read your draft. I think you already sent this, but, yeah, I say we keep it to the mailing list, you should ask for more people to read and come with comments, and yeah, maybe, yes, now we are out of time to keep the discussion. But, thank you.
Meiling Chen: Okay.
Renzo Navas: So, next, I think next presenter is me and Lidia. Thank you Meiling. I will take back the control. This is number six. We are already more than five minutes behind schedule, so I will try to be very brief. So, this is a report on the post-quantum, we call, the Post-Quantum ad-hoc Design Team. This is the presentation today. I will introduce you the Design Team and the objectives we set for it. Spoiler, we have four objectives. I will be presenting three of them, and Lidia, the most important one, she will speak for 15 minutes. So, these to the left, you have all the members of the Design Team. It's a public list. We had five weekly one-hour meetings, except the first one that was a little bit longer. Mostly Wednesday, no, not mostly, all Wednesday at this time. We have internal minutes and a shared folder, there were a lot of discussions based on inputs from everybody, but mostly by Lidia Pocero Fraile. So, Lidia, I want to publicly thank you for your awesome work. Lidia gave a lot of input, which was food for discussion on most of the Design Team meetings.
So, even at the first meeting we decided, okay, what what are our goals? And we have, like, one and a half months. We agreed that we should have clear objectives, and we reached consensus on these four. This is very important slide, so I will say verbatim what we have here. The first objective was the definition of a set of deployment scenarios where post-quantum ad-hoc is realistically deployable. Then, a recommendation on standardizing post-quantum cryptography cipher suites for ad-hoc method 0, signature-signature, and 4, PSK. Third objective, recommendation on standardizing new KEM-based authentication methods satisfying the deployment of scenarios defined in Objective 1. Fourth objective, a statement for Crypto Forum Research Group on LAKE requirements, potentially including the deployment scenario from Objective 1 for the standardization of lightweight, okay, we need to define what's lightweight, PQC algorithms.
To be honest, we've been, we spend 80% of the time just trying to reach consensus on Objective 1, but in extremis we did it, and Lidia, the floor is yours. You have 15 minutes to explain what we reached on Objective 1. I will give you the slides control. Yes.
Lidia Pocero Fraile: Thanks, and hi everyone. Well, to address Objective 1, which aims to define deployment scenarios where PQC of ad-hoc can be realistically deployed, we use the constrained environment classification from the RFC 7228 draft of the IoT Operations Working Group to estimate the performance and resource impact of the proposed post-quantum authentication method. More specifically, we use the C classes to classify memory constraint, the S classes to evaluate fragmentation and their different MTU constraint, and the B classes to estimate the handshake time-on-air under different effective link bit rates. With this approach, we evaluate the feasibility and performance of the different authentication methods in terms of memory footprint, PQC processing time, and communication cost.
Well, we consider four main PQC authentication methods. First, signature-based authentication using ad-hoc method 0 with the PQC signature and PQC KEM key exchange. Second, the pre-shared key based method using the ad-hoc pre-shared key draft together with PQC KEM key exchange. These two are described in the PQC suite draft. Third, the KEM-based authentication method where both key exchange and mutual authentication are performed using PQC KEMs. And finally, a KEM-based approach using post-quantum KEM schemes for both key exchange and authentication.
For all scenarios, we assume mutual authentication using the same authentication method on both sides, and credentials provided by reference. Regarding the evaluated PQC algorithms, we mainly considered NIST standardized schemes, excluding Kyber and Dilithium due to their large artifact size. And we also included compact signature candidates from the second NIST round with lower ad-hoc handshake size than Dilithium, and also MLCEM compact schemes such as Dawn and DCTDH. Most benchmark data comes from PQClean Cortex-M4 evaluation, except from Sphincs, Dawn, and DCTDH that is coming from the specific link where Cortex-M4 implementations are not yet available. Key signature and ciphertext size used on the message size calculations were obtained from the corresponding NIST PQC submission and their specifications.
Well, we classify the memory footprint of the PQC operations for each authentication method, so in the first column, considering different authentication algorithms and implementation variants on the second column, and for two MLCEM implementations as a key exchange in the third column in the table. When KEM-based authentication is used, the same MLCEM implementation is reused for both key exchange and authentication. For PSK authentication, use MLCEM only for the key exchange, while for signature-based authentication, we evaluate different signature algorithms with the same MLCEM key exchange method.
The last five rows show stack optimized implementations. The tables report the memory footprint in kilobytes associated with the public key and secret key used for the authentication, in the first column. For later calculation, we assume these credentials are stored in non-volatile memory, meaning flash memory, and then we have the flash and RAM required for the PQC operation of each method. Based on this, the next column identify the minimum C-class device capable of supporting each method according to the RAM and flash limit, so in the table. And finally, the last column show also the percent of RAM and flash consumed relative to the corresponding minimum supported device class. The principal observation from these results is that when stack optimized implementations are used, the PSK and KEM-based method with MLCEM-512 are feasible for deployment on Class C1 devices. Signature-based authentication using MLCEM together with ML-DSA becomes feasible starting from Class C2 devices, and on the other hand, signature-based method using MLCEM together with compact PQC signature candidates such as Falcon generally require at least Class C3 and C4.
Well, PQC algorithms introduce significantly larger public key signature and ciphertext size than classical cryptography. Therefore, we also evaluate the IP message size and total handshake size for each authentication method. To do this, we use the corresponding drafts for each method together with a common definition for the IP message file, shown at the table on the right. And the table then report the resulting IP message size and total handshake size in bytes. Using these calculations and considering the upper limit of the L2 MTU together with an estimated overhead compact overhead of 28 bytes, we evaluate two aspects. First, the minimum S-class for which no 6LoWPAN fragmentation is required, and second, the number of fragments required by each method under different S-class MTU constraints.
From these results, we can observe that pre-shared key and KEM-based method do not require fragmentation from S3 and above, while KEM and signature-based method with most of the compact NIST second round scheme achieve this from S4 and above. In contrast, signature-based method with standardized ML-DSA require S13 and above, and Falcon requires S12. However, based only on fragmentation, we cannot fully exclude any option, then we also need to evaluate how this fragmentation impact the time-on-air, together with the PQC processing time. That is what we make in the next slide.
To estimate the total handshake time, we take into account two main components. First, the PQC processing time, which is the dominant computational cost for each authentication method for a 50-20 MHz processor. And second, the estimation of time-on-air in a link-to-link scenario without packet loss, considering fragmentation and ACK overhead under different bit rates B and MTU size S classes. Well, the blue table show the resulting total handshake duration, taking into account both processing time and time-on-air for representative constrained networks such as the IEEE 802.15.4, BLE, Z-Wave, and NB-IoT, as well as some specific bit rates value to better illustrate the trends across the different B and S classes.
From these results, we observe a clear trade-off between processing cost and communication cost. KEM-based method achieve lower PQC processing time, but at the cost of larger message size, and compact signature-based scheme reduce time-on-air in a signature-based method but require higher processing time. And also, the KEM-based method achieve the smallest message size overall, but currently suffer from very large PQC processing times. More specifically, overall, pre-shared key based method achieve the lowest handshake time across most scenarios, and for the runner-up, the best options depend strongly on the available bit rate. At low bit rates below 10^5 bits per second, compact signature-based authentication becomes more competitive because time-on-air dominates. In contrast, above this 10^5 bits per second, KEM-based authentication becomes the best alternative since the lower PQC processing time dominate the total handshake duration.
Well, from this study, the following main observations can be highlighted: pre-shared key and KEM-based authentication with MLCEM-512 provide the lowest memory footprint and remains feasible even for constrained Class C1 devices. Pre-shared key authentication achieved the lowest processing time overall, followed by KEM-based authentication. Compact signature-based authentication significantly reduce time-on-air but generally requires more capable Class C3 or C4 devices. The best authentication method strongly depends on the available bit rate. For higher bit rate networks, KEM-based authentication provides the best total handshake performance. But for lower bit rate networks, compact signature-based schemes becomes more attractive because reducing time-on-air that becomes more important than reducing processing time. And finally, the KEM-based approach using these optimized implementations achieve the lowest network overhead, but currently has very high processing times, making it mainly attractive for powerful devices and extremely constrained low bit rates link where time-on-air dominate.
Well, based on the results from this objective, we believe that the three authentication approach: pre-shared key, KEM-based, and signature-based authentication should all be considered since they address different constrained environment requirements. And in general, we can identify four deployment scenarios. First, for constrained Class C1 and C2 devices, pre-shared key based authentication is the preferred option, complemented by the KEM-based authentication for non-pre-shared key environments, both using MLCEM-512. Second, for more capable Class C3 and C4 devices, all authentication methods become feasible. In higher bit rate networks, KEM-based authentication is generally the most suitable option due to its lower processing time, but third, in the low bit rate network, compact signature-based schemes becomes more attractive because reducing this communication cost because become more important than reducing processing time. And finally, the signature-based authentication using standardized ML-DSA can also operate on some Class C2 devices, but due to its large message size and corresponding time-on-air, it's mainly suitable for higher S and B classes network.
And this is, this is it. Thank you. So, if there are questions.
Mališa Vučinić: Thank you Lidia. I take over. I will be quick, so we have time for questions. Yes.
Apostolos Fournaris: Yeah, thank you, and thank you chairs. One question I have is on the last slide, if you go back one slide, you was saying that some of the properties, uh, sorry, one of the property which is this equivalence-based proof, are you saying that this is difficult in Tamarin, that's why you do in ProVerif, or what is the, what is the argument for doing it in ProVerif instead of, while you say that there are several properties which are verified in Tamarin, but why this property in ProVerif? Is it hard to do that? It takes more time, or is it about the computational sources, or what, what is the kind of reason for using a different tool for the same model? Can you explain a little bit?
Vaishnavi Sundararajan: Yeah, so basically, there is a notion of diff-equivalence in Tamarin as well, but it is fairly limited and not quite optimized for proving equivalence queries as much as ProVerif is. That's basically the only concern. And now that we have this Sapic+ functionality that is built-in, we can basically export a Tamarin model to ProVerif quite easily. So the overhead there is not very much, but we will get the optimization of ProVerif's back-end for proving equivalence properties. That's basically the only concern.
Mališa Vučinić: Thank you. I want to go back to the your last point, Lidia, so Working Group adoption. We didn't discuss privately with Malisa, but I mean, this is what the Design Team recommended, so yeah, we've be discussing around this for for quite a time, it was one of the suggestions of the Design Team, which we were part. So I don't want to be judge and part at the same time, but I think the way to proceed should be maybe ask who read the draft and or the opinion, yeah. Maybe a quick show of hands or, yes, first who read the draft.
Renzo Navas: Yeah, I will I will start, yeah, I will start the show of hands for who has read the draft.
Renzo Navas: Yeah, did not phrase the question well, but it's, it should be implied. So we have six hands so far, seven, no.
Apostolos Fournaris: Just to mention I've read the draft, but I guess that doesn't count because I'm one of the authors, so.
Renzo Navas: As author, it doesn't, it doesn't count, yes.
Renzo Navas: Shall we, so, I think we have, yes, quite a lot of people, so we can ask the second question, if today the Working Group wants to adopt this. What do you think, Malisa, you have more...
Mališa Vučinić: Yeah, yeah, I think that makes sense. Yes, I think that makes sense. I will terminate the show of hands for who has read the draft, so we have 10 hands for yes and 2 hands for no, out of 23 participants, I guess. So, that's, that's very good.
Mališa Vučinić: Yeah, but that's, that's probably no. So we have 10 hands, I don't know how many out of those are authors, but we can confirm on the mailing list about the adoption and ask for the adoption of this draft, I suppose, whether there are any opposing opinions. Does, are there any objections to this path forward?
I hear none. And okay, we are 1 minute over time, it was quite a, ah, you, you launch the, no, it's the, sorry.
Mališa Vučinić: It's the old one, yeah. I just, yeah, it's just the old one. So yeah, I propose we just proceed with the, with the mailing list directly.
Renzo Navas: Yes. So, well, thank you everybody for this quite packed agenda and discussions. And yeah, let's keep on the mailing list and see you on Vienna hopefully. We have I think a 2-hour meeting, so we will have more time. I wish you all a good Tuesday.
Mališa Vučinić: Yes, good Tuesday, and see you in Vienna.
Renzo Navas: See you in Vienna. Bye, thank you all.
Elsa Lopez-Perez: Bye, thank you.
Vaishnavi Sundararajan: Bye everyone, thank you.
Meiling Chen: Bye, thank you.