diff --git a/src/avatartranslator/toproverif/AVATAR2ProVerif.java b/src/avatartranslator/toproverif/AVATAR2ProVerif.java
index a95368b344094abc1b5fe44cd69c5b59f0702ee1..082abfe7f62fb011139bb477cd37bd68955620a8 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 0000000000000000000000000000000000000000..53ca95e6572377783e9b01231a2ce75ffea91ad1
--- /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 7b3f1749f6e6b09a6969ea46ada7ce2659bbb948..731852d25057bdeba81d7d640dfe2f71971248c8 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 be64de5a75b0fc2e71dd2ebd7653119b1bba9917..ed39452f829cd20da303b311f85718a83e1b44eb 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 9ed8d2440c939f8edbadabb7e8b456ee88d5c31e..318cd20b1c2553b1f4d173f983900b77e9cfbc51 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 6ecbf603504e342e44803a59aa6abd9ba82dbc02..af640f50fd4f49491d94eb6638a0043c021d13b9 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 44954829087d3b879960105d4260c6d9c1415cf7..6ed469873fcc2300d8155710c15f9367caf6d804 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)",