diff --git a/Makefile b/Makefile
index 0e94f6e0d08105aff00dca8447d3a316e028c21c..62dc40d99316e367be624c7949444b96a7eaba8c 100755
--- a/Makefile
+++ b/Makefile
@@ -79,7 +79,7 @@ RELEASE_STD_FILES_WINDIWS_EXE = ttool_windows.bat
RELEASE_STD_FILES_XML = manual-HW.xml DrinkMachineV10.xml WebV01.xml Protocol_example1.xml BasicExchange.xml SmartCardProtocol.xml ProtocolPatterns.xml COCOME_V50.xml CoffeeMachine_Avatar.xml Network_Avatar.xml MicroWaveOven_SafetySecurity_fullMethodo.xml
RELEASE_STD_FILES_LIB = TClock1.lib TTimerv01.lib
-RELEASE_STD_FILES_BIN = $(TTOOL_CONFIG) $(LAUNCHER_BINARY) $(TTOOL_BINARY) $(TIFTRANSLATOR_BINARY) $(TMLTRANSLATOR_BINARY) $(REMOTESIMULATOR_BINARY) $(RUNDSE_BINARY)
+RELEASE_STD_FILES_BIN = $(LAUNCHER_BINARY) $(TTOOL_BINARY) $(TIFTRANSLATOR_BINARY) $(TMLTRANSLATOR_BINARY) $(REMOTESIMULATOR_BINARY) $(RUNDSE_BINARY)
RELEASE_STD_FILES_LICENSES = LICENSE LICENSE_CECILL_ENG LICENSE_CECILL_FR
diff --git a/src/avatartranslator/AvatarBlockTemplate.java b/src/avatartranslator/AvatarBlockTemplate.java
index dba5305e5ed59a2d0cba79fc1e744ff72e270d9e..2c638ddf3bc88b5f631225f4e2c34ef89f185b3b 100644
--- a/src/avatartranslator/AvatarBlockTemplate.java
+++ b/src/avatartranslator/AvatarBlockTemplate.java
@@ -70,9 +70,8 @@ public class AvatarBlockTemplate {
AvatarSignal reset = new AvatarSignal("reset", AvatarSignal.IN, _referenceBlock);
AvatarSignal expire = new AvatarSignal("expire", AvatarSignal.OUT, _referenceBlock);
- // FIXME: I replaced this val attribute by using the aa attribute created earlier. Is it ok ?
- // AvatarAttribute val = new AvatarAttribute("value", AvatarType.INTEGER, ab, aa.getReferenceObject());
- set.addParameter(aa);
+ AvatarAttribute val = new AvatarAttribute("value", AvatarType.INTEGER, ab, aa.getReferenceObject());
+ set.addParameter(val);
ab.addSignal(set);
ab.addSignal(reset);
ab.addSignal(expire);
diff --git a/src/avatartranslator/AvatarGuard.java b/src/avatartranslator/AvatarGuard.java
index e9e70c6a7ade7c48d186e3c61b3f41148abcf95c..46043f147d6e3fa7490e51b01ebc997e967a0c36 100644
--- a/src/avatartranslator/AvatarGuard.java
+++ b/src/avatartranslator/AvatarGuard.java
@@ -70,6 +70,10 @@ public abstract class AvatarGuard {
return new AvatarGuardEmpty ();
String sane = AvatarGuard.sanitizeString (_guard);
+
+ if (sane.toLowerCase ().equals ("else"))
+ return new AvatarGuardElse ();
+
int indexRParen = 0;
AvatarTuple tuple = null;
diff --git a/src/avatartranslator/AvatarSyntaxChecker.java b/src/avatartranslator/AvatarSyntaxChecker.java
index e6a4240d12821c54067fad49bdbbaf9c2af7480c..95aa53d246de3fa944efffb75fc44979cdc131f1 100644
--- a/src/avatartranslator/AvatarSyntaxChecker.java
+++ b/src/avatartranslator/AvatarSyntaxChecker.java
@@ -72,7 +72,6 @@ public class AvatarSyntaxChecker {
String act = tmp;
-
for(AvatarAttribute aa: _ab.getAttributes()) {
act = Conversion.putVariableValueInString(AvatarSpecification.ops, act, aa.getName(), aa.getDefaultInitialValue());
}
@@ -251,4 +250,4 @@ public class AvatarSyntaxChecker {
-}
\ No newline at end of file
+}
diff --git a/src/avatartranslator/AvatarTerm.java b/src/avatartranslator/AvatarTerm.java
index 5d70393820ec1efe75dda52188b6d4611971e658..eb2d55ba5b693a0f1ca52c4c7c25acdbe9c60e18 100644
--- a/src/avatartranslator/AvatarTerm.java
+++ b/src/avatartranslator/AvatarTerm.java
@@ -58,6 +58,9 @@ public abstract class AvatarTerm extends AvatarElement {
}
public static AvatarTerm createFromString (AvatarBlock block, String toParse) {
+ if (toParse == null || toParse.isEmpty ())
+ return null;
+
AvatarTerm result = AvatarTermFunction.createFromString (block, toParse);
if (result != null)
return result;
@@ -70,14 +73,14 @@ public abstract class AvatarTerm extends AvatarElement {
result = block.getAvatarAttributeWithName (toParse);
if (result != null)
return result;
- TraceManager.addDev ("AvatarAttribute '" + toParse + "' couldn't be parsed");
+ //TraceManager.addDev ("AvatarAttribute '" + toParse + "' couldn't be parsed");
result = block.getAvatarConstantWithName (toParse);
if (result != null)
return result;
- TraceManager.addDev ("AvatarConstant '" + toParse + "' couldn't be parsed");
+ //TraceManager.addDev ("AvatarConstant '" + toParse + "' couldn't be parsed");
- TraceManager.addDev ("AvatarTerm '" + toParse + "' couldn't be parsed");
+ //TraceManager.addDev ("AvatarTerm '" + toParse + "' couldn't be parsed");
return null;
}
diff --git a/src/avatartranslator/AvatarTermFunction.java b/src/avatartranslator/AvatarTermFunction.java
index 6c7bbbc5fa56016816e3ae6bb75dbde87edd0a3e..6f585ddccf726ac00598bc0b58aef5feba4c6f3d 100644
--- a/src/avatartranslator/AvatarTermFunction.java
+++ b/src/avatartranslator/AvatarTermFunction.java
@@ -79,7 +79,7 @@ public class AvatarTermFunction extends AvatarTerm implements AvatarAction {
// Method was found and the arguments provided are correct
return new AvatarTermFunction (meth, argsTuple, block);
- TraceManager.addDev ("Function call '" + toParse + "' couldn't be parsed");
+ //TraceManager.addDev ("Function call '" + toParse + "' couldn't be parsed");
return null;
}
diff --git a/src/avatartranslator/AvatarTuple.java b/src/avatartranslator/AvatarTuple.java
index 13b8f70567b76dcf0f2c1e9ceede55548e4de4f0..7b961f070a8c5ba922d7183dbaab679d05cd2051 100644
--- a/src/avatartranslator/AvatarTuple.java
+++ b/src/avatartranslator/AvatarTuple.java
@@ -85,8 +85,8 @@ public class AvatarTuple extends AvatarTerm implements AvatarLeftHand {
result = argsTuple;
}
- if (result == null)
- TraceManager.addDev ("Tuple '" + toParse + "' couldn't be parsed");
+ //if (result == null)
+ //TraceManager.addDev ("Tuple '" + toParse + "' couldn't be parsed");
return result;
}
diff --git a/src/avatartranslator/toproverif/AVATAR2ProVerif.java b/src/avatartranslator/toproverif/AVATAR2ProVerif.java
index ea1d7103486ca32072f2c6d6215c7d072dda94b1..d685fd1db69710b6928e903d1a4e4b7170d74bb9 100755
--- a/src/avatartranslator/toproverif/AVATAR2ProVerif.java
+++ b/src/avatartranslator/toproverif/AVATAR2ProVerif.java
@@ -47,6 +47,7 @@ package avatartranslator.toproverif;
import java.util.LinkedList;
import java.util.HashMap;
+import java.util.HashSet;
import java.util.Vector;
import ui.CheckingError;
@@ -95,8 +96,8 @@ public class AVATAR2ProVerif implements AvatarTranslator {
private AvatarSpecification avspec;
private HashMap<AvatarAttribute, AvatarAttribute> pubs;
+ private HashMap<AvatarAttribute, AvatarAttribute> nameEquivalence;
- // TODO: add warnings
private Vector warnings;
public AVATAR2ProVerif(AvatarSpecification _avspec) {
@@ -114,6 +115,10 @@ public class AVATAR2ProVerif implements AvatarTranslator {
return this.warnings;
}
+ public AvatarSpecification getAvatarSpecification () {
+ return this.avspec;
+ }
+
public ProVerifSpec generateProVerif(boolean _debug, boolean _optimize, boolean _stateReachability, boolean _typed) {
this.warnings = new Vector();
@@ -128,15 +133,26 @@ public class AVATAR2ProVerif implements AvatarTranslator {
// TODO: Why remove Else guards ?
// this.avspec.removeElseGuards();
- this.makeHeader(_stateReachability);
-
LinkedList<AvatarAttribute> allKnowledge = this.makeStartingProcess();
+ this.makeHeader(_stateReachability);
+
this.makeBlocks(allKnowledge);
return this.spec;
}
+ public ProVerifOutputAnalyzer getOutputAnalyzer () {
+ return new ProVerifOutputAnalyzer (this);
+ }
+
+ public String getTrueName (AvatarAttribute attr) {
+ AvatarAttribute trueAttr = this.nameEquivalence.get (attr);
+ if (trueAttr == null)
+ return null;
+ return AVATAR2ProVerif.translateTerm (trueAttr, null);
+ }
+
private static String makeAttrName (String... _params) {
String result = "";
boolean first = true;
@@ -216,14 +232,25 @@ public class AVATAR2ProVerif implements AvatarTranslator {
}
/* Secrecy Assumptions */
+ HashSet<AvatarAttribute> secrecyChecked = new HashSet<AvatarAttribute> ();
+
this.spec.addDeclaration (new ProVerifComment ("Secrecy Assumptions"));
TraceManager.addDev("Secrecy Assumptions");
for (AvatarPragma pragma: this.avspec.getPragmas ())
if (pragma instanceof AvatarPragmaSecrecyAssumption)
for (AvatarAttribute attribute: pragma.getArgs ()) {
- String name = this.makeAttrName (attribute.getBlock ().getName (), attribute.getName ());
+ AvatarAttribute trueAttr = this.nameEquivalence.get (attribute);
+ if (trueAttr == null)
+ // TODO Warning
+ continue;
+ if (secrecyChecked.contains (trueAttr))
+ continue;
+
+ String name = AVATAR2ProVerif.translateTerm (trueAttr, null);
TraceManager.addDev("| " + name);
this.spec.addDeclaration (new ProVerifSecrecyAssum (name));
+
+ secrecyChecked.add (trueAttr);
}
/* Queries */
@@ -232,9 +259,18 @@ public class AVATAR2ProVerif implements AvatarTranslator {
for (AvatarPragma pragma: this.avspec.getPragmas ())
if (pragma instanceof AvatarPragmaSecret)
for (AvatarAttribute attribute: pragma.getArgs ()) {
- String varName = this.makeAttrName(attribute.getBlock ().getName (), attribute.getName ());
+ AvatarAttribute trueAttr = this.nameEquivalence.get (attribute);
+ if (trueAttr == null)
+ // TODO Warning
+ continue;
+ if (secrecyChecked.contains (trueAttr))
+ continue;
+
+ String varName = AVATAR2ProVerif.translateTerm (trueAttr, null);
this.spec.addDeclaration (new ProVerifQueryAtt (varName, true));
TraceManager.addDev("| attacker (" + varName + ")");
+
+ secrecyChecked.add (trueAttr);
}
// Queries for states
@@ -258,8 +294,8 @@ public class AVATAR2ProVerif implements AvatarTranslator {
AvatarAttributeState attrA = ((AvatarPragmaAuthenticity) pragma).getAttrA ();
AvatarAttributeState attrB = ((AvatarPragmaAuthenticity) pragma).getAttrB ();
if (attrA != null && attrB != null) {
- String sA = this.makeAttrName (attrA.getAttribute ().getBlock ().getName (), attrA.getAttribute ().getName (), attrA.getState ().getName ());
- String sB = this.makeAttrName (attrB.getAttribute ().getBlock ().getName (), attrB.getAttribute ().getName (), attrB.getState ().getName ());
+ 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)");
spec.addDeclaration (new ProVerifEvDecl ("authenticity__" + sA, new String[] {"bitstring"}));
spec.addDeclaration (new ProVerifEvDecl ("authenticity__" + sB, new String[] {"bitstring"}));
@@ -287,14 +323,16 @@ public class AVATAR2ProVerif implements AvatarTranslator {
String blockName, paramName;
// Store all the names that are system knowledge
- // Enable to raise warning when an attribute is bothe system and session knowledge
+ // Enable to raise warning when an attribute is both system and session knowledge
LinkedList<AvatarAttribute> systemKnowledge = new LinkedList<AvatarAttribute> ();
+ this.nameEquivalence = new HashMap<AvatarAttribute, AvatarAttribute> ();
+
TraceManager.addDev("Finding system knowledge");
for (AvatarPragma pragma: this.avspec.getPragmas ())
// Check if pragma is system initial knowledge
if (pragma instanceof AvatarPragmaInitialKnowledge && ((AvatarPragmaInitialKnowledge) pragma).isSystem ()) {
- String first = null;
+ AvatarAttribute first = null;
boolean containsPublicKey = false;
for (AvatarAttribute arg: pragma.getArgs ()) {
// ignore if the attribute was already declared
@@ -304,13 +342,14 @@ public class AVATAR2ProVerif implements AvatarTranslator {
ProVerifProcInstr tmpInstr;
// Check if it is the first from the list
if (first == null) {
- first = this.makeAttrName (arg.getBlock ().getName (), arg.getName ());
+ first = arg;
+ this.nameEquivalence.put (first, first);
AvatarAttribute privateK = this.pubs.get (arg);
// Check if it is a public key
if (privateK != null) {
containsPublicKey = true;
- String privateKStr = this.makeAttrName (privateK.getBlock ().getName (), privateK.getName ());
+ String privateKStr = AVATAR2ProVerif.translateTerm (privateK, null);
// Check if the corresponding private key has already been declared
if (!systemKnowledge.contains (privateK)) {
lastInstr = lastInstr.setNextInstr (new ProVerifProcNew (privateKStr, "bitstring"));
@@ -318,15 +357,20 @@ public class AVATAR2ProVerif implements AvatarTranslator {
}
// Let the public key
- lastInstr = lastInstr.setNextInstr (new ProVerifProcLet (new ProVerifVar[] {new ProVerifVar (first, "bitstring")}, PK_PK + "(" + privateKStr + ")"));;
+ lastInstr = lastInstr.setNextInstr (new ProVerifProcLet (new ProVerifVar[] {new ProVerifVar (AVATAR2ProVerif.translateTerm (first, null), "bitstring")}, PK_PK + "(" + privateKStr + ")"));;
// Make the public key public
- tmpInstr = new ProVerifProcRaw ("out (" + CH_MAINCH + ", " + first + ");");
+ tmpInstr = new ProVerifProcRaw ("out (" + CH_MAINCH + ", " + AVATAR2ProVerif.translateTerm (first, null) + ");");
} else
- tmpInstr = new ProVerifProcNew (first, "bitstring");
+ tmpInstr = new ProVerifProcNew (AVATAR2ProVerif.translateTerm (first, null), "bitstring");
} else {
// If there are more arguments after a public key ignore what follows
if (containsPublicKey) {
- // TODO: raise warning
+ CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "You can't define equality between public keys and other attributes.");
+ //ce.setAvatarBlock(arg.block);
+ //FIXME: quel TDiagramPanel ?
+ //ce.setTDiagramPanel(((AvatarDesignPanel)(avspec.getReferenceObject())).getAvatarSMDPanel(arg.block.getName()));
+ //ce.setTGComponent((TGComponent)(_asme.getReferenceObject()));
+ //warnings.add(ce);
break;
}
// If there is a public key in the middle, ignore it
@@ -335,12 +379,12 @@ public class AVATAR2ProVerif implements AvatarTranslator {
continue;
}
- String str = this.makeAttrName (arg.getBlock ().getName (), arg.getName ());
- tmpInstr = new ProVerifProcLet (new ProVerifVar[] {new ProVerifVar (str, "bitstring")}, first);
- first = str;
+ String str = AVATAR2ProVerif.translateTerm (arg, null);
+ tmpInstr = new ProVerifProcLet (new ProVerifVar[] {new ProVerifVar (str, "bitstring")}, AVATAR2ProVerif.translateTerm (first, null));
+ this.nameEquivalence.put (arg, first);
}
- TraceManager.addDev("| Initial system knowledge pragma: " + first);
+ TraceManager.addDev("| Initial system knowledge pragma: " + AVATAR2ProVerif.translateTerm (first, null));
lastInstr = lastInstr.setNextInstr (tmpInstr);
systemKnowledge.add (arg);
}
@@ -367,7 +411,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
for (AvatarPragma pragma: this.avspec.getPragmas ())
// Check if pragma is session initial knowledge
if (pragma instanceof AvatarPragmaInitialKnowledge && !((AvatarPragmaInitialKnowledge) pragma).isSystem ()) {
- String first = null;
+ AvatarAttribute first = null;
boolean containsPublicKey = false;
for (AvatarAttribute arg: pragma.getArgs ()) {
// ignore if the attribute was already declared
@@ -383,13 +427,14 @@ public class AVATAR2ProVerif implements AvatarTranslator {
ProVerifProcInstr tmpInstr;
// Check if it is the first from the list
if (first == null) {
- first = this.makeAttrName (arg.getBlock ().getName (), arg.getName ());
+ first = arg;
+ this.nameEquivalence.put (first, first);
AvatarAttribute privateK = this.pubs.get (arg);
// Check if it is a public key
if (privateK != null) {
containsPublicKey = true;
- String privateKStr = this.makeAttrName (privateK.getBlock ().getName (), privateK.getName ());
+ String privateKStr = AVATAR2ProVerif.translateTerm (privateK, null);
// Check if the corresponding private key has already been declared
if (!systemKnowledge.contains (privateK) && !sessionKnowledge.contains (privateK)) {
lastInstr = lastInstr.setNextInstr (new ProVerifProcNew (privateKStr, "bitstring"));
@@ -397,11 +442,11 @@ public class AVATAR2ProVerif implements AvatarTranslator {
}
// Let the public key
- lastInstr = lastInstr.setNextInstr (new ProVerifProcLet (new ProVerifVar[] {new ProVerifVar (first, "bitstring")}, PK_PK + "(" + privateKStr + ")"));;
+ lastInstr = lastInstr.setNextInstr (new ProVerifProcLet (new ProVerifVar[] {new ProVerifVar (AVATAR2ProVerif.translateTerm (first, null), "bitstring")}, PK_PK + "(" + privateKStr + ")"));;
// Make the public key public
- tmpInstr = new ProVerifProcRaw ("out (" + CH_MAINCH + ", " + first + ");");
+ tmpInstr = new ProVerifProcRaw ("out (" + CH_MAINCH + ", " + AVATAR2ProVerif.translateTerm (first, null) + ");");
} else
- tmpInstr = new ProVerifProcNew (first, "bitstring");
+ tmpInstr = new ProVerifProcNew (AVATAR2ProVerif.translateTerm (first, null), "bitstring");
} else {
// If there are more arguments after a public key ignore what follows
if (containsPublicKey) {
@@ -414,12 +459,12 @@ public class AVATAR2ProVerif implements AvatarTranslator {
continue;
}
- String str = this.makeAttrName (arg.getBlock ().getName (), arg.getName ());
- tmpInstr = new ProVerifProcLet (new ProVerifVar[] {new ProVerifVar (str, "bitstring")}, first);
- first = str;
+ this.nameEquivalence.put (arg, first);
+ String str = AVATAR2ProVerif.translateTerm (arg, null);
+ tmpInstr = new ProVerifProcLet (new ProVerifVar[] {new ProVerifVar (str, "bitstring")}, AVATAR2ProVerif.translateTerm (first, null));
}
- TraceManager.addDev("| Initial session knowledge pragma: " + first);
+ TraceManager.addDev("| Initial session knowledge pragma: " + AVATAR2ProVerif.translateTerm (first, null));
lastInstr = lastInstr.setNextInstr (tmpInstr);
sessionKnowledge.add (arg);
}
@@ -457,7 +502,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
private ProVerifVar[] getProVerifVarFromAttr (LinkedList<AvatarAttribute> attrs) {
LinkedList<ProVerifVar> result = new LinkedList<ProVerifVar> ();
for(AvatarAttribute aa: attrs)
- result.add (new ProVerifVar (this.makeAttrName (aa.getBlock ().getName (), aa.getName ()), "bitstring"));
+ result.add (new ProVerifVar (AVATAR2ProVerif.translateTerm (aa, null), "bitstring"));
return result.toArray (new ProVerifVar[result.size ()]);
}
@@ -487,12 +532,12 @@ public class AVATAR2ProVerif implements AvatarTranslator {
continue;
ProVerifProcInstr tmpInstr;
- String str = this.makeAttrName (arg.getBlock ().getName (), arg.getName ());
+ String str = AVATAR2ProVerif.translateTerm (arg, null);
AvatarAttribute privateK = this.pubs.get (arg);
// Check if it is a public key
if (privateK != null) {
- String privateKStr = this.makeAttrName (privateK.getBlock ().getName (), privateK.getName ());
+ String privateKStr = AVATAR2ProVerif.translateTerm (privateK, null);
// Check if the corresponding private key has already been declared
if (!allKnowledge.contains (privateK)) {
lastInstr = lastInstr.setNextInstr (new ProVerifProcNew (privateKStr, "bitstring"));
@@ -520,14 +565,14 @@ public class AVATAR2ProVerif implements AvatarTranslator {
// Generate a new process for every simplified element of the block's state machine
HashMap<AvatarStateMachineElement, Integer> simplifiedElements = ab.getStateMachine ().getSimplifiedElements ();
- HashMap<AvatarAttribute, Integer> attributeCmp = new HashMap<AvatarAttribute, Integer> ();
- for (AvatarAttribute attr: ab.getAttributes ())
- attributeCmp.put (attr, 0);
-
for (AvatarStateMachineElement asme: simplifiedElements.keySet ())
if (asme != null) {
+ HashMap<AvatarAttribute, Integer> attributeCmp = new HashMap<AvatarAttribute, Integer> ();
+ for (AvatarAttribute attr: ab.getAttributes ())
+ attributeCmp.put (attr, 0);
+
// Create the ProVerif process and add it to the ProVerif specification
- ProVerifProcInstr p = new ProVerifProcess(makeAttrName(ab.getName(), simplifiedElements.get (asme).toString ()), new ProVerifVar[] {});
+ ProVerifProcInstr p = new ProVerifProcess(AVATAR2ProVerif.makeAttrName(ab.getName(), simplifiedElements.get (asme).toString ()), new ProVerifVar[] {});
this.spec.addDeclaration (p);
// Read and decrypt control data: variables sent to the process and the call__num variable
@@ -537,7 +582,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
for (AvatarAttribute attr: ab.getAttributes ()) {
Integer c = attributeCmp.get (attr) + 1;
attributeCmp.put (attr, c);
- attributes.add (new ProVerifVar (this.makeAttrName (attr.getBlock ().getName (), attr.getName (), c.toString ()), "bitstring"));
+ attributes.add (new ProVerifVar (AVATAR2ProVerif.translateTerm (attr, attributeCmp), "bitstring"));
}
p = p.setNextInstr (new ProVerifProcLet (attributes.toArray (new ProVerifVar[attributes.size()]), CHCTRL_DECRYPT + " (chControlData)"));
@@ -579,7 +624,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
// If next is the root of a process send the attributes on the control channel
String tmp = "out (" + CHCTRL_CH + ", " + CHCTRL_ENCRYPT + " ((call__" + arg.block.getName () + "__" + n;
for(AvatarAttribute aa: arg.block.getAttributes ())
- tmp += ", " + this.makeAttrName (aa.getBlock ().getName (), aa.getName (), arg.attributeCmp.get (aa).toString ());
+ tmp += ", " + AVATAR2ProVerif.translateTerm (aa, arg.attributeCmp);
arg.lastInstr.setNextInstr (new ProVerifProcRaw (tmp + ")))"));
}
@@ -797,12 +842,12 @@ public class AVATAR2ProVerif implements AvatarTranslator {
AvatarAttributeState attrA = ((AvatarPragmaAuthenticity) pragma).getAttrA ();
AvatarAttributeState attrB = ((AvatarPragmaAuthenticity) pragma).getAttrB ();
if (attrA.getState ().getName ().equals (_asme.getName ())) {
- String sp = "authenticity__" + this.makeAttrName (attrA.getAttribute ().getBlock ().getName (), attrA.getAttribute ().getName (), _asme.getName ()) + " (" + this.makeAttrName (attrA.getAttribute ().getBlock ().getName (), attrA.getAttribute ().getName (), arg.attributeCmp.get (attrA.getAttribute ()).toString ()) + ")";
+ 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 ()) + ")";
TraceManager.addDev("| | authenticity event " + sp + "added");
_lastInstr = _lastInstr.setNextInstr (new ProVerifProcRaw ("event " + sp, true));
}
if (attrB.getState ().getName ().equals (_asme.getName ())) {
- String sp = "authenticity__" + this.makeAttrName (attrB.getAttribute ().getBlock ().getName (), attrB.getAttribute ().getName (), _asme.getName ()) + " (" + this.makeAttrName (attrB.getAttribute ().getBlock ().getName (), attrB.getAttribute ().getName (), arg.attributeCmp.get (attrB.getAttribute ()).toString ()) + ")";
+ 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 ()) + ")";
TraceManager.addDev("| | authenticity event " + sp + "added");
_lastInstr = _lastInstr.setNextInstr (new ProVerifProcRaw ("event " + sp, true));
}
@@ -820,9 +865,12 @@ public class AVATAR2ProVerif implements AvatarTranslator {
TraceManager.addDev("| | calling next ITE");
ProVerifProcITE ite = new ProVerifProcITE (AVATAR2ProVerif.translateGuard (((AvatarTransition) _asme.getNext (0)).getGuard ().getRealGuard (arg.lastASME), arg.attributeCmp));
+ HashMap<AvatarAttribute, Integer> attributeCmp = new HashMap<AvatarAttribute, Integer> (arg.attributeCmp);
+
arg.lastInstr = _lastInstr.setNextInstr (ite);
this.translateNext (_asme.getNext (0).getNext (0), arg);
+ arg.attributeCmp = attributeCmp;
arg.lastInstr = ite.getElse ();
this.translateNext (_asme.getNext (1).getNext (0), arg);
@@ -830,14 +878,17 @@ public class AVATAR2ProVerif implements AvatarTranslator {
TraceManager.addDev("| | non deterministic next state");
for (int i=0; i<nbOfNexts-1; i++) {
String choice = "choice__" + _asme.getName () + "__" + i;
- _lastInstr = _lastInstr.setNextInstr (new ProVerifProcNew (choice, "bistring"));
+ _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")}));
+
+ 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);
+ arg.attributeCmp = new HashMap<AvatarAttribute, Integer> (arg.attributeCmp);
arg.lastASME = _asme;
arg.lastInstr = _lastInstr.setNextInstr (ite);
this.translateNext (_asme.getNext (i), arg);
@@ -845,13 +896,34 @@ public class AVATAR2ProVerif implements AvatarTranslator {
_lastInstr = ite.getElse ();
}
+ arg.attributeCmp = attributeCmp;
arg.lastInstr = _lastInstr;
this.translateNext (_asme.getNext (nbOfNexts-1), arg);
}
}
public void translateRandom (AvatarRandom _asme, Object _arg) {
- // TODO: new
+ TraceManager.addDev("| Random");
+ ProVerifTranslatorParameter arg = (ProVerifTranslatorParameter) _arg;
+ ProVerifProcInstr _lastInstr = arg.lastInstr;
+
+ AvatarTerm term = AvatarTerm.createFromString (arg.block, _asme.getVariable ());
+ LinkedList<AvatarAttribute> names = new LinkedList<AvatarAttribute> ();
+
+ if (term instanceof AvatarAttribute)
+ names.add ((AvatarAttribute) term);
+ else if (term instanceof AvatarTuple)
+ for (AvatarTerm t: ((AvatarTuple) term).getComponents ())
+ if (t instanceof AvatarAttribute)
+ names.add ((AvatarAttribute) t);
+
+ for (AvatarAttribute attr: names) {
+ Integer c = arg.attributeCmp.get (attr) + 1;
+ arg.attributeCmp.put (attr, c);
+ _lastInstr = _lastInstr.setNextInstr (new ProVerifProcNew (AVATAR2ProVerif.translateTerm (attr, arg.attributeCmp), "bitstring"));
+ }
+
+ arg.lastInstr = _lastInstr;
this.translateNext (_asme.getNext(0), _arg);
}
@@ -869,7 +941,10 @@ public class AVATAR2ProVerif implements AvatarTranslator {
private static String translateTerm (AvatarTerm term, HashMap<AvatarAttribute, Integer> attributeCmp) {
if (term instanceof AvatarAttribute) {
AvatarAttribute attr = (AvatarAttribute) term;
- return AVATAR2ProVerif.makeAttrName (attr.getBlock ().getName (), attr.getName (), attributeCmp.get (attr).toString ());
+ if (attributeCmp != null)
+ return AVATAR2ProVerif.makeAttrName (attr.getBlock ().getName (), attr.getName (), attributeCmp.get (attr).toString ());
+ else
+ return AVATAR2ProVerif.makeAttrName (attr.getBlock ().getName (), attr.getName ());
}
if (term instanceof AvatarConstant) {
diff --git a/src/myutil/Conversion.java b/src/myutil/Conversion.java
index 1c38393be8cb1c18f84b4aada4b4859f07eb3187..0a689fc5731f7cb6e23a45545c13084771941b44 100755
--- a/src/myutil/Conversion.java
+++ b/src/myutil/Conversion.java
@@ -46,6 +46,7 @@
package myutil;
import java.util.*;
+import java.util.regex.*;
public class Conversion {
@@ -534,7 +535,20 @@ public class Conversion {
}
public static String putVariableValueInString(String[] ops, String expr, String variableName, String value) {
- //TraceManager.addDev("Putting variable value = " + value + " of " + variableName + " in " + expr);
+ //TraceManager.addDev("Putting variable value = " + value + " of " + variableName + " in " + expr);
+
+ // Escaping variableName and value in case there are special characters
+ String in = Pattern.quote (variableName);
+ String out = Matcher.quoteReplacement (value);
+
+ // Creating the pattern that matches words equal to variableName
+ Pattern pattern = Pattern.compile ("(\\b" + in + "\\b)");
+ Matcher matcher = pattern.matcher (expr);
+
+ // Replacing all the matches by the replacement value
+ return matcher.replaceAll (out).trim ();
+
+ /*
String ret = " " + expr + " ";
String name = " " + variableName + " ";
String s0;
@@ -552,9 +566,18 @@ public class Conversion {
}
return ret.trim();
+ */
}
public static String removeAllActionOps(String[] ops, String input, String replacementValue) {
+ String ret = input;
+ for (String op: ops) {
+ String out = new String (new char[op.length ()]).replace("\0", replacementValue);
+ ret = ret.replace (op, out);
+ }
+ return ret;
+
+ /*
String output = input;
String tmp;
int cpt;
@@ -569,6 +592,7 @@ public class Conversion {
output = replaceAllString(output, ops[i], tmp);
}
return output;
+ */
}
/**
diff --git a/src/proverifspec/ProVerifOutputAnalyzer.java b/src/proverifspec/ProVerifOutputAnalyzer.java
index 9743fa93d93bbccf2e939964eb0580f6a70d6ecd..34e759ffb8ee58830da905c5209759fa47b10b79 100644
--- a/src/proverifspec/ProVerifOutputAnalyzer.java
+++ b/src/proverifspec/ProVerifOutputAnalyzer.java
@@ -50,6 +50,10 @@ import java.util.regex.*;
import myutil.*;
import java.io.*;
+import avatartranslator.toproverif.AVATAR2ProVerif;
+import avatartranslator.AvatarAttribute;
+import avatartranslator.AvatarBlock;
+
public class ProVerifOutputAnalyzer {
@@ -63,24 +67,28 @@ public class ProVerifOutputAnalyzer {
private LinkedList<String> nonSatisfiedAuthenticity;
private LinkedList<String> errors;
private LinkedList<String> notproved;
- String typedEvent = "not event(";
- String untypedEvent = "not ev:";
- String typedFalse = ") is false";
- String typedTrue = ") is true";
- String untypedFalse = " is false";
- String untypedTrue = " is true";
- String typedSecret = "not attacker(";
- String untypedSecret = "not attacker:";
- String typedStrongAuth = "inj-event(authenticity__";
- String untypedStrongAuth = "evinj:authenticity__";
- String typedWeakAuth = "(but event(authenticity__";
- String untypedWeakAuth = "(but ev:authenticity__";
- String typedAuthSplit = "==> inj-event(authenticity__";
- String typedWeakAuthSplit = "==> event(authenticity__";
- String untypedAuthSplit = "==> evinj:authenticity__";
- String untypedWeakAuthSplit = "==> ev:authenticity__";
-
- public ProVerifOutputAnalyzer() {
+ private final static String typedEvent = "not event(";
+ private final static String untypedEvent = "not ev:";
+ private final static String typedFalse = ") is false";
+ private final static String typedTrue = ") is true";
+ 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 AVATAR2ProVerif avatar2proverif;
+
+ public ProVerifOutputAnalyzer(AVATAR2ProVerif avatar2proverif) {
+ this.avatar2proverif = avatar2proverif;
+
reachableEvents = new LinkedList<String>();
nonReachableEvents = new LinkedList<String>();
secretTerms = new LinkedList<String>();
@@ -94,54 +102,54 @@ public class ProVerifOutputAnalyzer {
}
public void analyzeTypedOutput(String _s) {
- String str, previous="";
+ String str, previous="";
int index0, index1;
BufferedReader reader = new BufferedReader(new StringReader(_s));
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]);
- }
- }
- else if (str.contains(typedSecret)){
- if (str.contains(typedTrue)){
- //Add string between tags
- secretTerms.add(str.split(Pattern.quote(typedSecret))[1].split("\\[")[0]);
- }
- else if (str.contains(typedFalse)) {
- nonSecretTerms.add(str.split(Pattern.quote(typedSecret))[1].split("\\[")[0]);
- }
- }
- else if (str.contains(typedStrongAuth)){
- if (str.contains(typedTrue)){
- //Add string between tags
- satisfiedAuthenticity.add(str.split(typedStrongAuth)[1].split(typedAuthSplit)[0].split("\\(")[0] + " ==> " + str.split(typedAuthSplit)[1].split("\\(")[0]);
- }
- 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(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]);
- }
- }
- }
- if (str.contains("Error:")){
- errors.add(str + ": " + previous);
- }
- else if (str.contains("cannot be proved")){
- notproved.add(str);
- }
+ 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]);
+ }
+ }
+ else if (str.contains(typedSecret)){
+ if (str.contains(typedTrue)){
+ //Add string between tags
+ secretTerms.add(str.split(Pattern.quote(typedSecret))[1].split("\\[")[0]);
+ }
+ else if (str.contains(typedFalse)) {
+ nonSecretTerms.add(str.split(Pattern.quote(typedSecret))[1].split("\\[")[0]);
+ }
+ }
+ else if (str.contains(typedStrongAuth)){
+ if (str.contains(typedTrue)){
+ //Add string between tags
+ satisfiedAuthenticity.add(str.split(typedStrongAuth)[1].split(typedAuthSplit)[0].split("\\(")[0] + " ==> " + str.split(typedAuthSplit)[1].split("\\(")[0]);
+ }
+ 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(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]);
+ }
+ }
+ }
+ if (str.contains("Error:")){
+ errors.add(str + ": " + previous);
+ }
+ else if (str.contains("cannot be proved")){
+ notproved.add(str);
+ }
}
previous = str;
} catch(IOException e) {
@@ -152,61 +160,60 @@ public class ProVerifOutputAnalyzer {
public void analyzeOutput(String _s, boolean isTyped) {
String str, previous="";
int index0, index1;
- if (isTyped) {
- analyzeTypedOutput(_s);
- return;
- }
+ 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]);
- }
- else if (str.contains(untypedFalse)) {
- reachableEvents.add(str.split(Pattern.quote(untypedEvent))[1].split("\\(")[0]);
- }
- }
- else if (str.contains(untypedSecret)){
- if (str.contains(untypedTrue)){
- //Add string between tags
- secretTerms.add(str.split(Pattern.quote(untypedSecret))[1].split("\\[")[0]);
- }
- else if (str.contains(untypedFalse)) {
- nonSecretTerms.add(str.split(Pattern.quote(untypedSecret))[1].split("\\[")[0]);
- }
- }
- 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]);
- }
- else if (str.contains(untypedFalse)) {
- nonSatisfiedAuthenticity.add(str.split(Pattern.quote(untypedStrongAuth))[1].split("\\(")[0] + " ==> " + str.split(Pattern.quote(untypedAuthSplit))[1].split("\\(")[0]);
- }
- }
- 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]);
- }
- }
- }
- if (str.contains("Error:")){
- errors.add(str + ": " + previous);
- }
- else if (str.contains("cannot be proved")){
- notproved.add(str);
- }
+ 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]);
+ }
+ else if (str.contains(untypedFalse)) {
+ reachableEvents.add(str.split(Pattern.quote(untypedEvent))[1].split("\\(")[0]);
+ }
+ }
+ else if (str.contains(untypedSecret)){
+ if (str.contains(untypedTrue)){
+ //Add string between tags
+ secretTerms.add(str.split(Pattern.quote(untypedSecret))[1].split("\\[")[0]);
+ }
+ else if (str.contains(untypedFalse)) {
+ nonSecretTerms.add(str.split(Pattern.quote(untypedSecret))[1].split("\\[")[0]);
+ }
+ }
+ 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]);
+ }
+ else if (str.contains(untypedFalse)) {
+ nonSatisfiedAuthenticity.add(str.split(Pattern.quote(untypedStrongAuth))[1].split("\\(")[0] + " ==> " + str.split(Pattern.quote(untypedAuthSplit))[1].split("\\(")[0]);
+ }
+ }
+ 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]);
+ }
+ }
+ }
+ 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 LinkedList<String> getReachableEvents() {
@@ -217,12 +224,30 @@ public class ProVerifOutputAnalyzer {
return nonReachableEvents;
}
- public LinkedList<String> getSecretTerms() {
- return secretTerms;
+ public LinkedList<AvatarAttribute> getSecretTerms() {
+ // FIXME composed Types ?
+ 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;
}
- public LinkedList<String> getNonSecretTerms() {
- return nonSecretTerms;
+ // FIXME what about cannot be proved ?
+
+ public LinkedList<AvatarAttribute> getNonSecretTerms() {
+ // FIXME composed Types ?
+ 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);
+ }
+ return result;
}
public LinkedList<String> getSatisfiedAuthenticity() {
diff --git a/src/ui/AvatarDesignPanel.java b/src/ui/AvatarDesignPanel.java
index f4abd6e2f483b2afdfff2441f02f4c2005809414..c8dd4c980faa7e068c7ad8f2137a9c8db33ffc01 100644
--- a/src/ui/AvatarDesignPanel.java
+++ b/src/ui/AvatarDesignPanel.java
@@ -54,6 +54,8 @@ import ui.avatarbd.*;
import ui.avatardd.*;
import ui.avatarsmd.*;
+import avatartranslator.AvatarAttribute;
+
import proverifspec.*;
@@ -337,62 +339,27 @@ public class AvatarDesignPanel extends TURTLEPanel {
resetModelBacktracingProVerif();
- String block, attr, state;
- int index;
- TAttribute a;
- int i;
- ListIterator iterator;
- TGComponent tgc;
-
// Confidential attributes
- for(String s: pvoa.getSecretTerms()) {
- index = s.indexOf("__");
- if (index != -1) {
- block = s.substring(0, index);
- attr = s.substring(index+2, s.length());
- index = attr.indexOf("__");
- if (index != -1) {
- attr = attr.substring(0, index);
- }
- else {
- index = attr.indexOf("_");
- if (index != -1){
- attr = attr.substring(0, index);
- }
- }
- //TraceManager.addDev("Analyzing block=" + block + " attr=" + attr);
- a = abdp.getAttributeByBlockName(block, attr);
- if (a != null) {
- //TraceManager.addDev("Setting conf to ok");
- a.setConfidentialityVerification(TAttribute.CONFIDENTIALITY_OK);
- }
- }
+ for(AvatarAttribute attribute: pvoa.getSecretTerms()) {
+ TAttribute a = abdp.getAttributeByBlockName(attribute.getBlock ().getName (), attribute.getName ());
+ if (a != null)
+ //TraceManager.addDev("Setting conf to ok");
+ a.setConfidentialityVerification(TAttribute.CONFIDENTIALITY_OK);
}
- for(String s: pvoa.getNonSecretTerms()) {
- index = s.indexOf("__");
- if (index != -1) {
- block = s.substring(0, index);
- attr = s.substring(index+2, s.length());
- index = attr.indexOf("__");
- if (index != -1) {
- attr = attr.substring(0, index);
- }
- else {
- index = attr.indexOf("_");
- if (index != -1){
- attr = attr.substring(0, index);
- }
- }
- //TraceManager.addDev("Analyzing block=" + block + " attr=" + attr);
- a = abdp.getAttributeByBlockName(block, attr);
- if (a != null) {
- //TraceManager.addDev("Setting conf to ok");
- a.setConfidentialityVerification(TAttribute.CONFIDENTIALITY_KO);
- }
- }
+ for(AvatarAttribute attribute: pvoa.getNonSecretTerms()) {
+ TAttribute a = abdp.getAttributeByBlockName(attribute.getBlock ().getName (), attribute.getName ());
+ if (a != null)
+ //TraceManager.addDev("Setting conf to ok");
+ a.setConfidentialityVerification(TAttribute.CONFIDENTIALITY_KO);
}
+ String block, state;
+ int index;
+ int i;
+ ListIterator iterator;
+ TGComponent tgc;
+
// Reachable states
for(String s: pvoa.getReachableEvents()) {
index = s.indexOf("__");
@@ -439,7 +406,6 @@ public class AvatarDesignPanel extends TURTLEPanel {
((AvatarSMDState)tgc).setSecurityInfo(AvatarSMDState.NOT_REACHABLE, state);
}
}
-
}
}
}
diff --git a/src/ui/GTURTLEModeling.java b/src/ui/GTURTLEModeling.java
index f3f86b49a4919bfca736557fdc5570ccc6d11fe3..e8d6b3b4c5049452f0ceb6ab50000c3f2cc22aad 100755
--- a/src/ui/GTURTLEModeling.java
+++ b/src/ui/GTURTLEModeling.java
@@ -624,6 +624,10 @@ public class GTURTLEModeling {
return avatarspec;
}
+ public ProVerifOutputAnalyzer getProVerifOutputAnalyzer () {
+ return this.avatar2proverif.getOutputAnalyzer ();
+ }
+
public boolean generateProVerifFromAVATAR(String _path, boolean _stateReachability, boolean _advancedTranslation, boolean _typed) {
avatar2proverif = new AVATAR2ProVerif(avatarspec);
//tml2uppaal.setChoiceDeterministic(choices);
diff --git a/src/ui/window/JDialogProVerifGeneration.java b/src/ui/window/JDialogProVerifGeneration.java
index 475a8e572c5ccd579fbe25d5dda4050178b479ca..89f83a114a6df684e1ec3fddc76d218666c34ac2 100644
--- a/src/ui/window/JDialogProVerifGeneration.java
+++ b/src/ui/window/JDialogProVerifGeneration.java
@@ -196,11 +196,11 @@ public class JDialogProVerifGeneration extends javax.swing.JDialog implements Ac
versionSimulator.setSelectedIndex(selectedItem);
versionSimulator.addActionListener(this);
jp01.add(versionSimulator, c01);
- //System.out.println("selectedItem=" + selectedItem);
+ //System.out.println("selectedItem=" + selectedItem);
- //devmode = new JCheckBox("Development version of the simulator");
- //devmode.setSelected(true);
- //jp01.add(devmode, c01);*/
+ //devmode = new JCheckBox("Development version of the simulator");
+ //devmode.setSelected(true);
+ //jp01.add(devmode, c01);*/
jp01.add(new JLabel(" "), c01);
@@ -323,65 +323,57 @@ public class JDialogProVerifGeneration extends javax.swing.JDialog implements Ac
hasError = false;
TraceManager.addDev("Thread started");
- File testFile;
+ File testFile;
try {
// Code generation
if (jp1.getSelectedIndex() == 0) {
jta.append("Generating ProVerif code\n");
testGo();
- pathCode = code1.getText();
- testFile = new File(pathCode);
- if (pathCode.isEmpty() || pathCode.trim().isEmpty()){
- pathCode="pvspec";
- }
- if (testFile.isDirectory()){
- if (pathCode.charAt(pathCode.length()-1) != '/'){
- pathCode = pathCode + "/";
- }
- pathCode = pathCode+"pvspec";
- }
- else {
- if (testFile.exists()){
- //Raise error
- System.out.println("FILE EXISTS!!!");
- }
- }
+ pathCode = code1.getText().trim ();
+
+ if (pathCode.isEmpty()){
+ pathCode="pvspec";
+ }
+
+ testFile = new File(pathCode);
+
+ if (testFile.isDirectory()){
+ if (!pathCode.endsWith (File.separator)){
+ pathCode += File.separator;
+ }
+ pathCode += "pvspec";
+ testFile = new File(pathCode);
+ }
+
+ if (testFile.exists()){
+ // FIXME Raise error
+ System.out.println("FILE EXISTS!!!");
+ }
+
if (mgui.gtm.generateProVerifFromAVATAR(pathCode, stateReachability.isSelected(), translationOfBooleanFunction.isSelected(), typedLanguage.isSelected())) {
jta.append("ProVerif code generation done\n");
} else {
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");
- //}
+
+ 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 {
- //Check for space at end
- if (exe2.getText().charAt(exe2.getText().length()-1) != ' '){
- exe2.setText(exe2.getText() + " ");
- }
- //Check if input file provided
- String filename = "pvspec";
- String[] args = exe2.getText().split(" ");
- if (args.length > 3){
- testFile = new File(args[3]);
- if (testFile.isFile()){
- filename = "";
- }
- }
-
- cmd = exe2.getText() + filename;
+
+ cmd = exe2.getText();
jta.append("Executing ProVerif code with command: \n" + cmd + "\n");
@@ -395,8 +387,8 @@ public class JDialogProVerifGeneration extends javax.swing.JDialog implements Ac
if (outputOfProVerif.isSelected()) {
jta.append(data);
}
-
- ProVerifOutputAnalyzer pvoa = new ProVerifOutputAnalyzer();
+
+ ProVerifOutputAnalyzer pvoa = mgui.gtm.getProVerifOutputAnalyzer ();
pvoa.analyzeOutput(data, typedLanguage.isSelected());
if (pvoa.getErrors().size() != 0) {
@@ -418,13 +410,13 @@ public class JDialogProVerifGeneration extends javax.swing.JDialog implements Ac
}
jta.append("\nConfidential Data:\n----------------\n");
- for(String re: pvoa.getSecretTerms()) {
- jta.append(re+"\n");
+ for(AvatarAttribute attr: pvoa.getSecretTerms()) {
+ jta.append(attr.getBlock ().getName () + "." + attr.getName () + "\n");
}
jta.append("\nNon Confidential Data:\n----------------\n");
- for(String re: pvoa.getNonSecretTerms()) {
- jta.append(re+"\n");
+ for(AvatarAttribute attr: pvoa.getNonSecretTerms()) {
+ jta.append(attr.getBlock ().getName () + "." + attr.getName () + "\n");
}
jta.append("\nSatisfied Strong Authenticity:\n----------------\n");
@@ -432,7 +424,7 @@ public class JDialogProVerifGeneration extends javax.swing.JDialog implements Ac
jta.append(re+"\n");
}
- jta.append("\nSatisfied Weak Authenticity:\n----------------\n");
+ jta.append("\nSatisfied Weak Authenticity:\n----------------\n");
for(String re: pvoa.getSatisfiedWeakAuthenticity()) {
jta.append(re+"\n");
}
@@ -493,27 +485,27 @@ public class JDialogProVerifGeneration extends javax.swing.JDialog implements Ac
protected void setButtons() {
switch(mode) {
- case NOT_STARTED:
- start.setEnabled(true);
- stop.setEnabled(false);
- close.setEnabled(true);
- //setCursor(Cursor.getPredefinedCursor(Cursor.DEFAULT_CURSOR));
- getGlassPane().setVisible(false);
- break;
- case STARTED:
- start.setEnabled(false);
- stop.setEnabled(true);
- close.setEnabled(false);
- getGlassPane().setVisible(true);
- //setCursor(Cursor.getPredefinedCursor(Cursor.WAIT_CURSOR));
- break;
- case STOPPED:
- default:
- start.setEnabled(false);
- stop.setEnabled(false);
- close.setEnabled(true);
- getGlassPane().setVisible(false);
- break;
+ case NOT_STARTED:
+ start.setEnabled(true);
+ stop.setEnabled(false);
+ close.setEnabled(true);
+ //setCursor(Cursor.getPredefinedCursor(Cursor.DEFAULT_CURSOR));
+ getGlassPane().setVisible(false);
+ break;
+ case STARTED:
+ start.setEnabled(false);
+ stop.setEnabled(true);
+ close.setEnabled(false);
+ getGlassPane().setVisible(true);
+ //setCursor(Cursor.getPredefinedCursor(Cursor.WAIT_CURSOR));
+ break;
+ case STOPPED:
+ default:
+ start.setEnabled(false);
+ stop.setEnabled(false);
+ close.setEnabled(true);
+ getGlassPane().setVisible(false);
+ break;
}
}