Noise Explorer beta

X1K

s ... a e, es b e, ee c s d se e f

握手模式分析

响应者用预共享的长期静态密钥进行初始化,假定发起者z可信信道上预先进行了认证。

消息 A 显示分析细节

消息 A, 由 发起者 发送, 不受益于发送者认证,不提供信息完整性。它可能是由任何一方发送的,包括主动攻击者. 消息内容得益于消息保密和一些前向保密:响应者的长期私钥泄露,即使在以后的日子里,也会导致消息内容被攻击者解密. 0,2

消息 B 显示分析细节

消息 B, 由 响应者 发送, 受益于发送者认证,并抗密钥泄露冒充。假设相应的私钥是安全的,这种认证是无法伪造的。但是,如果响应者与另外一个被泄露的发起者进行了单独的会话,那么这个另外的会话就可以用来伪造这个会话中发起者对这个消息的认证. 信息内容受益于一些信息保密和一些转发保密,但不足以抵御任何主动攻击者. 2,1

消息 C 显示分析细节

消息 C, 由 发起者 发送, 不受益于发送者认证,不提供信息完整性。它可能是由任何一方发送的,包括主动攻击者. 消息内容得益于消息保密强大的前向保密:如果临时私钥是安全的且响应者不是主动攻击者冒充的,消息内容就不能被解密. 0,5

消息 D 显示分析细节

消息 D, 由 响应者 发送, 受益于发送者和接收者认证,并抗密钥泄露冒充。假设相应的私人钥匙是安全的,这种认证是无法伪造的。. 在被动攻击者的情况下,消息内容受益于消息保密弱前向保密:如果响应者的长期静态密钥之前被泄露,那么发起者的长期静态密钥后来被泄露,就会导致消息内容被攻击者解密. 4,3

消息 E 显示分析细节

消息 E, 由 发起者 发送, 受益于发送者和接收者认证,并抗密钥泄露冒充。假设相应的私人钥匙是安全的,这种认证是无法伪造的。. 消息内容得益于消息保密强大的前向保密:如果临时私钥是安全的且响应者不是主动攻击者冒充的,消息内容就不能被解密. 4,5

消息 F 显示分析细节

消息 F, 由 响应者 发送, 受益于发送者和接收者认证,并抗密钥泄露冒充。假设相应的私人钥匙是安全的,这种认证是无法伪造的。. 消息内容得益于消息保密强大的前向保密:如果临时私钥是安全的且发起者不是主动攻击者冒充的,消息内容就不能被解密. 4,5

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

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

生成安全协议执行代码

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

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

获取实现 Wasm 实现