# Lightweight Authenticated Key Exchange (LAKE) - IETF 113 ## Monday, 21 March 2022 -- 13:30-15:30 UTC ### Notetakers: * Rikard Höglund * Marco Tiloca ### [Chairs](mailto:lake-chairs@ietf.org): * Mališa Vučinić * Stephen Farrell ### Useful Links: * [Charter](https://datatracker.ietf.org/group/lake/about) * [Mailing list](https://www.ietf.org/mailman/listinfo/Lake) * [Jabber room](xmpp:lake@jabber.ietf.org) * [Minutes](https://notes.ietf.org/notes-ietf-113-lake) * [Remote participation](https://meetings.conf.meetecho.com/ietf113/?group=lake&short=&item=1) ### Abbreviations * [MV] Mališa Vučinić * [MT] Marco Tiloca * [MS] Marek Serafin * [FM] Francisco Molina * [JPM] John Preuß Mattsson * [BM] Brendan Moran * [MCR] Michael Richardson * [BC] Baptiste Cottier * [CJ] Charlie Jacomme * [GS] Göran Selander * [SF] Scott Fluhrer * [SFA] Stephen Farrell * [MI] Marc Ilunga ### Action Items * EDHOC authors and Charlie Jacomme: To convert the remarks in "Symbolic model analysis" presentation to github issues. ### Minutes: * Administrivia (chairs) * SFA goes through the administrivia slides. * Chairs’ update (chairs) * MV: Lake traces draft has been adopted. Edhoc-12 is ready for formal analysis. Invitation to publish article in IEEE Computer Magazine. EDHOC spec was frozen since IETF 112, but updated in Github. * MV: The article in IEEE Computer Magazine summarizes the protocol and invites the academic community. * MV: Going over todays agenda which has focus on community feedback. March milestone has been pushed back to wait for more feedback from academic community. * Hackaton report (Marco Tiloca) * MT: Focus was on development, and testing. Malisa worked on his implementation in Rust. Goal was to provide a runnable minimal implementation, with a small size for EDHOC message 2. This relied on the ID Cred being KID (int) and using Static-Static. * MT: Testing was done with Malisa's implementation in Rust and Marco's in Java. The testing consisted of these parameters Cipher suite 2, method 3, CCS credential type, ID cred as KID. This test was successful with the same OSCORE master secret and salt generated. * MT: Next steps are to see that other implementations get updated to the latest spec, cover more testing of the traces document, and also test error messages. There is a separate document in CoRE that provides an optimization for combining EDHOC message 3 with an OSCORE request. * MV: In total we now have 9 implementations. * Developer feedback #1 (Francisco Molina) * FM: Focus on implementation for constrained settings. Related to the RIOT-fp project (http://future-proof-iot.github.io/RIOT-fp/about). The use case is about privacy-preserving contact tracing, with untrusted IPv6 over BLE. Using EDHOC to establish context between the contact server and the devices. Goal was to produce a generic C implementation of EDHOC suitable for microcontrollers, supporting all authentication methods, suites 1-4, and not using hardware acceleration. Aim was to reuse existing libraries. * FM: Implementation based on edhoc-05. Considered different CBOR libraries and crypto libraries. RIOT was selected as the platform to use. * MV: When you say testing with "no real certificates"*you mean usage of a dummy byte string value? * FM: Correct. * FM: Ended up with a C implementation EDHOC-C (summary of components and links on p12). Used py-edhoc for interoperability testing. * FM: We performed measurements of RAM/ROM footprint, where RAM usage varied alot depending on the method, and size of parameters. * FM (p14): time benchmark comparing different HW platforms and method 1 vs method 3. Most of the time usage is related to crypto operations (while measurements are coarse). * FM: Deployed this solution on RIOT. * JM (in chat): "Any comparision on performance between P-256 and Curve25519?" * FM: some figures for P-256 available, I will look up a paper * FM (p17): A number lessons learned listed in this slide * BM: On comparing different ciphersuites. MbedTLS does support AES-CCM, to fix in the slides (p8). * FM: Okay, thank you. * Developer feedback #2 (Marek Serafin) * MS: Going over the background and challenge they wish to solve and motivation for this work. Their current solution builds on CoAP, OSCORE, and EDHOC (with X509). * MS: Use of CoAP to transport RPC over protected with OSCORE or rather EDHOC. Considered transports are BLE, UDP, UART. Targeted multiple platforms which were embedded, mobile and cloud. * MS: For EDHOC libraries we wanted to keep code size small and chose the uOSCORE-uEDHOC library for Node JS, iOS and Embedded where we have a wrapper layer in between. For Android and Cloud we used our own EDHOC implementation AA EDHOC Java. For now we use EDHOC method 0 and cipher suite 2, with certificates as authentication credentials. The hardware platform used was NRF52840. * MS (p12): performance results when transporting over BLE; about 800 ms to complete EDHOC. * MV: 595 ms what does it refer to? * MS: Scanned over BLE, discovered GATT, and sent EDHOC message 1. * MCR: BLE has an encryption layer. Does GATT avoid it? * MS: Yes, it avoids the encryption layer. * MS: Over mobile phone BLE scan, connect, discovering GATT, running EDHOC (with X509) and RPC session setup takes less than 1 second. * MS: Future steps are a cloud HTTP to CoAP proxy with EDHOC & OSCORE, and Open source contributions (already doing for uOSCORE-uEDHOC), and developing a modern test vector generator. * FM: mBed TLS has Ed25519 support coming (exists in PRs). * Implementation security update (Mališa Vučinić, chair hat off) * MV: LAKE targets constrained environments and embedded systems. C is the dominant language (which is memory unsafe). Goal to have implementations that are provable to be correct and memory safe. * MV: Hacspec (https://github.com/hacspec/hacspec) methodology relies on a specification language that is a subset of Rust, the specification is executable and enables verification. * MV (p4): implement manually in Rust --> first F* model (automatic) --> Write and verify (manual) --> compile to verified C (automatic) * MV: Goals are the following: verifiable code for microcontrollers, minimal implementation, no dependencies (even standard libraries), rely on hardware acceleration, target (Native, CC2538, nRF52840), portable to other targets. * MV: Opposing goals to have this done with microcontroller as final target and verifiable in Hacspec because Hacspec relies on Rust standard library. Lot of time spent to correctly handle compressed/uncompressed elliptic curve coordinate representation. Development of a HW abstraction layer in Rus * MV: Produced minimal implementation after Hackathon which was tested with the Java implementation for Californium. Using static-static and CCS with integer kid. * MV (p8): Covering open questions and next steps, mostly on moving towards verified code for microcontrollers as running platform. * Computational model analysis (Baptiste Cottier) * BC: Security analysis can consider the symbolic or computational security model, with differences on the attacker's capabilities. * BC (p3): Showing EDHOC constraints and overview of static-static analysis * BC: Defined 128 bit security level. Wish to prove key privacy, mutual authentication and identity protection. * BC (p5): Definition of key privacy property * BC (p6): Definition of mutual authentication property. Is 128 bit security reached after a few AEAD messages? * MV: 127 bits security level agreed in requirement document. This refers to protected messages exchanged after EDHOC. You try to prove this can be achieved with the considered MAC size. Correct? * BC: That is correct. * JPM (on chat): I assume the 127 bit security in the req document comes from the average complexity of a brute force attacker. In practice it is reasonable to differentiate between offline and online attackers. * BC (p7): Definition of identity protection property. * SF (in chat): "I don't believe GCM gives you the '128 bit security from several 64-bit MAC validation' property you are looking for. If the attacker manages to find one forgery on a 64-bit GCM MAC, he can leverage that to perform more forgeries." * SF: Not sure you can achieve that security level with GCM, due to security properties of GCM. The attacker does a blind-guess for first forged message, if successful, he can forge later messages (so later messages do not increase security level). * SFA: Is this specific to GCM? Does it apply to CCM? * SF: It is specific to GCM? * SFA: I do not believe we have 64 bit MACs for GCM in the protocol. * SF: Good * MI: What did you define as a session key? * BC: The key that the two peers commonly share at the end. * MV: So PRK4x3m? * BC: Yes, although it may be the result of a further derivation step from it. * GS: Yes PRK4x3m or a secret derived from PRK4x3m and TH4. * JM: What is session key can be different in formal analysis than in EDHOC. We can come back to this. * MV: When do you expect to complete this work? * BC: 2 months would be enough to conclude. * MV: Let's sync up then before the next IETF meeting in July. * Symbolic model analysis (Charlie Jacomme) * CJ: Working on a protocol model for formal analysis of EDHOC (through applied-pi calculus). Solution can be exported to ProVerif and Tamarin to use them for creating proofs. * CJ (p3-4): Showing building blocks and primitive models * CJ (p5): Describing protocol model and limitations * CJ (p6): Presenting results depending on threat model. With basic model all is fine, with other models some properties were not verified as holding. * CJ (p7-11): suggestions for improvements as result of the analysis: * avoid potential misuse of current design * the session key does not authenticate TH_4 and is not linked to a particular execution; this handles a possible dishonest responder as able to control the final value of PRK4x3m --> add additional master secret derivation * a stored message may be resent yielding the reuse of IV and key --> forbid message recomputation * CA (on chat): I don't think that forbidding store-and-rederive will make implementations much more secure -- people who do things carelessly might still do it. We could use stronger wording to illustrate what breaks if one gets it wrong: better scare people off with concrete information that just say "forbidden" so people may or may not understand what the consequences are. * CJ: strengthen the Trusted Execution Environment implementation * CJ: possibility of impersonation attack (under specific assumptions on key leakage) --> increase dependence of MAC_2 with G_IY (require G_IY to compute the MAC) * Future proofing * if transcript collisions are ever possible for SHA-256 --> see a number of suggestions on p. 14 * CJ: Next steps are to deepen the analysis, keep the modules up to date and maybe look at a computation proof (with Squirrel) * MV: I propose as action item to authors to convert the list of remarks to Github issues. Then we discuss those on Github and the mailing list. * MV: Do you plan to keep the model up to date? * CJ: Yes. * MV: Do you plan to publish this work? * CJ: Yes * MV: Please forward/highlight any publication resulting from your work. * draft-ietf-lake-edhoc-latest & draft-ietf-lake-traces-latest (Göran Selander, 1) * GS: Since IETF 112 no new versions of EDHOC of traces were submitted. We have worked on the document on Github. * GS (p4): Going over list of main changes. Hope to make it clear what is part of the core protocol. * GS (p5): Update to compliance requirements. In the absence of an application profile specifying otherwise: MUST support cipher suite 2 and 3, MUST be able to parse padded messages. * GS (p6): Other updates: Error handling, exporter labels, can choose CID range (e.g. only int or only bstr), security & IANA considerations, and clarifications. * GS: Waiting for input from hackathon and analysis works. * GS (p8): Describing traces document (help for implementors) and updates to it on Github for now. First cipher suite 0 with method 0, then ciphers suite 2 with method 3. * GS: Next steps are to submit edhoc-13, address review comments, go for WGLC(?), submit traces-01 (and get it reviewed). * Next steps (chairs, 5 mins) * SFA: We can poll people working on analysis to see if they are fine with updating to draft v-13. * MV: Any objection? * SFA: We can also bring it to the mailing list. * JM (in chat): At a minimum we should resubmit 12 before it expires on 23 april * SFA: No need to worry too much * JM: We know that expired draft is not an issue, but people outside IETF may get the impression that the worked stopped. So better to not let it expire. * MV: So we have 1 month to decide if the analysis teams can update their models. I agree we should not let it expire. * JPM: There has been interest in the JSON test vectors. We will be working on updating the test vectors. * AOB (end of meeting, 15:31 UTC)