diff --git a/modeling/SmartCardProtocol.xml b/modeling/SmartCardProtocol.xml
index b37f3c480a40f8836a0ccbf7472c0ccddb29635d..b4f05650449f69637bb9d7f7ab1e62ebfdce1a90 100755
--- a/modeling/SmartCardProtocol.xml
+++ b/modeling/SmartCardProtocol.xml
@@ -6,7 +6,7 @@
<AvatarRDPanel name="AVATAR RD" minX="10" maxX="1400" minY="10" maxY="900" zoom="1.0" >
<COMPONENT type="301" id="17" >
<cdparam x="627" y="331" />
-<sizeparam width="428" height="87" minWidth="50" minHeight="20" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="366" height="87" minWidth="50" minHeight="20" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="UML Note" value="Modeling assumptions
diff --git a/src/tmltranslator/TMLActivityElement.java b/src/tmltranslator/TMLActivityElement.java
index ae0717014a0a40f05453007ea458b5c7abc726a6..429380cc809e8d197afc057273afdcd508485f0e 100755
--- a/src/tmltranslator/TMLActivityElement.java
+++ b/src/tmltranslator/TMLActivityElement.java
@@ -50,7 +50,7 @@ import java.util.*;
public class TMLActivityElement extends TMLElement{
protected Vector<TMLActivityElement> nexts;
-
+ public String securityContext="";
public TMLActivityElement(String _name, Object _referenceObject) {
super(_name, _referenceObject);
nexts = new Vector();
diff --git a/src/tmltranslator/TMLChannel.java b/src/tmltranslator/TMLChannel.java
index c15367b2d0d9a650e4b8333b3ae484c80087a8c1..bd74708c9e031bf20cace5e0195d6ca544f1add5 100755
--- a/src/tmltranslator/TMLChannel.java
+++ b/src/tmltranslator/TMLChannel.java
@@ -57,6 +57,7 @@ public class TMLChannel extends TMLCommunicationElement {
public static final int NBRNBW = 2;
public int confStatus;
public boolean checkConf;
+ public boolean checkAuth;
private int size;
private int type;
private int max;
diff --git a/src/tmltranslator/TMLEvent.java b/src/tmltranslator/TMLEvent.java
index 6df4a0e0fd0973b7c99f0b2824631ca471fdcc0c..fba4de5b74de82c4b47a048e5937abdd91389de7 100755
--- a/src/tmltranslator/TMLEvent.java
+++ b/src/tmltranslator/TMLEvent.java
@@ -55,6 +55,7 @@ public class TMLEvent extends TMLCommunicationElement {
protected boolean canBeNotified = false;
protected TMLTask origin, destination;
public int confStatus;
+ public boolean checkAuth;
public boolean checkConf;
public TMLCPrimitivePort port;
public TMLCPrimitivePort port2;
diff --git a/src/tmltranslator/TMLModeling.java b/src/tmltranslator/TMLModeling.java
index fc979e811ebeaa7ac8e7446a9bc56c6b25bea438..ea27efa40f70183cbbfa94c209f2eec62691032c 100755
--- a/src/tmltranslator/TMLModeling.java
+++ b/src/tmltranslator/TMLModeling.java
@@ -61,7 +61,7 @@ public class TMLModeling {
private ArrayList<TMLRequest> requests;
private ArrayList<TMLEvent> events;
private ArrayList<String[]> pragmas;
-
+ public ArrayList<SecurityPattern> securityPatterns;
private TMLElement correspondance[];
private boolean optimized = false;
@@ -608,7 +608,7 @@ public class TMLModeling {
if (channel!=null){
for (TMLCPrimitivePort port:channel.ports){
if (port.checkConf){
- port.checkStatus = 2;
+ port.checkConfStatus = 2;
port.mappingName= mappingName;
}
}
@@ -617,7 +617,7 @@ public class TMLModeling {
if (req !=null){
for (TMLCPrimitivePort port: req.ports){
if (port.checkConf){
- port.checkStatus = 2;
+ port.checkConfStatus = 2;
port.mappingName= mappingName;
}
@@ -626,11 +626,11 @@ public class TMLModeling {
TMLEvent ev = getEventByName(attr.getName().replaceAll("__eventData",""));
if (ev !=null){
if (ev.port.checkConf){
- ev.port.checkStatus=2;
+ ev.port.checkConfStatus=2;
ev.port.mappingName= mappingName;
}
if (ev.port2.checkConf){
- ev.port2.checkStatus=2;
+ ev.port2.checkConfStatus=2;
ev.port2.mappingName=mappingName;
}
}
@@ -658,7 +658,7 @@ public class TMLModeling {
if (channel!=null){
for (TMLCPrimitivePort port:channel.ports){
if (port.checkConf){
- port.checkStatus = 3;
+ port.checkConfStatus = 3;
port.mappingName= mappingName;
}
}
@@ -667,7 +667,7 @@ public class TMLModeling {
if (req !=null){
for (TMLCPrimitivePort port: req.ports){
if (port.checkConf){
- port.checkStatus = 3;
+ port.checkConfStatus = 3;
port.mappingName= mappingName;
}
}
@@ -675,10 +675,11 @@ public class TMLModeling {
TMLEvent ev = getEventByName(attr.getName().replaceAll("__eventData",""));
if (ev !=null){
if (ev.port.checkConf){
- ev.port.checkStatus=3;
+ ev.port.checkConfStatus=3;
+ ev.port.mappingName= mappingName;
}
if (ev.port2.checkConf){
- ev.port2.checkStatus=3;
+ ev.port2.checkConfStatus=3;
ev.port2.mappingName= mappingName;
}
}
@@ -698,37 +699,200 @@ public class TMLModeling {
}
}
}
-
- System.out.println("backtracing finished");
return;
}
+ public void backtraceAuthenticity(LinkedList<String> satisfiedAuthenticity, LinkedList<String> satisfiedWeakAuthenticity,LinkedList<String> nonSatisfiedAuthenticity, String mappingName){
+ for (String s: satisfiedAuthenticity){
+ String signalName = s.split("__chData")[0];
+ for (TMLTask t: getTasks()){
+ if (signalName.contains(t.getName())){
+ signalName = signalName.replace(t.getName()+"__","");
+ }
+ }
+ TMLChannel channel = getChannelByName(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("__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;
+ }
+ }
+ }
+ for (String s: satisfiedWeakAuthenticity){
+ String signalName = s.split("__chData")[0];
+ for (TMLTask t: getTasks()){
+ if (signalName.contains(t.getName())){
+ signalName = signalName.replace(t.getName()+"__","");
+ }
+ }
+ TMLChannel channel = getChannelByName(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;
+ }
+ }
+ }
+ for (String s: nonSatisfiedAuthenticity){
+ String signalName = s.split("__chData")[0];
+ for (TMLTask t: getTasks()){
+ if (signalName.contains(t.getName())){
+ signalName = signalName.replace(t.getName()+"__","");
+ }
+ }
+ TMLChannel channel = getChannelByName(signalName);
+ if (channel!=null){
+ for (TMLCPrimitivePort port:channel.ports){
+ if (port.checkAuth){
+ port.checkStrongAuthStatus = 3;
+ 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 = 3;
+ 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.checkStrongAuthStatus=3;
+ ev.port2.mappingName= mappingName;
+ }
+ if (ev.port2.checkAuth){
+ ev.port2.checkStrongAuthStatus=3;
+ ev.port2.mappingName= mappingName;
+ }
+ }
+ }
+ }
public void clearBacktracing(){
for (TMLChannel channel: getChannels()){
for (TMLCPrimitivePort port:channel.ports){
- if (port.checkStatus>1){
- port.checkStatus=1;
+ if (port.checkConfStatus>1){
+ port.checkConfStatus=1;
port.mappingName="???";
}
+ if (port.checkStrongAuthStatus>1 || port.checkWeakAuthStatus>1){
+ port.checkStrongAuthStatus = 1;
+ port.checkWeakAuthStatus=1;
+ }
}
}
for (TMLRequest req: getRequests()){
for (TMLCPrimitivePort port:req.ports){
- if (port.checkStatus>1){
- port.checkStatus=1;
+ if (port.checkConfStatus>1){
+ port.checkConfStatus=1;
port.mappingName="???";
}
+ if (port.checkStrongAuthStatus>1 || port.checkWeakAuthStatus>1){
+ port.checkStrongAuthStatus = 1;
+ port.checkWeakAuthStatus=1;
+ }
}
}
for (TMLEvent evt: getEvents()){
if (evt.port!=null && evt.port2!=null){
- if (evt.port.checkStatus>1){
- evt.port.checkStatus=1;
+ if (evt.port.checkConfStatus>1){
+ evt.port.checkConfStatus=1;
evt.port.mappingName="???";
}
- if (evt.port2.checkStatus>1){
- evt.port2.checkStatus=1;
+ if (evt.port.checkStrongAuthStatus>1 || evt.port.checkWeakAuthStatus>1){
+ evt.port.checkStrongAuthStatus=1;
+ evt.port.checkWeakAuthStatus=1;
+ }
+ if (evt.port2.checkConfStatus>1){
+ evt.port2.checkConfStatus=1;
evt.port2.mappingName="???";
}
+ if (evt.port2.checkStrongAuthStatus>1 || evt.port2.checkWeakAuthStatus>1){
+ evt.port2.checkStrongAuthStatus=1;
+ evt.port2.checkWeakAuthStatus=1;
+ }
}
}
return;
diff --git a/src/tmltranslator/TMLRequest.java b/src/tmltranslator/TMLRequest.java
index 9b0cc46dc7b0c3446782954147b8de769bc14aa2..8638add88698646adf5ca96b3f0f1de5ff82137f 100755
--- a/src/tmltranslator/TMLRequest.java
+++ b/src/tmltranslator/TMLRequest.java
@@ -55,6 +55,7 @@ public class TMLRequest extends TMLCommunicationElement {
protected ArrayList<String> paramNames;
public int confStatus;
public boolean checkConf;
+ public boolean checkAuth;
public ArrayList<TMLCPrimitivePort> ports;
public TMLRequest(String name, Object reference) {
super(name, reference);
diff --git a/src/tmltranslator/toavatar/TML2Avatar.java b/src/tmltranslator/toavatar/TML2Avatar.java
index d9b968264c5531d17a14dadc52925318443597ab..5edb3aa8311b561e83fa3d3a8ede6e43cf063ff4 100644
--- a/src/tmltranslator/toavatar/TML2Avatar.java
+++ b/src/tmltranslator/toavatar/TML2Avatar.java
@@ -77,6 +77,10 @@ public class TML2Avatar {
public HashMap<String, Integer> originDestMap = new HashMap<String, Integer>();
HashMap<String, AvatarSignal> signalMap = new HashMap<String, AvatarSignal>();
public HashMap<String, Object> stateObjectMap = new HashMap<String, Object>();
+
+ HashMap<String, AvatarAttributeState> signalAuthOriginMap = new HashMap<String, AvatarAttributeState>();
+ HashMap<String, AvatarAttributeState> signalAuthDestMap = new HashMap<String, AvatarAttributeState>();
+
List<AvatarSignal> signals = new ArrayList<AvatarSignal>();
private final static Integer channelPublic = 0;
private final static Integer channelPrivate = 1;
@@ -380,6 +384,7 @@ public class TML2Avatar {
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){
@@ -397,6 +402,10 @@ public class TML2Avatar {
if (block.getAvatarAttributeWithName(req.getName()+"__reqData")==null){
block.addAttribute(requestData);
}
+ if (req.checkAuth){
+ AvatarAttributeState authOrig = new AvatarAttributeState(req.getName()+"__origin",ae.getReferenceObject(),requestData, signalState);
+ signalAuthOriginMap.put(req.getName(), authOrig);
+ }
tran= new AvatarTransition(block, "__after_"+ae.getName(), ae.getReferenceObject());
elementList.add(signalState);
signalState.addNext(signalTran);
@@ -560,6 +569,10 @@ public class TML2Avatar {
if (block.getAvatarAttributeWithName(evt.getName()+"__eventData")==null){
block.addAttribute(eventData);
}
+ if (evt.checkAuth){
+ AvatarAttributeState authOrig = new AvatarAttributeState(evt.getName()+"__origin",ae.getReferenceObject(),eventData, signalState);
+ signalAuthOriginMap.put(evt.getName(), authOrig);
+ }
tran= new AvatarTransition(block, "__after_"+ae.getName(), ae.getReferenceObject());
elementList.add(signalState);
signalState.addNext(signalTran);
@@ -606,6 +619,16 @@ public class TML2Avatar {
elementList.add(as);
as.addNext(tran);
elementList.add(tran);
+ if (evt.checkAuth){
+ AvatarState afterSignalState = new AvatarState("aftersignalstate_"+ae.getName()+"_"+evt.getName(),ae.getReferenceObject());
+ tran.addNext(afterSignalState);
+ tran = new AvatarTransition(block, "__aftersignalstate_"+ae.getName(), ae.getReferenceObject());
+ afterSignalState.addNext(tran);
+ elementList.add(afterSignalState);
+ elementList.add(tran);
+ AvatarAttributeState authDest = new AvatarAttributeState(evt.getName()+"__destination",ae.getReferenceObject(),eventData, afterSignalState);
+ signalAuthDestMap.put(evt.getName(), authDest);
+ }
}
else {
//Notify Event, I don't know how to translate this
@@ -655,6 +678,31 @@ public class TML2Avatar {
else {
sig=signalMap.get(block.getName()+"__IN__"+ch.getName());
}
+ AvatarActionOnSignal as = new AvatarActionOnSignal(ae.getName(), sig, ae.getReferenceObject());
+ as.addValue(ch.getName()+"__chData");
+ tran= new AvatarTransition(block, "__after_"+ae.getName(), ae.getReferenceObject());
+ elementList.add(signalState);
+ signalState.addNext(signalTran);
+ elementList.add(signalTran);
+ signalTran.addNext(as);
+ as.addNext(tran);
+ elementList.add(as);
+ elementList.add(tran);
+ if (ch.checkAuth){
+ //Add aftersignal state
+ AvatarState afterSignalState = new AvatarState("aftersignalstate_"+ae.getName()+"_"+ch.getName(),ae.getReferenceObject());
+ tran.addNext(afterSignalState);
+ tran = new AvatarTransition(block, "__aftersignalstate_"+ae.getName(), ae.getReferenceObject());
+ afterSignalState.addNext(tran);
+ elementList.add(afterSignalState);
+ elementList.add(tran);
+ if (block.getAvatarAttributeWithName(ch.getName()+"__chData")==null){
+ AvatarAttribute channelData= new AvatarAttribute(ch.getName()+"__chData", AvatarType.INTEGER, block, null);
+ block.addAttribute(channelData);
+ }
+ AvatarAttributeState authDest = new AvatarAttributeState(ch.getName()+"__destination",ae.getReferenceObject(),block.getAvatarAttributeWithName(ch.getName()+"__chData"), afterSignalState);
+ signalAuthDestMap.put(ch.getName(), authDest);
+ }
}
else {
if (!signalMap.containsKey(block.getName()+"__OUT__"+ch.getName())){
@@ -670,25 +718,33 @@ public class TML2Avatar {
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());
- elementList.add(signalState);
- signalState.addNext(signalTran);
- elementList.add(signalTran);
- signalTran.addNext(as);
- as.addNext(tran);
- elementList.add(as);
- elementList.add(tran);
+ 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));
+ }
+ }
+ if (ch.checkAuth){
+ if (block.getAvatarAttributeWithName(ch.getName()+"__chData")==null){
+ AvatarAttribute channelData= new AvatarAttribute(ch.getName()+"__chData", AvatarType.INTEGER, block, null);
+ block.addAttribute(channelData);
+ }
+ AvatarAttributeState authOrigin = new AvatarAttributeState(ch.getName()+"__destination",ae.getReferenceObject(),block.getAvatarAttributeWithName(ch.getName()+"__chData"), signalState);
+ signalAuthOriginMap.put(ch.getName(), authOrigin);
+ }
+ AvatarActionOnSignal as = new AvatarActionOnSignal(ae.getName(), sig, ae.getReferenceObject());
+ as.addValue(ch.getName()+"__chData");
+ tran= new AvatarTransition(block, "__after_"+ae.getName(), ae.getReferenceObject());
+ elementList.add(signalState);
+ signalState.addNext(signalTran);
+ elementList.add(signalTran);
+ signalTran.addNext(as);
+ as.addNext(tran);
+ elementList.add(as);
+ elementList.add(tran);
+ }
}
else if (ae instanceof TMLForLoop){
TMLForLoop loop = (TMLForLoop)ae;
@@ -889,14 +945,17 @@ public class TML2Avatar {
for (TMLChannel channel: tmlmodel.getChannels()){
for (TMLCPrimitivePort p: channel.ports){
channel.checkConf = channel.checkConf || p.checkConf;
+ channel.checkAuth = channel.checkAuth || p.checkAuth;
}
}
for (TMLEvent event: tmlmodel.getEvents()){
event.checkConf = event.port.checkConf || event.port2.checkConf;
+ event.checkAuth = event.port.checkAuth || event.port2.checkAuth;
}
for (TMLRequest request: tmlmodel.getRequests()){
for (TMLCPrimitivePort p: request.ports){
request.checkConf = p.checkConf || request.checkConf;
+ request.checkAuth = p.checkAuth || request.checkAuth;
}
}
@@ -932,7 +991,7 @@ public class TML2Avatar {
AvatarAttribute req_loop_index= new AvatarAttribute("req_loop_index", AvatarType.INTEGER, block, null);
block.addAttribute(req_loop_index);
- TMLRequest request= tmlmodel.getRequestToMe(task);
+ //TMLRequest request= tmlmodel.getRequestToMe(task);
//Oh this is fun...let's restructure the state machine
//Create own start state, and ignore the returned one
List<AvatarStateMachineElement> elementList= translateState(task.getActivityDiagram().get(0), block);
@@ -981,7 +1040,8 @@ public class TML2Avatar {
//Add Requests, direct transition to start of state machine
- for (Object obj: tmlmodel.getRequestsToMe(task)){
+ for (Object obj: tmlmodel.getRequestsToMe(task)){
+ System.out.println("Building request ");
TMLRequest req = (TMLRequest) obj;
AvatarTransition incrTran = new AvatarTransition(block, "__after_loopstart__"+req.getName(), task.getActivityDiagram().get(0).getReferenceObject());
incrTran.addAction(AvatarTerm.createActionFromString(block,"req_loop_index = req_loop_index + 1"));
@@ -1004,25 +1064,34 @@ public class TML2Avatar {
as.addValue(req.getName()+"__reqData");
AvatarAttribute requestData= new AvatarAttribute(req.getName()+"__reqData", AvatarType.INTEGER, block, null);
block.addAttribute(requestData);
- for (int i=0; i< request.getNbOfParams(); i++){
- if (block.getAvatarAttributeWithName(request.getParam(i))==null){
+ for (int i=0; i< req.getNbOfParams(); i++){
+ if (block.getAvatarAttributeWithName(req.getParam(i))==null){
//Throw Error
as.addValue("tmp");
}
else {
- as.addValue(request.getParam(i));
+ as.addValue(req.getParam(i));
}
}
- AvatarTransition tran = new AvatarTransition(block, "__after_" + request.getName(), task.getActivityDiagram().get(0).getReferenceObject());
+ AvatarTransition tran = new AvatarTransition(block, "__after_" + req.getName(), task.getActivityDiagram().get(0).getReferenceObject());
as.addNext(tran);
asm.addElement(tran);
- tran.addNext(newStart);
- }
-
-
-
-
+ if (req.checkAuth){
+ AvatarState afterSignalState = new AvatarState("aftersignalstate_"+req.getName()+"_"+req.getName(),req.getReferenceObject());
+ AvatarTransition afterSignalTran = new AvatarTransition(block, "__aftersignalstate_"+req.getName(), req.getReferenceObject());
+ tran.addNext(afterSignalState);
+ afterSignalState.addNext(afterSignalTran);
+ asm.addElement(afterSignalState);
+ asm.addElement(afterSignalTran);
+ afterSignalTran.addNext(newStart);
+ AvatarAttributeState authDest = new AvatarAttributeState(req.getName()+"__destination",obj,requestData, afterSignalState);
+ signalAuthDestMap.put(req.getName(), authDest);
+ }
+ else {
+ tran.addNext(newStart);
+ }
+ }
asm.setStartState((AvatarStartState) ss);
@@ -1042,6 +1111,15 @@ public class TML2Avatar {
}
checkConnections();
checkChannels();
+
+ //Add authenticity pragmas
+ for (String s: signalAuthOriginMap.keySet()){
+ if (signalAuthDestMap.containsKey(s)){
+ AvatarPragmaAuthenticity pragma = new AvatarPragmaAuthenticity(s, signalAuthOriginMap.get(s).getReferenceObject(), signalAuthOriginMap.get(s), signalAuthDestMap.get(s));
+ avspec.addPragma(pragma);
+ }
+ }
+
//Create relations
//Channels are ?? to ??
//Requests are n to 1
@@ -1214,6 +1292,7 @@ public class TML2Avatar {
//System.out.println(avspec);
return avspec;
}
+
public void backtraceReachability(List<String> reachableStates, List<String> nonReachableStates){
for (String s: reachableStates){
if (stateObjectMap.containsKey(s.replace("enteringState__",""))){
diff --git a/src/ui/GTMLModeling.java b/src/ui/GTMLModeling.java
index 249ea14cccdec7bd58031712590d3dfa19c09210..3a7de92c90b25b5f9568c99d0d58fc9c9bb0b1d4 100755
--- a/src/ui/GTMLModeling.java
+++ b/src/ui/GTMLModeling.java
@@ -1471,6 +1471,21 @@ public class GTMLModeling {
((BasicErrorHighlight)tgc).setStateAction(ErrorHighlight.OK);
listE.addCor(tmlexecii, tgc);
+ } else if (tgc instanceof TMLADEncrypt) {
+ tmlexeci = new TMLExecI("execi", tgc);
+ tmlexeci.setAction("123");
+ activity.addElement(tmlexeci);
+ ((BasicErrorHighlight)tgc).setStateAction(ErrorHighlight.OK);
+ listE.addCor(tmlexeci, tgc);
+
+ } else if (tgc instanceof TMLADDecrypt) {
+ tmlexeci = new TMLExecI("decrypt", tgc);
+ tmlexeci.setAction("234");
+ activity.addElement(tmlexeci);
+ ((BasicErrorHighlight)tgc).setStateAction(ErrorHighlight.OK);
+ listE.addCor(tmlexeci, tgc);
+
+
} else if (tgc instanceof TMLADExecC) {
tmlexecc = new TMLExecC("execc", tgc);
tmlexecc.setAction(modifyString(((TMLADExecC)tgc).getDelayValue()));
diff --git a/src/ui/IconManager.java b/src/ui/IconManager.java
index cd6814a6710460ab2e1eb77fd08c7897359f2d3f..95301cac9e8e88d1df8dc7171080699f558e0ce9 100755
--- a/src/ui/IconManager.java
+++ b/src/ui/IconManager.java
@@ -109,6 +109,7 @@ public class IconManager {
public static ImageIcon imgic800, imgic802, imgic804, imgic806, imgic808, imgic810, imgic812;
public static ImageIcon imgic900, imgic902, imgic904, imgic906, imgic908, imgic910, imgic912, imgic914, imgic916, imgic918;
public static ImageIcon imgic920, imgic922, imgic924, imgic926, imgic928, imgic930;
+ public static ImageIcon imgic940, imgic941;
// Requirement diagrams
public static ImageIcon imgic1000, imgic1002, imgic1004,imgic1006,imgic1008, imgic1010, imgic1012, imgic1014, imgic1016, imgic1018;
public static ImageIcon imgic1050, imgic1052, imgic1054,imgic1056, imgic1058, imgic1060;
@@ -431,6 +432,8 @@ public class IconManager {
private static String icon926 = "images/tmladforeverloop.gif";
private static String icon928 = "images/tmladunorderedsequence.gif";
private static String icon930 = "images/tmladreadrequestarg.gif";
+ private static String icon940 = "images/tmladencrypt.gif";
+ private static String icon941 = "images/tmladdecrypt.gif";
// Requirement diagrams
private static String icon1000 = "images/reqdiag.gif";
@@ -832,6 +835,8 @@ public class IconManager {
imgic926 = getIcon(icon926);
imgic928 = getIcon(icon928);
imgic930 = getIcon(icon930);
+ imgic940 = getIcon(icon940);
+ imgic941 = getIcon(icon941);
imgic1000 = getIcon(icon1000);
imgic1002 = getIcon(icon1002);
diff --git a/src/ui/MainGUI.java b/src/ui/MainGUI.java
index da899a6f11bd6b148f7688f704abe4809f287519..4b86a4e9a2fc56f0a42fd45533fa103d2b3c20d6 100755
--- a/src/ui/MainGUI.java
+++ b/src/ui/MainGUI.java
@@ -3767,6 +3767,8 @@ 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));
+ System.out.println("backtracing finished");
}
else if (tp instanceof TMLComponentDesignPanel){
@@ -8557,6 +8559,10 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener, Pe
actionOnButton(TGComponentManager.COMPONENT, TGComponentManager.TMLAD_SELECT_EVT);
} else if (command.equals(actions[TGUIAction.TMLAD_RANDOM].getActionCommand())) {
actionOnButton(TGComponentManager.COMPONENT, TGComponentManager.TMLAD_RANDOM);
+ } else if (command.equals(actions[TGUIAction.TMLAD_ENCRYPT].getActionCommand())) {
+ actionOnButton(TGComponentManager.COMPONENT, TGComponentManager.TMLAD_ENCRYPT);
+ } else if (command.equals(actions[TGUIAction.TMLAD_DECRYPT].getActionCommand())) {
+ actionOnButton(TGComponentManager.COMPONENT, TGComponentManager.TMLAD_DECRYPT);
} else if (command.equals(actions[TGUIAction.TMLCTD_CCOMPONENT].getActionCommand())) {
actionOnButton(TGComponentManager.COMPONENT, TGComponentManager.TMLCTD_CCOMPONENT);
} else if (command.equals(actions[TGUIAction.TMLCTD_CREMOTECOMPONENT].getActionCommand())) {
diff --git a/src/ui/TGComponentManager.java b/src/ui/TGComponentManager.java
index e7d8183e85b46487561ddfe1a041bf87b5334926..7107a14e3507c6f67f3eaa41de8ffb66b7090172 100755
--- a/src/ui/TGComponentManager.java
+++ b/src/ui/TGComponentManager.java
@@ -236,6 +236,8 @@ public class TGComponentManager {
public static final int TMLAD_INTERVAL_DELAY = 1028;
public static final int TMLAD_FOR_EVER_LOOP = 1030;
public static final int TMLAD_READ_REQUEST_ARG = 1034;
+ public static final int TMLAD_ENCRYPT = 1035;
+ public static final int TMLAD_DECRYPT = 1036;
public static final int TMLARCHI_CPUNODE = 1100;
public static final int TMLARCHI_ARTIFACT = 1101;
@@ -1039,6 +1041,12 @@ public class TGComponentManager {
case TMLAD_RANDOM:
tgc = new TMLADRandom(x, y, tdp.getMinX(), tdp.getMaxX(), tdp.getMinY(), tdp.getMaxY(), false, null, tdp);
break;
+ case TMLAD_ENCRYPT:
+ tgc = new TMLADEncrypt(x, y, tdp.getMinX(), tdp.getMaxX(), tdp.getMinY(), tdp.getMaxY(), false, null, tdp);
+ break;
+ case TMLAD_DECRYPT:
+ tgc = new TMLADDecrypt(x, y, tdp.getMinX(), tdp.getMaxX(), tdp.getMinY(), tdp.getMaxY(), false, null, tdp);
+ break;
case TMLCTD_CCOMPONENT:
tgc = new TMLCCompositeComponent(x, y, tdp.getMinX(), tdp.getMaxX(), tdp.getMinY(), tdp.getMaxY(), false, null, tdp);
break;
@@ -1696,6 +1704,10 @@ public class TGComponentManager {
return TMLAD_UNORDERED_SEQUENCE;
} else if (tgc instanceof TMLADSelectEvt) {
return TMLAD_SELECT_EVT;
+ } else if (tgc instanceof TMLADEncrypt) {
+ return TMLAD_ENCRYPT;
+ } else if (tgc instanceof TMLADDecrypt) {
+ return TMLAD_DECRYPT;
} else if (tgc instanceof TMLADRandom) {
return TMLAD_RANDOM;
diff --git a/src/ui/TGUIAction.java b/src/ui/TGUIAction.java
index ab4cbb0e5c39ca63c1b90dbb1edc3204abffdcd3..9690d240a35cf9bd0e8895cec64a34d0657629ed 100755
--- a/src/ui/TGUIAction.java
+++ b/src/ui/TGUIAction.java
@@ -204,6 +204,9 @@ public class TGUIAction extends AbstractAction {
public static final int TMLAD_SELECT_EVT = 206;
public static final int TMLAD_RANDOM = 245;
public static final int TMLAD_READ_REQUEST_ARG = 335;
+
+ public static final int TMLAD_ENCRYPT = 430;
+ public static final int TMLAD_DECRYPT = 431;
public static final int TMLARCHI_EDIT = 216;
public static final int TMLARCHI_LINK = 217;
@@ -570,7 +573,7 @@ public class TGUIAction extends AbstractAction {
public static final int ACT_INTERNAL_SEARCH = 415;
//--
- public static final int NB_ACTION = 428;
+ public static final int NB_ACTION = 500;
private static final TAction [] actions = new TAction[NB_ACTION];
@@ -918,6 +921,12 @@ actions[ADD_VGMNNODE] = new TAction("add-add-vgmnnode", "Add a VGMN", IconManage
actions[TMLAD_RANDOM] = new TAction("add-tmlad-random", "Add random", IconManager.imgic924, IconManager.imgic924, "Select random", "Add a random operator to the currently opened TML Task activity diagram", 0);
actions[TMLAD_READ_REQUEST_ARG] = new TAction("add-tmladd-read-request-arg", "Reading request arguments", IconManager.imgic930, IconManager.imgic930, "Reading request arguments", "Add a reading request argument operator to the currently opened TML activity diagram", 0);
+
+
+ actions[TMLAD_ENCRYPT] = new TAction("add-tmlad-encrypt", "Add Encryption", IconManager.imgic940, IconManager.imgic940, "Encryption", "Add an encryption operator to the currently opened TML Task activity diagram", 0);
+ actions[TMLAD_DECRYPT] = new TAction("add-tmlad-decrypt", "Add Decryption", IconManager.imgic941, IconManager.imgic941, "Decryption", "Add a decryption operator to the currently opened TML Task activity diagram", 0);
+
+
actions[EBRDD_EDIT] = new TAction("edit-ebrdd-diagram", "Edit EBRDD", IconManager.imgic100, IconManager.imgic101, "Edit EBRDD", "Make it possible to edit the currently opened Event-Based Requirement Description Diagram", 0);
actions[EBRDD_CONNECTOR] = new TAction("add-ebrdd-connector", "Connect two operators together", IconManager.imgic202, IconManager.imgic202, "Connect two operators together", "Connect two operators of the currently opened Event-Based Requirement Description Diagram", 0);
actions[EBRDD_START] = new TAction("add-ebrdd-start", "Add Start state", IconManager.imgic222, IconManager.imgic222, "Start", "Add a start state to the currently opened Event-Based Requirement Description Diagram", 0);
diff --git a/src/ui/TMLComponentDesignPanel.java b/src/ui/TMLComponentDesignPanel.java
index d1246123ac1ff89c9ca69c2ed53bd78b41db0b8f..6adbf3327553aa1ac44fdbf5bc8fff5c943692b5 100755
--- a/src/ui/TMLComponentDesignPanel.java
+++ b/src/ui/TMLComponentDesignPanel.java
@@ -230,89 +230,5 @@ public class TMLComponentDesignPanel extends TURTLEPanel {
public String[] getAllOutRequests(String nameOfComponent) {
return tmlctdp.getAllOutRequests(nameOfComponent);
}
- public void modelBacktracingProVerif(ProVerifOutputAnalyzer pvoa) {
-
- resetModelBacktracingProVerif();
- TGComponent tgc;
- int index;
- ListIterator iterator;
- // Confidential attributes
- LinkedList<AvatarAttribute> secretAttributes = pvoa.getSecretTerms ();
- LinkedList<AvatarAttribute> nonSecretAttributes = pvoa.getNonSecretTerms ();
- for (AvatarAttribute attr: secretAttributes){
- System.out.println("!!!");
- iterator = tmlctdp.componentList.listIterator();
- while (iterator.hasNext()){
-
- tgc = (TGComponent)(iterator.next());
- 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;
- }
- }
- }
- }
- }
-/*
- 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);
- }
- }
- }
- }
- }
- }
- }
-*/
- LinkedList<String> notProved = pvoa.getNotProved ();
- LinkedList<String> satisfied = pvoa.getSatisfiedAuthenticity ();
- LinkedList<String> satisfiedWeak = pvoa.getSatisfiedWeakAuthenticity ();
- LinkedList<String> nonSatisfied = pvoa.getNonSatisfiedAuthenticity ();
- }
-
-
- public void resetModelBacktracingProVerif() {
- /*if (abdp == null) {
- return;
- }
-
- // Reset confidential attributes
- for(AvatarBDBlock block1: abdp.getFullBlockList()) {
- block1.resetConfidentialityOfAttributes();
- }
- for (Object tgc: abdp.getComponentList()){
- if (tgc instanceof AvatarBDPragma){
- AvatarBDPragma pragma = (AvatarBDPragma) tgc;
- pragma.authStrongMap.clear();
- pragma.authWeakMap.clear();
-
- }
- }
- // Reset reachable states
- for(int i=0; i<panels.size(); i++) {
- tdp = (TDiagramPanel)(panels.get(i));
- if (tdp instanceof AvatarSMDPanel) {
- ((AvatarSMDPanel)tdp).resetStateSecurityInfo();
- }
- }*/
- }
+
}
diff --git a/src/ui/images/tmladdecrypt.gif b/src/ui/images/tmladdecrypt.gif
new file mode 100755
index 0000000000000000000000000000000000000000..fc0523d687191d35570720df521cc5300f9cf8c4
Binary files /dev/null and b/src/ui/images/tmladdecrypt.gif differ
diff --git a/src/ui/images/tmladencrypt.gif b/src/ui/images/tmladencrypt.gif
new file mode 100755
index 0000000000000000000000000000000000000000..06d4e06cacdd33ec269de8dc5a5e85646180dcb9
Binary files /dev/null and b/src/ui/images/tmladencrypt.gif differ
diff --git a/src/ui/tmlad/TMLADReadChannel.java b/src/ui/tmlad/TMLADReadChannel.java
index 83ccd3c2e323749496ab1ff0ace57506238d695e..a77795c623ab831de1d6d0ce188df5dd79127d40 100755
--- a/src/ui/tmlad/TMLADReadChannel.java
+++ b/src/ui/tmlad/TMLADReadChannel.java
@@ -67,7 +67,7 @@ public class TMLADReadChannel extends TGCWithoutInternalComponent implements Che
protected String channelName = "ch";
protected String nbOfSamples= "1";
-
+ public String securityContext ="";
protected int stateOfError = 0; // Not yet checked
public final static int NOT_VERIFIED = 0;
@@ -170,12 +170,12 @@ public class TMLADReadChannel extends TGCWithoutInternalComponent implements Che
return;
}
- GraphicLib.arrowWithLine(g, 1, 0, 10, x-30, y+4, x-15, y+4, true);
- g.drawOval(x-11, y-3, 7, 9);
+ GraphicLib.arrowWithLine(g, 1, 0, 10, x-30, y-3, x-15, y-3, true);
+ g.drawOval(x-11, y-10, 7, 9);
g.setColor(c1);
- g.fillRect(x-12, y, 9, 7);
+ g.fillRect(x-12, y-7, 9, 7);
g.setColor(c);
- g.drawRect(x-12, y, 9, 7);
+ g.drawRect(x-12, y-7, 9, 7);
}
}
@@ -210,20 +210,22 @@ public class TMLADReadChannel extends TGCWithoutInternalComponent implements Che
public boolean editOndoubleClick(JFrame frame) {
- String [] labels = new String[2];
- String [] values = new String[2];
+ String [] labels = new String[3];
+ String [] values = new String[3];
labels[0] = "Channel name";
values[0] = channelName;
labels[1] = "Nb of samples";
values[1] = nbOfSamples;
+ labels[2] = "Security Pattern";
+ values[2] = securityContext;
ArrayList<String []> help = new ArrayList<String []>();
String[] allInChannels = tdp.getMGUI().getAllInChannels();
help.add(allInChannels);
- JDialogTwoString jdts = new JDialogTwoString(frame, "Setting channel's properties", "Channel name", channelName, "Nb of samples", nbOfSamples);
+ // JDialogTwoString jdts = new JDialogTwoString(frame, "Setting channel's properties", "Channel name", channelName, "Nb of samples", nbOfSamples);
- JDialogMultiString jdms = new JDialogMultiString(frame, "Setting channel's properties", 2, labels, values, help);
+ JDialogMultiString jdms = new JDialogMultiString(frame, "Setting channel's properties", 3, labels, values, help);
jdms.setSize(450, 300);
GraphicLib.centerOnParent(jdms);
jdms.show(); // blocked until dialog has been closed
@@ -231,7 +233,7 @@ public class TMLADReadChannel extends TGCWithoutInternalComponent implements Che
if (jdms.hasBeenSet() && (jdms.hasValidString(0))) {
channelName = jdms.getString(0);
nbOfSamples = jdms.getString(1);
-
+ securityContext = jdms.getString(2);
makeValue();
return true;
}
@@ -258,6 +260,8 @@ public class TMLADReadChannel extends TGCWithoutInternalComponent implements Che
sb.append(getChannelName());
sb.append("\" nbOfSamples=\"");
sb.append(getSamplesValue());
+ sb.append("\" secPattern=\"");
+ sb.append(securityContext);
sb.append("\" />\n");
sb.append("</extraparam>\n");
return new String(sb);
@@ -287,6 +291,7 @@ public class TMLADReadChannel extends TGCWithoutInternalComponent implements Che
if (elt.getTagName().equals("Data")) {
channelName = elt.getAttribute("channelName");
nbOfSamples = elt.getAttribute("nbOfSamples");
+ securityContext = elt.getAttribute("secPattern");
}
}
}
diff --git a/src/ui/tmlad/TMLADSendEvent.java b/src/ui/tmlad/TMLADSendEvent.java
index ceb05d5c505582b46ffaa5a31de87a352832dfc9..51537ac70be5ae16bdc72f3677f0a1ac3aa3eead 100755
--- a/src/ui/tmlad/TMLADSendEvent.java
+++ b/src/ui/tmlad/TMLADSendEvent.java
@@ -184,13 +184,12 @@ public class TMLADSendEvent extends TGCWithoutInternalComponent implements Check
return;
}
- GraphicLib.arrowWithLine(g, 1, 0, 10, x-30, y+4, x-15, y+4, true);
- g.drawOval(x-11, y-3, 7, 9);
+ GraphicLib.arrowWithLine(g, 1, 0, 10, x-30, y-3, x-15, y-3, true);
+ g.drawOval(x-11, y-10, 7, 9);
g.setColor(c1);
- g.fillRect(x-12, y, 9, 7);
+ g.fillRect(x-12, y-7, 9, 7);
g.setColor(c);
- g.drawRect(x-12, y, 9, 7);
-
+ g.drawRect(x-12, y-7, 9, 7);
}
}
public TGComponent isOnMe(int _x, int _y) {
diff --git a/src/ui/tmlad/TMLADSendRequest.java b/src/ui/tmlad/TMLADSendRequest.java
index 5a8ca642ac7195e87a49a81a831041694fdb5c50..06dc68d2c8c3b7a1bcefcae806c0376a7d771ed7 100755
--- a/src/ui/tmlad/TMLADSendRequest.java
+++ b/src/ui/tmlad/TMLADSendRequest.java
@@ -171,12 +171,12 @@ public class TMLADSendRequest extends TGCWithoutInternalComponent implements Che
return;
}
- GraphicLib.arrowWithLine(g, 1, 0, 10, x-30, y+4, x-15, y+4, true);
- g.drawOval(x-11, y-3, 7, 9);
+ GraphicLib.arrowWithLine(g, 1, 0, 10, x-30, y-3, x-15, y-3, true);
+ g.drawOval(x-11, y-10, 7, 9);
g.setColor(c1);
- g.fillRect(x-12, y, 9, 7);
+ g.fillRect(x-12, y-7, 9, 7);
g.setColor(c);
- g.drawRect(x-12, y, 9, 7);
+ g.drawRect(x-12, y-7, 9, 7);
}
}
diff --git a/src/ui/tmlad/TMLADWaitEvent.java b/src/ui/tmlad/TMLADWaitEvent.java
index d2b8951aee588508eee5059c0705815f7a8797f6..f146325162b45fded12783af9b4420c810dfdc64 100755
--- a/src/ui/tmlad/TMLADWaitEvent.java
+++ b/src/ui/tmlad/TMLADWaitEvent.java
@@ -173,12 +173,12 @@ public class TMLADWaitEvent extends TGCWithoutInternalComponent implements Check
return;
}
- GraphicLib.arrowWithLine(g, 1, 0, 10, x-30, y+4, x-15, y+4, true);
- g.drawOval(x-11, y-3, 7, 9);
+ GraphicLib.arrowWithLine(g, 1, 0, 10, x-30, y-3, x-15, y-3, true);
+ g.drawOval(x-11, y-10, 7, 9);
g.setColor(c1);
- g.fillRect(x-12, y, 9, 7);
+ g.fillRect(x-12, y-7, 9, 7);
g.setColor(c);
- g.drawRect(x-12, y, 9, 7);
+ g.drawRect(x-12, y-7, 9, 7);
}
}
diff --git a/src/ui/tmlad/TMLADWriteChannel.java b/src/ui/tmlad/TMLADWriteChannel.java
index 51454888c0e0c1e7b3366cafd836eacb5555bca6..0685f0ec290797688ee6bc51b8e073ae924aad1a 100755
--- a/src/ui/tmlad/TMLADWriteChannel.java
+++ b/src/ui/tmlad/TMLADWriteChannel.java
@@ -66,7 +66,7 @@ public class TMLADWriteChannel extends TGCWithoutInternalComponent implements Ch
protected String channelName = "ch";
protected String nbOfSamples= "1";
-
+ public String securityContext = "";
protected int stateOfError = 0; // Not yet checked
public final static int NOT_VERIFIED = 0;
@@ -168,12 +168,12 @@ public class TMLADWriteChannel extends TGCWithoutInternalComponent implements Ch
return;
}
- GraphicLib.arrowWithLine(g, 1, 0, 10, x-30, y+4, x-15, y+4, true);
- g.drawOval(x-11, y-3, 7, 9);
+ GraphicLib.arrowWithLine(g, 1, 0, 10, x-30, y-3, x-15, y-3, true);
+ g.drawOval(x-11, y-10, 7, 9);
g.setColor(c1);
- g.fillRect(x-12, y, 9, 7);
+ g.fillRect(x-12, y-7, 9, 7);
g.setColor(c);
- g.drawRect(x-12, y, 9, 7);
+ g.drawRect(x-12, y-7, 9, 7);
}
}
@@ -217,12 +217,14 @@ public class TMLADWriteChannel extends TGCWithoutInternalComponent implements Ch
}
public boolean editOndoubleClick(JFrame frame) {
- String [] labels = new String[2];
- String [] values = new String[2];
+ String [] labels = new String[3];
+ String [] values = new String[3];
labels[0] = "Channel name";
values[0] = channelName;
labels[1] = "Nb of samples";
values[1] = nbOfSamples;
+ labels[2] = "Security Pattern";
+ values[2] = securityContext;
ArrayList<String []> help = new ArrayList<String []>();
String[] allOutChannels = tdp.getMGUI().getAllOutChannels();
@@ -230,7 +232,7 @@ public class TMLADWriteChannel extends TGCWithoutInternalComponent implements Ch
//JDialogTwoString jdts = new JDialogTwoString(frame, "Setting channel's properties", "Channel name", channelName, "Nb of samples", nbOfSamples);
- JDialogMultiString jdms = new JDialogMultiString(frame, "Setting channel's properties", 2, labels, values, help);
+ JDialogMultiString jdms = new JDialogMultiString(frame, "Setting channel's properties", 3, labels, values, help);
jdms.setSize(450, 300);
GraphicLib.centerOnParent(jdms);
jdms.show(); // blocked until dialog has been closed
@@ -238,6 +240,7 @@ public class TMLADWriteChannel extends TGCWithoutInternalComponent implements Ch
if (jdms.hasBeenSet() && (jdms.hasValidString(0))) {
channelName = jdms.getString(0);
nbOfSamples = jdms.getString(1);
+ securityContext = jdms.getString(2);
makeValue();
return true;
@@ -253,6 +256,8 @@ public class TMLADWriteChannel extends TGCWithoutInternalComponent implements Ch
sb.append(channelName);
sb.append("\" nbOfSamples=\"");
sb.append(getSamplesValue());
+ sb.append("\" secPattern=\"");
+ sb.append(securityContext);
sb.append("\" />\n");
sb.append("</extraparam>\n");
return new String(sb);
@@ -282,6 +287,7 @@ public class TMLADWriteChannel extends TGCWithoutInternalComponent implements Ch
if (elt.getTagName().equals("Data")) {
channelName = elt.getAttribute("channelName");
nbOfSamples = elt.getAttribute("nbOfSamples");
+ securityContext = elt.getAttribute("secPattern");
}
}
}
diff --git a/src/ui/tmlad/TMLActivityDiagramToolBar.java b/src/ui/tmlad/TMLActivityDiagramToolBar.java
index d054d2a2ce0dfa343c471a53fccf2f8f17f2fdab..f8718c6f9e9c6c0920e4d6c343706a4ac3cc1007 100755
--- a/src/ui/tmlad/TMLActivityDiagramToolBar.java
+++ b/src/ui/tmlad/TMLActivityDiagramToolBar.java
@@ -72,6 +72,8 @@ public class TMLActivityDiagramToolBar extends TToolBar {
mgui.actions[TGUIAction.TMLAD_RANDOM].setEnabled(b);
mgui.actions[TGUIAction.TMLAD_EXECI].setEnabled(b);
mgui.actions[TGUIAction.TMLAD_EXECI_INTERVAL].setEnabled(b);
+ mgui.actions[TGUIAction.TMLAD_ENCRYPT].setEnabled(b);
+ mgui.actions[TGUIAction.TMLAD_DECRYPT].setEnabled(b);
mgui.actions[TGUIAction.TMLAD_EXECC].setEnabled(b);
mgui.actions[TGUIAction.TMLAD_EXECC_INTERVAL].setEnabled(b);
mgui.actions[TGUIAction.TMLAD_DELAY].setEnabled(b);
@@ -206,6 +208,13 @@ public class TMLActivityDiagramToolBar extends TToolBar {
this.addSeparator();
+
+ button = this.add(mgui.actions[TGUIAction.TMLAD_ENCRYPT]);
+ button.addMouseListener(mgui.mouseHandler);
+ button = this.add(mgui.actions[TGUIAction.TMLAD_DECRYPT]);
+ button.addMouseListener(mgui.mouseHandler);
+
+ this.addSeparator();
button = this.add(mgui.actions[TGUIAction.ACT_ENHANCE]);
button.addMouseListener(mgui.mouseHandler);
diff --git a/src/ui/tmlcompd/TMLCPrimitiveComponent.java b/src/ui/tmlcompd/TMLCPrimitiveComponent.java
index 69a5b5c9f2cfcc54fc86fd72d5d82ead44a3e9be..e81113bd61d0899399b84d4d00ea34f73119d17d 100755
--- a/src/ui/tmlcompd/TMLCPrimitiveComponent.java
+++ b/src/ui/tmlcompd/TMLCPrimitiveComponent.java
@@ -238,10 +238,10 @@ public class TMLCPrimitiveComponent extends TGCScalableWithInternalComponent imp
g.setFont(fold);
}
- public void drawVerification(Graphics g, int x, int y, int checkStatus){
+ public void drawVerification(Graphics g, int x, int y, int checkConfStatus){
Color c = g.getColor();
Color c1;
- switch(checkStatus) {
+ switch(checkConfStatus) {
case TAttribute.CONFIDENTIALITY_OK:
c1 = Color.green;
break;