[noise] Noise Explorer

[Nadim Kobeissi]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://moderncrypto.org/mail-archive/noise/attachments/20180522/0165fc58/attachment.html>