Noise Explorer beta

menu

设计新的模式 探索模式 命令行工具 科学论文

IKpsk2

s ... a e, es, s, ss b e, ee, se, psk c d

设计与探索 Noise 握手模式

Noise Explorer 是一个在线引擎，用于推理 Noise Protocol Framework (版本 34) 握手模式。 Noise Explorer 允许你：

• 设计 Noise 握手模式。 获取有效性检查，以验证你的设计是否符合规范。
• 生成形式化验证模型。 立即为任何你输入的 Noise 握手模式生成应用 pi 演算中的完整符号模型。 使用 ProVerif，这些模型可以针对具有恶意主体的被动和主动攻击者进行分析。 该模型的顶层进程和复杂的查询专门生成，与你的 Noise 握手模式相关，包括对强与弱的前向保密性和抵抗密钥泄露假冒的测试。
• 探索形式化验证结果的纲要。 由于复杂 Noise 握手模式的形式化验证可能需要时间并需要快速 CPU 硬件，因此 Noise Explorer 提供了一个纲要，详细说明了原始规范中描述的所有 Noise 握手模式的完整结果。 这些结果以比原始规范更全面的安全模型呈现，因为它包括恶意主体的参与。
• 生成安全软件实现。 Noise Explorer 可以自动生成你选择的 Noise 握手模式设计的安全实现，以 Go 或 Rust 编写。

设计你的 Noise 握手模式

IKpsk2: <- s ... -> e, es, s, ss <- e, ee, se, psk -> <-

解析成功完成。

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

获取主动攻击者模型 获取被动攻击者模型

生成安全协议实现代码

获取 Go 编写的实现 获取 Rust 编写的实现

生成用于 WebAssembly 构建的 Rust 实现代码

获取为 wasm 编写的实现

关于 Noise Explorer Symbolic Software | INRIA