消息 B 显示分析细节

消息 B, 由 响应者 发送, 不受益于发送者认证，不提供信息完整性。它可能是由任何一方发送的，包括主动攻击者. 信息内容受益于一些信息保密和一些转发保密，但不足以抵御任何主动攻击者. 0,1

消息 C 显示分析细节

消息 C, 由 发起者 发送, 不受益于发送者认证，不提供信息完整性。它可能是由任何一方发送的，包括主动攻击者. 信息内容受益于一些信息保密和一些转发保密，但不足以抵御任何主动攻击者. 0,1

消息 D 显示分析细节

消息 D, 由 响应者 发送, 不受益于发送者认证，不提供信息完整性。它可能是由任何一方发送的，包括主动攻击者. 信息内容受益于一些信息保密和一些转发保密，但不足以抵御任何主动攻击者. 0,1

生成用于形式化验证的密码学模型

获取模型 活动的攻击者 获取模型 被动攻击者 (passive attacker)

生成安全协议执行代码

获取实现 Go 语言实现 获取实现 Rust 语言实现

为 WebAssembly 构建生成的 Rust 实现代码。

获取实现 Wasm 实现