Noise Explorer: Design and Explore Noise Handshake Patterns

Noise Explorer is an online engine for reasoning about Noise Protocol Framework (revision 34) Handshake Patterns. It lets you design Noise handshake patterns, validate them against the specification, generate formal verification models in applied pi calculus (analyzable against passive and active attackers with malicious principals), explore a compendium of formal verification results (including all patterns from the original spec), and generate secure implementations in Go or Rust, even for WebAssembly.