From f02de2c866e51fa0bfbc134656a4884f82a6ac00 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mali=C5=A1a=20Vu=C4=8Dini=C4=87?= Date: Sun, 5 Nov 2023 14:09:52 +0100 Subject: [PATCH 1/3] Refactor decode_plaintext_3 --- lib/src/edhoc.rs | 79 +++++++++++++++++++++++++++++++++++------------- 1 file changed, 58 insertions(+), 21 deletions(-) diff --git a/lib/src/edhoc.rs b/lib/src/edhoc.rs index 4bceb381..f378ea46 100644 --- a/lib/src/edhoc.rs +++ b/lib/src/edhoc.rs @@ -287,7 +287,7 @@ pub fn r_process_message_3( let decoded_p3_res = decode_plaintext_3(&plaintext_3); if decoded_p3_res.is_ok() { - let (kid, mac_3, ead_3) = decoded_p3_res.unwrap(); + let (id_cred_i, mac_3, ead_3) = decoded_p3_res.unwrap(); // Step 3: If EAD is present make it available to the application let ead_success = if let Some(ead_3) = ead_3 { @@ -296,10 +296,17 @@ pub fn r_process_message_3( true }; if ead_success { - let (g_i, kid_i) = parse_cred(cred_i_expected).unwrap(); // FIXME + let (g_i, kid_i_expected) = parse_cred(cred_i_expected).unwrap(); // FIXME // compare the kid received with the kid expected in id_cred_i - if kid == kid_i { + let credentials_match = match id_cred_i { + IdCred::CompactKid(kid) => kid == kid_i_expected, + IdCred::FullCredential(cred_i_received) => { + cred_i_expected == cred_i_received + } + }; + + if credentials_match { // compute salt_4e3m let salt_4e3m = compute_salt_4e3m(&prk_3e2m, &th_3); // TODO compute prk_4e3m @@ -930,33 +937,58 @@ fn edhoc_kdf( fn decode_plaintext_3( plaintext_3: &BufferPlaintext3, -) -> Result<(u8, BytesMac3, Option), EDHOCError> { +) -> Result<(IdCred, BytesMac3, Option), EDHOCError> { let mut ead_3 = None::; let mut error = EDHOCError::UnknownError; let mut kid: u8 = 0xff; let mut mac_3: BytesMac3 = [0x00; MAC_LENGTH_3]; + let mut id_cred_i: IdCred = IdCred::CompactKid(0xFF); // check ID_CRED_I and MAC_3 - if (is_cbor_neg_int_1byte(plaintext_3.content[0]) || is_cbor_uint_1byte(plaintext_3.content[0])) - && (is_cbor_bstr_1byte_prefix(plaintext_3.content[1])) + let res = if (is_cbor_neg_int_1byte(plaintext_3.content[0]) + || is_cbor_uint_1byte(plaintext_3.content[0])) { + // KID kid = plaintext_3.content[0usize]; - // skip the CBOR magic byte as we know how long the MAC is - mac_3[..].copy_from_slice(&plaintext_3.content[2..2 + MAC_LENGTH_3]); - - // if there is still more to parse, the rest will be the EAD_3 - if plaintext_3.len > (2 + MAC_LENGTH_3) { - // NOTE: since the current implementation only supports one EAD handler, - // we assume only one EAD item - let ead_res = parse_ead(plaintext_3, 2 + MAC_LENGTH_3); - if ead_res.is_ok() { - ead_3 = ead_res.unwrap(); + id_cred_i = IdCred::CompactKid(plaintext_3.content[0usize]); + Ok(1) + } else if is_cbor_bstr_2bytes_prefix(plaintext_3.content[0]) + && is_cbor_uint_2bytes(plaintext_3.content[1]) + && (plaintext_3.content[2] as usize) < plaintext_3.len + { + // full credential + let cred_len = plaintext_3.content[2] as usize; + id_cred_i = IdCred::FullCredential(&plaintext_3.content[3..3 + cred_len]); + Ok(3 + cred_len) + } else { + // error + Err(()) + }; + + if res.is_ok() { + let mut offset = res.unwrap(); + + if (is_cbor_bstr_1byte_prefix(plaintext_3.content[1])) { + // skip the CBOR magic byte as we know how long the MAC is + offset += 1; + mac_3[..].copy_from_slice(&plaintext_3.content[offset..offset + MAC_LENGTH_3]); + + // if there is still more to parse, the rest will be the EAD_3 + if plaintext_3.len > (offset + MAC_LENGTH_3) { + // NOTE: since the current implementation only supports one EAD handler, + // we assume only one EAD item + let ead_res = parse_ead(plaintext_3, offset + MAC_LENGTH_3); + if ead_res.is_ok() { + ead_3 = ead_res.unwrap(); + error = EDHOCError::Success; + } else { + error = ead_res.unwrap_err(); + } + } else if plaintext_3.len == (offset + MAC_LENGTH_3) { error = EDHOCError::Success; } else { - error = ead_res.unwrap_err(); + error = EDHOCError::ParsingError; } - } else if plaintext_3.len == (2 + MAC_LENGTH_3) { - error = EDHOCError::Success; } else { error = EDHOCError::ParsingError; } @@ -965,7 +997,7 @@ fn decode_plaintext_3( } match error { - EDHOCError::Success => Ok((kid, mac_3, ead_3)), + EDHOCError::Success => Ok((id_cred_i, mac_3, ead_3)), _ => Err(error), } } @@ -1789,7 +1821,12 @@ mod tests { let plaintext_3_tv = BufferPlaintext3::from_hex(PLAINTEXT_3_TV); let kid_tv = ID_CRED_I_TV[ID_CRED_I_TV.len() - 1]; - let (kid, mac_3, ead_3) = decode_plaintext_3(&plaintext_3_tv).unwrap(); + let (id_cred_i, mac_3, ead_3) = decode_plaintext_3(&plaintext_3_tv).unwrap(); + + let kid = match id_cred_i { + IdCred::CompactKid(id_cred_i) => id_cred_i, + _ => panic!("Invalid ID_CRED_I"), + }; assert_eq!(mac_3, MAC_3_TV); assert_eq!(kid, kid_tv); From 2fbf6f7d9468e2715423301f2f91c21cdf6b50b6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mali=C5=A1a=20Vu=C4=8Dini=C4=87?= Date: Sun, 5 Nov 2023 14:52:40 +0100 Subject: [PATCH 2/3] Refactor r_process_message_3 per draft-tiloca-lake-implem-cons --- lib/src/edhoc.rs | 102 +++++++++++++++++++++++++++++++++++++++-------- lib/src/lib.rs | 2 +- 2 files changed, 86 insertions(+), 18 deletions(-) diff --git a/lib/src/edhoc.rs b/lib/src/edhoc.rs index f378ea46..ba9c54db 100644 --- a/lib/src/edhoc.rs +++ b/lib/src/edhoc.rs @@ -262,7 +262,7 @@ pub fn r_prepare_message_2( pub fn r_process_message_3( mut state: State, message_3: &BufferMessage3, - cred_i_expected: &[u8], + cred_i_expected: Option<&[u8]>, ) -> Result<(State, BytesHashLen), EDHOCError> { let State( mut current_state, @@ -278,6 +278,8 @@ pub fn r_process_message_3( ) = state; let mut error = EDHOCError::UnknownError; + let mut g_i: BytesP256ElemLen = Default::default(); + let mut cred_i = None; if current_state == EDHOCState::WaitMessage3 { let plaintext_3 = decrypt_message_3(&prk_3e2m, &th_3, message_3); @@ -287,26 +289,92 @@ pub fn r_process_message_3( let decoded_p3_res = decode_plaintext_3(&plaintext_3); if decoded_p3_res.is_ok() { + // The implementation currently supports the following two cases on handling the credentials: + // 1. R receives a kid and has a corresponding CRED_x passed in as cred_i_expected + // 2. R receives CRED_x by value in the message and uses it + // TODO: add support for fetching CRED_x based on kid received in the message let (id_cred_i, mac_3, ead_3) = decoded_p3_res.unwrap(); - // Step 3: If EAD is present make it available to the application - let ead_success = if let Some(ead_3) = ead_3 { - r_process_ead_3(ead_3).is_ok() - } else { - true - }; - if ead_success { - let (g_i, kid_i_expected) = parse_cred(cred_i_expected).unwrap(); // FIXME - - // compare the kid received with the kid expected in id_cred_i + // Processing of auth credentials according to draft-tiloca-lake-implem-cons + // Comments tagged with a number refer to steps in Section 4.3.1. of draft-tiloca-lake-implem-cons + cred_i = if let Some(cred_i_expected) = cred_i_expected { + // 1. Does ID_CRED_X point to a stored authentication credential? YES + // IMPL: compare cred_i_expected with id_cred + // IMPL: assume cred_i_expected is well formed + let (g_i_expected, kid_expected) = parse_cred(cred_i_expected).unwrap(); + g_i = g_i_expected; let credentials_match = match id_cred_i { - IdCred::CompactKid(kid) => kid == kid_i_expected, + IdCred::CompactKid(kid) => kid == kid_expected, IdCred::FullCredential(cred_i_received) => { cred_i_expected == cred_i_received } }; + // 2. Is this authentication credential still valid? + // IMPL,TODO: check cred_r_expected is still valid + + // Continue by considering CRED_X as the authentication credential of the other peer. + // IMPL: ready to proceed, including process ead_2 + if credentials_match { + Some(cred_i_expected) + } else { + None + } + } else { + // 1. Does ID_CRED_X point to a stored authentication credential? NO + // IMPL: cred_i_expected provided by application is None + // id_cred must be a full credential + if let IdCred::FullCredential(cred_i_received) = id_cred_i { + // 3. Is the trust model Pre-knowledge-only? NO (hardcoded to NO for now) + + // 4. Is the trust model Pre-knowledge + TOFU? YES (hardcoded to YES for now) + + // 6. Validate CRED_X. Generally a CCS has to be validated only syntactically and semantically, unlike a certificate or a CWT. + // Is the validation successful? + // IMPL: parse_cred(cred_r) and check it is valid + match parse_cred(cred_i_received) { + Ok((g_i_received, _kid_received)) => { + // 5. Is the authentication credential authorized for use in the context of this EDHOC session? + // IMPL,TODO: we just skip this step for now + + // 7. Store CRED_X as valid and trusted. + // Pair it with consistent credential identifiers, for each supported type of credential identifier. + // IMPL: cred_r = id_cred + g_i = g_i_received; + Some(cred_i_received) + } + Err(_) => None, + } + } else { + // IMPL: should have gotten a full credential + None + } + }; + + // 8. Is this authentication credential good to use in the context of this EDHOC session? + // IMPL,TODO: we just skip this step for now + + // IMPL: stop if cred_r is None + if let Some(valid_cred_i) = cred_i { + // Phase 2: + // - Process EAD_X items that have not been processed yet, and that can be processed before message verification + // IMPL: we are sure valid_cred_i is a full credential + + // Step 3: If EAD is present make it available to the application + let ead_res = if let Some(ead_3) = ead_3 { + // IMPL: if EAD-zeroconf is present, then id_cred must contain a full credential + // at this point, in case of EAD = zeroconf, if it works it means that: + // - the Voucher has been verified + // - the received valid_cred_i (aka cred_i) has been authenticated + r_process_ead_3(ead_3) + } else { + Ok(()) + }; + + if ead_res.is_ok() { + // verify mac_3 + // compute salt_4e3m let salt_4e3m = compute_salt_4e3m(&prk_3e2m, &th_3); // TODO compute prk_4e3m @@ -316,14 +384,14 @@ pub fn r_process_message_3( let expected_mac_3 = compute_mac_3( &prk_4e3m, &th_3, - &get_id_cred(cred_i_expected), - cred_i_expected, + &get_id_cred(valid_cred_i), + valid_cred_i, ); // verify mac_3 if mac_3 == expected_mac_3 { error = EDHOCError::Success; - let th_4 = compute_th_4(&th_3, &plaintext_3, cred_i_expected); + let th_4 = compute_th_4(&th_3, &plaintext_3, valid_cred_i); let mut th_4_buf: BytesMaxContextBuffer = [0x00; MAX_KDF_CONTEXT_LEN]; th_4_buf[..th_4.len()].copy_from_slice(&th_4[..]); @@ -365,10 +433,10 @@ pub fn r_process_message_3( error = EDHOCError::MacVerificationFailed; } } else { - error = EDHOCError::UnknownPeer; + error = EDHOCError::EADError; } } else { - error = EDHOCError::EADError; + error = EDHOCError::UnknownPeer; } } else { error = decoded_p3_res.unwrap_err(); diff --git a/lib/src/lib.rs b/lib/src/lib.rs index 1368bf4d..22af7631 100644 --- a/lib/src/lib.rs +++ b/lib/src/lib.rs @@ -99,7 +99,7 @@ impl<'a> EdhocResponderState<'a> { self: &mut EdhocResponderState<'a>, message_3: &BufferMessage3, ) -> Result<[u8; SHA256_DIGEST_LEN], EDHOCError> { - match r_process_message_3(self.state, message_3, self.cred_i.unwrap()) { + match r_process_message_3(self.state, message_3, self.cred_i) { Ok((state, prk_out)) => { self.state = state; Ok(prk_out) From 0db3145f9869edd8d5eddbe9fb3f70946284ca14 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mali=C5=A1a=20Vu=C4=8Dini=C4=87?= Date: Mon, 6 Nov 2023 15:00:47 +0100 Subject: [PATCH 3/3] fix: Fix CI fstar generation based on env var. --- .github/workflows/build-and-test.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/build-and-test.yml b/.github/workflows/build-and-test.yml index f5645312..379f4a01 100644 --- a/.github/workflows/build-and-test.yml +++ b/.github/workflows/build-and-test.yml @@ -66,7 +66,7 @@ jobs: needs: unit-tests runs-on: ubuntu-latest if: >- - vars.SHOULD_GENERATE_FSTAR == 1 && + ${{ vars.SHOULD_GENERATE_FSTAR == ‘true’ }} && ((github.event_name == 'workflow_dispatch') || (github.event_name == 'push' && startsWith(github.event.ref, 'refs/tags'))) steps: