Noise Explorer: a push-button online engine for designing and formally verifying any Noise protocol.
The Noise Protocol Framework1 has contributed to the evolution of secure channel protocol design ever since its introduction in 2015, being integrated into class-leading secure networking tools such as WireGuard and secure messengers such as WhatsApp. Now, Symbolic Software presents Noise Explorer, an online engine for securely designing, prototyping and formally verifying any Noise protocol using a full-featured interface.
Start using Noise Explorer.
View a formal verification report generated by Noise Explorer.
Design Noise Handshake Patterns.
You've got a secure channel use case and want to design your own Noise protocol to match it. Using Noise Explorer, you can immediately obtain validity checks that verify if your design conforms to the specification. Also, a convenient illustration in your browser. From there, generating formal models is a push-button affair.
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 ProVerif2, 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.
Collaborating and contributing to the Noise Protocol Framework.
Ever since Noise Explorer's release, we have collaborated with the authors of the Noise Protocol Framework to provide the first comprehensive formal verification results for all Noise Handshake Patterns. They are now listed in the original Noise Protocol Framework specification. We plan to continue this collaboration as new versions of the specification are released.
[1] While Noise Explorer is developed by Symbolic Software, the Noise Protocol Framework is not.
[2] ProVerif is developed by the PROSECCO research team at INRIA, who have also provided invaluable insight and assistance with the development of Noise Explorer.