消息模式分析

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

发送中的 消息 C

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

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).

由于消息C不包含任何令牌，因此它被认为是纯粹的“应用数据”类型消息，旨在传输被加密的有效载荷。

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

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

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

接受中的 消息 C

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

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) ).

由于消息C不包含任何令牌，因此它被认为是纯粹的“应用数据”类型消息，旨在传输被加密的有效载荷。

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

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

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

请求与结果

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

身份认证等级 1: 通过

RESULT event(RecvMsg(bob,alice,stagepack_c(sid_b),m)) ==> event(SendMsg(alice,c_1211,stagepack_c(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_c(sid_b),m)) ==> event(SendMsg(alice,c_1211,stagepack_c(sid_a),m)) || event(LeakS(phase0,alice)) is true.

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

身份认证等级 3: 通过

RESULT event(RecvMsg(bob,alice,stagepack_c(sid_b),m)) ==> event(SendMsg(alice,bob,stagepack_c(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_c(sid_b),m)) ==> event(SendMsg(alice,bob,stagepack_c(sid_a),m)) || event(LeakS(phase0,alice)) is true.

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

保密等级 1: 通过

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

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

保密等级 2: 通过

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

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

保密等级 3: 通过

RESULT attacker_p1(msg_c(alice,bob,sid_a)) ==> event(LeakS(phase0,bob)) || (event(LeakS(phase1,bob)) && event(LeakS(p,alice))) is true.

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

保密等级 4: 通过

RESULT attacker_p1(msg_c(alice,bob,sid_a)) ==> event(LeakS(phase0,bob)) || (event(LeakS(phase1,bob)) && event(LeakS(p,alice))) is true.

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

保密等级 5: 通过

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

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