[noise] Noise Explorer

[Justin Cormack]

Can you add the one way patterns too? They should not take much compute...

Justin


On 22 May 2018 at 10:42, Nadim Kobeissi <nadim at symbolic.software> wrote:
> Dear friends, colleagues and fellow enthusiasts,
> I hereby present to you research that I have been preparing for some time. I
> kindly request your assessment and feedback at this stage.
>
> 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.
>
> Noise Explorer is a new software engine for reasoning about Noise Handshake
> Patterns. Noise Explorer allows to:
>
>     - 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.
>
>     - 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.
>
>     - 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.
>
> 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.
>
> Please access Noise Explorer using this address: https://noiseexplorer.com
>
> 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!
>
> 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.
>
> 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.
>
> Nadim Kobeissi
> Symbolic Software • https://symbolic.software
> Sent from office
>
> _______________________________________________
> Noise mailing list
> Noise at moderncrypto.org
> https://moderncrypto.org/mailman/listinfo/noise
>