Re: [Lake] Security levels for EDHOC for formal verification

[John Mattsson <[e-mail]>]

Hi,

I tried to summarize this email discussion in a document in the GitHub repository. Might be that you want to cite a document rather than the email discussion. Maybe it will also help other researchers as well. Should be noted that the document has not been approved by LAKE. Some of the text in the document such as security level against online and offline attacks might be good to put into the EDHOC document.

https://github.com/lake-wg/edhoc/blob/master/Security%20Level/Security%20Levels%20and%20Design%20Goals%20of%20EDHOC.txt

Cheers,
John

-----Original Message-----
From: John Mattsson <[e-mail]>
Date: Friday, 12 February 2021 at 18:11
To: Karthik Bhargavan <[e-mail]>
Cc: "[e-mail]" <[e-mail]>
Subject: Re: [Lake] Security levels for EDHOC for formal verification

I forgot the TLS Finished MAC in my quick summary yesterday. TLS 1.2 had a 12 byte MAC and TLS 1.3 has a huge 32 byte MAC. Together with the record layer MAC TLS 1.3 always has at least 40 bytes MAC. This is probably overkill, but EDHOC definitely be significantly weaker on this aspect. Especially the static DH with 8 byte MAC.

Göran and I will try to collect the requested usage assumptions and write them down some form that can be referenced. A new -00 draft or a txt file on the LAKE WG github.

/John

-----Original Message-----
From: John Mattsson <[e-mail]>
Date: Friday, 12 February 2021 at 00:07
To: Karthik Bhargavan <[e-mail]>
Cc: "[e-mail]" <[e-mail]>
Subject: Re: [Lake] Security levels for EDHOC for formal verification

Thanks Karthik,

>This is useful information and provides a good basis for discussion.
>It is particularly interesting to see the places where you specify that the EDHOC security >guarantee is expected to meet (or exceed) TLS 1.3,
>because these provide clear goals we’d like to focus on during formal verification.

[John] That sounds good. I think TLS 1.3 is a very good basis for further discussion. Both TLS 1.3 and EDHOC are based on SIGMA. If there is a large difference, that is something that the LAKE WG should discuss. Another design aspect that I can think of is:
 - TLS 1.3 uses nonces and therefore more entropy. TLS 1.3 security level against huge pre-computed rainbow tables would be higher than EDHOC.

The Static DH authentication is of course quite different from TLS 1.3. I think it should have equal of greater security than TLS 1.3 with PSK authentication. EDHOC with Static DH authentication should be stronger than EDHOC with signature authentication is some aspects (the key derivation includes three shared secrets instead of one and it should be stronger against key leakage), but weaker in some aspects as the authentication security is bounded by the AEAD tag length.

>As Rene says, the proof itself relies primarily on standard crypto assumptions about the >underlying constructions, but one of the interesting aspects of LAKE and COSE is that we >are trying to minimize message sizes (e.g. by using shorter authentication tags).
>It is therefore important to understand the concrete security goals in terms of the >expected security level so we can make sure that one of the message size optimizations >isn’t unexpectedly breaking the security of the protocol.
>Conversely, known the target security level may also allow us to identify new cryptographic >optimisations that have not been considered yet.

Yes, looking forward to you results.

>In addition to the sizes of the crypto keys, it would also be useful to know how many EDHOC >session is an intitiator/responder expected to participate in (per day, and over its >lifetime.)
>How much data do we expect to send in each session?
>What is a reasonable compromise window for each device; e.g. would it be ok to refresh the >ECDH keys every hour, or once every day?

[John] I hope that other people in the WG can help me fill in these assumptions:

- I think a typical device would run EDHOC quite seldom. In the extreme, a sensor or actuator might run it only once during its 10 year lifetime, but maybe a more reasonable estimate is every month/year when it receives a firmware update? A cloud server might run EDHOC very very often (many times per second) with differnet devices.

- I think other people in the group have much better answers for how much data an average IoT device sends per time unit.
  Also what do you mean by session? Current work in progress is that OSCORE will rekey frequently to get FS without rerunnign the full EDHOC. This would be similar to TLS 1.3 KeyUpdate. As the details are not completely specified yet, I do not know if you can model this but any comments or suggestion would be very welcome.

- Which ECDH keys do you mean? EDHOC currently states that the ephemeral keys MUST NOT be reused so they are erased from memory after each run. The Static ECDH keys used for ES ECDH authentication would typically be much more long lived. It is common to use IoT authentication keys for the lifetime of a device, i.e., around 10 years, but recently there has been a trend in the HTTPS world to use shorter lifetimes (1 year instead of 3 years).

>It would be great to collect a compendium of both usage constraints like these >and concrete security targets so we can make sure the protocol (and its >recommended ciphersuite) satisfies them.

[John] I guess we can turn this discussion into a appendix or some other form of document that you can reference.

Cheers,
John

-----Original Message-----
From: Karthik Bhargavan <[e-mail]>
Date: Thursday, 11 February 2021 at 17:40
To: John Mattsson <[e-mail]>
Cc: "[e-mail]" <[e-mail]>
Subject: Re: [Lake] Security levels for EDHOC for formal verification

Thanks John,

This is useful information and provides a good basis for discussion.
It is particularly interesting to see the places where you specify that the EDHOC security guarantee is expected to meet (or exceed) TLS 1.3,
because these provide clear goals we’d like to focus on during formal verification.

As Rene says, the proof itself relies primarily on standard crypto assumptions about the underlying constructions, but one of the interesting aspects of LAKE and COSE is that we are trying to minimize message sizes (e.g. by using shorter authentication tags).
It is therefore important to understand the concrete security goals in terms of the expected security level so we can make sure that one of the message size optimizations isn’t unexpectedly breaking the security of the protocol.
Conversely, known the target security level may also allow us to identify new cryptographic optimisations that have not been considered yet.

In addition to the sizes of the crypto keys, it would also be useful to know how many EDHOC session is an intitiator/responder expected to participate in (per day, and over its lifetime.)
How much data do we expect to send in each session?
What is a reasonable compromise window for each device; e.g. would it be ok to refresh the ECDH keys every hour, or once every day?

It would be great to collect a compendium of both usage constraints like these and concrete security targets so we can make sure the protocol (and its recommended ciphersuite) satisfies them.

Best,
-Karthik


> On 11 Feb 2021, at 09:13, John Mattsson <john.mattsson=[e-mail]> wrote:
> 
> Hi,
> 
> There was a request from Karthik to have specified security levels for EDHOC so that formal verification can verify or falsify the claims. This is not trivial. Below is a first try. Let's discuss if this is enough or if more or different information is needed.
> 
> The design objectives of EDHOC has been to have approximatly the same security level as TLS when the same algorithms are used, but to have much smaller messages. Just like TLS I think the expected security level depends heavily on the chosen algorithms and the method. Method 3 should be comparable with TLS 1.3 with mutual certificate based authentication. Methed 0 is a bit trickier to compare to TLS.
> 
> In general there should not be much difference between EDHOC and TLS 1.3 when certificate based authentication is used. The exported keys should be a bit stronger as EDHOC include message_2 and the for Static DH also the private authentication keys. The Static DH Method with 64 bit tags does not offer the same security level as TLS 1.3 with certificate-based authentication, but should offer better security than TLS 1.3 with PSK authentication and short tags.
> 
> EDHOC can use all algorithms defined for COSE (but maybe you will restrict your work to
> the pre-defined cipher suites). Below are the relevant algorithms defined for COSE.
> 
> EDHOC AEAD algorithm:
> ---------------------------
> AES-CCM-16-64-128
> AES-CCM-16-64-256
> AES-CCM-64-64-128
> AES-CCM-64-64-256
> AES-CCM-16-128-128
> AES-CCM-16-128-256
> AES-CCM-64-128-128
> AES-CCM-64-128-256
> A128GCM
> A192GCM
> A256GCM
> ChaCha20/Poly1305
> 
> EDHOC hash algorithm
> ---------------------------
> SHAKE256
> SHA-512
> SHA-384
> SHAKE128
> SHA-512/256
> SHA-256
> [SHA-1 and SHA-256/64 not allowed]
> 
> EDHOC ECDH curve
> ---------------------------
> P-256
> P-384
> P-521
> X25519
> X448
> Wei25519 (expected to be registered soon)
> [Ed25519, Ed448, secp256k1 are not allowed] 
> 
> EDHOC signature algorithm
> ---------------------------
> ES256
> ES512
> ES384
> EdDSA
> ES256K
> 
> EDHOC signature algorithm curve
> ---------------------------
> P-256 (ECDSA only)
> P-384 (ECDSA only)
> P-521 (ECDSA only)
> Ed25519 (EdDSA only)
> Ed448 (EdDSA only)
> secp256k1 (ECDSA only)
> [X25519, X448 are not allowed] 
> 
> (Non-ECC signatures algorithms are supposed to be allowed as well. I think the draft needs to be updated.)
> 
> Below are two initial ways to express the security level, one as a function of the Mehtod and algorithms. The second as a comparision with TLS 1.3. In general, EDHOC with the weakest options SHALL offer 64-bit security against on-line attacks and 128-bit security against off-line attacks. I think this aligns with TLS 1.3.
> 
> Let me know if this is enough for the formal verification, if you need something different, or if something is missing. It would be good if somebody reviews the information is this mail.
> 
> 
> EDHOC security levels for different aspects
> ---------------------------
> 
> The security level of confidenciality protection against passive attackers should be the key length of the AEAD (128, 192, or 256 bits).
> 
> The security lebel of integrity protection and confidentiality against active attackers should be the tag length of the AEAD (64 or 128 bits)
> 
> The authentication security in the static DH modes are determined by the  tag length of the AEAD (64 or 128 bits)
> 
> The authentication security in the Signature Key modes are determined by the security level of the signature algorithm (128, 192, or 256 bit)
> 
> The integrity protection of some fields are detemined by the security level of the signature algorithm (128, 192, or 256 bit).
> 
> 
> 
> EDHOC security levels compared with TLS 1.3
> ---------------------------
> 
> Method 0 (2* Signature Key ) should offer the same security level as TLS 1.3 with the same algorithms.
> 
> 0. (AES-CCM-16-64-128, SHA-256, X25519, EdDSA, Ed25519)
> 1. (AES-CCM-16-128-128, SHA-256, X25519, EdDSA, Ed25519)
> 4. (A128GCM, SHA-256, X25519, ES256, P-256)
> 5  (A256GCM, SHA-384, P-384, ES384, P-384)
> 
> 
> Method 0 (2* Static DH Key ) is a bit trickier.
> 
> 0. (AES-CCM-16-64-128, SHA-256, X25519, EdDSA, 
> 
> The authentication security level here is bounded by the 128-bit tag. Should offer at least the same security level as TLS 1.3 with PSK authentication with CCM_8, and the other algorithms the same.
> 
> 1. (AES-CCM-16-128-128, SHA-256, X25519, EdDSA, Ed25519)
> 4. (A128GCM, SHA-256, X25519, ES256, P-256)
> 
> Should both offer similar security level as TLS 1.3 with certificate authentication and the the other algorithms the same.
> 
> 5	(A256GCM, SHA-384, P-384, ES384, P-384)
> 
> The authentication security level here is bounded by the 128-bit tag.
> 
> Cheers,
> John
> 
> 
> -- 
> Lake mailing list
> [e-mail]
> https://www.ietf.org/mailman/listinfo/lake