Skip to content

Commit

Permalink
Merge branch 'main' into crypto-as-trait-2
Browse files Browse the repository at this point in the history
  • Loading branch information
@chrysn
chrysn committed Nov 9, 2023
2 parents 71b3e52 + da310f4 commit bd426ed
Show file tree
Hide file tree
Showing 3 changed files with 144 additions and 43 deletions.
9 changes: 5 additions & 4 deletions .github/workflows/build-and-test.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -65,9 +65,10 @@ jobs:
generate-fstar:
needs: unit-tests
runs-on: ubuntu-latest
if: >-
vars.SHOULD_GENERATE_FSTAR == 1 &&
((github.event_name == 'workflow_dispatch') || (github.event_name == 'push' && startsWith(github.event.ref, 'refs/tags')))
if: false
# FIXME: commenting out until we fix hax execution
# if: >-
# ((github.event_name == 'workflow_dispatch') || (github.event_name == 'push' && startsWith(github.event.ref, 'refs/tags')))

steps:
- name: Checkout edhoc-rs
Expand All @@ -85,7 +86,7 @@ jobs:

- name: Generate fstar code using the main library and the hacspec crypto backend
run: |
docker run --rm -v ${{ github.workspace }}:/edhoc-rs hacspec-v2 bash -c "cd edhoc-rs && cargo-hax -C -p edhoc-rs -p edhoc-crypto -p edhoc-ead --no-default-features --features="crypto-hacspec, ead-none" --release \; into -i '-c_wrapper::** -edhoc_rs::generate_connection_identifier_cbor -edhoc_rs::generate_connection_identifier' fstar"
docker run --rm -v ${{ github.workspace }}:/edhoc-rs hacspec-v2 bash -c "cd edhoc-rs && cargo-hax -C -p edhoc-rs -p edhoc-crypto -p edhoc-ead-none --no-default-features --features="crypto-hacspec, ead-none" --release \; into -i '-c_wrapper::** -edhoc_rs::generate_connection_identifier_cbor -edhoc_rs::generate_connection_identifier' fstar"
zip -j -r edhoc-rs-fstar.zip $(find . -name *fst)
- name: Upload artifact
Expand Down
171 changes: 138 additions & 33 deletions lib/src/edhoc.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -276,7 +276,7 @@ pub fn r_process_message_3(
mut state: State,
crypto: &mut impl CryptoTrait,
message_3: &BufferMessage3,
cred_i_expected: &[u8],
cred_i_expected: Option<&[u8]>,
) -> Result<(State, BytesHashLen), EDHOCError> {
let State(
mut current_state,
Expand All @@ -292,6 +292,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(crypto, &prk_3e2m, &th_3, message_3);
Expand All @@ -301,19 +303,92 @@ 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();
// 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();

// 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_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

// 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()
if credentials_match {
Some(cred_i_expected)
} else {
None
}
} else {
true
// 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
}
};
if ead_success {
let (g_i, kid_i) = parse_cred(cred_i_expected).unwrap(); // FIXME

// compare the kid received with the kid expected in id_cred_i
if kid == kid_i {
// 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(crypto, &prk_3e2m, &th_3);
// TODO compute prk_4e3m
Expand All @@ -324,14 +399,14 @@ pub fn r_process_message_3(
crypto,
&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(crypto, &th_3, &plaintext_3, cred_i_expected);
let th_4 = compute_th_4(crypto, &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[..]);
Expand Down Expand Up @@ -380,10 +455,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();
Expand Down Expand Up @@ -971,33 +1046,58 @@ fn edhoc_kdf(

fn decode_plaintext_3(
plaintext_3: &BufferPlaintext3,
) -> Result<(u8, BytesMac3, Option<EADItem>), EDHOCError> {
) -> Result<(IdCred, BytesMac3, Option<EADItem>), EDHOCError> {
let mut ead_3 = None::<EADItem>;
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;
}
Expand All @@ -1006,7 +1106,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),
}
}
Expand Down Expand Up @@ -1906,7 +2006,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);
Expand Down
7 changes: 1 addition & 6 deletions lib/src/lib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -101,12 +101,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,
&mut default_crypto(),
message_3,
self.cred_i.unwrap(),
) {
match r_process_message_3(self.state, &mut default_crypto(), message_3, self.cred_i) {
Ok((state, prk_out)) => {
self.state = state;
Ok(prk_out)
Expand Down

0 comments on commit bd426ed

Please sign in to comment.