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. Immediately obtain validity checks that verify if your design conforms to the specification. Also, a convenient illustration in your browser.
• Generate Cryptographic Models for Formal Verification. 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. The models can also be used as a foundation for further modeling in CryptoVerif.
• 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.

Design your Noise Handshake Pattern

Download Cryptographic Models for Formal Verification

Download Model active attacker Download Model passive attacker

Download Secure Protocol Implementation Code

Soon, Noise Explorer will also automatically generate a secure implementation of your chosen Noise Handshake Pattern design, written in ProScript, a secure subset of JavaScript.