Message B is the second message in the XK 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.
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 (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).
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 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:
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, 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) ).
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 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:
RESULT event(RecvMsg(alice,bob,stagepack_b(sid_a),m)) ==> event(SendMsg(bob,c_1277,stagepack_b(sid_b),m)) || event(LeakS(phase0,bob)) || event(LeakS(phase0,alice)) 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 static key compromised before the session began.
RESULT event(RecvMsg(alice,bob,stagepack_b(sid_a),m)) ==> event(SendMsg(bob,c_1277,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 static key compromised before the session began.
RESULT event(RecvMsg(alice,bob,stagepack_b(sid_a),m)) ==> event(SendMsg(bob,alice,stagepack_b(sid_b),m)) || event(LeakS(phase0,bob)) || event(LeakS(phase0,alice)) 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 static key compromised before the session began.
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.
RESULT attacker_p1(msg_b(bob,alice,sid_b)) ==> event(LeakS(px,alice)) 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 static key either before or after the protocol session.
RESULT attacker_p1(msg_b(bob,alice,sid_b)) ==> event(LeakS(px,alice)) 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 static key either before or after the protocol session.
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 static key before the protocol session, or after the protocol session along with Bob's static key at any time.
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 static key before the protocol session, or after the protocol session along with Bob's static key at any time.
RESULT attacker_p1(msg_b(bob,alice,sid_b)) ==> event(LeakS(phase0,alice)) 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 static key before the protocol session.