From 7e7a890727ac497be2a8797247fe97a13a079cee Mon Sep 17 00:00:00 2001
From: Florian Lugou <florian.lugou@telecom-paristech.fr>
Date: Thu, 6 Apr 2017 16:55:05 +0200
Subject: [PATCH] Added Diffie-Hellman to crypto blocks
---
.../toproverif/AVATAR2ProVerif.java | 6 ++
src/proverifspec/ProVerifEquation.java | 60 +++++++++++++++++++
src/proverifspec/ProVerifPiSyntaxer.java | 5 ++
src/proverifspec/ProVerifPitypeSyntaxer.java | 18 ++++++
src/proverifspec/ProVerifSyntaxer.java | 1 +
.../toproverif/TML2ProVerif.java | 6 ++
src/ui/AvatarMethod.java | 1 +
7 files changed, 97 insertions(+)
create mode 100644 src/proverifspec/ProVerifEquation.java
diff --git a/src/avatartranslator/toproverif/AVATAR2ProVerif.java b/src/avatartranslator/toproverif/AVATAR2ProVerif.java
index a95368b344..082abfe7f6 100755
--- a/src/avatartranslator/toproverif/AVATAR2ProVerif.java
+++ b/src/avatartranslator/toproverif/AVATAR2ProVerif.java
@@ -83,6 +83,8 @@ public class AVATAR2ProVerif implements AvatarTranslator {
private final static String SK_ENCRYPT = "sencrypt";
private final static String SK_DECRYPT = "sdecrypt";
+ private final static String DH_DH = "DH";
+
private final static String MAC_MAC = "MAC";
private final static String MAC_VERIFYMAC = "verifyMAC";
@@ -447,6 +449,10 @@ public class AVATAR2ProVerif implements AvatarTranslator {
this.spec.addDeclaration (new ProVerifFunc (SK_ENCRYPT, new String[] {"bitstring", "bitstring"}, "bitstring"));
this.spec.addDeclaration (new ProVerifReduc (new ProVerifVar[] {new ProVerifVar ("x", "bitstring"), new ProVerifVar ("k", "bitstring")}, SK_DECRYPT + " (" + SK_ENCRYPT + " (x, k), k) = x"));
+ this.spec.addDeclaration (new ProVerifComment ("Diffie-Hellman"));
+ this.spec.addDeclaration (new ProVerifFunc (DH_DH, new String[] {"bitstring", "bitstring"}, "bitstring"));
+ this.spec.addDeclaration (new ProVerifEquation (new ProVerifVar[] {new ProVerifVar ("x", "bitstring"), new ProVerifVar ("y", "bitstring")}, DH_DH + " (" + PK_PK + " (x), y) = " + DH_DH + " (" + PK_PK + " (y), x)"));
+
this.spec.addDeclaration (new ProVerifComment ("MAC"));
this.spec.addDeclaration (new ProVerifFunc (MAC_MAC, new String[] {"bitstring", "bitstring"}, "bitstring"));
this.spec.addDeclaration (new ProVerifFunc (MAC_VERIFYMAC, new String[] {"bitstring", "bitstring", "bitstring"}, "bitstring",
diff --git a/src/proverifspec/ProVerifEquation.java b/src/proverifspec/ProVerifEquation.java
new file mode 100644
index 0000000000..53ca95e657
--- /dev/null
+++ b/src/proverifspec/ProVerifEquation.java
@@ -0,0 +1,60 @@
+/**Copyright or (C) or Copr. GET / ENST, Telecom-Paris, Ludovic Apvrille
+ *
+ * ludovic.apvrille AT enst.fr
+ *
+ * This software is a computer program whose purpose is to allow the
+ * edition of TURTLE analysis, design and deployment diagrams, to
+ * allow the generation of RT-LOTOS or Java code from this diagram,
+ * and at last to allow the analysis of formal validation traces
+ * obtained from external tools, e.g. RTL from LAAS-CNRS and CADP
+ * from INRIA Rhone-Alpes.
+ *
+ * This software is governed by the CeCILL license under French law and
+ * abiding by the rules of distribution of free software. You can use,
+ * modify and/ or redistribute the software under the terms of the CeCILL
+ * license as circulated by CEA, CNRS and INRIA at the following URL
+ * "http://www.cecill.info".
+ *
+ * As a counterpart to the access to the source code and rights to copy,
+ * modify and redistribute granted by the license, users are provided only
+ * with a limited warranty and the software's author, the holder of the
+ * economic rights, and the successive licensors have only limited
+ * liability.
+ *
+ * In this respect, the user's attention is drawn to the risks associated
+ * with loading, using, modifying and/or developing or reproducing the
+ * software by the user in light of its specific status of free software,
+ * that may mean that it is complicated to manipulate, and that also
+ * therefore means that it is reserved for developers and experienced
+ * professionals having in-depth computer knowledge. Users are therefore
+ * encouraged to load and test the software's suitability as regards their
+ * requirements in conditions enabling the security of their systems and/or
+ * data to be ensured and, more generally, to use and operate it in the
+ * same conditions as regards security.
+ *
+ * The fact that you are presently reading this means that you have had
+ * knowledge of the CeCILL license and that you accept its terms.
+ *
+ * /**
+ * Class ProVerifFunc
+ * Creation: 06/04/2017
+ * @version 1.0 06/04/2017
+ * @author Florian LUGOU
+ * @see
+ */
+
+package proverifspec;
+
+public class ProVerifEquation implements ProVerifDeclaration {
+ protected ProVerifVar[] vars;
+ protected String formula;
+
+ public ProVerifEquation (ProVerifVar[] _vars, String _formula) {
+ this.vars = _vars;
+ this.formula = _formula;
+ }
+
+ public void translate (ProVerifSyntaxer _syntaxer, int _alinea) {
+ _syntaxer.translateEquation (this, _alinea);
+ }
+}
diff --git a/src/proverifspec/ProVerifPiSyntaxer.java b/src/proverifspec/ProVerifPiSyntaxer.java
index 7b3f1749f6..731852d250 100644
--- a/src/proverifspec/ProVerifPiSyntaxer.java
+++ b/src/proverifspec/ProVerifPiSyntaxer.java
@@ -83,6 +83,11 @@ public class ProVerifPiSyntaxer extends ProVerifSyntaxer {
this.fullSpec += ".";
}
+ protected void translateEquation (ProVerifEquation _node, int _alinea) {
+ this.fullSpec += "\n" + this.printAlinea (_alinea);
+ this.fullSpec += "equation " + _node.formula + ".";
+ }
+
protected void translateVar (ProVerifVar _node, int _alinea) {
this.fullSpec += "\n" + this.printAlinea (_alinea);
if (_node.priv)
diff --git a/src/proverifspec/ProVerifPitypeSyntaxer.java b/src/proverifspec/ProVerifPitypeSyntaxer.java
index be64de5a75..ed39452f82 100644
--- a/src/proverifspec/ProVerifPitypeSyntaxer.java
+++ b/src/proverifspec/ProVerifPitypeSyntaxer.java
@@ -117,6 +117,24 @@ public class ProVerifPitypeSyntaxer extends ProVerifSyntaxer {
this.fullSpec += ".";
}
+ protected void translateEquation (ProVerifEquation _node, int _alinea) {
+ this.fullSpec += "\n" + this.printAlinea (_alinea);
+ this.fullSpec += "equation ";
+ if (_node.vars.length > 0) {
+ this.fullSpec += "forall ";
+ boolean first = true;
+ for (ProVerifVar var: _node.vars) {
+ if (first)
+ first = false;
+ else
+ this.fullSpec += ", ";
+ this.fullSpec += var.name + ": " + var.type;
+ }
+ this.fullSpec += "; ";
+ }
+ this.fullSpec += _node.formula + ".";
+ }
+
protected void translateVar (ProVerifVar _node, int _alinea) {
this.fullSpec += "\n" + this.printAlinea (_alinea);
this.fullSpec += "free " + _node.name + ": " + _node.type;
diff --git a/src/proverifspec/ProVerifSyntaxer.java b/src/proverifspec/ProVerifSyntaxer.java
index 9ed8d2440c..318cd20b1c 100644
--- a/src/proverifspec/ProVerifSyntaxer.java
+++ b/src/proverifspec/ProVerifSyntaxer.java
@@ -185,6 +185,7 @@ public abstract class ProVerifSyntaxer {
protected abstract void translateConst (ProVerifConst _node, int _alinea);
protected abstract void translateFunc (ProVerifFunc _node, int _alinea);
protected abstract void translateReduc (ProVerifReduc _node, int _alinea);
+ protected abstract void translateEquation (ProVerifEquation _node, int _alinea);
protected abstract void translateVar (ProVerifVar _node, int _alinea);
protected abstract void translateQueryAtt (ProVerifQueryAtt _node, int _alinea);
protected abstract void translateQueryEv (ProVerifQueryEv _node, int _alinea);
diff --git a/src/tmltranslator/toproverif/TML2ProVerif.java b/src/tmltranslator/toproverif/TML2ProVerif.java
index 6ecbf60350..af640f50fd 100644
--- a/src/tmltranslator/toproverif/TML2ProVerif.java
+++ b/src/tmltranslator/toproverif/TML2ProVerif.java
@@ -82,6 +82,8 @@ public class TML2ProVerif {
private final static String SK_ENCRYPT = "sencrypt";
private final static String SK_DECRYPT = "sdecrypt";
+ private final static String DH_DH = "DH";
+
private final static String MAC_MAC = "MAC";
private final static String MAC_VERIFYMAC = "verifyMAC";
@@ -317,6 +319,10 @@ public class TML2ProVerif {
this.spec.addDeclaration (new ProVerifFunc (SK_ENCRYPT, new String[] {"bitstring", "bitstring"}, "bitstring"));
this.spec.addDeclaration (new ProVerifReduc (new ProVerifVar[] {new ProVerifVar ("x", "bitstring"), new ProVerifVar ("k", "bitstring")}, SK_DECRYPT + " (" + SK_ENCRYPT + " (x, k), k) = x"));
+ this.spec.addDeclaration (new ProVerifComment ("Diffie-Hellman"));
+ this.spec.addDeclaration (new ProVerifFunc (DH_DH, new String[] {"bitstring", "bitstring"}, "bitstring"));
+ this.spec.addDeclaration (new ProVerifEquation (new ProVerifVar[] {new ProVerifVar ("x", "bitstring"), new ProVerifVar ("y", "bitstring")}, DH_DH + " (" + PK_PK + " (x), y) = " + DH_DH + " (" + PK_PK + " (y), x)"));
+
this.spec.addDeclaration (new ProVerifComment ("MAC"));
this.spec.addDeclaration (new ProVerifFunc (MAC_MAC, new String[] {"bitstring", "bitstring"}, "bitstring"));
this.spec.addDeclaration (new ProVerifFunc (MAC_VERIFYMAC, new String[] {"bitstring", "bitstring", "bitstring"}, "bitstring",
diff --git a/src/ui/AvatarMethod.java b/src/ui/AvatarMethod.java
index 4495482908..6ed469873f 100644
--- a/src/ui/AvatarMethod.java
+++ b/src/ui/AvatarMethod.java
@@ -66,6 +66,7 @@ public class AvatarMethod {
"Key getpk(Message cert)",
"Message sencrypt(Message msg, Key k)",
"Message sdecrypt(Message msg, Key k)",
+ "Key DH(Key pubK, Key privK)",
"Message hash(Message msg)",
"Message MAC(Message msg, Key k)",
"bool verifyMAC(Message msg, Key k, Message macmsg)",
--
GitLab