From 79cdcd29e510cf88220bd912e9a2ddf064e65560 Mon Sep 17 00:00:00 2001
From: Florian Lugou <florian.lugou@telecom-paristech.fr>
Date: Mon, 22 May 2017 13:00:00 +0200
Subject: [PATCH] Refactoring ProVerif results to be objects instead of strings
---
.../AvatarAttributeState.java | 5 +
src/avatartranslator/AvatarPragma.java | 6 +-
.../AvatarPragmaAuthenticity.java | 9 +
.../AvatarPragmaReachability.java | 80 +++
src/avatartranslator/AvatarPragmaSecret.java | 20 +-
.../toproverif/AVATAR2ProVerif.java | 95 +--
src/proverifspec/ProVerifOutputAnalyzer.java | 508 +++++++++-----
src/proverifspec/ProVerifQueryAuthResult.java | 73 ++
src/proverifspec/ProVerifQueryResult.java | 66 ++
src/tmltranslator/TMLModeling.java | 653 ++++++++----------
src/tmltranslator/toavatar/TML2Avatar.java | 107 ++-
src/ui/AvatarDesignPanel.java | 214 +++---
src/ui/GTURTLEModeling.java | 33 +-
src/ui/MainGUI.java | 8 +-
src/ui/avatarsmd/AvatarSMDState.java | 1 +
.../window/JDialogProverifVerification.java | 570 +++++++--------
16 files changed, 1429 insertions(+), 1019 deletions(-)
create mode 100644 src/avatartranslator/AvatarPragmaReachability.java
create mode 100644 src/proverifspec/ProVerifQueryAuthResult.java
create mode 100644 src/proverifspec/ProVerifQueryResult.java
diff --git a/src/avatartranslator/AvatarAttributeState.java b/src/avatartranslator/AvatarAttributeState.java
index 2729e49974..77d10bb47f 100644
--- a/src/avatartranslator/AvatarAttributeState.java
+++ b/src/avatartranslator/AvatarAttributeState.java
@@ -74,4 +74,9 @@ public class AvatarAttributeState extends AvatarElement {
this.cloneLinkToReferenceObjects (result);
return result;
}
+
+ public String toString()
+ {
+ return this.attribute.getBlock().getName().replaceAll("__", ".") + "." + this.state.getName() + "." + this.attribute.getName();
+ }
}
diff --git a/src/avatartranslator/AvatarPragma.java b/src/avatartranslator/AvatarPragma.java
index 134916b807..161dae6f43 100644
--- a/src/avatartranslator/AvatarPragma.java
+++ b/src/avatartranslator/AvatarPragma.java
@@ -352,10 +352,12 @@ public abstract class AvatarPragma extends AvatarElement {
}
switch(header){
case "Confidentiality":
- pragmas.add(new AvatarPragmaSecret(str, obj, attrs));
+ for (AvatarAttribute attr: attrs)
+ pragmas.add(new AvatarPragmaSecret(str, obj, attr));
break;
case "Secret":
- pragmas.add(new AvatarPragmaSecret(str, obj, attrs));
+ for (AvatarAttribute attr: attrs)
+ pragmas.add(new AvatarPragmaSecret(str, obj, attr));
break;
case "SecrecyAssumption":
pragmas.add(new AvatarPragmaSecrecyAssumption(str, obj, attrs));
diff --git a/src/avatartranslator/AvatarPragmaAuthenticity.java b/src/avatartranslator/AvatarPragmaAuthenticity.java
index c1b9204e9f..6c50405536 100644
--- a/src/avatartranslator/AvatarPragmaAuthenticity.java
+++ b/src/avatartranslator/AvatarPragmaAuthenticity.java
@@ -74,6 +74,15 @@ public class AvatarPragmaAuthenticity extends AvatarPragma {
return attrB;
}
+ @Override
+ public String toString()
+ {
+ if (this.attrA == null || this.attrB == null)
+ return "<undefined>";
+
+ return this.attrA.toString() + " ==> " + this.attrB.toString();
+ }
+
@Override
public AvatarPragmaAuthenticity advancedClone (AvatarSpecification avspec) {
AvatarPragmaAuthenticity result = new AvatarPragmaAuthenticity (this.name, this.referenceObject, this.attrA.advancedClone(avspec), this.attrB.advancedClone(avspec));
diff --git a/src/avatartranslator/AvatarPragmaReachability.java b/src/avatartranslator/AvatarPragmaReachability.java
new file mode 100644
index 0000000000..3c6b1a7017
--- /dev/null
+++ b/src/avatartranslator/AvatarPragmaReachability.java
@@ -0,0 +1,80 @@
+/**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 AvatarPragmaReachability
+ * Creation: 19/05/2017
+ * @version 1.0 19/05/2017
+ * @author Florian LUGOU
+ * @see
+ */
+
+package avatartranslator;
+
+public class AvatarPragmaReachability extends AvatarPragma {
+ private AvatarState state;
+ private AvatarBlock block;
+
+ public AvatarPragmaReachability(String _name, Object _referenceObject, AvatarBlock block, AvatarState state)
+ {
+ super(_name, _referenceObject);
+ this.block = block;
+ this.state = state;
+ }
+
+ public AvatarState getState()
+ {
+ return this.state;
+ }
+
+ public AvatarBlock getBlock()
+ {
+ return this.block;
+ }
+
+ public String toString()
+ {
+ return this.block.getName().replaceAll("__", ".") + "." + this.state.getName();
+ }
+
+ @Override
+ public AvatarPragmaReachability advancedClone(AvatarSpecification avspec)
+ {
+ // !!! Should never be called !!!
+ return null;
+ }
+}
diff --git a/src/avatartranslator/AvatarPragmaSecret.java b/src/avatartranslator/AvatarPragmaSecret.java
index 2bc660ce9b..597fc706b1 100644
--- a/src/avatartranslator/AvatarPragmaSecret.java
+++ b/src/avatartranslator/AvatarPragmaSecret.java
@@ -52,22 +52,24 @@ import myutil.*;
public class AvatarPragmaSecret extends AvatarPragma {
- private LinkedList<AvatarAttribute> arguments;
+ private AvatarAttribute argument;
- public AvatarPragmaSecret(String _name, Object _referenceObject, LinkedList<AvatarAttribute> args) {
+ public AvatarPragmaSecret(String _name, Object _referenceObject, AvatarAttribute arg) {
super(_name, _referenceObject);
- arguments = args;
+ this.argument = arg;
}
- public LinkedList<AvatarAttribute> getArgs(){
- return arguments;
+ public AvatarAttribute getArg(){
+ return this.argument;
+ }
+
+ public String toString()
+ {
+ return this.argument.getBlock().getName().replaceAll("__", ".") + "." + this.argument.getName();
}
@Override
public AvatarPragmaSecret advancedClone (AvatarSpecification avspec) {
- LinkedList<AvatarAttribute> l = new LinkedList<AvatarAttribute> ();
- for (AvatarAttribute aa: this.arguments)
- l.add (avspec.getMatchingAttribute(aa));
- AvatarPragmaSecret result = new AvatarPragmaSecret (this.name, this.referenceObject, l);
+ AvatarPragmaSecret result = new AvatarPragmaSecret (this.name, this.referenceObject, avspec.getMatchingAttribute(this.argument));
this.cloneLinkToReferenceObjects (result);
return result;
}
diff --git a/src/avatartranslator/toproverif/AVATAR2ProVerif.java b/src/avatartranslator/toproverif/AVATAR2ProVerif.java
index 0c912ef84f..2eb730688c 100755
--- a/src/avatartranslator/toproverif/AVATAR2ProVerif.java
+++ b/src/avatartranslator/toproverif/AVATAR2ProVerif.java
@@ -63,7 +63,7 @@ import avatartranslator.*;
public class AVATAR2ProVerif implements AvatarTranslator {
- private final static String ATTR_DELIM = "__";
+ public final static String ATTR_DELIM = "___";
private final static String UNKNOWN = "UNKNOWN";
@@ -91,8 +91,8 @@ public class AVATAR2ProVerif implements AvatarTranslator {
private final static String HASH_HASH = "hash";
private final static String CH_MAINCH = "ch";
- private final static String CH_ENCRYPT = "privChEnc__";
- private final static String CH_DECRYPT = "privChDec__";
+ private final static String CH_ENCRYPT = "privChEnc" + ATTR_DELIM;
+ private final static String CH_DECRYPT = "privChDec" + ATTR_DELIM;
private final static String CHCTRL_CH = "chControl";
private final static String CHCTRL_ENCRYPT = "chControlEnc";
@@ -486,7 +486,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
this.spec.addDeclaration (new ProVerifConst (ZERO, "bitstring"));
this.spec.addDeclaration (new ProVerifFunc (PEANO_N, new String[] {"bitstring"}, "bitstring"));
- /* Declare all the call__*** variables */
+ /* Declare all the call*** variables */
List<AvatarBlock> blocks = this.avspec.getListOfBlocks();
// String action = "(";
for(AvatarBlock block: blocks) {
@@ -495,7 +495,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
simplifiedElements.put (block.getStateMachine ().getStartState (), new Integer (0));
for (AvatarStateMachineElement asme: simplifiedElements.keySet ())
- this.spec.addDeclaration (new ProVerifVar ("call__" + block.getName() + "__" + simplifiedElements.get (asme), "bitstring", true));
+ this.spec.addDeclaration (new ProVerifVar ("call" + ATTR_DELIM + block.getName() + ATTR_DELIM + simplifiedElements.get (asme), "bitstring", true));
}
this.spec.addDeclaration (new ProVerifComment ("Constants"));
@@ -536,19 +536,20 @@ public class AVATAR2ProVerif implements AvatarTranslator {
TraceManager.addDev("Queries Secret");
for (AvatarPragma pragma: this.avspec.getPragmas ())
if (pragma instanceof AvatarPragmaSecret)
- for (AvatarAttribute attribute: ((AvatarPragmaSecret) pragma).getArgs ()) {
- AvatarAttribute trueAttr = this.nameEquivalence.get (attribute);
- if (trueAttr == null)
- trueAttr = attribute;
- if (this.secrecyChecked.contains (trueAttr))
- continue;
-
- String varName = AVATAR2ProVerif.translateTerm (trueAttr, null);
- this.spec.addDeclaration (new ProVerifQueryAtt (varName, true));
- TraceManager.addDev("| attacker (" + varName + ")");
-
- this.secrecyChecked.add (trueAttr);
- }
+ {
+ AvatarAttribute attribute = ((AvatarPragmaSecret) pragma).getArg ();
+ AvatarAttribute trueAttr = this.nameEquivalence.get (attribute);
+ if (trueAttr == null)
+ trueAttr = attribute;
+ if (this.secrecyChecked.contains (trueAttr))
+ continue;
+
+ String varName = AVATAR2ProVerif.translateTerm (trueAttr, null);
+ this.spec.addDeclaration (new ProVerifQueryAtt (varName, true));
+ TraceManager.addDev("| attacker (" + varName + ")");
+
+ this.secrecyChecked.add (trueAttr);
+ }
// Queries for states
TraceManager.addDev ("Queries Event (" + (this.stateReachability == JDialogProverifVerification.REACHABILITY_ALL ? "ALL" : this.stateReachability == JDialogProverifVerification.REACHABILITY_SELECTED ? "SELECTED" : "NONE") + ")");
@@ -565,9 +566,9 @@ public class AVATAR2ProVerif implements AvatarTranslator {
visited.add (asme);
if (asme instanceof AvatarState && (this.stateReachability == JDialogProverifVerification.REACHABILITY_ALL || ((AvatarState) asme).isCheckable ())) {
- this.spec.addDeclaration (new ProVerifQueryEv (new ProVerifVar[] {}, "enteringState__" + block.getName() + "__" + asme.getName()));
- this.spec.addDeclaration (new ProVerifEvDecl ("enteringState__" + block.getName() + "__" + asme.getName(), new String[] {}));
- TraceManager.addDev("| event (enteringState__" + block.getName() + "__" + asme.getName() + ")");
+ this.spec.addDeclaration (new ProVerifQueryEv (new ProVerifVar[] {}, "enteringState" + ATTR_DELIM + block.getName() + ATTR_DELIM + asme.getName()));
+ this.spec.addDeclaration (new ProVerifEvDecl ("enteringState" + ATTR_DELIM + block.getName() + ATTR_DELIM + asme.getName(), new String[] {}));
+ TraceManager.addDev("| event (enteringState" + ATTR_DELIM + block.getName() + ATTR_DELIM + asme.getName() + ")");
}
for (AvatarStateMachineElement _asme: asme.getNexts ())
@@ -587,16 +588,16 @@ public class AVATAR2ProVerif implements AvatarTranslator {
if (attrA != null && attrB != null) {
String sA = AVATAR2ProVerif.makeAttrName (attrA.getAttribute ().getBlock ().getName (), attrA.getAttribute ().getName (), attrA.getState ().getName ());
String sB = AVATAR2ProVerif.makeAttrName (attrB.getAttribute ().getBlock ().getName (), attrB.getAttribute ().getName (), attrB.getState ().getName ());
- TraceManager.addDev("| authenticity__" + sB + " (dummyM) ==> authenticity__" + sA + " (dummyM)");
+ TraceManager.addDev("| authenticity" + ATTR_DELIM + sB + " (dummyM) ==> authenticity" + ATTR_DELIM + sA + " (dummyM)");
if (!authenticityEvents.contains (sA)) {
authenticityEvents.add (sA);
- spec.addDeclaration (new ProVerifEvDecl ("authenticity__" + sA, new String[] {"bitstring"}));
+ spec.addDeclaration (new ProVerifEvDecl ("authenticity" + ATTR_DELIM + sA, new String[] {"bitstring"}));
}
if (!authenticityEvents.contains (sB)) {
authenticityEvents.add (sB);
- spec.addDeclaration (new ProVerifEvDecl ("authenticity__" + sB, new String[] {"bitstring"}));
+ spec.addDeclaration (new ProVerifEvDecl ("authenticity" + ATTR_DELIM + sB, new String[] {"bitstring"}));
}
- spec.addDeclaration (new ProVerifQueryEvinj (new ProVerifVar[] {new ProVerifVar ("dummyM", "bitstring")}, "authenticity__" + sB + " (dummyM)", "authenticity__" + sA + " (dummyM)"));
+ spec.addDeclaration (new ProVerifQueryEvinj (new ProVerifVar[] {new ProVerifVar ("dummyM", "bitstring")}, "authenticity" + ATTR_DELIM + sB + " (dummyM)", "authenticity" + ATTR_DELIM + sA + " (dummyM)"));
}
}
}
@@ -605,7 +606,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
TraceManager.addDev("\n\n=+=+=+ Making Starting Process +=+=+=");
// Create starting process
- ProVerifProcess p = new ProVerifProcess("starting__", new ProVerifVar[] {});
+ ProVerifProcess p = new ProVerifProcess("starting" + ATTR_DELIM, new ProVerifVar[] {});
ProVerifProcInstr lastInstr = p;
// Get all the blocks
@@ -724,12 +725,12 @@ public class AVATAR2ProVerif implements AvatarTranslator {
HashMap<AvatarStateMachineElement, Integer> simplifiedElements = block.getStateMachine ().getSimplifiedElements ();
if (simplifiedElements.get (block.getStateMachine ().getStartState ()) == null)
- paral.addInstr (new ProVerifProcCall (block.getName () + "__0", new ProVerifVar[] {new ProVerifVar ("sessionID", "bitstring")}));
+ paral.addInstr (new ProVerifProcCall (block.getName () + ATTR_DELIM + "0", new ProVerifVar[] {new ProVerifVar ("sessionID", "bitstring")}));
for (AvatarStateMachineElement asme: simplifiedElements.keySet ()) {
globing = new ProVerifProcRawGlobing ("!", "");
paral.addInstr (globing);
- globing.getIntra ().setNextInstr (new ProVerifProcCall (block.getName () + "__" + simplifiedElements.get (asme), new ProVerifVar[] {new ProVerifVar ("sessionID", "bitstring")}));
+ globing.getIntra ().setNextInstr (new ProVerifProcCall (block.getName () + ATTR_DELIM + simplifiedElements.get (asme), new ProVerifVar[] {new ProVerifVar ("sessionID", "bitstring")}));
}
}
@@ -827,7 +828,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
TraceManager.addDev("Finding processes");
paral = new ProVerifProcParallel ();
for(AvatarBlock block: blocks)
- paral.addInstr (new ProVerifProcCall (block.getName() + "__start", processArgs.toArray (new ProVerifVar[processArgs.size ()])));
+ paral.addInstr (new ProVerifProcCall (block.getName() + ATTR_DELIM + "start", processArgs.toArray (new ProVerifVar[processArgs.size ()])));
lastInstr = lastInstr.setNextInstr (paral);
// Set main process
@@ -878,7 +879,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
List<ProVerifVar> processArgs = new LinkedList<ProVerifVar>( knowledgeArray );//.clone ();
processArgs.add (new ProVerifVar ("sessionID", "bitstring"));
- ProVerifProcInstr lastInstr = new ProVerifProcess(ab.getName() + "__start", processArgs.toArray (new ProVerifVar[processArgs.size ()]));
+ ProVerifProcInstr lastInstr = new ProVerifProcess(ab.getName() + ATTR_DELIM + "start", processArgs.toArray (new ProVerifVar[processArgs.size ()]));
spec.addDeclaration (lastInstr);
// Create a ProVerif Variable corresponding to each attribute block
@@ -923,9 +924,9 @@ public class AVATAR2ProVerif implements AvatarTranslator {
// Call the first "real" process
this.dummyDataCounter ++;
- String strong = "strong__" + AVATAR2ProVerif.makeAttrName (ab.getName (), "0") + this.dummyDataCounter;
+ String strong = "strong" + ATTR_DELIM + AVATAR2ProVerif.makeAttrName (ab.getName (), "0") + this.dummyDataCounter;
lastInstr = lastInstr.setNextInstr (new ProVerifProcIn (CHCTRL_CH, new ProVerifVar[] {new ProVerifVar (strong, "bitstring")}));
- String tmp = "out (" + CHCTRL_CH + ", " + CHCTRL_ENCRYPT + " ((sessionID, call__" + ab.getName () + "__0" + ", " + strong;
+ String tmp = "out (" + CHCTRL_CH + ", " + CHCTRL_ENCRYPT + " ((sessionID, call" + ATTR_DELIM + ab.getName () + ATTR_DELIM + "0" + ", " + strong;
for(ProVerifVar aa: this.getAttributesFromBlock (ab))
tmp += ", " + aa.getName ();
lastInstr = lastInstr.setNextInstr (new ProVerifProcRaw (tmp + ")))"));
@@ -947,15 +948,15 @@ public class AVATAR2ProVerif implements AvatarTranslator {
ProVerifProcInstr p = new ProVerifProcess(AVATAR2ProVerif.makeAttrName(ab.getName(), simplifiedElements.get (asme).toString ()), new ProVerifVar[] {new ProVerifVar ("sessionID", "bitstring")});
this.spec.addDeclaration (p);
- // Read and decrypt control data: variables sent to the process and the call__num variable
+ // Read and decrypt control data: variables sent to the process and the call*** variable
this.dummyDataCounter ++;
- strong = "strong__" + AVATAR2ProVerif.makeAttrName (ab.getName(), simplifiedElements.get (asme).toString ()) + this.dummyDataCounter;
+ strong = "strong" + ATTR_DELIM + AVATAR2ProVerif.makeAttrName (ab.getName(), simplifiedElements.get (asme).toString ()) + this.dummyDataCounter;
p = p.setNextInstr (new ProVerifProcNew (strong, "bitstring"));
p = p.setNextInstr (new ProVerifProcRaw ("out (" + CHCTRL_CH + ", " + strong + ");"));
p = p.setNextInstr (new ProVerifProcIn (CHCTRL_CH, new ProVerifVar[] {new ProVerifVar ("chControlData", "bitstring")}));
LinkedList<ProVerifVar> attributes = new LinkedList<ProVerifVar> ();
attributes.add (new ProVerifVar ("sessionID", "bitstring", false, true));
- attributes.add (new ProVerifVar ("call__" + ab.getName () + "__" + simplifiedElements.get (asme), "bitstring", false, true));
+ attributes.add (new ProVerifVar ("call" + ATTR_DELIM + ab.getName () + ATTR_DELIM + simplifiedElements.get (asme), "bitstring", false, true));
attributes.add (new ProVerifVar (strong, "bitstring", false, true));
for (AvatarAttribute attr: ab.getAttributes ()) {
Integer c = attributeCmp.get (attr) + 1;
@@ -998,9 +999,9 @@ public class AVATAR2ProVerif implements AvatarTranslator {
if (n != null) {
// If next is the root of a process send the attributes on the control channel
this.dummyDataCounter ++;
- String strong = "strong__" + AVATAR2ProVerif.makeAttrName (arg.block.getName (), n.toString ()) + this.dummyDataCounter;
+ String strong = "strong" + ATTR_DELIM + AVATAR2ProVerif.makeAttrName (arg.block.getName (), n.toString ()) + this.dummyDataCounter;
arg.lastInstr = arg.lastInstr.setNextInstr (new ProVerifProcIn (CHCTRL_CH, new ProVerifVar[] {new ProVerifVar (strong, "bitstring")}));
- String tmp = "out (" + CHCTRL_CH + ", " + CHCTRL_ENCRYPT + " ((sessionID, call__" + arg.block.getName () + "__" + n + ", " + strong;
+ String tmp = "out (" + CHCTRL_CH + ", " + CHCTRL_ENCRYPT + " ((sessionID, call" + ATTR_DELIM + arg.block.getName () + ATTR_DELIM + n + ", " + strong;
for(AvatarAttribute aa: arg.block.getAttributes ())
tmp += ", " + AVATAR2ProVerif.translateTerm (aa, arg.attributeCmp);
@@ -1037,7 +1038,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
// Use a dummy name if no value is sent
if (_asme.getNbOfValues() == 0) {
this.dummyDataCounter ++;
- _lastInstr = _lastInstr.setNextInstr (new ProVerifProcNew ("data__" + this.dummyDataCounter, "bitstring"));
+ _lastInstr = _lastInstr.setNextInstr (new ProVerifProcNew ("data" + ATTR_DELIM + this.dummyDataCounter, "bitstring"));
}
String tmp = "out (" + CH_MAINCH + ", ";
@@ -1047,7 +1048,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
tmp +="(";
}
if (_asme.getNbOfValues() == 0)
- tmp += "data__" + this.dummyDataCounter;
+ tmp += "data" + ATTR_DELIM + this.dummyDataCounter;
else {
boolean first = true;
for(String value: _asme.getValues ()) {
@@ -1085,7 +1086,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
LinkedList<ProVerifVar> vars = new LinkedList<ProVerifVar> ();
if (_asme.getNbOfValues() == 0) {
this.dummyDataCounter ++;
- vars.add (new ProVerifVar ("data__" + this.dummyDataCounter, "bitstring"));
+ vars.add (new ProVerifVar ("data" + ATTR_DELIM + this.dummyDataCounter, "bitstring"));
} else
for(String value: _asme.getValues ()) {
AvatarTerm term = AvatarTerm.createFromString (arg.block, value);
@@ -1296,7 +1297,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
if (this.stateReachability == JDialogProverifVerification.REACHABILITY_ALL ||
(this.stateReachability == JDialogProverifVerification.REACHABILITY_SELECTED && _asme.isCheckable ()))
// Adding an event for reachability of the state
- _lastInstr = _lastInstr.setNextInstr (new ProVerifProcRaw ("event enteringState__" + arg.block.getName() + "__" + _asme.getName() + "()", true));
+ _lastInstr = _lastInstr.setNextInstr (new ProVerifProcRaw ("event enteringState" + ATTR_DELIM + arg.block.getName() + ATTR_DELIM + _asme.getName() + "()", true));
// Adding an event if authenticity is concerned with that state
HashSet<String> authenticityEvents = new HashSet<String> ();
@@ -1308,7 +1309,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
TraceManager.addDev ("DEBUG: " + attrA.getAttribute ());
TraceManager.addDev ("DEBUG: " + attrA.getAttribute ().getBlock ());
TraceManager.addDev ("DEBUG: " + arg.attributeCmp.get (attrA.getAttribute()));
- String sp = "authenticity__" + AVATAR2ProVerif.makeAttrName (attrA.getAttribute ().getBlock ().getName (), attrA.getAttribute ().getName (), _asme.getName ()) + " (" + AVATAR2ProVerif.makeAttrName (attrA.getAttribute ().getBlock ().getName (), attrA.getAttribute ().getName (), arg.attributeCmp.get (attrA.getAttribute ()).toString ()) + ")";
+ String sp = "authenticity" + ATTR_DELIM + AVATAR2ProVerif.makeAttrName (attrA.getAttribute ().getBlock ().getName (), attrA.getAttribute ().getName (), _asme.getName ()) + " (" + AVATAR2ProVerif.makeAttrName (attrA.getAttribute ().getBlock ().getName (), attrA.getAttribute ().getName (), arg.attributeCmp.get (attrA.getAttribute ()).toString ()) + ")";
if (!authenticityEvents.contains (sp)) {
authenticityEvents.add (sp);
TraceManager.addDev("| | authenticity event " + sp + "added");
@@ -1316,7 +1317,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
}
}
if (attrB.getAttribute ().getBlock () == arg.block && attrB.getState ().getName ().equals (_asme.getName ())) {
- String sp = "authenticity__" + AVATAR2ProVerif.makeAttrName (attrB.getAttribute ().getBlock ().getName (), attrB.getAttribute ().getName (), _asme.getName ()) + " (" + AVATAR2ProVerif.makeAttrName (attrB.getAttribute ().getBlock ().getName (), attrB.getAttribute ().getName (), arg.attributeCmp.get (attrB.getAttribute ()).toString ()) + ")";
+ String sp = "authenticity" + ATTR_DELIM + AVATAR2ProVerif.makeAttrName (attrB.getAttribute ().getBlock ().getName (), attrB.getAttribute ().getName (), _asme.getName ()) + " (" + AVATAR2ProVerif.makeAttrName (attrB.getAttribute ().getBlock ().getName (), attrB.getAttribute ().getName (), arg.attributeCmp.get (attrB.getAttribute ()).toString ()) + ")";
if (!authenticityEvents.contains (sp)) {
authenticityEvents.add (sp);
TraceManager.addDev("| | authenticity event " + sp + "added");
@@ -1352,16 +1353,16 @@ public class AVATAR2ProVerif implements AvatarTranslator {
} else {
TraceManager.addDev("| | non deterministic next state");
for (int i=0; i<nbOfNexts-1; i++) {
- String choice = "choice__" + _asme.getName () + "__" + i;
+ String choice = "choice" + ATTR_DELIM + _asme.getName () + ATTR_DELIM + i;
_lastInstr = _lastInstr.setNextInstr (new ProVerifProcNew (choice, "bitstring"));
_lastInstr = _lastInstr.setNextInstr (new ProVerifProcRaw ("out (" + CH_MAINCH + ", " + choice + ");"));
}
- _lastInstr = _lastInstr.setNextInstr (new ProVerifProcIn (CH_MAINCH, new ProVerifVar[] {new ProVerifVar ("choice__" + _asme.getName (), "bitstring")}));
+ _lastInstr = _lastInstr.setNextInstr (new ProVerifProcIn (CH_MAINCH, new ProVerifVar[] {new ProVerifVar ("choice" + ATTR_DELIM + _asme.getName (), "bitstring")}));
HashMap<AvatarAttribute, Integer> attributeCmp = arg.attributeCmp;
for (int i=0; i<nbOfNexts-1; i++) {
- String choice = "choice__" + _asme.getName () + "__" + i;
- ProVerifProcITE ite = new ProVerifProcITE ("choice__" + _asme.getName () + " = " + choice);
+ String choice = "choice" + ATTR_DELIM + _asme.getName () + ATTR_DELIM + i;
+ ProVerifProcITE ite = new ProVerifProcITE ("choice" + ATTR_DELIM + _asme.getName () + " = " + choice);
arg.attributeCmp = new HashMap<AvatarAttribute, Integer> (attributeCmp);
arg.lastASME = _asme;
diff --git a/src/proverifspec/ProVerifOutputAnalyzer.java b/src/proverifspec/ProVerifOutputAnalyzer.java
index 05515fee96..7047ef033c 100644
--- a/src/proverifspec/ProVerifOutputAnalyzer.java
+++ b/src/proverifspec/ProVerifOutputAnalyzer.java
@@ -45,242 +45,404 @@
package proverifspec;
-import java.util.*;
-import java.util.regex.*;
-import myutil.*;
-import java.io.*;
+import java.io.BufferedReader;
+import java.io.StringReader;
+import java.io.IOException;
+import java.util.HashMap;
+import java.util.LinkedList;
+import java.util.List;
+import java.util.regex.Pattern;
+
+import myutil.TraceManager;
import avatartranslator.toproverif.AVATAR2ProVerif;
import avatartranslator.AvatarAttribute;
import avatartranslator.AvatarBlock;
+import avatartranslator.AvatarState;
+import avatartranslator.AvatarPragma;
+import avatartranslator.AvatarPragmaAuthenticity;
+import avatartranslator.AvatarPragmaReachability;
+import avatartranslator.AvatarPragmaSecret;
public class ProVerifOutputAnalyzer {
-
-
- private LinkedList<String> reachableEvents;
- private LinkedList<String> nonReachableEvents;
- private LinkedList<String> secretTerms;
- private LinkedList<String> nonSecretTerms;
- private LinkedList<String> satisfiedAuthenticity;
- private LinkedList<String> satisfiedWeakAuthenticity;
- private LinkedList<String> nonSatisfiedAuthenticity;
- private LinkedList<String> errors;
- private LinkedList<String> notproved;
- private final static String typedEvent = "not event(";
- private final static String untypedEvent = "not ev:";
+ private final static String typedEvent = "not event(enteringState" + AVATAR2ProVerif.ATTR_DELIM;
+ private final static String untypedEvent = "not ev:enteringState" + AVATAR2ProVerif.ATTR_DELIM;
private final static String typedFalse = ") is false";
private final static String typedTrue = ") is true";
+ private final static String typedCannotBeProved = ") cannot be proved";
+ private final static String untypedCannotBeProved = " cannot be proved";
private final static String untypedFalse = " is false";
private final static String untypedTrue = " is true";
private final static String typedSecret = "not attacker(";
private final static String untypedSecret = "not attacker:";
- private final static String typedStrongAuth = "inj-event(authenticity__";
- private final static String untypedStrongAuth = "evinj:authenticity__";
- private final static String typedWeakAuth = "(but event(authenticity__";
- private final static String untypedWeakAuth = "(but ev:authenticity__";
- private final static String typedAuthSplit = "==> inj-event(authenticity__";
- private final static String typedWeakAuthSplit = "==> event(authenticity__";
- private final static String untypedAuthSplit = "==> evinj:authenticity__";
- private final static String untypedWeakAuthSplit = "==> ev:authenticity__";
+ private final static String typedStrongAuth = "inj-event(authenticity" + AVATAR2ProVerif.ATTR_DELIM;
+ private final static String untypedStrongAuth = "evinj:authenticity" + AVATAR2ProVerif.ATTR_DELIM;
+ private final static String typedWeakAuth = "(but event(authenticity" + AVATAR2ProVerif.ATTR_DELIM;
+ private final static String untypedWeakAuth = "(but ev:authenticity" + AVATAR2ProVerif.ATTR_DELIM;
+ private final static String typedWeakNonAuth = "(even event(authenticity" + AVATAR2ProVerif.ATTR_DELIM;
+ private final static String untypedWeakNonAuth = "(even ev:authenticity" + AVATAR2ProVerif.ATTR_DELIM;
+ private final static String typedAuthSplit = "==> inj-event(authenticity" + AVATAR2ProVerif.ATTR_DELIM;
+ private final static String typedWeakAuthSplit = "==> event(authenticity" + AVATAR2ProVerif.ATTR_DELIM;
+ private final static String untypedAuthSplit = "==> evinj:authenticity" + AVATAR2ProVerif.ATTR_DELIM;
+ private final static String untypedWeakAuthSplit = "==> ev:authenticity" + AVATAR2ProVerif.ATTR_DELIM;
+
+ private HashMap<AvatarPragma, ProVerifQueryResult> results;
+ private LinkedList<String> errors;
private AVATAR2ProVerif avatar2proverif;
public ProVerifOutputAnalyzer(AVATAR2ProVerif avatar2proverif) {
this.avatar2proverif = avatar2proverif;
-
- reachableEvents = new LinkedList<String>();
- nonReachableEvents = new LinkedList<String>();
- secretTerms = new LinkedList<String>();
- nonSecretTerms = new LinkedList<String>();
- satisfiedAuthenticity = new LinkedList<String>();
- satisfiedWeakAuthenticity = new LinkedList<String>();
- nonSatisfiedAuthenticity = new LinkedList<String>();
-
- errors = new LinkedList<String>();
- notproved = new LinkedList<String>();
+ this.errors = null;
+ this.results = null;
}
- public void analyzeTypedOutput(String _s) {
- String str, previous="";
- int index0, index1;
-
+ public void analyzeOutput(String _s, boolean isTyped) {
BufferedReader reader = new BufferedReader(new StringReader(_s));
+ List<AvatarPragma> pragmas = this.avatar2proverif.getAvatarSpecification().getPragmas();
+ String previous = null;
+ String str;
+ ProVerifQueryAuthResult previousAuthPragma = null;
+
+ this.results = new HashMap<AvatarPragma, ProVerifQueryResult> ();
+ this.errors = new LinkedList<String>();
+
try {
- while ((str = reader.readLine()) != null) {
- if (str.contains("RESULT")){
- if (str.contains(typedEvent)){
- if (str.contains(typedTrue)){
- //Add string between tags
- //Pattern.quote converts string into regex adding escape characters
- nonReachableEvents.add(str.split(Pattern.quote(typedEvent))[1].split(Pattern.quote(typedTrue))[0]);
- }
- else if (str.contains(typedFalse)) {
- reachableEvents.add(str.split(Pattern.quote(typedEvent))[1].split(Pattern.quote(typedFalse))[0]);
+
+ // Loop through every line in the output
+ while ((str = reader.readLine()) != null)
+ {
+ // Found a line with a RESULT
+ if (str.startsWith("RESULT "))
+ {
+ // Remove 'RESULT ' at the begining
+ str = str.substring(7);
+ TraceManager.addDev("[DEBUG] Found Result : " + str);
+
+ // This concerns an enteringState event
+ if (str.startsWith(isTyped ? typedEvent : untypedEvent))
+ {
+ TraceManager.addDev("[DEBUG] Reachability");
+ str = str.substring((isTyped ? typedEvent : untypedEvent).length());
+ String stateName = null;
+ boolean proved = true;
+ boolean satisfied = true;
+
+ previousAuthPragma = null;
+
+ if (isTyped)
+ {
+ if (str.contains(typedTrue))
+ {
+ satisfied = false;
+ stateName = str.split(Pattern.quote(typedTrue))[0];
+ }
+ else if (str.contains(typedFalse))
+ {
+ // TODO: Add trace
+ stateName = str.split(Pattern.quote(typedFalse))[0];
+ }
+ else if (str.contains(typedCannotBeProved))
+ {
+ // TODO: Add trace
+ proved = false;
+ stateName = str.split(Pattern.quote(typedCannotBeProved))[0];
+ }
}
- }
- else if (str.contains(typedSecret)){
- if (str.contains(typedTrue)){
- //Add string between tags
- secretTerms.add(str.split(Pattern.quote(typedSecret))[1].split("\\[")[0]);
+ else
+ {
+ stateName = str.split("\\(")[0];
+ if (str.contains(untypedTrue))
+ {
+ satisfied = false;
+ }
+ else if (str.contains(untypedFalse))
+ {
+ // TODO: Add trace
+ }
+ else if (str.contains(untypedCannotBeProved))
+ {
+ // TODO: Add trace
+ proved = false;
+ }
}
- else if (str.contains(typedFalse)) {
- nonSecretTerms.add(str.split(Pattern.quote(typedSecret))[1].split("\\[")[0]);
+
+ AvatarPragmaReachability reachabilityPragma = this.getAvatarPragmaReachabilityFromString(stateName);
+ if (reachabilityPragma != null)
+ {
+ TraceManager.addDev("[DEBUG] " + reachabilityPragma.toString());
+ this.results.put(reachabilityPragma, new ProVerifQueryResult(proved, satisfied));
}
}
- else if (str.contains(typedStrongAuth)){
- if (str.contains(typedTrue)){
- //Add string between tags
- satisfiedAuthenticity.add(str.split(Pattern.quote(typedStrongAuth))[1].split("\\(")[0] + " ==> " + str.split(Pattern.quote(typedAuthSplit))[1].split("\\(")[0]);
+
+ // This concerns a confidentiality check
+ else if (str.contains(isTyped ? typedSecret : untypedSecret))
+ {
+ String attributeName = str.substring((isTyped ? typedSecret : untypedSecret).length()).split("\\[")[0];
+ TraceManager.addDev("[DEBUG] Confidentiality");
+
+ boolean proved = true;
+ boolean satisfied = true;
+
+ previousAuthPragma = null;
+
+ if (str.contains(isTyped ? typedFalse : untypedFalse))
+ {
+ // TODO: Add trace
+ satisfied = false;
}
- else if (str.contains(typedFalse)) {
- nonSatisfiedAuthenticity.add(str.split(Pattern.quote(typedStrongAuth))[1].split("\\(")[0] + " ==> " + str.split(Pattern.quote(typedAuthSplit))[1].split("\\(")[0]);
+ else if (str.contains(isTyped ? typedCannotBeProved : untypedCannotBeProved))
+ {
+ // TODO: Add trace
+ proved = false;
}
- else if (str.contains("cannot be proved")){
- notproved.add("Strong Authenticity "+ str.split(Pattern.quote(typedStrongAuth))[1].split("\\(")[0] + " ==> " + str.split(Pattern.quote(typedAuthSplit))[1].split("\\(")[0]);
- }
- }
- else if (str.contains(typedWeakAuth)) {
- if (str.contains(typedTrue)){
- //Add string between tags
- satisfiedWeakAuthenticity.add(str.split(Pattern.quote(typedWeakAuth))[1].split("\\(")[0] + " ==> " + str.split(Pattern.quote(typedWeakAuthSplit))[1].split("\\(")[0]);
+
+ AvatarAttribute attribute = this.getAvatarAttributeFromString(attributeName);
+ if (attribute != null)
+ {
+ for (AvatarPragma pragma: pragmas)
+ {
+ ProVerifQueryResult res = new ProVerifQueryResult(proved, satisfied);
+ if (pragma instanceof AvatarPragmaSecret
+ && this.avatar2proverif.getTrueName(((AvatarPragmaSecret) pragma).getArg()).equals(attributeName))
+ {
+ TraceManager.addDev("[DEBUG] " + pragma.toString());
+ this.results.put(pragma, res);
+ }
+ }
}
- else if (str.contains("cannot be proved")){
- notproved.add("Weak Authenticity "+ str.split(Pattern.quote(typedWeakAuth))[1].split("\\(")[0] + " ==> " + str.split(Pattern.quote(typedWeakAuthSplit))[1].split("\\(")[0]);
- }
}
- }
- if (str.contains("Error:")){
- errors.add(str + ": " + previous);
- }
- else if (str.contains("cannot be proved")){
- // notproved.add(str);
- }
- previous = str;
- }
- } catch(IOException e) {
- e.printStackTrace();
- }
- }
- public void analyzeOutput(String _s, boolean isTyped) {
- String str, previous="";
- int index0, index1;
- if (isTyped) {
- analyzeTypedOutput(_s);
- return;
- }
- BufferedReader reader = new BufferedReader(new StringReader(_s));
- try {
- while ((str = reader.readLine()) != null) {
- if (str.contains("RESULT")){
- if (str.contains(untypedEvent)){
- if (str.contains(untypedTrue)){
- //Add string between tags
- //Pattern.quote converts string into regex adding escape characters
- nonReachableEvents.add(str.split(Pattern.quote(untypedEvent))[1].split("\\(")[0]);
+ // This concerns a strong authenticity check
+ else if (str.contains(isTyped ? typedStrongAuth : untypedStrongAuth))
+ {
+ str = str.substring((isTyped ? typedStrongAuth : untypedStrongAuth).length());
+ TraceManager.addDev("[DEBUG] Authenticity");
+
+ String attributeStateName1 = null;
+ String attributeStateName2 = null;
+ boolean proved = true;
+ boolean satisfied = true;
+
+ previousAuthPragma = null;
+
+ if (isTyped)
+ {
+ attributeStateName1 = str.split("\\(")[0];
+ attributeStateName2 = str.split(Pattern.quote(typedAuthSplit))[1].split("\\(")[0];
+ if (str.contains(typedFalse))
+ {
+ // TODO: Add trace
+ satisfied = false;
+ }
+ else if (str.contains(typedCannotBeProved))
+ {
+ // TODO: Add trace
+ proved = false;
+ }
}
- else if (str.contains(untypedFalse)) {
- reachableEvents.add(str.split(Pattern.quote(untypedEvent))[1].split("\\(")[0]);
+ else
+ {
+ attributeStateName1 = str.split("\\(")[0];
+ attributeStateName2 = str.split(untypedAuthSplit)[1].split("\\(")[0];
+ if (str.contains(untypedFalse))
+ {
+ // TODO: Add trace
+ satisfied = false;
+ }
+ else if (str.contains(untypedCannotBeProved))
+ {
+ // TODO: Add trace
+ proved = false;
+ }
}
- }
- else if (str.contains(untypedSecret)){
- if (str.contains(untypedTrue)){
- //Add string between tags
- secretTerms.add(str.split(Pattern.quote(untypedSecret))[1].split("\\[")[0]);
+
+ AvatarAttribute attribute1 = null;
+ AvatarAttribute attribute2 = null;
+ AvatarState state1 = null;
+ AvatarState state2 = null;
+
+ String[] tmp = attributeStateName1.split(AVATAR2ProVerif.ATTR_DELIM);
+ if (tmp.length == 3)
+ {
+ attribute1 = this.getAvatarAttributeFromString(tmp[0] + AVATAR2ProVerif.ATTR_DELIM + tmp[1]);
+ state1 = this.getAvatarStateFromString(tmp[0] + AVATAR2ProVerif.ATTR_DELIM + tmp[2]);
}
- else if (str.contains(untypedFalse)) {
- nonSecretTerms.add(str.split(Pattern.quote(untypedSecret))[1].split("\\[")[0]);
+
+ tmp = attributeStateName2.split(AVATAR2ProVerif.ATTR_DELIM);
+ if (tmp.length == 3)
+ {
+ attribute2 = this.getAvatarAttributeFromString(tmp[0] + AVATAR2ProVerif.ATTR_DELIM + tmp[1]);
+ state2 = this.getAvatarStateFromString(tmp[0] + AVATAR2ProVerif.ATTR_DELIM + tmp[2]);
}
- }
- else if (str.contains(untypedStrongAuth)){
- if (str.contains(untypedTrue)){
- //Add string between tags
- satisfiedAuthenticity.add(str.split(untypedStrongAuth)[1].split(untypedAuthSplit)[0].split("\\(")[0] + " ==> " + str.split(untypedAuthSplit)[1].split("\\(")[0]);
+
+ if (attribute1 != null && attribute2 != null && state1 != null && state2 != null)
+ {
+ for (AvatarPragma pragma: pragmas)
+ {
+ if (pragma instanceof AvatarPragmaAuthenticity)
+ {
+ AvatarPragmaAuthenticity pragmaAuth = (AvatarPragmaAuthenticity) pragma;
+ if (pragmaAuth.getAttrA().getState() == state2
+ && pragmaAuth.getAttrA().getAttribute() == attribute2
+ && pragmaAuth.getAttrB().getState() == state1
+ && pragmaAuth.getAttrB().getAttribute() == attribute1)
+ {
+ previousAuthPragma = new ProVerifQueryAuthResult(proved, satisfied);
+ TraceManager.addDev("[DEBUG] " + pragma);
+ this.results.put(pragma, previousAuthPragma);
+ break;
+ }
+ }
+ }
}
- else if (str.contains(untypedFalse)) {
- nonSatisfiedAuthenticity.add(str.split(Pattern.quote(untypedStrongAuth))[1].split("\\(")[0] + " ==> " + str.split(Pattern.quote(untypedAuthSplit))[1].split("\\(")[0]);
+ }
+
+ // This concerns a satsified weak authenticity check
+ else if (str.contains(isTyped ? typedWeakAuth : untypedWeakAuth))
+ {
+
+ if (previousAuthPragma != null)
+ {
+ previousAuthPragma.setWeakSatisfied(true);
}
- else if (str.contains("cannot be proved")){
- notproved.add("Strong Authenticity "+ str.split(Pattern.quote(untypedStrongAuth))[1].split("\\(")[0] + " ==> " + str.split(Pattern.quote(untypedAuthSplit))[1].split("\\(")[0]);
- }
+ previousAuthPragma = null;
}
- else if (str.contains(untypedWeakAuth)) {
- if (str.contains(untypedTrue)){
- //Add string between tags
- satisfiedWeakAuthenticity.add(str.split(Pattern.quote(untypedWeakAuth))[1].split("\\(")[0] + " ==> " + str.split(Pattern.quote(untypedWeakAuthSplit))[1].split("\\(")[0]);
- }
- else if (str.contains("cannot be proved")){
- notproved.add("Weak Authenticity "+ str.split(Pattern.quote(untypedWeakAuth))[1].split("\\(")[0] + " ==> " + str.split(Pattern.quote(untypedWeakAuthSplit))[1].split("\\(")[0]);
- }
+
+ // This concerns a failed weak authenticity check
+ else if (str.contains(isTyped ? typedWeakAuth : untypedWeakAuth))
+ {
+
+ if (previousAuthPragma != null)
+ {
+ previousAuthPragma.setWeakSatisfied(false);
+ }
+ previousAuthPragma = null;
}
}
- if (str.contains("Error:")){
- errors.add(str + ": " + previous);
+
+ // Found an error
+ else if (str.contains("Error:"))
+ {
+ this.errors.add(str + ": " + previous);
}
- else if (str.contains("cannot be proved")){
- // notproved.add(str);
- }
- previous = str;
+
+ previous = str;
}
+
+ TraceManager.addDev("[DEBUG] --- END ---");
+
} catch(IOException e) {
e.printStackTrace();
}
}
- public LinkedList<String> getReachableEvents() {
- return reachableEvents;
+ private AvatarAttribute getAvatarAttributeFromString(String name)
+ {
+ String[] tmp = name.split(AVATAR2ProVerif.ATTR_DELIM);
+ if (tmp.length != 2)
+ return null;
+
+ AvatarBlock block = this.avatar2proverif.getAvatarSpecification().getBlockWithName(tmp[0]);
+ if (block == null)
+ return null;
+
+ return block.getAvatarAttributeWithName(tmp[1]);
}
- public LinkedList<String> getNonReachableEvents() {
- return nonReachableEvents;
+ private AvatarPragmaReachability getAvatarPragmaReachabilityFromString(String name)
+ {
+ String[] tmp = name.split(AVATAR2ProVerif.ATTR_DELIM);
+ if (tmp.length != 2)
+ return null;
+
+ AvatarBlock block = this.avatar2proverif.getAvatarSpecification().getBlockWithName(tmp[0]);
+ if (block == null)
+ return null;
+
+ AvatarState state = block.getStateMachine().getStateWithName(tmp[1]);
+ if (state == null)
+ return null;
+
+ return new AvatarPragmaReachability("reachability" + AVATAR2ProVerif.ATTR_DELIM + name, null, block, state);
}
- public LinkedList<AvatarAttribute> getSecretTerms() {
- LinkedList<AvatarAttribute> result = new LinkedList<AvatarAttribute> ();
- for (AvatarBlock block: this.avatar2proverif.getAvatarSpecification ().getListOfBlocks ())
- for (AvatarAttribute attr: block.getAttributes ()) {
- String trueName = this.avatar2proverif.getTrueName (attr);
- if (this.secretTerms.contains (trueName))
- result.add (attr);
- }
- return result;
+ private AvatarState getAvatarStateFromString(String name)
+ {
+ String[] tmp = name.split(AVATAR2ProVerif.ATTR_DELIM);
+ if (tmp.length != 2)
+ return null;
+
+ AvatarBlock block = this.avatar2proverif.getAvatarSpecification().getBlockWithName(tmp[0]);
+ if (block == null)
+ return null;
+
+ AvatarState state = block.getStateMachine().getStateWithName(tmp[1]);
+
+ return state;
}
- // FIXME what about cannot be proved ?
+ public HashMap<AvatarPragma, ProVerifQueryResult> getResults()
+ {
+ return this.results;
+ }
- public LinkedList<String> getNonSecretStrings(){
- return nonSecretTerms;
- }
+ public HashMap<AvatarPragmaSecret, ProVerifQueryResult> getConfidentialityResults()
+ {
+ if (this.results == null)
+ return null;
- public LinkedList<AvatarAttribute> getNonSecretTerms() {
- LinkedList<AvatarAttribute> result = new LinkedList<AvatarAttribute> ();
- for (AvatarBlock block: this.avatar2proverif.getAvatarSpecification ().getListOfBlocks ())
- for (AvatarAttribute attr: block.getAttributes ()) {
- String trueName = this.avatar2proverif.getTrueName (attr);
- if (this.nonSecretTerms.contains (trueName))
- result.add (attr);
+ HashMap<AvatarPragmaSecret, ProVerifQueryResult> resultMap = new HashMap<AvatarPragmaSecret, ProVerifQueryResult> ();
+
+ for (AvatarPragma pragma: this.results.keySet())
+ {
+ if (pragma instanceof AvatarPragmaSecret)
+ {
+ resultMap.put((AvatarPragmaSecret) pragma, this.results.get(pragma));
}
- return result;
- }
+ }
- public LinkedList<String> getSatisfiedAuthenticity() {
- return satisfiedAuthenticity;
+ return resultMap;
}
- public LinkedList<String> getSatisfiedWeakAuthenticity() {
- return satisfiedWeakAuthenticity;
+
+ public HashMap<AvatarPragmaReachability, ProVerifQueryResult> getReachabilityResults()
+ {
+ if (this.results == null)
+ return null;
+
+ HashMap<AvatarPragmaReachability, ProVerifQueryResult> resultMap = new HashMap<AvatarPragmaReachability, ProVerifQueryResult> ();
+
+ for (AvatarPragma pragma: this.results.keySet())
+ {
+ if (pragma instanceof AvatarPragmaReachability)
+ {
+ resultMap.put((AvatarPragmaReachability) pragma, this.results.get(pragma));
+ }
+ }
+
+ return resultMap;
}
- public LinkedList<String> getNonSatisfiedAuthenticity() {
- return nonSatisfiedAuthenticity;
+ public HashMap<AvatarPragmaAuthenticity, ProVerifQueryAuthResult> getAuthenticityResults()
+ {
+ if (this.results == null)
+ return null;
+
+ HashMap<AvatarPragmaAuthenticity, ProVerifQueryAuthResult> resultMap = new HashMap<AvatarPragmaAuthenticity, ProVerifQueryAuthResult> ();
+
+ for (AvatarPragma pragma: this.results.keySet())
+ {
+ if (pragma instanceof AvatarPragmaAuthenticity)
+ {
+ resultMap.put((AvatarPragmaAuthenticity) pragma, (ProVerifQueryAuthResult) this.results.get(pragma));
+ }
+ }
+
+ return resultMap;
}
public LinkedList<String> getErrors() {
return errors;
}
-
- public LinkedList<String> getNotProved() {
- return notproved;
- }
-
}
diff --git a/src/proverifspec/ProVerifQueryAuthResult.java b/src/proverifspec/ProVerifQueryAuthResult.java
new file mode 100644
index 0000000000..63c037f4ef
--- /dev/null
+++ b/src/proverifspec/ProVerifQueryAuthResult.java
@@ -0,0 +1,73 @@
+/**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 ProVerifQueryAuthResult
+ * Creation: 19/05/2017
+ * @version 1.0 19/05/2017
+ * @author Florian LUGOU
+ * @see
+ */
+
+package proverifspec;
+
+public class ProVerifQueryAuthResult extends ProVerifQueryResult {
+ protected boolean weakSatisfied, weakProved;
+
+ public ProVerifQueryAuthResult(boolean proved, boolean satisfied)
+ {
+ super(proved, satisfied);
+ this.weakSatisfied = true;
+ this.weakProved = (proved && satisfied);
+ }
+
+ public boolean isWeakProved()
+ {
+ return this.weakProved;
+ }
+
+ public boolean isWeakSatisfied()
+ {
+ return this.weakSatisfied;
+ }
+
+ public void setWeakSatisfied(boolean satisfied)
+ {
+ this.weakProved = true;
+ this.weakSatisfied = satisfied;
+ }
+}
diff --git a/src/proverifspec/ProVerifQueryResult.java b/src/proverifspec/ProVerifQueryResult.java
new file mode 100644
index 0000000000..abea9bfbe4
--- /dev/null
+++ b/src/proverifspec/ProVerifQueryResult.java
@@ -0,0 +1,66 @@
+/**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 ProVerifQueryResult
+ * Creation: 17/05/2017
+ * @version 1.0 17/05/2017
+ * @author Florian LUGOU
+ * @see
+ */
+
+package proverifspec;
+
+public class ProVerifQueryResult {
+ protected boolean satisfied, proved;
+
+ public ProVerifQueryResult(boolean proved, boolean satisfied)
+ {
+ this.satisfied = satisfied;
+ this.proved = proved;
+ }
+
+ public boolean isProved()
+ {
+ return this.proved;
+ }
+
+ public boolean isSatisfied()
+ {
+ return this.satisfied;
+ }
+}
diff --git a/src/tmltranslator/TMLModeling.java b/src/tmltranslator/TMLModeling.java
index bee0b1c30e..fb1c6b281c 100755
--- a/src/tmltranslator/TMLModeling.java
+++ b/src/tmltranslator/TMLModeling.java
@@ -692,15 +692,22 @@ public class TMLModeling {
}
public void backtrace(ProVerifOutputAnalyzer pvoa, String mappingName){
- System.out.println("Backtracing Confidentiality");
- LinkedList<AvatarAttribute> secretAttributes = pvoa.getSecretTerms ();
- LinkedList<AvatarAttribute> nonSecretAttributes = pvoa.getNonSecretTerms ();
- for (AvatarAttribute attr: secretAttributes){
+ //System.out.println("Backtracing Confidentiality");
+ HashMap<AvatarPragmaSecret, ProVerifQueryResult> confResults = pvoa.getConfidentialityResults();
+
+ for (AvatarPragmaSecret pragma: confResults.keySet()) {
+ ProVerifQueryResult result = confResults.get(pragma);
+ if (!result.isProved())
+ continue;
+ int r = result.isSatisfied() ? 2 : 3;
+
+ AvatarAttribute attr = pragma.getArg();
+
TMLChannel channel = getChannelByShortName(attr.getName().replaceAll("_chData",""));
if (channel!=null){
for (TMLCPrimitivePort port:channel.ports){
if (port.checkConf){
- port.checkConfStatus = 2;
+ port.checkConfStatus = r;
port.mappingName= mappingName;
}
}
@@ -709,7 +716,7 @@ public class TMLModeling {
if (req !=null){
for (TMLCPrimitivePort port: req.ports){
if (port.checkConf){
- port.checkConfStatus = 2;
+ port.checkConfStatus = r;
port.mappingName= mappingName;
}
}
@@ -717,29 +724,28 @@ public class TMLModeling {
TMLEvent ev = getEventByName(attr.getName().replaceAll("_eventData",""));
if (ev !=null){
if (ev.port.checkConf){
- ev.port.checkConfStatus=2;
+ ev.port.checkConfStatus=r;
ev.port.mappingName= mappingName;
}
if (ev.port2.checkConf){
- ev.port2.checkConfStatus=2;
+ ev.port2.checkConfStatus=r;
ev.port2.mappingName=mappingName;
}
}
List<String> channels=secChannelMap.get(attr.getName());
- if (channels!=null){
- for (String channelName: channels){
- // if (channelName!=null){
- channel = getChannelByShortName(channelName);
- if (channel!=null){
- for (TMLCPrimitivePort port:channel.ports){
- if (port.checkConf){
- port.checkSecConfStatus = 2;
- port.secName= attr.getName();
- }
- }
- }
- }
- }
+ if (channels != null) {
+ for (String channelName: channels) {
+ channel = getChannelByShortName(channelName);
+ if (channel!=null){
+ for (TMLCPrimitivePort port:channel.ports){
+ if (port.checkConf){
+ port.checkSecConfStatus = r;
+ port.secName= attr.getName();
+ }
+ }
+ }
+ }
+ }
for (TMLTask t:getTasks()){
if (t.getReferenceObject()==null){
continue;
@@ -749,381 +755,322 @@ public class TMLModeling {
comp.mappingName=mappingName;
for (TAttribute a: comp.getAttributes ())
if (a.getId().equals(attr.getName()))
- a.setConfidentialityVerification(TAttribute.CONFIDENTIALITY_OK);
- }
- }
- }
- for (AvatarAttribute attr: nonSecretAttributes){
- TMLChannel channel = getChannelByShortName(attr.getName().replaceAll("_chData",""));
- if (channel!=null){
- for (TMLCPrimitivePort port:channel.ports){
- if (port.checkConf){
- port.checkConfStatus = 3;
- port.mappingName= mappingName;
- }
- }
- }
- TMLRequest req = getRequestByName(attr.getName().replaceAll("_reqData",""));
- if (req !=null){
- for (TMLCPrimitivePort port: req.ports){
- if (port.checkConf){
- port.checkConfStatus = 3;
- port.mappingName= mappingName;
- }
- }
- }
- TMLEvent ev = getEventByName(attr.getName().replaceAll("_eventData",""));
- if (ev !=null){
- if (ev.port.checkConf){
- ev.port.checkConfStatus=3;
- ev.port.mappingName= mappingName;
- }
- if (ev.port2.checkConf){
- ev.port2.checkConfStatus=3;
- ev.port2.mappingName= mappingName;
- }
- }
- List<String> channels=secChannelMap.get(attr.getName());
- if (channels!=null){
- for (String channelName: channels){
-// if (channelName!=null){
- channel = getChannelByShortName(channelName);
- if (channel!=null){
- for (TMLCPrimitivePort port:channel.ports){
- if (port.checkConf){
- port.checkSecConfStatus = 3;
- port.secName= attr.getName();
- }
- }
- }
- }
- }
- for (TMLTask t:getTasks()){
- if (t.getReferenceObject() instanceof TMLCPrimitiveComponent){
- TMLCPrimitiveComponent comp = (TMLCPrimitiveComponent) t.getReferenceObject();
- comp.mappingName=mappingName;
- for (TAttribute a: comp.getAttributes ())
- if (a.getId().equals(attr.getName()) &&t.getName().equals(attr.getBlock().getName()))
- a.setConfidentialityVerification(TAttribute.CONFIDENTIALITY_KO);
+ a.setConfidentialityVerification(result.isSatisfied() ? TAttribute.CONFIDENTIALITY_OK : TAttribute.CONFIDENTIALITY_KO);
}
}
}
- System.out.println("Finished backtracing");
- return;
}
- public void backtraceAuthenticity(LinkedList<String> satisfiedAuthenticity, LinkedList<String> satisfiedWeakAuthenticity,LinkedList<String> nonSatisfiedAuthenticity, String mappingName){
- System.out.println("secchannelmap " + secChannelMap);
+
+ public void backtraceAuthenticity(HashMap<AvatarPragmaAuthenticity, ProVerifQueryAuthResult> authenticityResults, String mappingName) {
// System.out.println("Backtracing Authenticity");
- for (String s: satisfiedAuthenticity){
- String signalName = s.split("_chData")[0];
- /*for (TMLTask t: getTasks()){
- if (signalName.contains(t.getName())){
- signalName = signalName.replace(t.getName()+"__","");
- }
- }*/
- signalName = signalName.split("__")[1];
- TMLChannel channel = getChannelByShortName(signalName);
- if (channel!=null){
- for (TMLCPrimitivePort port:channel.ports){
- if (port.checkAuth){
- port.checkStrongAuthStatus = 2;
- port.mappingName= mappingName;
+ for (AvatarPragmaAuthenticity pragma: authenticityResults.keySet()) {
+ ProVerifQueryAuthResult result = authenticityResults.get(pragma);
+ // TODO: deal directly with pragma instead of s
+ String s = pragma.getAttrB().getAttribute().getBlock().getName()
+ + "__" + pragma.getAttrB().getAttribute().getName()
+ + "__" + pragma.getAttrB().getState().getName()
+ + " ==> "
+ + pragma.getAttrA().getAttribute().getBlock().getName()
+ + "__" + pragma.getAttrA().getAttribute().getName()
+ + "__" + pragma.getAttrA().getState().getName();
+
+ if (result.isProved() && result.isSatisfied())
+ {
+ String signalName = s.split("_chData")[0];
+ /*for (TMLTask t: getTasks()){
+ if (signalName.contains(t.getName())){
+ signalName = signalName.replace(t.getName()+"__","");
+ }
+ }*/
+ signalName = signalName.split("__")[1];
+ TMLChannel channel = getChannelByShortName(signalName);
+ if (channel!=null){
+ for (TMLCPrimitivePort port:channel.ports){
+ if (port.checkAuth){
+ port.checkStrongAuthStatus = 2;
+ port.mappingName= mappingName;
+ }
}
}
- }
- signalName = s.split("_reqData")[0];
- for (TMLTask t: getTasks()){
- if (signalName.contains(t.getName())){
- signalName = signalName.replace(t.getName()+"__","");
- }
- }
- TMLRequest req = getRequestByName(signalName);
- if (req !=null){
- for (TMLCPrimitivePort port: req.ports){
- if (port.checkAuth){
- port.checkStrongAuthStatus = 2;
- port.mappingName= mappingName;
+ signalName = s.split("_reqData")[0];
+ for (TMLTask t: getTasks()){
+ if (signalName.contains(t.getName())){
+ signalName = signalName.replace(t.getName()+"__","");
}
- }
- }
- signalName = s.split("_eventData")[0];
- for (TMLTask t: getTasks()){
- if (signalName.contains(t.getName())){
- signalName = signalName.replace(t.getName()+"__","");
- }
- }
- TMLEvent ev = getEventByName(signalName);
- if (ev !=null){
- if (ev.port.checkAuth){
- ev.port.checkStrongAuthStatus=2;
- ev.port2.mappingName= mappingName;
- }
- if (ev.port2.checkAuth){
- ev.port2.checkStrongAuthStatus=2;
- ev.port2.mappingName= mappingName;
- }
- }
-
- signalName = s.split("__decrypt")[0];
- /*for (TMLTask t: getTasks()){
- if (signalName.contains(t.getName())){
- signalName = signalName.replace(t.getName()+"__","");
- }
- }*/
- signalName=signalName.split("__")[1];
- List<String> channels=secChannelMap.get(signalName);
- if (channels!=null){
- for (String channelName: channels){
- // if (channelName!=null){
- channel = getChannelByShortName(channelName);
- if (channel!=null){
- for (TMLCPrimitivePort port:channel.ports){
- if (port.checkAuth){
- port.checkStrongAuthStatus = 2;
- port.secName= signalName;
- }
- }
- }
- }
- }
- }
- for (String s: satisfiedWeakAuthenticity){
- String signalName = s.split("_chData")[0];
- signalName = signalName.split("__")[1];
- TMLChannel channel = getChannelByShortName(signalName);
- if (channel!=null){
- for (TMLCPrimitivePort port:channel.ports){
- if (port.checkAuth){
- port.checkWeakAuthStatus = 2;
- port.mappingName= mappingName;
+ }
+ TMLRequest req = getRequestByName(signalName);
+ if (req !=null){
+ for (TMLCPrimitivePort port: req.ports){
+ if (port.checkAuth){
+ port.checkStrongAuthStatus = 2;
+ port.mappingName= mappingName;
+ }
}
}
- }
- signalName = s.split("_reqData")[0];
- for (TMLTask t: getTasks()){
- if (signalName.contains(t.getName())){
- signalName = signalName.replace(t.getName()+"__","");
- }
- }
- TMLRequest req = getRequestByName(signalName);
- if (req !=null){
- for (TMLCPrimitivePort port: req.ports){
- if (port.checkAuth){
- port.checkWeakAuthStatus = 2;
- port.mappingName= mappingName;
+ signalName = s.split("_eventData")[0];
+ for (TMLTask t: getTasks()){
+ if (signalName.contains(t.getName())){
+ signalName = signalName.replace(t.getName()+"__","");
}
}
- }
- signalName = s.split("__eventData")[0];
- for (TMLTask t: getTasks()){
- if (signalName.contains(t.getName())){
- signalName = signalName.replace(t.getName()+"__","");
- }
- }
- TMLEvent ev = getEventByName(signalName);
- if (ev !=null){
- if (ev.port.checkAuth){
- ev.port.checkWeakAuthStatus=2;
- ev.port2.mappingName= mappingName;
- }
- if (ev.port2.checkAuth){
- ev.port2.checkWeakAuthStatus=2;
- ev.port2.mappingName= mappingName;
- }
- }
- signalName = s.split("__decrypt")[0];
- /*for (TMLTask t: getTasks()){
- if (signalName.contains(t.getName())){
- signalName = signalName.replace(t.getName()+"__","");
- }
- }*/
- signalName = signalName.split("__")[1];
- List<String> channels=secChannelMap.get(signalName);
- if (channels!=null){
- for (String channelName:channels){
-// if (channelName!=null){
- System.out.println("original channel " + channelName);
- channel = getChannelByShortName(channelName);
- if (channel!=null){
- for (TMLCPrimitivePort port:channel.ports){
- if (port.checkAuth){
- port.checkWeakAuthStatus = 2;
- port.secName= signalName;
- }
- }
- }
- }
- }
- }
- for (String s: nonSatisfiedAuthenticity){
- System.out.println(s);
- String signalName = s.split("_chData")[0];
- /*for (TMLTask t: getTasks()){
- System.out.println(t.getName());
- if (signalName.contains(t.getName().split("__")[1])){
- signalName = signalName.split(t.getName().split("__")[1]+"__")[0];
- }
- }*/
- signalName = signalName.split("__")[1];
- // System.out.println("channels " + channels.get(0).getName());
- // System.out.println("signalName " + signalName);
- TMLChannel channel = getChannelByShortName(signalName);
- if (channel!=null){
- System.out.println("adding auth results to channel " + channel.getName());
- for (TMLCPrimitivePort port:channel.ports){
- if (port.checkAuth){
-
- port.checkStrongAuthStatus = 3;
- port.mappingName= mappingName;
+ TMLEvent ev = getEventByName(signalName);
+ if (ev !=null){
+ if (ev.port.checkAuth){
+ ev.port.checkStrongAuthStatus=2;
+ ev.port2.mappingName= mappingName;
}
- }
- }
- signalName = s.split("_reqData")[0];
- for (TMLTask t: getTasks()){
- if (signalName.contains(t.getName())){
- signalName = signalName.replace(t.getName()+"__","");
- }
- }
- TMLRequest req = getRequestByName(signalName);
- if (req !=null){
- for (TMLCPrimitivePort port: req.ports){
- if (port.checkAuth){
- port.checkStrongAuthStatus = 3;
- port.mappingName= mappingName;
+ if (ev.port2.checkAuth){
+ ev.port2.checkStrongAuthStatus=2;
+ ev.port2.mappingName= mappingName;
}
}
- }
- signalName = s.split("_eventData")[0];
- for (TMLTask t: getTasks()){
- if (signalName.contains(t.getName())){
- signalName = signalName.replace(t.getName()+"__","");
- }
- }
- TMLEvent ev = getEventByName(signalName);
- if (ev !=null){
- if (ev.port.checkAuth){
- ev.port.checkStrongAuthStatus=3;
- ev.port2.mappingName= mappingName;
- }
- if (ev.port2.checkAuth){
- ev.port2.checkStrongAuthStatus=3;
- ev.port2.mappingName= mappingName;
+
+ signalName = s.split("__decrypt")[0];
+ /*for (TMLTask t: getTasks()){
+ if (signalName.contains(t.getName())){
+ signalName = signalName.replace(t.getName()+"__","");
+ }
+ }*/
+ signalName=signalName.split("__")[1];
+ List<String> channels=secChannelMap.get(signalName);
+ if (channels!=null) {
+ for (String channelName: channels) {
+ channel = getChannelByShortName(channelName);
+ if (channel!=null){
+ for (TMLCPrimitivePort port:channel.ports){
+ if (port.checkAuth){
+ port.checkStrongAuthStatus = 2;
+ port.secName= signalName;
+ }
+ }
+ }
+ }
}
- }
- //Backtrace for security patterns
- signalName = s.split("__decrypt")[0];
- /*for (TMLTask t: getTasks()){
- if (signalName.contains(t.getName())){
- signalName = signalName.replace(t.getName()+"__","");
- }
- }*/
- List<String> channels=secChannelMap.get(signalName);
- if (channels!=null){
- for (String channelName:channels){
-// if (channelName!=null){
- channel = getChannelByShortName(channelName);
- if (channel!=null){
- for (TMLCPrimitivePort port:channel.ports){
- if (port.checkAuth){
- port.checkStrongAuthStatus = 3;
- port.secName= signalName;
- }
- }
- }
- }
- }
- }
- //In case of HSM
- for (String s: nonSatisfiedAuthenticity){
- String signalName = s.split("__decrypt")[0];
- signalName = signalName.split("__")[1];
- List<String> channels=secChannelMap.get(signalName);
- if (channels!=null){
- for (String channelName: channels){
- //if (channelName!=null){
- if (channelName.contains("retData_") || channelName.contains("data_")){
- channelName=channelName.replaceAll("retData_","").replaceAll("data_","");
- //channelName=channelName.split("__retData_")[1];
- String header= channelName.split("__retData_")[0];
- for (TMLTask t: getTasks()){
+ //In case of HSM
+ signalName = s.split("__decrypt")[0];
+ signalName = signalName.split("__")[1];
+ channels=secChannelMap.get(signalName);
+ if (channels!=null){
+ for (String channelName: channels){
+ if (channelName.contains("retData_") || channelName.contains("data_")){
+ channelName=channelName.replaceAll("retData_","").replaceAll("data_","");
+ String header= channelName.split("__retData_")[0];
+ for (TMLTask t: getTasks()){
if (channelName.contains(t.getName().split("__")[1])){
- channelName = channelName.replace("_"+t.getName().split("__")[1],"");
+ channelName = channelName.replace("_"+t.getName().split("__")[1],"");
}
- }
- TMLChannel channel = getChannelByShortName(channelName);
- if (channel!=null){
-
- for (TMLCPrimitivePort port:channel.ports){
+ }
+ channel = getChannelByShortName(channelName);
+ if (channel!=null){
+ for (TMLCPrimitivePort port:channel.ports){
if (port.checkAuth){
- port.checkWeakAuthStatus = 3;
+ port.checkStrongAuthStatus = 2;
port.secName= signalName;
}
}
}
- }
- }
}
+ }
}
- for (String s: satisfiedWeakAuthenticity){
- String signalName = s.split("__decrypt")[0];
- signalName = signalName.split("__")[1];
- List<String> channels=secChannelMap.get(signalName);
- if (channels!=null){
- for (String channelName: channels){
-// if (channelName!=null){
- if (channelName.contains("retData_") || channelName.contains("data_")){
- channelName=channelName.replaceAll("retData_","").replaceAll("data_","");
- //channelName=channelName.split("__retData_")[1];
- String header= channelName.split("__retData_")[0];
- for (TMLTask t: getTasks()){
+ }
+
+ if (result.isWeakProved() && result.isWeakSatisfied())
+ {
+ String signalName = s.split("_chData")[0];
+ signalName = signalName.split("__")[1];
+ TMLChannel channel = getChannelByShortName(signalName);
+ if (channel!=null){
+ for (TMLCPrimitivePort port:channel.ports){
+ if (port.checkAuth){
+ port.checkWeakAuthStatus = 2;
+ port.mappingName= mappingName;
+ }
+ }
+ }
+ signalName = s.split("_reqData")[0];
+ for (TMLTask t: getTasks()){
+ if (signalName.contains(t.getName())){
+ signalName = signalName.replace(t.getName()+"__","");
+ }
+ }
+ TMLRequest req = getRequestByName(signalName);
+ if (req !=null){
+ for (TMLCPrimitivePort port: req.ports){
+ if (port.checkAuth){
+ port.checkWeakAuthStatus = 2;
+ port.mappingName= mappingName;
+ }
+ }
+ }
+ signalName = s.split("__eventData")[0];
+ for (TMLTask t: getTasks()){
+ if (signalName.contains(t.getName())){
+ signalName = signalName.replace(t.getName()+"__","");
+ }
+ }
+ TMLEvent ev = getEventByName(signalName);
+ if (ev !=null){
+ if (ev.port.checkAuth){
+ ev.port.checkWeakAuthStatus=2;
+ ev.port2.mappingName= mappingName;
+ }
+ if (ev.port2.checkAuth){
+ ev.port2.checkWeakAuthStatus=2;
+ ev.port2.mappingName= mappingName;
+ }
+ }
+ signalName = s.toString().split("__decrypt")[0];
+ /*for (TMLTask t: getTasks()){
+ if (signalName.contains(t.getName())){
+ signalName = signalName.replace(t.getName()+"__","");
+ }
+ }*/
+ signalName = signalName.split("__")[1];
+ List<String> channels=secChannelMap.get(signalName);
+ if (channels!=null){
+ for (String channelName:channels){
+ channel = getChannelByShortName(channelName);
+ if (channel!=null){
+ for (TMLCPrimitivePort port:channel.ports){
+ if (port.checkAuth){
+ port.checkWeakAuthStatus = 2;
+ port.secName= signalName;
+ }
+ }
+ }
+ }
+ }
+
+ //In case of HSM
+ signalName = s.split("__decrypt")[0];
+ signalName = signalName.split("__")[1];
+ channels=secChannelMap.get(signalName);
+ if (channels!=null){
+ for (String channelName: channels){
+ if (channelName.contains("retData_") || channelName.contains("data_")){
+ channelName=channelName.replaceAll("retData_","").replaceAll("data_","");
+ String header= channelName.split("__retData_")[0];
+ for (TMLTask t: getTasks()){
if (channelName.contains(t.getName().split("__")[1])){
- channelName = channelName.replace("_"+t.getName().split("__")[1],"");
+ channelName = channelName.replace("_"+t.getName().split("__")[1],"");
}
- }
- TMLChannel channel = getChannelByShortName(channelName);
- if (channel!=null){
- for (TMLCPrimitivePort port:channel.ports){
+ }
+ channel = getChannelByShortName(channelName);
+ if (channel!=null){
+ for (TMLCPrimitivePort port:channel.ports){
if (port.checkAuth){
port.checkWeakAuthStatus = 2;
port.secName= signalName;
}
}
}
- }
- }
}
+ }
+ }
+ }
+
+ if (result.isProved() && !result.isSatisfied())
+ {
+ System.out.println(s.toString());
+ String signalName = s.toString().split("_chData")[0];
+ /*for (TMLTask t: getTasks()){
+ System.out.println(t.getName());
+ if (signalName.contains(t.getName().split("__")[1])){
+ signalName = signalName.split(t.getName().split("__")[1]+"__")[0];
+ }
+ }*/
+ signalName = signalName.split("__")[1];
+ TMLChannel channel = getChannelByShortName(signalName);
+ if (channel!=null){
+ System.out.println("adding auth results to channel " + channel.getName());
+ for (TMLCPrimitivePort port:channel.ports){
+ if (port.checkAuth){
+
+ port.checkStrongAuthStatus = 3;
+ port.mappingName= mappingName;
+ }
+ }
+ }
+ signalName = s.toString().split("_reqData")[0];
+ for (TMLTask t: getTasks()){
+ if (signalName.contains(t.getName())){
+ signalName = signalName.replace(t.getName()+"__","");
+ }
+ }
+ TMLRequest req = getRequestByName(signalName);
+ if (req !=null){
+ for (TMLCPrimitivePort port: req.ports){
+ if (port.checkAuth){
+ port.checkStrongAuthStatus = 3;
+ port.mappingName= mappingName;
+ }
+ }
+ }
+ signalName = s.toString().split("_eventData")[0];
+ for (TMLTask t: getTasks()){
+ if (signalName.contains(t.getName())){
+ signalName = signalName.replace(t.getName()+"__","");
+ }
+ }
+ TMLEvent ev = getEventByName(signalName);
+ if (ev !=null){
+ if (ev.port.checkAuth){
+ ev.port.checkStrongAuthStatus=3;
+ ev.port2.mappingName= mappingName;
+ }
+ if (ev.port2.checkAuth){
+ ev.port2.checkStrongAuthStatus=3;
+ ev.port2.mappingName= mappingName;
+ }
+ }
+
+ signalName = s.split("__decrypt")[0];
+ List<String> channels=secChannelMap.get(signalName);
+ if (channels!=null){
+ for (String channelName:channels){
+ channel = getChannelByShortName(channelName);
+ if (channel!=null){
+ for (TMLCPrimitivePort port:channel.ports){
+ if (port.checkAuth){
+ port.checkStrongAuthStatus = 3;
+ port.secName= signalName;
+ }
+ }
+ }
+ }
}
- for (String s: satisfiedAuthenticity){
- String signalName = s.split("__decrypt")[0];
- signalName = signalName.split("__")[1];
- List<String> channels=secChannelMap.get(signalName);
- if (channels!=null){
- for (String channelName: channels){
-// if (channelName!=null){
- if (channelName.contains("retData_") || channelName.contains("data_")){
- channelName=channelName.replaceAll("retData_","").replaceAll("data_","");
- //channelName=channelName.split("__retData_")[1];
- String header= channelName.split("__retData_")[0];
- for (TMLTask t: getTasks()){
+
+ //In case of HSM
+ signalName = s.split("__decrypt")[0];
+ signalName = signalName.split("__")[1];
+ channels=secChannelMap.get(signalName);
+ if (channels!=null){
+ for (String channelName: channels){
+ if (channelName.contains("retData_") || channelName.contains("data_")){
+ channelName=channelName.replaceAll("retData_","").replaceAll("data_","");
+ String header= channelName.split("__retData_")[0];
+ for (TMLTask t: getTasks()){
if (channelName.contains(t.getName().split("__")[1])){
- channelName = channelName.replace("_"+t.getName().split("__")[1],"");
+ channelName = channelName.replace("_"+t.getName().split("__")[1],"");
}
- }
- TMLChannel channel = getChannelByShortName(channelName);
- if (channel!=null){
- for (TMLCPrimitivePort port:channel.ports){
+ }
+ channel = getChannelByShortName(channelName);
+ if (channel!=null){
+ for (TMLCPrimitivePort port:channel.ports){
if (port.checkAuth){
- port.checkStrongAuthStatus = 2;
+ port.checkWeakAuthStatus = 3;
port.secName= signalName;
}
}
}
- }
- }
- }
- }
+ }
+ }
+ }
+ }
+ }
}
+
public void clearBacktracing(){
for (TMLChannel channel: getChannels()){
for (TMLCPrimitivePort port:channel.ports){
diff --git a/src/tmltranslator/toavatar/TML2Avatar.java b/src/tmltranslator/toavatar/TML2Avatar.java
index 95431f3bc8..846e24026a 100644
--- a/src/tmltranslator/toavatar/TML2Avatar.java
+++ b/src/tmltranslator/toavatar/TML2Avatar.java
@@ -59,6 +59,8 @@ import ui.TGComponent;
import myutil.*;
import avatartranslator.*;
+import proverifspec.ProVerifQueryResult;
+
public class TML2Avatar {
private TMLMapping tmlmap;
private TMLModeling tmlmodel;
@@ -1079,11 +1081,10 @@ public class TML2Avatar {
sig=signalOutMap.get(ch.getName());
}
if (ch.checkConf){
- LinkedList<AvatarAttribute> attrs = new LinkedList<AvatarAttribute>();
if (!attrsToCheck.contains(getName(ch.getName())+"_chData")){
- attrs.add(new AvatarAttribute(getName(ch.getName())+"_chData", AvatarType.INTEGER, block, null));
+ AvatarAttribute attr = new AvatarAttribute(getName(ch.getName())+"_chData", AvatarType.INTEGER, block, null);
attrsToCheck.add(getName(ch.getName())+"_chData");
- avspec.addPragma(new AvatarPragmaSecret("#Confidentiality "+block.getName() + "."+ch.getName()+"_chData", ch.getReferenceObject(), attrs));
+ avspec.addPragma(new AvatarPragmaSecret("#Confidentiality "+block.getName() + "."+ch.getName()+"_chData", ch.getReferenceObject(), attr));
}
}
if (ch.checkAuth){
@@ -1594,11 +1595,9 @@ public class TML2Avatar {
for (SecurityPattern secPattern: secPatterns){
AvatarAttribute sec = new AvatarAttribute(secPattern.name, AvatarType.INTEGER, block, null);
AvatarAttribute enc = new AvatarAttribute(secPattern.name+"_encrypted", AvatarType.INTEGER, block, null);
- LinkedList<AvatarAttribute> attrs = new LinkedList<AvatarAttribute>();
block.addAttribute(sec);
block.addAttribute(enc);
- attrs.add(sec);
- avspec.addPragma(new AvatarPragmaSecret("#Confidentiality "+block.getName() + "."+ secPattern.name, null, attrs));
+ avspec.addPragma(new AvatarPragmaSecret("#Confidentiality "+block.getName() + "."+ secPattern.name, null, sec));
}
}
@@ -1955,65 +1954,45 @@ public class TML2Avatar {
return avspec;
}
- // public void backtracePatterns(List<Stri
-
- public void backtraceReachability(List<String> reachableStates, List<String> nonReachableStates){
- // System.out.println(stateObjectMap);
- for (String s: reachableStates){
- if (stateObjectMap.containsKey(s.replace("enteringState__",""))){
- Object obj = stateObjectMap.get(s.replace("enteringState__",""));
- if (obj instanceof TMLADWriteChannel){
- TMLADWriteChannel wc =(TMLADWriteChannel) obj;
- wc.reachabilityInformation=1;
- }
- if (obj instanceof TMLADReadChannel){
- TMLADReadChannel wc =(TMLADReadChannel) obj;
- wc.reachabilityInformation=1;
- }
-
- if (obj instanceof TMLADSendEvent){
- TMLADSendEvent wc =(TMLADSendEvent) obj;
- wc.reachabilityInformation=1;
- }
-
- if (obj instanceof TMLADSendRequest){
- TMLADSendRequest wc =(TMLADSendRequest) obj;
- wc.reachabilityInformation=1;
- }
- if (obj instanceof TMLADWaitEvent){
- TMLADWaitEvent wc =(TMLADWaitEvent) obj;
- wc.reachabilityInformation=1;
- }
- }
- }
- for (String s:nonReachableStates){
- if (stateObjectMap.containsKey(s.replace("enteringState__",""))){
- Object obj = stateObjectMap.get(s.replace("enteringState__",""));
- if (obj instanceof TMLADWriteChannel){
- TMLADWriteChannel wc =(TMLADWriteChannel) obj;
- wc.reachabilityInformation=2;
- }
- if (obj instanceof TMLADReadChannel){
- TMLADReadChannel wc =(TMLADReadChannel) obj;
- wc.reachabilityInformation=2;
- }
-
- if (obj instanceof TMLADSendEvent){
- TMLADSendEvent wc =(TMLADSendEvent) obj;
- wc.reachabilityInformation=2;
- }
-
- if (obj instanceof TMLADSendRequest){
- TMLADSendRequest wc =(TMLADSendRequest) obj;
- wc.reachabilityInformation=2;
- }
- if (obj instanceof TMLADWaitEvent){
- TMLADWaitEvent wc =(TMLADWaitEvent) obj;
- wc.reachabilityInformation=2;
- }
- }
- }
+ public void backtraceReachability(HashMap<AvatarPragmaReachability, ProVerifQueryResult> reachabilityResults) {
+ for (AvatarPragmaReachability pragma: reachabilityResults.keySet())
+ {
+ ProVerifQueryResult result = reachabilityResults.get(pragma);
+ if (!result.isProved())
+ continue;
+
+ int r = result.isSatisfied() ? 1 : 2;
+
+ String s = pragma.getBlock().getName() + "__" + pragma.getState().getName();
+
+ if (stateObjectMap.containsKey(s)) {
+ Object obj = stateObjectMap.get(s);
+ if (obj instanceof TMLADWriteChannel){
+ TMLADWriteChannel wc =(TMLADWriteChannel) obj;
+ wc.reachabilityInformation=r;
+ }
+ if (obj instanceof TMLADReadChannel){
+ TMLADReadChannel wc =(TMLADReadChannel) obj;
+ wc.reachabilityInformation=r;
+ }
+
+ if (obj instanceof TMLADSendEvent){
+ TMLADSendEvent wc =(TMLADSendEvent) obj;
+ wc.reachabilityInformation=r;
+ }
+
+ if (obj instanceof TMLADSendRequest){
+ TMLADSendRequest wc =(TMLADSendRequest) obj;
+ wc.reachabilityInformation=r;
+ }
+ if (obj instanceof TMLADWaitEvent){
+ TMLADWaitEvent wc =(TMLADWaitEvent) obj;
+ wc.reachabilityInformation=r;
+ }
+ }
+ }
}
+
public void distributeKeys(){
List<TMLTask> tasks = tmlmap.getTMLModeling().getTasks();
for (TMLTask t:accessKeys.keySet()){
diff --git a/src/ui/AvatarDesignPanel.java b/src/ui/AvatarDesignPanel.java
index 0c64a975ff..faf8ef4d91 100644
--- a/src/ui/AvatarDesignPanel.java
+++ b/src/ui/AvatarDesignPanel.java
@@ -55,6 +55,9 @@ import ui.avatardd.*;
import ui.avatarsmd.*;
import avatartranslator.AvatarAttribute;
+import avatartranslator.AvatarPragmaSecret;
+import avatartranslator.AvatarPragmaReachability;
+import avatartranslator.AvatarPragmaAuthenticity;
import proverifspec.*;
@@ -364,8 +367,21 @@ public class AvatarDesignPanel extends TURTLEPanel {
resetModelBacktracingProVerif();
// Confidential attributes
- LinkedList<AvatarAttribute> secretAttributes = pvoa.getSecretTerms ();
- LinkedList<AvatarAttribute> nonSecretAttributes = pvoa.getNonSecretTerms ();
+ HashMap<AvatarPragmaSecret, ProVerifQueryResult> confResults = pvoa.getConfidentialityResults();
+ LinkedList<AvatarAttribute> secretAttributes = new LinkedList<AvatarAttribute> ();
+ LinkedList<AvatarAttribute> nonSecretAttributes = new LinkedList<AvatarAttribute> ();
+ for (AvatarPragmaSecret pragma: confResults.keySet())
+ {
+ ProVerifQueryResult result = confResults.get(pragma);
+ if (result.isProved())
+ {
+ if (result.isSatisfied())
+ secretAttributes.add(pragma.getArg());
+ else
+ nonSecretAttributes.add(pragma.getArg());
+ }
+ }
+
for (AvatarBDBlock bdBlock: abdp.getFullBlockList ())
for (TAttribute tattr: bdBlock.getAttributeList ()) {
if (tattr.getType () == TAttribute.OTHER) {
@@ -403,69 +419,34 @@ public class AvatarDesignPanel extends TURTLEPanel {
}
}
- String block, state;
- int index;
- int i;
- Iterator<TGComponent> iterator;
- TGComponent tgc;
// Reachable states
- for(String s: pvoa.getReachableEvents()) {
- index = s.indexOf("__");
- if (index != -1) {
- block = s.substring(index+2, s.length());
- index = block.indexOf("__");
- if (index != -1) {
- state = block.substring(index+2, block.length());
- block = block.substring(0, index);
- TraceManager.addDev("Block=" + block + " state=" + state);
- for(i=0; i<panels.size(); i++) {
- tdp = (TDiagramPanel)(panels.get(i));
- if ((tdp instanceof AvatarSMDPanel) && (tdp.getName().compareTo(block) == 0)){
- iterator = ((TDiagramPanel)(panels.get(i))).getComponentList().listIterator();
- while(iterator.hasNext()) {
- tgc = iterator.next();
- if (tgc instanceof AvatarSMDState) {
- ((AvatarSMDState)tgc).setSecurityInfo(AvatarSMDState.REACHABLE, state);
- }
+ HashMap<AvatarPragmaReachability, ProVerifQueryResult> reachResults = pvoa.getReachabilityResults();
+ for (AvatarPragmaReachability pragma: reachResults.keySet())
+ {
+ ProVerifQueryResult result = reachResults.get(pragma);
+ if (result.isProved())
+ {
+ for(int i=0; i<panels.size(); i++) {
+ tdp = (TDiagramPanel)(panels.get(i));
+ if ((tdp instanceof AvatarSMDPanel) && (tdp.getName().compareTo(pragma.getBlock().getName()) == 0)) {
+ Iterator<TGComponent> iterator = ((TDiagramPanel)(panels.get(i))).getComponentList().listIterator();
+ while(iterator.hasNext()) {
+ TGComponent tgc = iterator.next();
+ if (tgc instanceof AvatarSMDState) {
+ ((AvatarSMDState)tgc).setSecurityInfo(
+ result.isSatisfied() ? AvatarSMDState.REACHABLE : AvatarSMDState.NOT_REACHABLE,
+ pragma.getState().getName());
}
-
}
- }
- }
- }
- }
- for(String s: pvoa.getNonReachableEvents()) {
- index = s.indexOf("__");
- if (index != -1) {
- block = s.substring(index+2, s.length());
- index = block.indexOf("__");
- if (index != -1) {
- state = block.substring(index+2, block.length());
- block = block.substring(0, index);
- TraceManager.addDev("Block=" + block + " state=" + state);
- for(i=0; i<panels.size(); i++) {
- tdp = (TDiagramPanel)(panels.get(i));
- if ((tdp instanceof AvatarSMDPanel) && (tdp.getName().compareTo(block) == 0)){
- iterator = ((TDiagramPanel)(panels.get(i))).getComponentList().listIterator();
- while(iterator.hasNext()) {
- tgc = (TGComponent)(iterator.next());
- if (tgc instanceof AvatarSMDState) {
- ((AvatarSMDState)tgc).setSecurityInfo(AvatarSMDState.NOT_REACHABLE, state);
- }
- }
- }
+ break;
}
}
}
}
- LinkedList<String> notProved = pvoa.getNotProved ();
- LinkedList<String> satisfied = pvoa.getSatisfiedAuthenticity ();
- LinkedList<String> satisfiedWeak = pvoa.getSatisfiedWeakAuthenticity ();
- LinkedList<String> nonSatisfied = pvoa.getNonSatisfiedAuthenticity ();
-
+ HashMap<AvatarPragmaAuthenticity, ProVerifQueryAuthResult> authResults = pvoa.getAuthenticityResults();
for (Object ob: abdp.getComponentList())
if (ob instanceof AvatarBDPragma) {
AvatarBDPragma pragma = (AvatarBDPragma) ob;
@@ -495,29 +476,53 @@ public class AvatarDesignPanel extends TURTLEPanel {
LinkedList<TAttribute> types = abdp.getAttributesOfDataType (tattrA.getTypeOther ());
int toBeFound = types.size ();
- int weakLeft = types.size();
boolean ko = false;
+ boolean weakKo = false;
boolean isNotProved = false;
+ boolean weakIsNotProved = false;
for (TAttribute type: types) {
- String evA = argA[0] + "__" + argA[2] + "__"+ type.getId () + "__" + argA[1];
- String evB = argB[0] + "__" + argB[2] + "__"+ type.getId () + "__" + argB[1];
- String ev = evB + " ==> " + evA;
- if (satisfiedWeak.contains (ev)) {
- weakLeft--;
- }
- if (nonSatisfied.contains (ev)) {
- ko = true;
- } else if (notProved.contains (ev)) {
- toBeFound --;
- isNotProved = true;
- } else if (satisfied.contains (ev)) {
+ for (AvatarPragmaAuthenticity pragmaAuth: authResults.keySet())
+ {
+ if (!pragmaAuth.getAttrA().getAttribute().getBlock().getName().equals(argA[0].replaceAll("\\.", "__"))
+ || !pragmaAuth.getAttrB().getAttribute().getBlock().getName().equals(argB[0].replaceAll("\\.", "__"))
+ || !pragmaAuth.getAttrA().getAttribute().getName().equals(argA[2] + "__" + type.getId())
+ || !pragmaAuth.getAttrB().getAttribute().getName().equals(argB[2] + "__" + type.getId())
+ || !pragmaAuth.getAttrA().getState().getName().equals(argA[1].replaceAll("\\.", "__"))
+ || !pragmaAuth.getAttrB().getState().getName().equals(argB[1].replaceAll("\\.", "__")))
+ continue;
+
+ ProVerifQueryAuthResult result = authResults.get(pragmaAuth);
toBeFound --;
+
+ if (result.isProved())
+ {
+ if (!result.isSatisfied())
+ {
+ ko = true;
+ }
+ }
+ else
+ {
+ isNotProved = true;
+ }
+
+ if (result.isWeakProved())
+ {
+ if (!result.isWeakSatisfied())
+ {
+ weakKo = true;
+ }
+ }
+ else
+ {
+ weakIsNotProved = true;
+ }
+
+ break;
}
}
- if (weakLeft==0){
- pragma.authWeakMap.put(prop, 1);
- }
+
if (ko)
pragma.authStrongMap.put(prop, 2);
else if (toBeFound == 0) {
@@ -526,18 +531,63 @@ public class AvatarDesignPanel extends TURTLEPanel {
else
pragma.authStrongMap.put(prop, 1);
}
+
+ if (weakKo)
+ pragma.authWeakMap.put(prop, 2);
+ else if (toBeFound == 0) {
+ if (weakIsNotProved)
+ pragma.authWeakMap.put(prop, 3);
+ else
+ pragma.authWeakMap.put(prop, 1);
+ }
+
} else {
- String evA = argA[0] + "__" + argA[2] + "__" + argA[1];
- String evB = argB[0] + "__" + argB[2] + "__" + argB[1];
- String ev = evB + " ==> " + evA;
- if (satisfiedWeak.contains (ev))
- pragma.authWeakMap.put(prop, 1);
- if (nonSatisfied.contains (ev))
- pragma.authStrongMap.put(prop, 2);
- else if (notProved.contains (ev))
- pragma.authStrongMap.put(prop, 3);
- else if (satisfied.contains (ev))
- pragma.authStrongMap.put(prop, 1);
+ for (AvatarPragmaAuthenticity pragmaAuth: authResults.keySet())
+ {
+ if (!pragmaAuth.getAttrA().getAttribute().getBlock().getName().equals(argA[0].replaceAll("\\.", "__"))
+ || !pragmaAuth.getAttrB().getAttribute().getBlock().getName().equals(argB[0].replaceAll("\\.", "__"))
+ || !pragmaAuth.getAttrA().getAttribute().getName().equals(argA[2])
+ || !pragmaAuth.getAttrB().getAttribute().getName().equals(argB[2])
+ || !pragmaAuth.getAttrA().getState().getName().equals(argA[1].replaceAll("\\.", "__"))
+ || !pragmaAuth.getAttrB().getState().getName().equals(argB[1].replaceAll("\\.", "__")))
+ continue;
+
+ ProVerifQueryAuthResult result = authResults.get(pragmaAuth);
+
+ if (result.isProved())
+ {
+ if (result.isSatisfied())
+ {
+ pragma.authStrongMap.put(prop, 1);
+ }
+ else
+ {
+ pragma.authStrongMap.put(prop, 2);
+ }
+ }
+ else
+ {
+ pragma.authStrongMap.put(prop, 3);
+ }
+
+ if (result.isWeakProved())
+ {
+ if (result.isWeakSatisfied())
+ {
+ pragma.authWeakMap.put(prop, 1);
+ }
+ else
+ {
+ pragma.authWeakMap.put(prop, 2);
+ }
+ }
+ else
+ {
+ pragma.authWeakMap.put(prop, 3);
+ }
+
+ break;
+ }
}
}
}
diff --git a/src/ui/GTURTLEModeling.java b/src/ui/GTURTLEModeling.java
index 5ffe6b313d..be72945a25 100755
--- a/src/ui/GTURTLEModeling.java
+++ b/src/ui/GTURTLEModeling.java
@@ -77,6 +77,8 @@ import avatartranslator.AvatarActionOnSignal;
import avatartranslator.AvatarAttribute;
import avatartranslator.AvatarBlock;
import avatartranslator.AvatarPragma;
+import avatartranslator.AvatarPragmaSecret;
+import avatartranslator.AvatarPragmaAuthenticity;
import avatartranslator.AvatarRelation;
import avatartranslator.AvatarSpecification;
import avatartranslator.AvatarStartState;
@@ -90,6 +92,8 @@ import avatartranslator.toproverif.AVATAR2ProVerif;
import avatartranslator.totpn.AVATAR2TPN;
import avatartranslator.toturtle.AVATAR2TURTLE;
import avatartranslator.touppaal.AVATAR2UPPAAL;
+import proverifspec.ProVerifQueryResult;
+import proverifspec.ProVerifQueryAuthResult;
import ddtranslator.DDSyntaxException;
import ddtranslator.DDTranslator;
import launcher.LauncherException;
@@ -2095,23 +2099,24 @@ public class GTURTLEModeling {
ProVerifOutputAnalyzer pvoa = getProVerifOutputAnalyzer ();
pvoa.analyzeOutput(data, true);
- for (String nonConf: pvoa.getNonSecretStrings()){
- nonSecChans.add(nonConf);
- TraceManager.addDev(nonConf + " is not secret");
- //Find all tasks that receive this data
-
- TMLChannel chan = map.getTMLModeling().getChannelByShortName(nonConf.split("__")[1].replaceAll("_chData",""));
+ HashMap<AvatarPragmaSecret, ProVerifQueryResult> confResults = pvoa.getConfidentialityResults();
+ for (AvatarPragmaSecret pragma: confResults.keySet()) {
+ if (confResults.get(pragma).isProved() && !confResults.get(pragma).isSatisfied())
+ {
+ nonSecChans.add(pragma.getArg().getBlock().getName() + "__" + pragma.getArg().getName());
+ TraceManager.addDev(pragma.getArg().getBlock().getName() + "." + pragma.getArg().getName()+ " is not secret");
+ TMLChannel chan = map.getTMLModeling().getChannelByShortName(pragma.getArg().getName().replaceAll("_chData",""));
for (String block:chan.getTaskNames()){
- nonSecChans.add(block+"__"+nonConf.split("__")[1]);
+ nonSecChans.add(block+"__"+pragma.getArg().getName());
}
+ }
}
- for (String nonAuth: pvoa.getNonSatisfiedAuthenticity()) {
- String chanName= nonAuth.split("_chData")[0];
- nonAuthChans.add(chanName);
- String ch2=nonAuth.split(" ==> ")[1];
- ch2=ch2.split("_chData")[0];
- nonAuthChans.add(ch2);
- TraceManager.addDev(nonAuth);
+ HashMap<AvatarPragmaAuthenticity, ProVerifQueryAuthResult> authResults = pvoa.getAuthenticityResults();
+ for (AvatarPragmaAuthenticity pragma: authResults.keySet()) {
+ if (authResults.get(pragma).isProved() && !authResults.get(pragma).isSatisfied()) {
+ nonAuthChans.add(pragma.getAttrA().getAttribute().getBlock().getName() + "__" + pragma.getAttrA().getState().getName().replaceAll("_chData", ""));
+ nonAuthChans.add(pragma.getAttrB().getAttribute().getBlock().getName() + "__" + pragma.getAttrB().getState().getName().replaceAll("_chData", ""));
+ }
}
TraceManager.addDev("all results displayed");
diff --git a/src/ui/MainGUI.java b/src/ui/MainGUI.java
index 437664cda1..052fe533ee 100644
--- a/src/ui/MainGUI.java
+++ b/src/ui/MainGUI.java
@@ -3698,14 +3698,14 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener, Pe
}*/
gtm.getTMLMapping().getTMLModeling().clearBacktracing();
gtm.getTMLMapping().getTMLModeling().backtrace(pvoa, getTabName(tp));
- gtm.getTML2Avatar().backtraceReachability(pvoa.getReachableEvents(), pvoa.getNonReachableEvents());
- gtm.getTMLMapping().getTMLModeling().backtraceAuthenticity(pvoa.getSatisfiedAuthenticity(), pvoa.getSatisfiedWeakAuthenticity(), pvoa.getNonSatisfiedAuthenticity(), getTabName(tp));
+ gtm.getTML2Avatar().backtraceReachability(pvoa.getReachabilityResults());
+ gtm.getTMLMapping().getTMLModeling().backtraceAuthenticity(pvoa.getAuthenticityResults(), getTabName(tp));
}
else if (tp instanceof TMLComponentDesignPanel){
gtm.getTMLMapping().getTMLModeling().clearBacktracing();
gtm.getTMLMapping().getTMLModeling().backtrace(pvoa, "Default Mapping");
- gtm.getTML2Avatar().backtraceReachability(pvoa.getReachableEvents(), pvoa.getNonReachableEvents());
- gtm.getTMLMapping().getTMLModeling().backtraceAuthenticity(pvoa.getSatisfiedAuthenticity(), pvoa.getSatisfiedWeakAuthenticity(), pvoa.getNonSatisfiedAuthenticity(), "Default Mapping");
+ gtm.getTML2Avatar().backtraceReachability(pvoa.getReachabilityResults());
+ gtm.getTMLMapping().getTMLModeling().backtraceAuthenticity(pvoa.getAuthenticityResults(), "Default Mapping");
}
return;
}
diff --git a/src/ui/avatarsmd/AvatarSMDState.java b/src/ui/avatarsmd/AvatarSMDState.java
index 02a8f9bf9c..c81e3676a4 100644
--- a/src/ui/avatarsmd/AvatarSMDState.java
+++ b/src/ui/avatarsmd/AvatarSMDState.java
@@ -783,6 +783,7 @@ public class AvatarSMDState extends TGCScalableWithInternalComponent implements
//TraceManager.addDev("Setting state " + _name + " as info=" + _info);
securityInformation = _info;
}
+ // FIXME: does it really work? Name comes in the form "s1__s2__s3" and we compare only to "s1", "s2" and "s3"
for(int i=0; i<nbInternalTGComponent; i++) {
if (tgcomponent[i] instanceof AvatarSMDState) {
((AvatarSMDState)tgcomponent[i]).setSecurityInfo(_info, _name);
diff --git a/src/ui/window/JDialogProverifVerification.java b/src/ui/window/JDialogProverifVerification.java
index f16e53df6a..d0fd40f669 100644
--- a/src/ui/window/JDialogProverifVerification.java
+++ b/src/ui/window/JDialogProverifVerification.java
@@ -7,8 +7,7 @@
* 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.
- *
+ * 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
@@ -63,10 +62,12 @@ import ui.*;
import launcher.*;
-public class JDialogProverifVerification extends javax.swing.JDialog implements ActionListener, Runnable, MasterProcessInterface {
+public class JDialogProverifVerification extends javax.swing.JDialog implements ActionListener, ListSelectionListener, MouseListener, Runnable, MasterProcessInterface {
private static final Insets insets = new Insets(0, 0, 0, 0);
-
+ private static final Insets WEST_INSETS = new Insets(0, 0, 0, 0);
+ private static final Insets EAST_INSETS = new Insets(0, 0, 0, 0);
+
protected MainGUI mgui;
private String textC1 = "Generate ProVerif code in: ";
@@ -87,23 +88,32 @@ public class JDialogProverifVerification extends javax.swing.JDialog implements
int mode;
//components
- protected JTextArea jta;
+ protected JPanel jta;
protected JButton start;
protected JButton stop;
protected JButton close;
-
+
//protected JRadioButton exe, exeint;
//protected ButtonGroup exegroup;
protected JLabel gen, comp, exe;
protected JTextField code1, code2, unitcycle, compiler1, exe1, exe2, exe3, exe2int, loopLimit;
//protected JTabbedPane jp1;
protected JScrollPane jsp;
- protected JCheckBox outputOfProVerif, typedLanguage;
+ protected JCheckBox typedLanguage;
protected JRadioButton stateReachabilityAll, stateReachabilitySelected, stateReachabilityNone;
protected ButtonGroup stateReachabilityGroup;
protected JComboBox versionSimulator;
+ private JList<AvatarPragma> reachableEventsList;
+ private JList<AvatarPragma> nonReachableEventsList;
+ private JList<AvatarPragma> secretTermsList;
+ private JList<AvatarPragma> nonSecretTermsList;
+ private JList<AvatarPragma> satisfiedStrongAuthList;
+ private JList<AvatarPragma> satisfiedWeakAuthList;
+ private JList<AvatarPragma> nonSatisfiedAuthList;
+ private JList<AvatarPragma> nonProvedList;
+
private Thread t;
private boolean go = false;
private boolean hasError = false;
@@ -113,6 +123,19 @@ public class JDialogProverifVerification extends javax.swing.JDialog implements
protected RshClient rshc;
+ private class ProVerifVerificationException extends Exception {
+ private String message;
+
+ public ProVerifVerificationException(String message)
+ {
+ this.message = message;
+ }
+
+ public String getMessage()
+ {
+ return this.message;
+ }
+ };
/** Creates new form */
public JDialogProverifVerification(Frame f, MainGUI _mgui, String title, String _hostProVerif, String _pathCode, String _pathExecute) {
@@ -134,8 +157,7 @@ public class JDialogProverifVerification extends javax.swing.JDialog implements
myInitComponents();
pack();
- //getGlassPane().addMouseListener( new MouseAdapter() {});
- getGlassPane().setCursor(Cursor.getPredefinedCursor(Cursor.WAIT_CURSOR));
+ // getGlassPane().setCursor(Cursor.getPredefinedCursor(Cursor.WAIT_CURSOR));
}
protected void myInitComponents() {
@@ -144,10 +166,27 @@ public class JDialogProverifVerification extends javax.swing.JDialog implements
}
private void addComponent(Container container, Component component, int gridx, int gridy,
- int gridwidth, int gridheight, int anchor, int fill) {
- GridBagConstraints gbc = new GridBagConstraints(gridx, gridy, gridwidth, gridheight, 1.0, 1.0,
- anchor, fill, insets, 0, 0);
- container.add(component, gbc);
+ int gridwidth, int gridheight, int anchor, int fill) {
+ GridBagConstraints gbc = new GridBagConstraints(gridx, gridy, gridwidth, gridheight, 1.0, 1.0,
+ anchor, fill, insets, 0, 0);
+ container.add(component, gbc);
+ }
+
+ private GridBagConstraints createGbc(int x, int y) {
+ GridBagConstraints gbc = new GridBagConstraints();
+ gbc.gridx = x;
+ gbc.gridy = y;
+ gbc.gridwidth = 1;
+ gbc.gridheight = 1;
+
+ gbc.anchor = (x == 0) ? GridBagConstraints.WEST : GridBagConstraints.EAST;
+ gbc.fill = (x == 0) ? GridBagConstraints.BOTH
+ : GridBagConstraints.HORIZONTAL;
+
+ gbc.insets = (x == 0) ? WEST_INSETS : EAST_INSETS;
+ gbc.weightx = (x == 0) ? 0.1 : 1.0;
+ gbc.weighty = 1.0;
+ return gbc;
}
protected void initComponents() {
@@ -155,146 +194,65 @@ public class JDialogProverifVerification extends javax.swing.JDialog implements
Container c = getContentPane();
setFont(new Font("Helvetica", Font.PLAIN, 14));
c.setLayout(new BorderLayout());
- //setDefaultCloseOperation(JFrame.DISPOSE_ON_CLOSE);
-
- //jp1 = new JTabbedPane();
JPanel jp01 = new JPanel();
GridBagLayout gridbag01 = new GridBagLayout();
- //GridBagConstraints c01 = new GridBagConstraints();
jp01.setLayout(gridbag01);
jp01.setBorder(new javax.swing.border.TitledBorder("Verification options"));
-
+
gen = new JLabel(textC1);
- addComponent(jp01, gen, 0, 0, 1, 1, GridBagConstraints.CENTER, GridBagConstraints.BOTH);
- //genJava.addActionListener(this);
- //jp01.add(gen, c01);
+ addComponent(jp01, gen, 0, 0, 1, 1, GridBagConstraints.CENTER, GridBagConstraints.BOTH);
- //c01.gridwidth = GridBagConstraints.REMAINDER; //end row
code1 = new JTextField(pathCode, 100);
- addComponent(jp01, code1, 1, 0, 3, 1, GridBagConstraints.EAST, GridBagConstraints.BOTH);
- //jp01.add(code1, c01);
+ addComponent(jp01, code1, 1, 0, 3, 1, GridBagConstraints.EAST, GridBagConstraints.BOTH);
-
- //jp01.add(new JLabel(" "), c01);
- //c01.gridwidth = GridBagConstraints.REMAINDER; //end row
+ exe = new JLabel(textC2);
+ addComponent(jp01, exe, 0, 1, 1, 1, GridBagConstraints.EAST, GridBagConstraints.BOTH);
- exe = new JLabel(textC2);
- //jp01.add(exe, c01);
- addComponent(jp01, exe, 0, 1, 1, 1, GridBagConstraints.EAST, GridBagConstraints.BOTH);
+ exe2 = new JTextField(pathExecute, 100);
+ addComponent(jp01, exe2, 1, 1, 3, 1, GridBagConstraints.CENTER, GridBagConstraints.BOTH);
- exe2 = new JTextField(pathExecute + " -in pi ", 100);
- addComponent(jp01, exe2, 1, 1, 3, 1, GridBagConstraints.CENTER, GridBagConstraints.BOTH);
-
+ addComponent(jp01, new JLabel("Compute state reachability: "), 0, 3, 1, 1, GridBagConstraints.CENTER, GridBagConstraints.BOTH);
- //jp01.add(new JLabel(" "), c01);
- //c01.gridx = 0;
- // //c01.gridy = 3;
- //c01.gridwidth = 1;
- //c01.gridwidth = GridBagConstraints.REMAINDER; //end row
-
- //jp01.add(new JLabel("Compute state reachability: "), c01);
- addComponent(jp01, new JLabel("Compute state reachability: "), 0, 3, 1, 1, GridBagConstraints.CENTER, GridBagConstraints.BOTH);
- //c01.gridwidth = GridBagConstraints.REMAINDER; //end row
-
- //jp01.add(new JLabel("hi there: "), c01);
- //jp01.add(new JLabel("hi hi there: "), c01);
-
-
-
stateReachabilityGroup = new ButtonGroup ();
- //c01.gridy = 5;
- //c01.gridx = 1;
- /*JPanel bl1 = new JPanel();
-
- //c01.gridwidth = 1;*/
stateReachabilityAll = new JRadioButton("all");
- //bl1.add(stateReachabilityAll);
- addComponent(jp01, stateReachabilityAll, 1, 3, 1, 1, GridBagConstraints.CENTER, GridBagConstraints.BOTH);
-
+ addComponent(jp01, stateReachabilityAll, 1, 3, 1, 1, GridBagConstraints.CENTER, GridBagConstraints.BOTH);
+
- //c01.gridx = 2;
stateReachabilitySelected = new JRadioButton("selected");
- //bl1.add(stateReachabilitySelected);
- addComponent(jp01, stateReachabilitySelected, 2, 3, 1, 1, GridBagConstraints.CENTER, GridBagConstraints.BOTH);
+ addComponent(jp01, stateReachabilitySelected, 2, 3, 1, 1, GridBagConstraints.CENTER, GridBagConstraints.BOTH);
- //c01.gridx = 3;
- //c01.gridwidth = GridBagConstraints.REMAINDER; //end row
- stateReachabilityNone = new JRadioButton("none");
- addComponent(jp01, stateReachabilityNone, 3, 3, 1, 1, GridBagConstraints.CENTER, GridBagConstraints.BOTH);
- //bl1.add(stateReachabilityNone);
- //jp01.add(bl1, c01);
+ stateReachabilityNone = new JRadioButton("none");
+ addComponent(jp01, stateReachabilityNone, 3, 3, 1, 1, GridBagConstraints.CENTER, GridBagConstraints.BOTH);
stateReachabilityGroup.add (stateReachabilityAll);
stateReachabilityGroup.add (stateReachabilitySelected);
stateReachabilityGroup.add (stateReachabilityNone);
stateReachabilityAll.setSelected(true);
- //c01.gridx = GridBagConstraints.RELATIVE;
- //c01.gridy = GridBagConstraints.RELATIVE;
typedLanguage = new JCheckBox("Generate typed Pi calculus");
typedLanguage.setSelected(true);
- //jp01.add(typedLanguage, c01);
- addComponent(jp01, typedLanguage, 0, 4, 1, 1, GridBagConstraints.CENTER, GridBagConstraints.BOTH);
-
- /*c01.gridwidth= 1;
- //c01.gridwidth = GridBagConstraints.REMAINDER; //end row
- //JPanel pan1 = new JPanel();*/
- addComponent(jp01, new JLabel("Limit on loop iterations:"), 0, 5, 1, 1, GridBagConstraints.CENTER, GridBagConstraints.BOTH);
- //jp01.add(new JLabel("Limit on loop iterations:"), c01);
- //c01.gridwidth= GridBagConstraints.REMAINDER;
- loopLimit = new JTextField("1", 3);
- addComponent(jp01, loopLimit, 1, 5, 2, 1, GridBagConstraints.CENTER, GridBagConstraints.BOTH);
- //jp01.add(loopLimit, c01);
- //jp01.add(pan1, c01);*/
- /*optimizemode = new JCheckBox("Optimize code");
- optimizemode.setSelected(optimizeModeSelected);
- jp01.add(optimizemode, c01);
-
- jp01.add(new JLabel("Simulator used:"), c01);
-
- versionSimulator = new JComboBox(simus);
- versionSimulator.setSelectedIndex(selectedItem);
- versionSimulator.addActionListener(this);
- jp01.add(versionSimulator, c01);
- //System.out.println("selectedItem=" + selectedItem);
-
- //devmode = new JCheckBox("Development version of the simulator");
- //devmode.setSelected(true);
- //jp01.add(devmode, c01);
-
- //jp01.add(new JLabel(" "), c01);
-
- //jp1.add("Generate code", jp01);*/
-
-
-
+ addComponent(jp01, typedLanguage, 0, 4, 1, 1, GridBagConstraints.CENTER, GridBagConstraints.BOTH);
- outputOfProVerif = new JCheckBox("Show output of ProVerif");
- outputOfProVerif.setSelected(false);
- //jp01.add(outputOfProVerif, c01);*/
- addComponent(jp01, outputOfProVerif, 0, 6, 2, 1, GridBagConstraints.CENTER, GridBagConstraints.BOTH);
-
-
- //jp1.add("Execute", jp03);
+ addComponent(jp01, new JLabel("Limit on loop iterations:"), 0, 5, 1, 1, GridBagConstraints.CENTER, GridBagConstraints.BOTH);
+ loopLimit = new JTextField("1", 3);
+ addComponent(jp01, loopLimit, 1, 5, 2, 1, GridBagConstraints.CENTER, GridBagConstraints.BOTH);
c.add(jp01, BorderLayout.NORTH);
- jta = new ScrolledJTextArea();
- jta.setEditable(false);
- jta.setMargin(new Insets(10, 10, 10, 10));
- jta.setTabSize(3);
- jta.append("Select options and then, click on 'start' to launch ProVerif code generation / compilation\n");
+ jta = new JPanel();
+ jta.setLayout(new GridBagLayout());
+ jta.setBorder(new javax.swing.border.TitledBorder("Verification results"));
Font f = new Font("Courrier", Font.BOLD, 12);
jta.setFont(f);
- jsp = new JScrollPane(jta, JScrollPane.VERTICAL_SCROLLBAR_ALWAYS, JScrollPane.HORIZONTAL_SCROLLBAR_ALWAYS);
- jsp.setPreferredSize(new Dimension(300,300));
+ jsp = new JScrollPane(jta, JScrollPane.VERTICAL_SCROLLBAR_AS_NEEDED, JScrollPane.HORIZONTAL_SCROLLBAR_AS_NEEDED);
+ jsp.setPreferredSize(new Dimension(300,300));
c.add(jsp, BorderLayout.CENTER);
start = new JButton("Start", IconManager.imgic53);
@@ -315,7 +273,6 @@ public class JDialogProverifVerification extends javax.swing.JDialog implements
jp2.add(close);
c.add(jp2, BorderLayout.SOUTH);
-
}
public void actionPerformed(ActionEvent evt) {
@@ -364,192 +321,228 @@ public class JDialogProverifVerification extends javax.swing.JDialog implements
}
}
+ class ProVerifResultSection {
+ String title;
+ LinkedList<AvatarPragma> results;
+ JList<AvatarPragma> jlist;
+
+ ProVerifResultSection(String title, LinkedList<AvatarPragma> results, JList<AvatarPragma> jlist)
+ {
+ this.title = title;
+ this.results = results;
+ this.jlist = jlist;
+ }
+ };
+
public void run() {
- String cmd;
- String list, data;
+ String list;
int cycle = 0;
hasError = false;
TraceManager.addDev("Thread started");
+ this.jta.removeAll();
File testFile;
try {
- // Code generation
- //if (jp1.getSelectedIndex() == 0) {
- jta.append("Generating ProVerif code\n");
-
- testGo();
- pathCode = code1.getText().trim ();
-
- if (pathCode.isEmpty() || pathCode.endsWith(File.separator)) {
- pathCode += "pvspec";
- }
-
- testFile = new File(pathCode);
- if (testFile != null && testFile.isDirectory()){
- pathCode += File.separator;
- pathCode += "pvspec";
- testFile = new File(pathCode);
- }
-
- File dir = null;
- if (testFile != null)
- {
- dir = testFile.getParentFile();
- }
-
- if (testFile == null || dir == null || !dir.exists()) {
- jta.append("Error: invalid file: " + pathCode + "\n");
- mode = STOPPED;
- setButtons();
- return;
- }
-
-
- if (testFile.exists()){
- // FIXME Raise error
- System.out.println("FILE EXISTS!!!");
- }
-
- if (
- mgui.gtm.generateProVerifFromAVATAR(
- pathCode,
- stateReachabilityAll.isSelected () ? REACHABILITY_ALL : stateReachabilitySelected.isSelected () ? REACHABILITY_SELECTED : REACHABILITY_NONE,
- typedLanguage.isSelected(),
- loopLimit.getText())
- ) {
- jta.append("ProVerif code generation done\n");
- } else {
- setError();
- jta.append("Could not generate proverif code\n");
- }
-
- if (typedLanguage.isSelected()){
- exe2.setText(pathExecute + " -in pitype ");
- }
- else {
- exe2.setText(pathExecute + " -in pi ");
- }
-
- exe2.setText(exe2.getText()+pathCode);
- //if (mgui.gtm.getCheckingWarnings().size() > 0) {
- jta.append("" + mgui.gtm.getCheckingWarnings().size() + " warning(s)\n");
- //}
- //}
testGo();
- // Execute
- //if (jp1.getSelectedIndex() == 1) {
- try {
+ pathCode = code1.getText().trim ();
- cmd = exe2.getText();
+ if (pathCode.isEmpty() || pathCode.endsWith(File.separator)) {
+ pathCode += "pvspec";
+ }
- jta.append("Executing ProVerif code with command: \n" + cmd + "\n");
+ testFile = new File(pathCode);
- rshc = new RshClient(hostProVerif);
- // Assuma data are on the remote host
- // Command
+ if (testFile != null && testFile.isDirectory()){
+ pathCode += File.separator;
+ pathCode += "pvspec";
+ testFile = new File(pathCode);
+ }
- data = processCmd(cmd);
+ File dir = null;
+ if (testFile != null)
+ {
+ dir = testFile.getParentFile();
+ }
+ if (testFile == null || dir == null || !dir.exists()) {
+ mode = STOPPED;
+ setButtons();
+ throw new ProVerifVerificationException("Error: invalid file: " + pathCode);
+ }
- if (outputOfProVerif.isSelected()) {
- jta.append(data);
- }
- ProVerifOutputAnalyzer pvoa = mgui.gtm.getProVerifOutputAnalyzer ();
- pvoa.analyzeOutput(data, typedLanguage.isSelected());
+ if (testFile.exists()){
+ // FIXME Raise error if modified since last
+ System.out.println("FILE EXISTS!!!");
+ }
- if (pvoa.getErrors().size() != 0) {
- jta.append("\nErrors found in the generated code:\n----------------\n");
- for(String error: pvoa.getErrors()) {
- jta.append(error+"\n");
- }
+ if (
+ mgui.gtm.generateProVerifFromAVATAR(
+ pathCode,
+ stateReachabilityAll.isSelected () ? REACHABILITY_ALL : stateReachabilitySelected.isSelected () ? REACHABILITY_SELECTED : REACHABILITY_NONE,
+ typedLanguage.isSelected(),
+ loopLimit.getText())
+ ) {
+ } else {
+ this.hasError = true;
+ throw new ProVerifVerificationException("Could not generate proverif code");
+ }
- } else {
+ String cmd = exe2.getText().trim();
- jta.append("\nReachable states:\n----------------\n");
- for(String re: pvoa.getReachableEvents()) {
- jta.append(re+"\n");
- }
+ if (this.typedLanguage.isSelected())
+ {
+ cmd += " -in pitype ";
+ }
+ else
+ {
+ cmd += " -in pi ";
+ }
- jta.append("\nNon reachable states:\n----------------\n");
- for(String re: pvoa.getNonReachableEvents()) {
- jta.append(re+"\n");
- }
+ cmd += pathCode;
+ //jta.append("" + mgui.gtm.getCheckingWarnings().size() + " warning(s)\n");
+ testGo();
- jta.append("\nConfidential Data:\n----------------\n");
- for(AvatarAttribute attr: pvoa.getSecretTerms()) {
- jta.append(attr.getBlock ().getName () + "." + attr.getName () + "\n");
+ rshc = new RshClient(hostProVerif);
+ rshc.setCmd(cmd);
+ rshc.sendExecuteCommandRequest();
+ String data = rshc.getDataFromProcess();
+
+ ProVerifOutputAnalyzer pvoa = mgui.gtm.getProVerifOutputAnalyzer ();
+ pvoa.analyzeOutput(data, typedLanguage.isSelected());
+
+ if (pvoa.getErrors().size() != 0) {
+ int y = 0;
+
+ JLabel label = new JLabel("Errors found in the generated code:");
+ label.setAlignmentX(Component.LEFT_ALIGNMENT);
+ this.jta.add(label, this.createGbc(0, y++));
+ label = new JLabel("----------------");
+ label.setAlignmentX(Component.LEFT_ALIGNMENT);
+ this.jta.add(label, this.createGbc(0, y++));
+ this.jta.add(Box.createRigidArea(new Dimension(0,5)), this.createGbc(0, y++));
+ for(String error: pvoa.getErrors()) {
+ label = new JLabel(error);
+ label.setAlignmentX(Component.LEFT_ALIGNMENT);
+ this.jta.add(label,this.createGbc(0, y++));
+ }
+ } else {
+ LinkedList<AvatarPragma> reachableEvents = new LinkedList<AvatarPragma> ();
+ LinkedList<AvatarPragma> nonReachableEvents = new LinkedList<AvatarPragma> ();
+ LinkedList<AvatarPragma> secretTerms = new LinkedList<AvatarPragma> ();
+ LinkedList<AvatarPragma> nonSecretTerms = new LinkedList<AvatarPragma> ();
+ LinkedList<AvatarPragma> satisfiedStrongAuth = new LinkedList<AvatarPragma> ();
+ LinkedList<AvatarPragma> satisfiedWeakAuth = new LinkedList<AvatarPragma> ();
+ LinkedList<AvatarPragma> nonSatisfiedAuth = new LinkedList<AvatarPragma> ();
+ LinkedList<AvatarPragma> nonProved = new LinkedList<AvatarPragma> ();
+
+ HashMap<AvatarPragma, ProVerifQueryResult> results = pvoa.getResults();
+ for (AvatarPragma pragma: results.keySet())
+ {
+ if (pragma instanceof AvatarPragmaReachability)
+ {
+ ProVerifQueryResult r = results.get(pragma);
+ if (r.isProved())
+ {
+ if (r.isSatisfied())
+ reachableEvents.add(pragma);
+ else
+ nonReachableEvents.add(pragma);
}
+ else
+ nonProved.add(pragma);
+ }
- jta.append("\nNon Confidential Data:\n----------------\n");
- for(AvatarAttribute attr: pvoa.getNonSecretTerms()) {
- jta.append(attr.getBlock ().getName () + "." + attr.getName () + "\n");
+ else if (pragma instanceof AvatarPragmaSecret)
+ {
+ ProVerifQueryResult r = results.get(pragma);
+ if (r.isProved())
+ {
+ if (r.isSatisfied())
+ secretTerms.add(pragma);
+ else
+ nonSecretTerms.add(pragma);
}
+ else
+ nonProved.add(pragma);
+ }
- jta.append("\nSatisfied Strong Authenticity:\n----------------\n");
- for(String re: pvoa.getSatisfiedAuthenticity()) {
- jta.append(re+"\n");
+ else if (pragma instanceof AvatarPragmaAuthenticity)
+ {
+ ProVerifQueryAuthResult r = (ProVerifQueryAuthResult) results.get(pragma);
+ if (!r.isWeakProved())
+ {
+ nonProved.add(pragma);
}
-
- jta.append("\nSatisfied Weak Authenticity:\n----------------\n");
- for(String re: pvoa.getSatisfiedWeakAuthenticity()) {
- jta.append(re+"\n");
+ else
+ {
+ if (!r.isProved())
+ nonProved.add(pragma);
+ if (r.isProved() && r.isSatisfied())
+ satisfiedStrongAuth.add(pragma);
+ else if (r.isWeakSatisfied())
+ satisfiedWeakAuth.add(pragma);
+ else
+ nonSatisfiedAuth.add(pragma);
}
+ }
+ }
- jta.append("\nNon Satisfied Strong Authenticity:\n----------------\n");
- for(String re: pvoa.getNonSatisfiedAuthenticity()) {
- jta.append(re+"\n");
- }
+ LinkedList<ProVerifResultSection> sectionsList = new LinkedList<ProVerifResultSection> ();
+ sectionsList.add(new ProVerifResultSection("Reachable states:", reachableEvents, this.reachableEventsList));
+ sectionsList.add(new ProVerifResultSection("Non reachable states:", nonReachableEvents, this.nonReachableEventsList));
+ sectionsList.add(new ProVerifResultSection("Confidential Data:", secretTerms, this.secretTermsList));
+ sectionsList.add(new ProVerifResultSection("Non confidential Data:", nonSecretTerms, this.nonSecretTermsList));
+ sectionsList.add(new ProVerifResultSection("Satisfied Strong Authenticity:", satisfiedStrongAuth, this.satisfiedStrongAuthList));
+ sectionsList.add(new ProVerifResultSection("Satisfied Weak Authenticity:", satisfiedWeakAuth, this.satisfiedWeakAuthList));
+ sectionsList.add(new ProVerifResultSection("Non Satisfied Authenticity:", nonSatisfiedAuth, this.nonSatisfiedAuthList));
+ sectionsList.add(new ProVerifResultSection("Not Proved Queries:", nonProved, this.nonProvedList));
- jta.append("\nNon proved queries:\n----------------\n");
- for(String re: pvoa.getNotProved()) {
- jta.append(re+"\n");
- }
- }
+ int y = 0;
- mgui.modelBacktracingProVerif(pvoa);
-
- jta.append("\nAll done\n");
- } catch (LauncherException le) {
- jta.append("Error: " + le.getMessage() + "\n");
- mode = STOPPED;
- setButtons();
- return;
- } catch (Exception e) {
- mode = STOPPED;
- setButtons();
- return;
+ for (ProVerifResultSection section: sectionsList)
+ {
+ if (!section.results.isEmpty())
+ {
+ JLabel label = new JLabel(section.title);
+ label.setAlignmentX(Component.LEFT_ALIGNMENT);
+ this.jta.add(label, this.createGbc(0, y++));
+ this.jta.add(Box.createRigidArea(new Dimension(0,5)), this.createGbc(0, y++));
+ section.jlist = new JList<AvatarPragma> (section.results.toArray (new AvatarPragma[0]));
+ section.jlist.setSelectionMode(ListSelectionModel.SINGLE_SELECTION);
+ section.jlist.addMouseListener(this);
+ section.jlist.setAlignmentX(Component.LEFT_ALIGNMENT);
+ this.jta.add(section.jlist, this.createGbc(0, y++));
+ this.jta.add(Box.createRigidArea(new Dimension(0,10)), this.createGbc(0, y++));
+ }
}
- //}
+ }
+
+ mgui.modelBacktracingProVerif(pvoa);
- /*if ((hasError == false) && (jp1.getSelectedIndex() < 1)) {
- jp1.setSelectedIndex(jp1.getSelectedIndex() + 1);
- }*/
+ mode = NOT_STARTED;
+ } catch (LauncherException le) {
+ JLabel label = new JLabel("Error: " + le.getMessage());
+ label.setAlignmentX(Component.LEFT_ALIGNMENT);
+ this.jta.add(label, this.createGbc(0, 0));
+ mode = STOPPED;
} catch (InterruptedException ie) {
- jta.append("Interrupted\n");
+ mode = NOT_STARTED;
+ } catch (ProVerifVerificationException pve) {
+ JLabel label = new JLabel("Error: " + pve.getMessage());
+ label.setAlignmentX(Component.LEFT_ALIGNMENT);
+ this.jta.add(label, this.createGbc(0, 0));
+ mode = STOPPED;
+ } catch (Exception e) {
+ mode = STOPPED;
}
- jta.append("\n\nReady to process next command\n");
- checkMode();
setButtons();
- //System.out.println("Selected item=" + selectedItem);
- }
-
- protected String processCmd(String cmd) throws LauncherException {
- rshc.setCmd(cmd);
- String s = null;
- rshc.sendExecuteCommandRequest();
- s = rshc.getDataFromProcess();
- return s;
- }
-
- protected void checkMode() {
- mode = NOT_STARTED;
}
protected void setButtons() {
@@ -558,7 +551,6 @@ public class JDialogProverifVerification extends javax.swing.JDialog implements
start.setEnabled(true);
stop.setEnabled(false);
close.setEnabled(true);
- //setCursor(Cursor.getPredefinedCursor(Cursor.DEFAULT_CURSOR));
getGlassPane().setVisible(false);
break;
case STARTED:
@@ -566,7 +558,6 @@ public class JDialogProverifVerification extends javax.swing.JDialog implements
stop.setEnabled(true);
close.setEnabled(false);
getGlassPane().setVisible(true);
- //setCursor(Cursor.getPredefinedCursor(Cursor.WAIT_CURSOR));
break;
case STOPPED:
default:
@@ -578,15 +569,52 @@ public class JDialogProverifVerification extends javax.swing.JDialog implements
}
}
- public boolean hasToContinue() {
- return (go == true);
+ @Override
+ public void setError()
+ {
+ this.hasError = true;
+ }
+
+ @Override
+ public void appendOut(String s)
+ {
+ }
+
+ @Override
+ public boolean hasToContinue()
+ {
+ return this.go;
+ }
+
+ @Override
+ public void mouseClicked(MouseEvent e)
+ {
+ }
+
+ @Override
+ public void mouseEntered(MouseEvent e)
+ {
+ }
+
+ @Override
+ public void mouseExited(MouseEvent e)
+ {
+ }
+
+ @Override
+ public void mousePressed(MouseEvent e)
+ {
}
- public void appendOut(String s) {
- jta.append(s);
+ @Override
+ public void mouseReleased(MouseEvent e)
+ {
+ // TODO: add contextual menu
}
- public void setError() {
- hasError = true;
+ @Override
+ public void valueChanged(ListSelectionEvent e)
+ {
+ // TODO: unselect the other lists
}
}
--
GitLab