Noise Explorer is an online engine for reasoning about Noise Protocol Framework Handshake Patterns. https://noiseexplorer.com
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
Nadim Kobeissi 84b5feda10
Fix versions.json path.
5 months ago
html Fix versions.json path. 5 months ago
implementations Release Noise Explorer v1.0.1 7 months ago
models Revert Confidentiality 4 and 3. 9 months ago
patterns Remove NOSE. 10 months ago
results Update most patterns. 9 months ago
src Update repository addresses. 5 months ago
.gitignore Resolves #36: Added Makefile and README to Rust implementations targeting WASM. 8 months ago
.releaserc Resolves #16: Automated Versioning 7 months ago
.travis.yml Fix #37: Removed the ability to clone some types in Rust/Wasm implmentations 7 months ago
CHANGELOG.md Release Noise Explorer v1.0.1 7 months ago
CONTRIBUTING.md Add CONTRIBUTING.md 6 months ago
LICENSE.md Initial public commit. 1 year ago
README.md Release Noise Explorer v1.0.1 7 months ago

README.md

Noise Explorer

Version 1.0.1, based on Noise Protocol Revision 34.

Overview

The Noise Explorer command-line tool can parse Noise Handshake Patterns according to the original specification. It can generate cryptographic models for formal verification, including security queries, top-level processes and malicious principals, for testing against an active or passive attacker. Noise Explorer can also generate fully functional discrete implementations for any Noise Handshake Pattern, written in the Go and Rust programming languages, as well as WebAssembly binaries.

Noise Explorer can also render results from the ProVerif output into an elegant and easy to read HTML format: the pattern results that can be explored on Noise Explorer were generated using the Noise Explorer command-line tool.

Status

Output Functional Reliable Tests
ProVerif ✔️ ✔️ ✔️
Go ✔️ ✔️ ✔️
Rust ✔️ ✔️ ✔️
Wasm ✔️ ✔️ ✔️

Usage

$> node noiseExplorer --help
Noise Explorer version 0.3 (specification revision 34)
Noise Explorer has three individual modes: generation, rendering and web interface.

Generation:
--generate=(json|pv|go|rs|wasm): Specify output format.
--pattern=[file]: Specify input pattern file (required).
--attacker=(active|passive): Specify ProVerif attacker type (default: active).

Rendering:
--render: Render results from ProVerif output files into HTML.
--pattern=[file]: Specify input pattern file (required).
--activeModel=[file]: Specify ProVerif active attacker model (required).
--activeResults=[file]: Specify active results file for --render (required).
--passiveResults=[file]: Specify passive results file for --render (required).

Web interface:
--web=(port): Make Noise Explorer's web interface available at http://localhost:(port) (default: 8000).

Help:
--help: View this help text.

Requirements

  1. Node is required for running Noise Explorer locally.
  2. ProVerif is required for verifying generated models.
  3. Go and Rust are required for running generated implementations.
  4. Google Chrome is required for testing Wasm implementations.

Preparation

  1. cd src
  2. make dependencies
  3. make parser

Usage

node noiseExplorer --help

Model Generation

To quickly translate all Noise handshake patterns in the patterns folder to ProVerif models, simply run make models after completing the steps outlined in the Preparation section of this document. The models will be available in the models folder.

Implementation Generation

To quickly translate all Noise handshake patterns in the patterns folder to Go, Rust and Wasm implementations, simply run make implementations after completing the steps outlined in the Preparation section of this document. The software will be available in the implementations folder. Note that the implementations found under implementations/wasm and the ones found under implementations/rust use different cryptographic libraries for compatibility purposes.

WebAssembly Binaries

Wasm binaries and relevant helper files are found under implementations/wasm/*/pkg. To re-compile the Wasm binaries run make wasm after generating implementations using make implementations.

Implementation Testing

Running make tests will verify these implementations against test vectors obtained from Cacophony, a Haskell implementation of the Noise Protocol Framework. Testing Wasm implementations will utilize Google Chrome in headless mode.

Implementation Documentation

To view the documentation of a generated Rust implementation, navigate to the directory of the desired pattern and run cargo doc --open --no-deps.

Contributors and License

Authored by Symbolic Software. Released under the GNU General Public License, version 3.