From c5444aad707aec233e8d766a6ebed967b1846853 Mon Sep 17 00:00:00 2001
From: Florian Lugou <florian.lugou@telecom-paristech.fr>
Date: Tue, 6 Oct 2015 16:48:45 +0000
Subject: [PATCH] fixes for guards translation with ProVerif
---
src/avatartranslator/AvatarGuard.java | 2 +-
src/avatartranslator/AvatarGuardElse.java | 2 ++
.../toproverif/AVATAR2ProVerif.java | 23 ++++++++-----------
src/proverifspec/ProVerifSyntaxer.java | 7 +++++-
src/ui/AvatarDesignPanel.java | 2 +-
5 files changed, 19 insertions(+), 17 deletions(-)
diff --git a/src/avatartranslator/AvatarGuard.java b/src/avatartranslator/AvatarGuard.java
index 46043f147d..1ac4db5233 100644
--- a/src/avatartranslator/AvatarGuard.java
+++ b/src/avatartranslator/AvatarGuard.java
@@ -82,7 +82,7 @@ public abstract class AvatarGuard {
indexRParen = AvatarGuard.getMatchingRParen (sane, 3);
first = AvatarGuard.createFromString (block, sane.substring (4, indexRParen));
- if (indexRParen == sane.length ()) {
+ if (indexRParen >= sane.length ()-1) {
if (first instanceof AvatarComposedGuard)
return new AvatarUnaryGuard ("not(", ")", (AvatarComposedGuard) first);
else
diff --git a/src/avatartranslator/AvatarGuardElse.java b/src/avatartranslator/AvatarGuardElse.java
index b2027a78dc..578f65fd32 100644
--- a/src/avatartranslator/AvatarGuardElse.java
+++ b/src/avatartranslator/AvatarGuardElse.java
@@ -58,9 +58,11 @@ public class AvatarGuardElse extends AvatarGuard {
public AvatarGuard getRealGuard (AvatarStateMachineElement precedent) {
AvatarGuard result = null;
+
for (AvatarStateMachineElement asme: precedent.getNexts ()) {
if (! (asme instanceof AvatarTransition))
continue;
+
AvatarGuard guard = ((AvatarTransition) asme).getGuard ();
if (guard == this)
continue;
diff --git a/src/avatartranslator/toproverif/AVATAR2ProVerif.java b/src/avatartranslator/toproverif/AVATAR2ProVerif.java
index a86f6da47d..6a246b014e 100755
--- a/src/avatartranslator/toproverif/AVATAR2ProVerif.java
+++ b/src/avatartranslator/toproverif/AVATAR2ProVerif.java
@@ -269,13 +269,8 @@ public class AVATAR2ProVerif implements AvatarTranslator {
if (pragma instanceof AvatarPragmaSecrecyAssumption)
for (AvatarAttribute attribute: pragma.getArgs ()) {
AvatarAttribute trueAttr = this.nameEquivalence.get (attribute);
- if (trueAttr == null) {
- CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "You can't test confidentiality of attribute " + attribute.getBlock ().getName () + "." + attribute.getName () + " unless you declare it as initial knowledge.");
- ce.setTDiagramPanel(((AvatarDesignPanel)(this.avspec.getReferenceObject())).getAvatarBDPanel());
- ce.setTGComponent((TGComponent)pragma.getReferenceObject ());
- warnings.add(ce);
- continue;
- }
+ if (trueAttr == null)
+ trueAttr = attribute;
if (secrecyChecked.contains (trueAttr))
continue;
@@ -293,13 +288,8 @@ public class AVATAR2ProVerif implements AvatarTranslator {
if (pragma instanceof AvatarPragmaSecret)
for (AvatarAttribute attribute: pragma.getArgs ()) {
AvatarAttribute trueAttr = this.nameEquivalence.get (attribute);
- if (trueAttr == null) {
- CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "You can't test confidentiality of attribute " + attribute.getBlock ().getName () + "." + attribute.getName () + " unless you declare it as initial knowledge.");
- ce.setTDiagramPanel(((AvatarDesignPanel)(this.avspec.getReferenceObject())).getAvatarBDPanel());
- ce.setTGComponent((TGComponent)pragma.getReferenceObject ());
- warnings.add(ce);
- continue;
- }
+ if (trueAttr == null)
+ trueAttr = attribute;
if (secrecyChecked.contains (trueAttr))
continue;
@@ -949,6 +939,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
if (nbOfNexts == 1) {
arg.lastInstr = _lastInstr;
+ arg.lastASME = _asme;
this.translateNext (_asme.getNext(0), arg);
} else if (_asme.hasElseChoiceType1()) {
@@ -958,10 +949,12 @@ public class AVATAR2ProVerif implements AvatarTranslator {
HashMap<AvatarAttribute, Integer> attributeCmp = new HashMap<AvatarAttribute, Integer> (arg.attributeCmp);
arg.lastInstr = _lastInstr.setNextInstr (ite);
+ arg.lastASME = _asme;
this.translateNext (_asme.getNext (0).getNext (0), arg);
arg.attributeCmp = attributeCmp;
arg.lastInstr = ite.getElse ();
+ arg.lastASME = _asme;
this.translateNext (_asme.getNext (1).getNext (0), arg);
} else {
@@ -988,6 +981,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
arg.attributeCmp = attributeCmp;
arg.lastInstr = _lastInstr;
+ arg.lastASME = _asme;
this.translateNext (_asme.getNext (nbOfNexts-1), arg);
}
}
@@ -1014,6 +1008,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
}
arg.lastInstr = _lastInstr;
+ arg.lastASME = _asme;
this.translateNext (_asme.getNext(0), _arg);
}
diff --git a/src/proverifspec/ProVerifSyntaxer.java b/src/proverifspec/ProVerifSyntaxer.java
index cc6ad31657..9ed8d2440c 100644
--- a/src/proverifspec/ProVerifSyntaxer.java
+++ b/src/proverifspec/ProVerifSyntaxer.java
@@ -124,8 +124,13 @@ public abstract class ProVerifSyntaxer {
protected void translateProcITE (ProVerifProcITE _node, int _alinea) {
this.fullSpec += "\n" + this.printAlinea (_alinea);
this.fullSpec += "if " + _node.cond + " then";
- if (_node.next != null)
+ if (_node.next != null) {
+ if (_node.elseInstr.next != null)
+ this.fullSpec += " (";
this.translate (_node.next, _alinea+1);
+ if (_node.elseInstr.next != null)
+ this.fullSpec += ")";
+ }
else
this.fullSpec += " 0";
if (_node.elseInstr.next != null) {
diff --git a/src/ui/AvatarDesignPanel.java b/src/ui/AvatarDesignPanel.java
index c8dd4c980f..abc9009b41 100644
--- a/src/ui/AvatarDesignPanel.java
+++ b/src/ui/AvatarDesignPanel.java
@@ -341,7 +341,7 @@ public class AvatarDesignPanel extends TURTLEPanel {
// Confidential attributes
for(AvatarAttribute attribute: pvoa.getSecretTerms()) {
- TAttribute a = abdp.getAttributeByBlockName(attribute.getBlock ().getName (), attribute.getName ());
+ TAttribute a = abdp.getAttributeByBlockName(attribute.getBlock ().getName (), attribute.getName ().split ("_")[0]);
if (a != null)
//TraceManager.addDev("Setting conf to ok");
a.setConfidentialityVerification(TAttribute.CONFIDENTIALITY_OK);
--
GitLab