Design and Explore Noise Handshake Patterns

Noise Explorer is an online engine for reasoning about Noise Protocol Framework (revision 34) Handshake Patterns. Noise Explorer allows you to:

• Design Noise Handshake Patterns. Obtain validity checks that verify if your design conforms to the specification.
• Generate Formal Verification Models. Instantly generate full symbolic models in the applied pi calculus for any Noise Handshake Pattern that you enter. Using ProVerif, these models can be analyzed against passive and active attackers with malicious principals. The model's top-level process and sophisticated queries are specifically generated to be relevant to your Noise Handshake Pattern, including tests for strong vs. weak forward secrecy and resistance to key compromise impersonation.
• Explore a Compendium of Formal Verification Results. Since formal verification for complex Noise Handshake Patterns can take time and require fast CPU hardware, Noise Explorer comes with a compendium detailing the full results of all Noise Handshake Patterns described in the original specification. These results are presented with a security model that is even more comprehensive than the original specification, since it includes the participation of a malicious principal.
• Generate Secure Software Implementations. Noise Explorer can automatically generate a secure implementation of your chosen Noise Handshake Pattern design, written in Go or Rust.

Design your Noise Handshake Pattern

Generate Cryptographic Models for Formal Verification

Get Model active attacker Get Model passive attacker

Generate Secure Protocol Implementation Code

Get Implementation written in go Get Implementation written in rust

Generate Rust Implementation Code for WebAssembly Builds

Get Implementation written for wasm