<div dir="ltr">Dear friends, colleagues and fellow enthusiasts,<br>I hereby present to you research that I have been preparing for some time. I kindly request your assessment and feedback at this stage.<br><br>Noise was introduced by Trevor as a framework for designing and building cryptographic protocols. Supporting advanced protocol features, Noise reduces the task of describing protocols to a small language where messages over the network, Diffie-Hellman operations and key management are explicit, but where the rest (state management, record hashing, etc.) is completely implicit and handled by a set of derived rules. Noise has been used as the foundation for WireGuard and for WhatsApp's wire protocol and has established a promising new method in which to reason about cryptographic protocol design.<br><br>Noise Explorer is a new software engine for reasoning about Noise Handshake Patterns. Noise Explorer allows to:<br>   <br>    - Design Noise Handshake Patterns. This allows for immediate validity checks that verify if the design strictly conforms to the original Noise specification (for example, preventing a static public key from being communicated twice), as well as convenient visualizations.<br><br>    - Generate Cryptographic Models for Formal Verification. Instantly generate full symbolic models in the applied pi calculus for any Noise Handshake Pattern. Using the ProVerif protocol verifier, 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 the 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.<br><br>    - 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.<br><br>In addition to the above, Noise Explorer will also soon also automatically generate a secure implementation of the user's chosen Noise Handshake Pattern design, written in ProScript, a secure subset of JavaScript.<br><div><br></div><div>Please access Noise Explorer using this address: <a href="https://noiseexplorer.com">https://noiseexplorer.com</a><br></div><div><br></div><div>Regarding the compendium of patterns included on the website, I also request that you send me additional Noise Handshake Patterns, so that I can use Noise Explorer to generate formal models, pretty HTML results, and then post these too in the compendium: let's keep the compendium growing with more and more information and formal analysis of all kinds of different Noise Handshake Patterns!</div><div><br></div><div>
Soon, more details will follow in which I will discuss and justify the 
chosen translation rules from Noise to the applied pi calculus. I will 
describe the reasoning behind our top-level process generation and 
queries for sophisticated authenticity and confidentiality goals, among 
other more academic details.

<br></div><div>
<div><br></div><div>I look forward to reading your feedback so that 
Noise Explorer can reach its full potential of being the ultimate online
 compendium for reasoning about, designing, studying, implementing and 
proving the various Noise Handshake Patterns that we can now design 
thanks to Trevor's wonderful work.</div>

</div><br>Nadim Kobeissi<br>Symbolic Software • <a href="https://symbolic.software">https://symbolic.software</a><br>Sent from office</div>