Symbolic Software

Noise Explorer: 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.
Read the Noise Explorer scientific paper.
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.

Generate secure implementations in Rust and Go.

Noise Explorer can also automatically generate software implementations for arbitrary Noise Handshake Patterns. We target Go and Rust for code generation given their relevance in systems where secure channel protocols are frequently required as well as their adoption by Mozilla, Google, CloudFlare, Facebook and others.
Noise Explorer’s ability to generate software implementations complements its ability to assist with designing and formally verifying handshake patterns: immediately after the pattern is designed and its security guarantees are ascertained, it can be prototyped in production systems with a software implementation that is safe to use.

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.