Message Pattern Analysis

Message C is the third message in the NNpsk2 Noise Handshake Pattern. It is sent from the initiator to the responder. 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 C affects the protocol.

Sending Message C

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

letfun writeMessage_c(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 (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 (hs, message_buffer).

Since Message C contains no tokens, it is considered purely an "AppData" type message meant to transfer encrypted payloads.

If a static public key was communicated as part of this message, it would have been encrypted as ciphertext1. However, since the initiator does not communicate a static public key here, that value is left empty.

Message C'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 C

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

letfun readMessage_c(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 (ss:symmetricstate, plaintext:bitstring, valid2:bool) = decryptAndHash(ss, ciphertext) in if ((valid1 && valid2)) then ( let hs = handshakestatepack(ss, s, e, rs, re, psk, initiator) in (hs, plaintext, true) ).

Since Message C contains no tokens, it is considered purely an "AppData" type message meant to transfer encrypted payloads.

If a static public key was communicated as part of this message, it would have been encrypted as ciphertext1. However, since the initiator does not communicate a static public key here, that value is left empty.

Message C'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 C is tested against four authentication queries and five confidentiality queries.

Authentication Grade 1: Passed

RESULT event(RecvMsg(bob,alice,stagepack_c(sid_b),m)) ==> event(SendMsg(alice,c_1117,stagepack_c(sid_a),m)) || event(LeakPsk(phase0,alice,bob)) || event(LeakPsk(phase0,alice,bob)) is true.

In this query, we test for sender authentication and message integrity. If Bob receives a valid message from Alice, then Alice must have sent that message to someone, or Alice had their PSK compromised before the session began, or Bob had their PSK compromised before the session began.

Authentication Grade 2: Passed

RESULT event(RecvMsg(bob,alice,stagepack_c(sid_b),m)) ==> event(SendMsg(alice,c_1117,stagepack_c(sid_a),m)) || event(LeakPsk(phase0,alice,bob)) is true.

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

Authentication Grade 3: Passed

RESULT event(RecvMsg(bob,alice,stagepack_c(sid_b),m)) ==> event(SendMsg(alice,bob,stagepack_c(sid_a),m)) || event(LeakPsk(phase0,alice,bob)) || event(LeakPsk(phase0,alice,bob)) is true.

In this query, we test for sender and receiver authentication and message integrity. If Bob receives a valid message from Alice, then Alice must have sent that message to Bob specifically, or Alice had their PSK compromised before the session began, or Bob had their PSK compromised before the session began.

Authentication Grade 4: Passed

RESULT event(RecvMsg(bob,alice,stagepack_c(sid_b),m)) ==> event(SendMsg(alice,bob,stagepack_c(sid_a),m)) || event(LeakPsk(phase0,alice,bob)) is true.

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

Confidentiality Grade 1: Passed

RESULT attacker_p1(msg_c(alice,bob,sid_a)) ==> event(LeakPsk(py,alice,bob)) 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 Bob's PSK either before or after the protocol session.

Confidentiality Grade 2: Passed

RESULT attacker_p1(msg_c(alice,bob,sid_a)) ==> event(LeakPsk(py,alice,bob)) is true.

In this query, we test for message secrecy by checking if an active attacker is able to retrieve the payload plaintext only by compromising Bob's PSK either before or after the protocol session.

Confidentiality Grade 3: Passed

RESULT attacker_p1(msg_c(alice,bob,sid_a)) ==> (event(LeakS(phase0,bob)) && event(LeakPsk(phase0,alice,bob))) || (event(LeakS(px,bob)) && event(LeakPsk(py,alice,bob)) && event(LeakS(pz,alice))) 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 Bob's PSK before the protocol session, or after the protocol session along with Alice's PSK at any time.

Confidentiality Grade 4: Failed

RESULT attacker_p1(msg_c(alice,bob,sid_a)) ==> (event(LeakS(phase0,bob)) && event(LeakPsk(phase0,alice,bob))) || (event(LeakS(px,bob)) && event(LeakPsk(py,alice,bob)) && event(LeakS(pz,alice))) 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 Bob's PSK before the protocol session, or after the protocol session along with Alice's PSK at any time.

Confidentiality Grade 5: Passed

RESULT attacker_p1(msg_c(alice,bob,sid_a)) ==> event(LeakPsk(phase0,alice,bob)) is true.

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 Bob's PSK before the protocol session.