-
Notifications
You must be signed in to change notification settings - Fork 6
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
ef2cf76
commit ce74d65
Showing
719 changed files
with
12,611 additions
and
6,116 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,71 +1,71 @@ | ||
| <!DOCTYPE html> | ||
| <html lang="en"> | ||
|
|
||
| <head> | ||
| <meta charset="utf-8" /> | ||
| <title>Noise Explorer: Command-Line Tool</title> | ||
| <meta name="keywords" content="noise protocol, protocol verification, formal verification, noise protocol framework, symbolic verification" /> | ||
| <meta name="description" content="Noise Explorer is an online engine for reasoning about Noise Protocol Framework Handshake Patterns. Noise Explorer allows you to design and validate Noise Handshake Patterns, to generate cryptographic models for formal verification and to explore a compendium of formal verification results for the most popular and relevant Noise Handshake Patterns in use today." /> | ||
| <link rel="image_src" href="https://noiseexplorer.com/res/img/logo.svg" /> | ||
| <link rel="icon" type="image/png" href="../res/img/logo.svg" /> | ||
| <link href="../res/css/style.css" rel="stylesheet" /> | ||
| <link href="../res/css/fonts.css" rel="stylesheet" /> | ||
| <script></script> | ||
| </head> | ||
|
|
||
| <body> | ||
| <div class="header"> | ||
| <img id="logo" src="../res/img/logo.svg" alt="" /> | ||
| <h1>Noise Explorer <span class="beta">beta</span></h1> | ||
| </div> | ||
| <div class="nav"> | ||
| <span class="menu">menu</span> | ||
| <div class="navLinks"> | ||
| <a href="..">Design New Pattern</a> | ||
| <a href="../patterns">Explore Patterns</a> | ||
| <a href="#" class="currentNav">Command-Line Tool</a> | ||
| <a href="https://eprint.iacr.org/2018/766">Scientific Paper</a> | ||
| </div> | ||
| </div> | ||
| <div class="results singleColumn"> | ||
| <div class="resultsExplanation"> | ||
| <h2>Noise Explorer Command-Line Tool</h2> | ||
| <p>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. </p> | ||
| <p>Noise Explorer can also render results from the ProVerif output into an elegant and easy to read HTML format: the <a href="../patterns">pattern results</a> that can be explored on this very website were generated using the Noise Explorer command-line tool.</p> | ||
| <pre> | ||
| $> 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. | ||
| --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. | ||
| </pre> | ||
| <h2>License</h2> | ||
| <p>All Noise Explorer software, including this website, is licensed under the <a href="https://www.gnu.org/licenses/gpl-3.0.en.html" target="_blank">GNU General Public License, Version 3</a>.</p> | ||
| <h2>Download Noise Explorer for your Computer</h2> | ||
| <p>You are welcome to view the Noise Explorer <a href="https://source.symbolic.software/noiseexplorer/noiseexplorer" target="_blank">code repository</a>.</p> | ||
| </div> | ||
| </div> | ||
| <div class="footer"> | ||
| <span class="about">about</span> | ||
| <span>Noise Explorer</span> | ||
| <span style="float:right"><a href="https://symbolic.software" target="_blank">Symbolic Software</a> | <a href="http://prosecco.gforge.inria.fr/" target="_blank">INRIA</a></span> | ||
| </div> | ||
| </body> | ||
|
|
||
| </html> | ||
| <!DOCTYPE html> | ||
| <html lang="en"> | ||
|
|
||
| <head> | ||
| <meta charset="utf-8" /> | ||
| <title>Noise Explorer: Command-Line Tool</title> | ||
| <meta name="keywords" content="noise protocol, protocol verification, formal verification, noise protocol framework, symbolic verification" /> | ||
| <meta name="description" content="Noise Explorer is an online engine for reasoning about Noise Protocol Framework Handshake Patterns. Noise Explorer allows you to design and validate Noise Handshake Patterns, to generate cryptographic models for formal verification and to explore a compendium of formal verification results for the most popular and relevant Noise Handshake Patterns in use today." /> | ||
| <link rel="image_src" href="https://noiseexplorer.com/res/img/logo.svg" /> | ||
| <link rel="icon" type="image/png" href="../res/img/logo.svg" /> | ||
| <link href="../res/css/style.css" rel="stylesheet" /> | ||
| <link href="../res/css/fonts.css" rel="stylesheet" /> | ||
| <script></script> | ||
| </head> | ||
|
|
||
| <body> | ||
| <div class="header"> | ||
| <img id="logo" src="../res/img/logo.svg" alt="" /> | ||
| <h1>Noise Explorer <span class="beta">beta</span></h1> | ||
| </div> | ||
| <div class="nav"> | ||
| <span class="menu">menu</span> | ||
| <div class="navLinks"> | ||
| <a href="..">Design New Pattern</a> | ||
| <a href="../patterns">Explore Patterns</a> | ||
| <a href="#" class="currentNav">Command-Line Tool</a> | ||
| <a href="https://eprint.iacr.org/2018/766">Scientific Paper</a> | ||
| </div> | ||
| </div> | ||
| <div class="results singleColumn"> | ||
| <div class="resultsExplanation"> | ||
| <h2>Noise Explorer Command-Line Tool</h2> | ||
| <p>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. </p> | ||
| <p>Noise Explorer can also render results from the ProVerif output into an elegant and easy to read HTML format: the <a href="../patterns">pattern results</a> that can be explored on this very website were generated using the Noise Explorer command-line tool.</p> | ||
| <pre> | ||
| $> 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. | ||
| --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. | ||
| </pre> | ||
| <h2>License</h2> | ||
| <p>All Noise Explorer software, including this website, is licensed under the <a href="https://www.gnu.org/licenses/gpl-3.0.en.html" target="_blank">GNU General Public License, Version 3</a>.</p> | ||
| <h2>Download Noise Explorer for your Computer</h2> | ||
| <p>You are welcome to view the Noise Explorer <a href="https://github.com/symbolicsoft/noiseexplorer" target="_blank">code repository</a>.</p> | ||
| </div> | ||
| </div> | ||
| <div class="footer"> | ||
| <span class="about">about</span> | ||
| <span>Noise Explorer</span> | ||
| <span style="float:right"><a href="https://symbolic.software" target="_blank">Symbolic Software</a> | <a href="http://prosecco.gforge.inria.fr/" target="_blank">INRIA</a></span> | ||
| </div> | ||
| </body> | ||
|
|
||
| </html> |
Oops, something went wrong.