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.
| Output | Functional | Reliable | Tests |
|---|---|---|---|
| ProVerif | ✔️ | ✔️ | ✔️ |
| Go | ✔️ | ✔️ | ✔️ |
| Rust | ✔️ | ✔️ | ✔️ |
| Wasm | ✔️ | ✔️ | ✔️ |
$> 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.
- Node is required for running Noise Explorer locally.
- ProVerif is required for verifying generated models.
- Go and Rust are required for running generated implementations.
- Google Chrome is required for testing Wasm implementations.
cd srcmake dependenciesmake parser
node noiseExplorer --help
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.
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.
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.
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.
To view the documentation of a generated Rust implementation, navigate to the directory of the desired pattern and run cargo doc --open --no-deps.
Authored by Symbolic Software. Released under the GNU General Public License, version 3.