Noise Explorer
Noise Explorer is an online engine for reasoning about Noise Protocol Framework Handshake Patterns. The Noise Explorer command-line tool can parse Noise Handshake Patterns according to the original specification. It can generate cryptographic models for formal verification, including security queries, top-level processes and malicious principals, for testing against an active or passive attacker. Noise Explorer can also generate fully functional discrete implementations for any Noise Handshake Pattern, written in the Go and Rust programming languages. Noise Explorer can also render results from the ProVerif output into an elegant and easy to read HTML format: the pattern results that can be explored on Noise Explorer were generated using the Noise Explorer command-line tool. 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.
