diff --git a/src/proverifspec/ProVerifOutputAnalyzer.java b/src/proverifspec/ProVerifOutputAnalyzer.java
index 2fa47657d5aa20306bf72207f8a5dc4f128e1a4b..1d0025cde8a9f5bbcfad2c3f2ea69a8c6a5b53fb 100644
--- a/src/proverifspec/ProVerifOutputAnalyzer.java
+++ b/src/proverifspec/ProVerifOutputAnalyzer.java
@@ -263,7 +263,6 @@ public class ProVerifOutputAnalyzer {
public LinkedList<String> getSatisfiedAuthenticity() {
return satisfiedAuthenticity;
}
-
public LinkedList<String> getSatisfiedWeakAuthenticity() {
return satisfiedWeakAuthenticity;
}
diff --git a/src/tmltranslator/TMLChannel.java b/src/tmltranslator/TMLChannel.java
index fd0cb9548029448b7b1ca4f678f05e3de528c78c..917896b39122ad6696faad01ac5cb8a765b7160d 100755
--- a/src/tmltranslator/TMLChannel.java
+++ b/src/tmltranslator/TMLChannel.java
@@ -48,7 +48,7 @@ package tmltranslator;
import myutil.*;
import java.util.*;
-
+import ui.tmlcompd.TMLCPrimitivePort;
public class TMLChannel extends TMLCommunicationElement {
@@ -60,7 +60,9 @@ public class TMLChannel extends TMLCommunicationElement {
private int size;
private int type;
private int max;
-
+ public TMLCPrimitivePort port;
+ public TMLCPrimitivePort port2;
+ public ArrayList<TMLCPrimitivePort> ports;
// Used on for 1 -> 1 channel
protected TMLTask originTask, destinationTask;
protected TMLPort originPort, destinationPort; // Not used by the simulator
@@ -82,6 +84,7 @@ public class TMLChannel extends TMLCommunicationElement {
destinationTasks = new ArrayList<TMLTask>();
originPorts = new ArrayList<TMLPort>();
destinationPorts = new ArrayList<TMLPort>();
+ ports = new ArrayList<TMLCPrimitivePort>();
}
diff --git a/src/tmltranslator/TMLEvent.java b/src/tmltranslator/TMLEvent.java
index 3e344ab97197f13fbff159b9d97375e0fdb74851..85aa4d49baf8ecf781d1e5c1a56c13e156ef393e 100755
--- a/src/tmltranslator/TMLEvent.java
+++ b/src/tmltranslator/TMLEvent.java
@@ -46,7 +46,7 @@
package tmltranslator;
import java.util.*;
-
+import ui.tmlcompd.TMLCPrimitivePort;
public class TMLEvent extends TMLCommunicationElement {
protected Vector params; // List of various types of parameters
@@ -56,6 +56,8 @@ public class TMLEvent extends TMLCommunicationElement {
protected TMLTask origin, destination;
public static int confStatus;
public static boolean checkConf;
+ public TMLCPrimitivePort port;
+ public TMLCPrimitivePort port2;
/*public TMLEvent(String name, Object reference) {
super(name, reference);
params = new Vector();
diff --git a/src/tmltranslator/TMLModeling.java b/src/tmltranslator/TMLModeling.java
index 8fa0d7071a4b297a7bdac68cc2fb1a577206431c..8b25648f94bf6d7c7972be7fa7dde22748f33892 100755
--- a/src/tmltranslator/TMLModeling.java
+++ b/src/tmltranslator/TMLModeling.java
@@ -47,6 +47,9 @@ package tmltranslator;
import java.util.*;
import myutil.*;
+import ui.tmlcompd.*;
+import avatartranslator.*;
+import proverifspec.*;
//import compiler.expression.*;
@@ -596,7 +599,94 @@ public class TMLModeling {
}
return list;
}
-
+ public void backtrace(ProVerifOutputAnalyzer pvoa, String mappingName){
+ LinkedList<AvatarAttribute> secretAttributes = pvoa.getSecretTerms ();
+ LinkedList<AvatarAttribute> nonSecretAttributes = pvoa.getNonSecretTerms ();
+ for (AvatarAttribute attr: secretAttributes){
+ System.out.println("Attribute " + attr.getName());
+ TMLChannel channel = getChannelByName(attr.getName().replaceAll("__chData",""));
+ if (channel!=null){
+ System.out.println("write to chan " + channel.getName());
+ for (TMLCPrimitivePort port:channel.ports){
+ port.checkStatus = 2;
+ port.mappingName= mappingName;
+ }
+ }
+ TMLRequest req = getRequestByName(attr.getName().replaceAll("__reqData",""));
+ if (req !=null){
+ System.out.println("write to req " + req.getName());
+ for (TMLCPrimitivePort port: req.ports){
+ port.checkStatus=2;
+ port.mappingName= mappingName;
+ }
+ }
+ TMLEvent ev = getEventByName(attr.getName().replaceAll("__eventData",""));
+ if (ev !=null){
+ System.out.println("write to event " + ev.getName());
+ ev.port.checkStatus=2;
+ ev.port.mappingName= mappingName;
+ }
+ }
+ for (AvatarAttribute attr: nonSecretAttributes){
+ TMLChannel channel = getChannelByName(attr.getName().replaceAll("__chData",""));
+ if (channel!=null){
+ System.out.println("write to ch " + channel.getName());
+ for (TMLCPrimitivePort port:channel.ports){
+ port.checkStatus = 3;
+ port.mappingName= mappingName;
+ }
+ }
+ TMLRequest req = getRequestByName(attr.getName().replaceAll("__reqData",""));
+ if (req !=null){
+ System.out.println("write to req " + req.getName());
+ for (TMLCPrimitivePort port: req.ports){
+ port.checkStatus=3;
+ port.mappingName= mappingName;
+ }
+ }
+ TMLEvent ev = getEventByName(attr.getName().replaceAll("__eventData",""));
+ if (ev !=null){
+ System.out.println("write to event " + ev.getName());
+ ev.port.checkStatus=3;
+ ev.port2.checkStatus=3;
+ ev.port.mappingName= mappingName;
+ }
+ }
+ System.out.println("backtracing finished");
+ return;
+ }
+ public void clearBacktracing(){
+ for (TMLChannel channel: getChannels()){
+ System.out.println("Channel " + channel.getName());
+ for (TMLCPrimitivePort port:channel.ports){
+ if (port.checkStatus>1){
+ port.checkStatus=1;
+ port.mappingName="???";
+ }
+ }
+ }
+ for (TMLRequest req: getRequests()){
+ for (TMLCPrimitivePort port:req.ports){
+ if (port.checkStatus>1){
+ port.checkStatus=1;
+ port.mappingName="???";
+ }
+ }
+ }
+ for (TMLEvent evt: getEvents()){
+ if (evt.port!=null && evt.port2!=null){
+ if (evt.port.checkStatus>1){
+ evt.port.checkStatus=1;
+ evt.port.mappingName="???";
+ }
+ if (evt.port2.checkStatus>1){
+ evt.port2.checkStatus=1;
+ evt.port2.mappingName="???";
+ }
+ }
+ }
+ return;
+ }
public ArrayList<TMLEvent> getEvents(TMLTask t) {
TMLEvent evt;
ArrayList<TMLEvent> list = new ArrayList<TMLEvent>();
diff --git a/src/tmltranslator/TMLRequest.java b/src/tmltranslator/TMLRequest.java
index a951d8cfac1e3eb6b989b39e55cdf6409fa3c98e..d36524359dbb68b7e7eebc4c85e99a8c5f8db0c0 100755
--- a/src/tmltranslator/TMLRequest.java
+++ b/src/tmltranslator/TMLRequest.java
@@ -46,7 +46,7 @@
package tmltranslator;
import java.util.*;
-
+import ui.tmlcompd.TMLCPrimitivePort;
public class TMLRequest extends TMLCommunicationElement {
protected Vector params; // List of various types of parameters
@@ -55,11 +55,13 @@ public class TMLRequest extends TMLCommunicationElement {
protected ArrayList<String> paramNames;
public static int confStatus;
public static boolean checkConf;
+ public ArrayList<TMLCPrimitivePort> ports;
public TMLRequest(String name, Object reference) {
super(name, reference);
params = new Vector();
originTasks = new ArrayList<TMLTask>();
paramNames = new ArrayList<String>();
+ ports = new ArrayList<TMLCPrimitivePort>();
}
public int getNbOfParams() {
diff --git a/src/tmltranslator/toavatar/TML2Avatar.java b/src/tmltranslator/toavatar/TML2Avatar.java
index 2d8561319059766506759e1d599b1726f0c4dbd4..3b5c76b76e95bf4eae423d4e6d28867a8c391bef 100644
--- a/src/tmltranslator/toavatar/TML2Avatar.java
+++ b/src/tmltranslator/toavatar/TML2Avatar.java
@@ -77,12 +77,13 @@ public class TML2Avatar {
private final static Integer channelPrivate = 1;
private final static Integer channelUnreachable = 2;
AvatarSpecification avspec;
-
+ ArrayList<String> attrsToCheck;
List<String> allStates;
public TML2Avatar(TMLMapping tmlmap) {
this.tmlmap = tmlmap;
this.tmlmodel = tmlmap.getTMLModeling();
allStates = new ArrayList<String>();
+ attrsToCheck=new ArrayList<String>();
}
public void checkConnections(){
@@ -355,6 +356,22 @@ public class TML2Avatar {
else {
sig=signalMap.get(block.getName()+"__OUT__"+req.getName());
}
+ if (req.checkConf){
+ LinkedList<AvatarAttribute> attrs = new LinkedList<AvatarAttribute>();
+ if (!attrsToCheck.contains(req.getName()+"__reqData")){
+ attrs.add(new AvatarAttribute(req.getName()+"__reqData", AvatarType.INTEGER, block, null));
+ attrsToCheck.add(req.getName()+"__reqData");
+ }
+ for (int i=0; i<sr.getNbOfParams(); i++){
+ if (block.getAvatarAttributeWithName(sr.getParam(i))!=null && !attrsToCheck.contains(sr.getParam(i))){
+ attrs.add(block.getAvatarAttributeWithName(sr.getParam(i)));
+ attrsToCheck.add(sr.getParam(i));
+ }
+ }
+ if (attrs.size()>0){
+ avspec.addPragma(new AvatarPragmaSecret("#Confidentiality "+block.getName() + "."+req.getName()+"__reqData", req.getReferenceObject(), attrs));
+ }
+ }
AvatarActionOnSignal as= new AvatarActionOnSignal(ae.getName(), sig, ae.getReferenceObject());
for (int i=0; i<sr.getNbOfParams(); i++){
if (block.getAvatarAttributeWithName(sr.getParam(i))==null){
@@ -369,7 +386,9 @@ public class TML2Avatar {
//Create new value to send....
AvatarAttribute requestData= new AvatarAttribute(req.getName()+"__reqData", AvatarType.INTEGER, block, null);
as.addValue(req.getName()+"__reqData");
- block.addAttribute(requestData);
+ if (block.getAvatarAttributeWithName(req.getName()+"__reqData")==null){
+ block.addAttribute(requestData);
+ }
tran= new AvatarTransition(block, "__after_"+ae.getName(), ae.getReferenceObject());
elementList.add(as);
as.addNext(tran);
@@ -499,15 +518,33 @@ public class TML2Avatar {
if (block.getAvatarAttributeWithName(aee.getParam(i))==null){
//Throw Error
System.out.println("Missing Attribute " + aee.getParam(i));
- as.addValue("tmp");
}
else {
as.addValue(aee.getParam(i));
}
}
+ if (evt.checkConf){
+ LinkedList<AvatarAttribute> attrs = new LinkedList<AvatarAttribute>();
+ if (!attrsToCheck.contains(evt.getName()+"__eventData")){
+ attrs.add(new AvatarAttribute(evt.getName()+"__eventData", AvatarType.INTEGER, block, null));
+ attrsToCheck.add(evt.getName()+"__eventData");
+ }
+ for (int i=0; i<aee.getNbOfParams(); i++){
+ if (block.getAvatarAttributeWithName(aee.getParam(i))!=null && !attrsToCheck.contains(aee.getParam(i))){
+ attrs.add(block.getAvatarAttributeWithName(aee.getParam(i)));
+ attrsToCheck.add(aee.getParam(i));
+ }
+ }
+ if (attrs.size()>0){
+ avspec.addPragma(new AvatarPragmaSecret("#Confidentiality "+block.getName() + "."+evt.getName()+"__eventData", evt.getReferenceObject(), attrs));
+ }
+
+ }
AvatarAttribute eventData= new AvatarAttribute(evt.getName()+"__eventData", AvatarType.INTEGER, block, null);
as.addValue(evt.getName()+"__eventData");
- block.addAttribute(eventData);
+ if (block.getAvatarAttributeWithName(evt.getName()+"__eventData")==null){
+ block.addAttribute(eventData);
+ }
tran= new AvatarTransition(block, "__after_"+ae.getName(), ae.getReferenceObject());
elementList.add(as);
as.addNext(tran);
@@ -537,7 +574,9 @@ public class TML2Avatar {
}
AvatarAttribute eventData= new AvatarAttribute(evt.getName()+"__eventData", AvatarType.INTEGER, block, null);
as.addValue(evt.getName()+"__eventData");
- block.addAttribute(eventData);
+ if (block.getAvatarAttributeWithName(evt.getName()+"__eventData")==null){
+ block.addAttribute(eventData);
+ }
tran= new AvatarTransition(block, "__after_"+ae.getName(), ae.getReferenceObject());
elementList.add(as);
as.addNext(tran);
@@ -582,7 +621,9 @@ public class TML2Avatar {
signalMap.put(block.getName()+"__IN__"+ch.getName(), sig);
block.addSignal(sig);
AvatarAttribute channelData= new AvatarAttribute(ch.getName()+"__chData", AvatarType.INTEGER, block, null);
- block.addAttribute(channelData);
+ if (block.getAvatarAttributeWithName(ch.getName()+"__chData")==null){
+ block.addAttribute(channelData);
+ }
}
else {
sig=signalMap.get(block.getName()+"__IN__"+ch.getName());
@@ -595,19 +636,22 @@ public class TML2Avatar {
block.addSignal(sig);
signalMap.put(block.getName()+"__OUT__"+ch.getName(), sig);
AvatarAttribute channelData= new AvatarAttribute(ch.getName()+"__chData", AvatarType.INTEGER, block, null);
- LinkedList<AvatarAttribute> attrs = new LinkedList<AvatarAttribute>();
- block.addAttribute(channelData);
- attrs.add(channelData);
- if (ch.checkConf){
- System.out.println("channel " + ch.getName());
- System.out.println("block " + block.getName());
- avspec.addPragma(new AvatarPragmaSecret("#Confidentiality "+block.getName() + "."+ch.getName()+"__chData", ch.getReferenceObject(), attrs));
+ if (block.getAvatarAttributeWithName(ch.getName()+"__chData")==null){
+ block.addAttribute(channelData);
}
}
else {
sig=signalMap.get(block.getName()+"__OUT__"+ch.getName());
}
}
+ if (ch.checkConf){
+ LinkedList<AvatarAttribute> attrs = new LinkedList<AvatarAttribute>();
+ if (!attrsToCheck.contains(ch.getName()+"__chData")){
+ attrs.add(new AvatarAttribute(ch.getName()+"__chData", AvatarType.INTEGER, block, null));
+ attrsToCheck.add(ch.getName()+"__chData");
+ avspec.addPragma(new AvatarPragmaSecret("#Confidentiality "+block.getName() + "."+ch.getName()+"__chData", ch.getReferenceObject(), attrs));
+ }
+ }
AvatarActionOnSignal as = new AvatarActionOnSignal(ae.getName(), sig, ae.getReferenceObject());
as.addValue(ch.getName()+"__chData");
tran= new AvatarTransition(block, "__after_"+ae.getName(), ae.getReferenceObject());
@@ -784,6 +828,7 @@ public class TML2Avatar {
System.out.println("Failed to generate specification");
return avspec;
}
+ attrsToCheck.clear();
ArrayList<TMLTask> tasks = tmlmap.getTMLModeling().getTasks();
for (TMLTask task:tasks){
AvatarBlock block = new AvatarBlock(task.getName(), avspec, task.getReferenceObject());
@@ -1056,7 +1101,7 @@ public class TML2Avatar {
}
}
//Check if we matched up all signals
- System.out.println(avspec);
+ //System.out.println(avspec);
return avspec;
}
diff --git a/src/ui/GTMLModeling.java b/src/ui/GTMLModeling.java
index fdcec189289ece138a3870498ddbee0a0299c02b..f8e660831eea60e5bc285e1718aa2c0b0c853971 100755
--- a/src/ui/GTMLModeling.java
+++ b/src/ui/GTMLModeling.java
@@ -717,9 +717,11 @@ public class GTMLModeling {
addToTable(makeName(port2, port2.getFather().getValue()) + "/" + name2, name);
channel = new TMLChannel(name, port1);
- channel.checkConf= port1.checkConf;
+ channel.checkConf= port1.checkConf || port2.checkConf;
channel.setSize(port1.getSize());
channel.setMax(port1.getMax());
+ channel.ports.add(port1);
+ channel.ports.add(port2);
if (port1.isBlocking() && port2.isBlocking()) {
channel.setType(TMLChannel.BRBW);
} else if (!port1.isBlocking() && port2.isBlocking()) {
@@ -813,7 +815,13 @@ public class GTMLModeling {
// Channel attributes
port = (TMLCPrimitivePort)(portstome.get(0));
channel = new TMLChannel(name, port1);
+ channel.ports.add(port1);
channel.checkConf= port1.checkConf;
+ for(j=0; j<portstome.size(); j++) {
+ TMLCPrimitivePort p = (TMLCPrimitivePort)(portstome.get(j));
+ channel.checkConf= p.checkConf || channel.checkConf;
+ channel.ports.add(p);
+ }
channel.setSize(port1.getSize());
channel.setMax(port1.getMax());
if (port1.isBlocking() && port.isBlocking()) {
@@ -953,6 +961,7 @@ public class GTMLModeling {
} else {
event = new TMLEvent(name, port1, -1, port1.isBlocking());
}
+ event.checkConf= port1.checkConf;
for(i=0; i<port1.getNbMaxAttribute(); i++) {
tt = port1.getParamAt(i);
if ((tt != null) && (tt.getType() != TType.NONE)) {
@@ -1094,7 +1103,8 @@ public class GTMLModeling {
}
request = new TMLRequest(name, port1);
-
+ request.checkConf = port1.checkConf;
+ request.ports.add(port1);
for(i=0; i<port1.getNbMaxAttribute(); i++) {
tt = port1.getParamAt(i);
if ((tt != null) && (tt.getType() != TType.NONE)) {
diff --git a/src/ui/MainGUI.java b/src/ui/MainGUI.java
index a1af6246fe5c0eea4cd3ee810413631e17c2c0b4..b62b72df7105dc5287196c0c5a20429cf14c99c8 100755
--- a/src/ui/MainGUI.java
+++ b/src/ui/MainGUI.java
@@ -3758,11 +3758,18 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener, Pe
getCurrentTDiagramPanel().repaint();
}
else if (tp instanceof TMLArchiPanel) {
+ /* for (int i=0; i<tabs.size(); i++){
+ tp = (TURTLEPanel)(tabs.elementAt(i));
+ if (tp instanceof TMLComponentDesignPanel) {
+ ((TMLComponentDesignPanel)tp).modelBacktracingProVerif(pvoa);
+ }
+ }*/
+ System.out.println("BACKTRACE");
+ gtm.getTMLMapping().getTMLModeling().clearBacktracing();
+ gtm.getTMLMapping().getTMLModeling().backtrace(pvoa, getTabName(tp));
}
else if (tp instanceof TMLComponentDesignPanel){
- TMLComponentDesignPanel tap = (TMLComponentDesignPanel) tp;
- tap.modelBacktracingProVerif(pvoa);
- getCurrentTDiagramPanel().repaint();
+
}
return;
}
diff --git a/src/ui/TMLComponentDesignPanel.java b/src/ui/TMLComponentDesignPanel.java
index 2bc486ced59834f0a93f810b314f9f9aaf192ec0..d1246123ac1ff89c9ca69c2ed53bd78b41db0b8f 100755
--- a/src/ui/TMLComponentDesignPanel.java
+++ b/src/ui/TMLComponentDesignPanel.java
@@ -241,12 +241,19 @@ public class TMLComponentDesignPanel extends TURTLEPanel {
LinkedList<AvatarAttribute> nonSecretAttributes = pvoa.getNonSecretTerms ();
for (AvatarAttribute attr: secretAttributes){
System.out.println("!!!");
- iterator = tmlctdp.getPrimitiveComponentList().listIterator();
+ iterator = tmlctdp.componentList.listIterator();
while (iterator.hasNext()){
+
tgc = (TGComponent)(iterator.next());
- if (tgc instanceof TMLCPrimitivePort){
- System.out.println("port "+tgc);
- ((TMLCPrimitivePort)tgc).checkStatus =2;
+ System.out.println("NEXT " + tgc);
+ if (tgc instanceof TMLCPrimitiveComponent){
+ ArrayList<TMLCPrimitivePort> ports = ((TMLCPrimitiveComponent) tgc).getAllInternalPrimitivePorts();
+ for (TMLCPrimitivePort p:ports){
+ if (p.checkStatus>0){
+ System.out.println(p.getName());
+// p.checkStatus=3;
+ }
+ }
}
}
}
diff --git a/src/ui/tmlcompd/TMLCPrimitivePort.java b/src/ui/tmlcompd/TMLCPrimitivePort.java
index cd667a7e6f7c38b7037f614c01323fb4b856f217..c76c6e351f0da86556c5870b2cfcfb4aa2e83068 100755
--- a/src/ui/tmlcompd/TMLCPrimitivePort.java
+++ b/src/ui/tmlcompd/TMLCPrimitivePort.java
@@ -112,7 +112,7 @@ public abstract class TMLCPrimitivePort extends TGCScalableWithInternalComponent
editable = true;
removable = true;
userResizable = false;
- checkConf=false;
+ checkConf=true;
commName = "comm";
//value = "MyName";
makeValue();
@@ -318,7 +318,9 @@ public abstract class TMLCPrimitivePort extends TGCScalableWithInternalComponent
g.drawString(lname, x+width - w - 1, y+(int)(si)-2);
}
}*/
- drawVerification(g);
+
+ drawVerification(g);
+
g.setFont(fold);
drawParticularity(g);
@@ -342,12 +344,14 @@ public abstract class TMLCPrimitivePort extends TGCScalableWithInternalComponent
default:
return;
}
- g.drawString(mappingName, x, y);
- g.drawOval(x+6, y-10, 6, 9);
- g.setColor(c1);
- g.fillRect(x+4, y-7, 9, 7);
- g.setColor(c);
- g.drawRect(x+4, y-7, 9, 7);
+ g.drawString(mappingName, x-15, y-8);
+ g.drawOval(x-10, y, 6, 9);
+ g.setColor(c1);
+ g.fillRect(x-12, y+3, 9, 7);
+ g.setColor(c);
+ g.drawRect(x-12, y+3, 9, 7);
+
+
}
@@ -449,7 +453,6 @@ public abstract class TMLCPrimitivePort extends TGCScalableWithInternalComponent
TMLCPrimitiveComponent tgc = (TMLCPrimitiveComponent)(getFather());
otherTypes = tgc.getAllRecords();
}
-
JDialogTMLCompositePort jda = new JDialogTMLCompositePort(commName, typep, list[0], list[1], list[2], list[3], list[4], isOrigin, isFinite, isBlocking, ""+maxSamples, ""+widthSamples, isLossy, lossPercentage, maxNbOfLoss, frame, "Port properties", otherTypes, dataFlowType, associatedEvent, isPrex, isPostex, checkConf);
jda.setSize(350, 700);
GraphicLib.centerOnParent(jda);