From 8518fea010c4f64bb2534f4ccdae3bb7489e68b0 Mon Sep 17 00:00:00 2001
From: Ludovic Apvrille <ludovic.apvrille@telecom-paris.fr>
Date: Mon, 20 Mar 2023 20:29:11 +0100
Subject: [PATCH] Adding more information on security in the internal help of
TTool
---
.../resources/help/securityverification.html | 52 +++++++++++++++----
.../resources/help/securityverification.md | 12 ++++-
2 files changed, 53 insertions(+), 11 deletions(-)
diff --git a/src/main/resources/help/securityverification.html b/src/main/resources/help/securityverification.html
index 5130fe3148..c58a9a7b51 100644
--- a/src/main/resources/help/securityverification.html
+++ b/src/main/resources/help/securityverification.html
@@ -8,12 +8,18 @@
<style>
code{white-space: pre-wrap;}
span.smallcaps{font-variant: small-caps;}
- span.underline{text-decoration: underline;}
- div.column{display: inline-block; vertical-align: top; width: 50%;}
+ div.columns{display: flex; gap: min(4vw, 1.5em);}
+ div.column{flex: auto; overflow-x: auto;}
div.hanging-indent{margin-left: 1.5em; text-indent: -1.5em;}
ul.task-list{list-style: none;}
+ ul.task-list li input[type="checkbox"] {
+ width: 0.8em;
+ margin: 0 0.8em 0.2em -1.6em;
+ vertical-align: middle;
+ }
.display.math{display: block; text-align: center; margin: 0.5rem auto;}
</style>
+ <link rel="stylesheet" href="/Users/ludovicapvrille/TTool/src/main/resources/help/help.css" />
<!--[if lt IE 9]>
<script src="//cdnjs.cloudflare.com/ajax/libs/html5shiv/3.7.3/html5shiv-printshiv.min.js"></script>
<![endif]-->
@@ -21,18 +27,46 @@
<body>
<h1 id="security-verification">Security verification</h1>
<h2 id="main-principle">Main principle</h2>
-<p>Security verification can be performed either from <a href="file://mapping.html">DIPLODOCUS mapping diagrams</a> or from <a href="file://avatarsoftwaredesign.html">AVATAR design diagrams</a>.</p>
-<p>The security verification consists in transforming a diagram and its security properties into a ProVerif specification, and then colling ProVerif to check for the satisfaction of security properties. while ProVerif runs, TTool indicates which properties could be proved and backtraces the results to diagrams, using locks next to perperties or elements involved in these properties. A green lock indicates a satisfied property, a greay lock indicates that the property could not be proved, and a red lock indicates that the property could be proved as violated.</p>
-<h2 id="proverif-installation-and-configuration">ProVerif installation and configuration</h2>
-<p>We advice to install the latest version of ProVerif on your computer. We usually install ProVerif using <em>opam</em>:</p>
+<p>Security verification can be performed either from <a
+href="file://mapping.html">DIPLODOCUS mapping diagrams</a> or from <a
+href="file://avatarsoftwaredesign.html">AVATAR design diagrams</a>.</p>
+<p>The security verification consists in transforming a diagram and its
+security properties into a ProVerif specification, and then colling
+ProVerif to check for the satisfaction of security properties. while
+ProVerif runs, TTool indicates which properties could be proved and
+backtraces the results to diagrams, using locks next to perperties or
+elements involved in these properties. A green lock indicates a
+satisfied property, a greay lock indicates that the property could not
+be proved, and a red lock indicates that the property could be proved as
+violated.</p>
+<h2 id="attacker-model">Attacker model</h2>
+<p>An important point to note: the assumed attacker model is Dolev-Yao,
+that is a, attacker can retreive messages from public channel, rework
+messages according to his/her knowledge and inject messages. We also
+assume that the attack knows about all cryptographic primitives
+available in TTool. Thus, an attacker can use symetric cryptography,
+asymetric cryptography, MAC, hash, etc.</p>
+<p><strong>Private channels</strong> cypher data with symetric
+encryption, i.e., they ensure condifentiality and integrity (also known
+as weak authenticity), but not (strong) authenticity.</p>
+<h2 id="proverif-installation-and-configuration">ProVerif installation
+and configuration</h2>
+<p>We advice to install the latest version of ProVerif on your computer.
+We usually install ProVerif using <em>opam</em>:</p>
<pre><code>$ opam install proverif</code></pre>
-<p>Once proverif has been installed, TTool must be configured. TTool relies on a .xml configuration file (by default: config.xml). Open this configuration file and configure:</p>
-<p>The directory in which TTool generated ProVerif specifications. For instance:</p>
+<p>Once proverif has been installed, TTool must be configured. TTool
+relies on a .xml configuration file (by default: config.xml). Open this
+configuration file and configure:</p>
+<p>The directory in which TTool generated ProVerif specifications. For
+instance:</p>
<pre><code><ProVerifCodeDirectory data="/home/foo/TTool/proverif/" /></code></pre>
<p>The path to the ProVerif executable. For instance:</p>
<pre><code><ProVerifVerifierPath data="/home/foo/bin/proverif" /></code></pre>
<h2 id="security-properties">Security properties</h2>
-<h2 id="investigating-verification-results">Investigating verification results</h2>
+<p>Three security properties can be investigated: - Confidentiality -
+Integrity (or weak authenticity) - (Strong) authenticity</p>
+<h2 id="investigating-verification-results">Investigating verification
+results</h2>
<h2 id="advanced-concepts">Advanced concepts</h2>
</body>
</html>
diff --git a/src/main/resources/help/securityverification.md b/src/main/resources/help/securityverification.md
index 7171dc6d5a..6157e7f38f 100644
--- a/src/main/resources/help/securityverification.md
+++ b/src/main/resources/help/securityverification.md
@@ -6,6 +6,12 @@ Security verification can be performed either from [DIPLODOCUS mapping diagrams]
The security verification consists in transforming a diagram and its security properties into a ProVerif specification, and then colling ProVerif to check for the satisfaction of security properties. while ProVerif runs, TTool indicates which properties could be proved and backtraces the results to diagrams, using locks next to perperties or elements involved in these properties. A green lock indicates a satisfied property, a greay lock indicates that the property could not be proved, and a red lock indicates that the property could be proved as violated.
+## Attacker model
+
+An important point to note: the assumed attacker model is Dolev-Yao, that is a, attacker can retreive messages from public channel, rework messages according to his/her knowledge and inject messages. We also assume that the attack knows about all cryptographic primitives available in TTool. Thus, an attacker can use symetric cryptography, asymetric cryptography, MAC, hash, etc.
+
+**Private channels** cypher data with symetric encryption, i.e., they ensure condifentiality and integrity (also known as weak authenticity), but not (strong) authenticity.
+
## ProVerif installation and configuration
@@ -30,8 +36,10 @@ The path to the ProVerif executable. For instance:
## Security properties
-
-
+Three security properties can be investigated:
+- Confidentiality
+- Integrity (or weak authenticity)
+- (Strong) authenticity
## Investigating verification results
--
GitLab