消息模式分析

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

发送中的 消息 A

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

letfun writeMessage_a(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, rs)) in let ss = mixKey(ss, dh(s, rs)) 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).

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

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

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

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

如果静态公钥作为此消息的一部分进行了通信，那么它将被加密为 ciphertext1。然而，由于发起者在这里没有传递静态公钥，因此该值将被留为空值。

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

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

接受中的 消息 A

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

letfun readMessage_a(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(s, re)) in let ss = mixKey(ss, dh(s, rs)) 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 let (ssi:symmetricstate, cs1:cipherstate, cs2:cipherstate) = split(ss) in (hs, plaintext, true, cs1, cs2) ).

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

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

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

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

如果静态公钥作为此消息的一部分进行了通信，那么它将被加密为 ciphertext1。然而，由于发起者在这里没有传递静态公钥，因此该值将被留为空值。

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

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

请求与结果

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

身份认证等级 1: 通过

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

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

身份认证等级 2: 失败

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

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

身份认证等级 3: 通过

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

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

身份认证等级 4: 失败

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

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

保密等级 1: 通过

RESULT attacker_p1(msg_a(alice,bob,sid_a)) ==> event(LeakS(px,bob)) is true.

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

保密等级 2: 通过

RESULT attacker_p1(msg_a(alice,bob,sid_a)) ==> event(LeakS(px,bob)) is true.

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

保密等级 3: 失败

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

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

保密等级 4: 失败

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

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

保密等级 5: 失败

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

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