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
parsing completed successfully.
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
