Message Pattern Analysis

Message B is the second message in the NX Noise Handshake Pattern. It is sent from the responder to the initiator. In this detailed analysis, we attempt to give you some insight into the protocol logic underlying this message. The insight given here does not fully extend down to fully illustrate the exact state transformations conducted by the formal model, but it does describe them at least informally in order to help illustrate how Message B affects the protocol.

Sending Message B

In the applied pi calculus, the initiator's process prepares Message B using the following function:

letfun writeMessage_b(me:principal, them:principal, hs:handshakestate, payload:bitstring, sid:sessionid) = let (ss:symmetricstate, s:keypair, e:keypair, rs:key, re:key, psk:key, initiator:bool) = handshakestateunpack(hs) in let (ne:bitstring, ns:bitstring, ciphertext:bitstring) = (empty, empty, empty) in let e = generate_keypair(key_e(me, them, sid)) in let ne = key2bit(getpublickey(e)) in let ss = mixHash(ss, ne) in (* No PSK, so skipping mixKey *) let ss = mixKey(ss, dh(e, re)) in let s = generate_keypair(key_s(me)) in let (ss:symmetricstate, ns:bitstring) = encryptAndHash(ss, key2bit(getpublickey(s))) in let ss = mixKey(ss, dh(s, re)) in let (ss:symmetricstate, ciphertext:bitstring) = encryptAndHash(ss, payload) in let hs = handshakestatepack(ss, s, e, rs, re, psk, initiator) in let message_buffer = concat3(ne, ns, ciphertext) in let (ssi:symmetricstate, cs1:cipherstate, cs2:cipherstate) = split(ss) in (hs, message_buffer, cs1, cs2).

How each token is processed by the responder:

• e: Signals that the responder is sending a fresh ephemeral key share as part of this message. This token adds the following state transformations to writeMessage_b:
• • mixHash, which hashes the new key into the session hash.

• ee: Signals that the responder is calculating a Diffie-Hellman shared secret derived from the initiator's ephemeral key and the responder's ephemeral key as part of this message. This token adds the following state transformations to writeMessage_b:
• • mixKey, which calls the HKDF function using, as input, the existing SymmetricState key, and dh(e, re), the Diffie-Hellman share calculated from the initiator's ephemeral key and the responder's ephemeral key.

• s: Signals that the responder is sending a static key share as part of this message. This token adds the following state transformations to writeMessage_b:
• • encryptAndHash is called on the static public key. If any prior Diffie-Hellman shared secret was established between the sender and the recipient, this allows the responder to communicate their long-term identity with some degree of confidentiality.

• es: Signals that the responder is calculating a Diffie-Hellman shared secret derived from the initiator's ephemeral key and the responder's static key as part of this message. This token adds the following state transformations to writeMessage_b:
• • mixKey, which calls the HKDF function using, as input, the existing SymmetricState key, and dh(e, rs), the Diffie-Hellman share calculated from the initiator's ephemeral key and the responder's static key.

Message B's payload, which is modeled as the output of the function msg_a(initiatorIdentity, responderIdentity, sessionId), is encrypted as ciphertext2. This invokes the following operations:

• encryptAndHash, which performs an authenticated encryption with added data (AEAD) on the payload, with the session hash as the added data (encryptWithAd) and mixHash, which hashes the encrypted payload into the next session hash.

Receiving Message B

In the applied pi calculus, the initiator's process prepares Message B using the following function:

letfun readMessage_b(me:principal, them:principal, hs:handshakestate, message:bitstring, sid:sessionid) = let (ss:symmetricstate, s:keypair, e:keypair, rs:key, re:key, psk:key, initiator:bool) = handshakestateunpack(hs) in let (ne:bitstring, ns:bitstring, ciphertext:bitstring) = deconcat3(message) in let valid1 = true in let re = bit2key(ne) in let ss = mixHash(ss, key2bit(re)) in (* No PSK, so skipping mixKey *) let ss = mixKey(ss, dh(e, re)) in let (ss:symmetricstate, ne:bitstring, valid1:bool) = decryptAndHash(ss, ns) in let rs = bit2key(ne) in let ss = mixKey(ss, dh(e, rs)) in let (ss:symmetricstate, plaintext:bitstring, valid2:bool) = decryptAndHash(ss, ciphertext) in if ((valid1 && valid2) && (rs = getpublickey(generate_keypair(key_s(them))))) then ( let hs = handshakestatepack(ss, s, e, rs, re, psk, initiator) in let (ssi:symmetricstate, cs1:cipherstate, cs2:cipherstate) = split(ss) in (hs, plaintext, true, cs1, cs2) ).

How each token is processed by the initiator:

• e: Signals that the initiator is receiving a fresh ephemeral key share as part of this message. This token adds the following state transformations to readMessage_b:
• • mixHash, which hashes the new key into the session hash.

• ee: Signals that the initiator is calculating a Diffie-Hellman shared secret derived from the initiator's ephemeral key and the responder's ephemeral key as part of this message. This token adds the following state transformations to readMessage_b:
• • mixKey, which calls the HKDF function using, as input, the existing SymmetricState key, and dh(e, re), the Diffie-Hellman share calculated from the initiator's ephemeral key and the responder's ephemeral key.

• s: Signals that the initiator is receiving a static key share as part of this message. This token adds the following state transformations to readMessage_b:
• • encryptAndHash is called on the static public key. If any prior Diffie-Hellman shared secret was established between the sender and the recipient, this allows the responder to communicate their long-term identity with some degree of confidentiality.

• es: Signals that the initiator is calculating a Diffie-Hellman shared secret derived from the initiator's ephemeral key and the responder's static key as part of this message. This token adds the following state transformations to readMessage_b:
• • mixKey, which calls the HKDF function using, as input, the existing SymmetricState key, and dh(e, rs), the Diffie-Hellman share calculated from the initiator's ephemeral key and the responder's static key.

Message B's payload, which is modeled as the output of the function msg_a(initiatorIdentity, responderIdentity, sessionId), is encrypted as ciphertext2. This invokes the following operations:

• decryptAndHash, which performs an authenticated decryption with added data (AEAD) on the payload, with the session hash as the added data (decryptWithAd) and mixHash, which hashes the encrypted payload into the next session hash.

Queries and Results

Message B is tested against four authentication queries and five confidentiality queries.

Authentication Grade 1: Passed

RESULT event(RecvMsg(alice,bob,stagepack_b(sid_a),m)) ==> event(SendMsg(bob,c_1108,stagepack_b(sid_b),m)) || event(LeakS(phase0,bob)) is true.

In this query, we test for sender authentication and message integrity. If Alice receives a valid message from Bob, then Bob must have sent that message to someone, or Bob had their static key compromised before the session began, or Alice had their long term keys, which are not used, compromised before the session began.

Authentication Grade 2: Passed

RESULT event(RecvMsg(alice,bob,stagepack_b(sid_a),m)) ==> event(SendMsg(bob,c_1108,stagepack_b(sid_b),m)) || event(LeakS(phase0,bob)) is true.

In this query, we test for sender authentication and is Key Compromise Impersonation resistance. If Alice receives a valid message from Bob, then Bob must have sent that message to someone, or Bob had their long term keys, which are not used, compromised before the session began.

Authentication Grade 3: Failed

RESULT event(RecvMsg(alice,bob,stagepack_b(sid_a),m)) ==> event(SendMsg(bob,alice,stagepack_b(sid_b),m)) || event(LeakS(phase0,bob)) cannot be proved.

In this query, we test for sender and receiver authentication and message integrity. If Alice receives a valid message from Bob, then Bob must have sent that message to Alice specifically, or Bob had their static key compromised before the session began, or Alice had their long term keys, which are not used, compromised before the session began.

Authentication Grade 4: Failed

RESULT event(RecvMsg(alice,bob,stagepack_b(sid_a),m)) ==> event(SendMsg(bob,alice,stagepack_b(sid_b),m)) || event(LeakS(phase0,bob)) cannot be proved.

In this query, we test for sender and receiver authentication and is Key Compromise Impersonation resistance. If Alice receives a valid message from Bob, then Bob must have sent that message to Alice specifically, or Bob had their static key compromised before the session began.

Confidentiality Grade 1: Passed

RESULT not attacker_p1(msg_b(bob,alice,sid_b)) is true.

In this query, we test for message secrecy by checking if a passive attacker is able to retrieve the payload plaintext only by compromising Alice's long term keys, which are not used, either before or after the protocol session.

Confidentiality Grade 2: Failed

RESULT not attacker_p1(msg_b(bob,alice,sid_b)) cannot be proved.

In this query, we test for message secrecy by checking if an active attacker is able to retrieve the payload plaintext only by compromising Alice's long term keys, which are not used, either before or after the protocol session.

Confidentiality Grade 3: Passed

RESULT attacker_p1(msg_b(bob,alice,sid_b)) ==> event(LeakS(phase0,alice)) || (event(LeakS(px,alice)) && event(LeakS(pz,bob))) is true.

In this query, we test for forward secrecy by checking if a passive attacker is able to retrieve the payload plaintext only by compromising Alice's long term keys, which are not used, before the protocol session, or after the protocol session along with Bob's static key at any time.

Confidentiality Grade 4: Failed

RESULT attacker_p1(msg_b(bob,alice,sid_b)) ==> event(LeakS(phase0,alice)) || (event(LeakS(px,alice)) && event(LeakS(pz,bob))) cannot be proved.

In this query, we test for weak forward secrecy by checking if an active attacker is able to retrieve the payload plaintext only by compromising Alice's long term keys, which are not used, before the protocol session, or after the protocol session along with Bob's static key at any time.

Confidentiality Grade 5: Failed

RESULT not attacker_p1(msg_b(bob,alice,sid_b)) cannot be proved.

In this query, we test for strong forward secrecy by checking if an active attacker is able to retrieve the payload plaintext only by compromising Alice's long term keys, which are not used, before the protocol session.