消息模式分析

消息 B 是在 XX Noise 握手模式中的第 二 条消息。是由响应者发给发起者的。 在此详细分析中，我们试图给您一些关于此消息背后协议逻辑的见解。这里给出的见解并不能完全扩展到完全说明形式化模型所进行的确切的状态转换，但至少进行了非正式的描述，以帮助说明消息 B 如何影响协议。

发送中的 消息 B

在应用Π计算的过程中，发起者过程使用以下函数准备消息：B。

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

令牌被响应者处理的方式：

• e：表示响应者是发送 一个新的临时密钥共享作为这个消息的一部分。此令牌将以下状态转换添加到 writeMessage_b：
• • mixHash，将新的密钥哈希到会话哈希中。

• ee：表示响应者是计算 一个由发起者产生的 Diffie-Hellman 共享密钥 临时密钥与响应者的临时密钥作为这个消息的一部分。此令牌将以下状态转换添加到 writeMessage_b：
• • mixKey，使用现有的SymmetricState密钥和从发起者的 临时密钥与响应者的临时密钥 计算出的 Diffie-Hellman dh(e, re) 作为输入，调用HKDF函数。

• s：表示响应者是发送 一个静态密钥共享作为这个消息的一部分。此令牌将以下状态转换添加到 writeMessage_b：
• • encryptAndHash，被在静态公钥上调用。如果发送者和接收者之间事先建立了任何 Diffie-Hellman 共享密钥，这将允许响应者以某种程度的保密性来传达他们的长期身份。

• es：表示响应者是计算 一个由发起者产生的 Diffie-Hellman 共享密钥 临时密钥与响应者的静态密钥作为这个消息的一部分。此令牌将以下状态转换添加到 writeMessage_b：
• • mixKey，使用现有的SymmetricState密钥和从发起者的 临时密钥与响应者的静态密钥 计算出的 Diffie-Hellman dh(e, rs) 作为输入，调用HKDF函数。

消息B的载荷被建模为函数msg_a(发起者身份, 响应者身份, 会话ID)的输出，被加密为ciphertext2。这将调用以下操作：

• encryptAndHash 在有效载荷上执行带有附加数据的验证加密(AEAD)，并将会话哈希作为附加数据(encryptWithAd)和mixHash，它将加密后的有效载荷哈希到下一个会话哈希中。

接受中的 消息 B

在应用Π计算的过程中，发起者过程使用以下函数准备消息：B。

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 (hs, plaintext, true) ).

令牌被发起者处理的方式：

• e：表示发起者是接收 一个新的临时密钥共享作为这个消息的一部分。此令牌将以下状态转换添加到 readMessage_b：
• • mixHash，将新的密钥哈希到会话哈希中。

• ee：表示发起者是计算 一个由发起者产生的 Diffie-Hellman 共享密钥 临时密钥与响应者的临时密钥作为这个消息的一部分。此令牌将以下状态转换添加到 readMessage_b：
• • mixKey，使用现有的SymmetricState密钥和从发起者的 临时密钥与响应者的临时密钥 计算出的 Diffie-Hellman dh(e, re) 作为输入，调用HKDF函数。

• s：表示发起者是接收 一个静态密钥共享作为这个消息的一部分。此令牌将以下状态转换添加到 readMessage_b：
• • encryptAndHash，被在静态公钥上调用。如果发送者和接收者之间事先建立了任何 Diffie-Hellman 共享密钥，这将允许响应者以某种程度的保密性来传达他们的长期身份。

• es：表示发起者是计算 一个由发起者产生的 Diffie-Hellman 共享密钥 临时密钥与响应者的静态密钥作为这个消息的一部分。此令牌将以下状态转换添加到 readMessage_b：
• • mixKey，使用现有的SymmetricState密钥和从发起者的 临时密钥与响应者的静态密钥 计算出的 Diffie-Hellman dh(e, rs) 作为输入，调用HKDF函数。

消息B的载荷被建模为函数msg_a(发起者身份, 响应者身份, 会话ID)的输出，被加密为ciphertext2。这将调用以下操作：

• decryptAndHash 在有效载荷上执行带有附加数据的验证解密(AEAD)，并将会话哈希作为附加数据(decryptWithAd)和mixHash，它将加密后的有效载荷哈希到下一个会话哈希中。

请求与结果

消息B是针对4个认证查询和5个保密查询进行测试。

身份认证等级 1: 通过

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

在这个查询中，我们测试发送者身份认证和消息完整性。如果Alice收到Bob的有效消息，那么Bob一定是将该消息发送给了某人，或者Bob在会话开始之前，他们的静态密钥就已经泄露了，或者Alice在会话开始之前，他们的静态密钥就已经泄露了

身份认证等级 2: 通过

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

在这个查询中，我们测试发送者身份认证与其是否抵抗假冒密钥。如果Alice收到Bob的有效消息，那么Bob一定是将该消息发送给了某人，或者Bob在会话开始之前，他们的静态密钥已经被泄露了。

身份认证等级 3: 失败

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.

在这个查询中，我们测试发送者和接收者的身份验证以及消息的完整性。如果Alice收到Bob发来的有效消息，那么Bob一定是向Alice，或者Bob在会话开始之前，他们的静态密钥就已经被泄露了，或者Alice在会话开始之前，他们的静态密钥就已经被泄露了。

身份认证等级 4: 失败

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.

在这个查询中，我们测试发送者和接收者的身份验证以及是否抵抗假冒密钥。如果Alice收到Bob的有效消息，那么Bob一定是将该消息发送给Alice专门发送了该消息，或者Bob在会话开始之前，他们的静态密钥已经被泄露了

保密等级 1: 通过

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

在这个查询中，我们通过检查被动攻击者是否只能通过在协议会话之前或之后破坏Alice的静态密钥，来测试消息保密性。

保密等级 2: 失败

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

在这个查询中，我们测试消息保密性，检查主动攻击者是否只能通过在协议会话之前或之后破坏Alice的静态密钥来检索有效载荷的明文。

保密等级 3: 通过

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

在这个查询中，我们通过检查被动攻击者是否只能通过破坏Alice的lice来检索有效载荷明文来测试前向保密性。在协议会话之前后的任何时候与Bob的静态密钥一起进行检索。

保密等级 4: 失败

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

在这个查询中，我们通过检查主动攻击者是否只能通过破坏Alice的lice来检索有效载荷明文来测试弱前向保密性。在协议会话之前后的任何时候与Bob的静态密钥一起，都能检索到明文。

保密等级 5: 失败

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

在这个查询中，我们通过检查主动攻击者是否能够在协议会话之前只有通过破坏Alice的静态密钥来检索有效载荷明文来测试强前向保密性。