IKpsk2

设计并探索 Noise 握手模式

Noise Explorer 用于推理 Noise 协议框架 (修订版 34) 握手模式的在线引擎。 Noise Explorer 允许您：

设计 Noise 握手模式。获得有效性检查，以验证您的设计是否符合规范。
生成形式化验证模型。针对您输入的任何噪声握手模式，在应用∏计算中即时生成完整的符号模型。使用 ProVerif，可以针对具有恶意原件的被动和主动攻击者分析这些模型。该模型的顶层流程和复杂的查询是专门生成的，与您的噪声握手模式相关，包括强与弱的前向保密性和抗密钥泄露冒充性测试。
探索形式化验证结果概要。由于复杂的噪声握手模式的形式化验证可能需要时间，并且需要快速的 CPU 硬件，因此 Noise Explorer 附带了一个简编，详细介绍了原始规范中描述的所有噪声握手模式的全部结果。这些结果与安全模型一起呈现，该模型甚至比原始规范更全面，因为它包括了恶意操作者的参与。
生成安全的软件实现。Noise Explorer 可以自动生成您所选择的 Noise 握手模式设计的安全实现，该设计以 Go或Rust 编写。