diff --git a/src/main/java/tmltranslator/TMLModeling.java b/src/main/java/tmltranslator/TMLModeling.java
index 5f1ee08f75ff1b852e990c9eac1a5741954a1c86..3b5a0543f9bc37bbaf7ca0a3afe97a58c20dc885 100755
--- a/src/main/java/tmltranslator/TMLModeling.java
+++ b/src/main/java/tmltranslator/TMLModeling.java
@@ -900,22 +900,21 @@ public class TMLModeling<E> {
+ "__" + pragma.getAttrA().getAttribute().getName()
+ "__" + pragma.getAttrA().getState().getName();
- TraceManager.addDev("\n\n **Backtracing Authenticity s=" + s + " **");
- if (result.isProved() && !result.isSatisfied()) {
- TraceManager.addDev("Backtracing Authenticity proved but not satisfied");
- String signalName = s.toString().split("_chData")[0];
- signalName = signalName.split("__")[signalName.split("__").length - 1];
-
- TMLChannel channel = getChannelByShortName(signalName);
-
- if (channel == null) {
- channel = getChannelByDestinationPortName(signalName);
+ TraceManager.addDev("\n\n **Backtracing Authenticity s=" + s + " **");
+ if (result.isProved() && result.isSatisfied()) {
+ TraceManager.addDev("Backtracing Authenticity proved and satisfied" );
+ String signalName = s.split("_chData")[0];
+ for (TMLTask t : getTasks()) {
+ if (signalName.contains(t.getName())) {
+ signalName = signalName.replace(t.getName() + "__", "");
+ }
}
+ signalName = signalName.split("__")[1];
+ TMLChannel channel = getChannelByShortName(signalName);
if (channel != null) {
for (TMLPortWithSecurityInformation port : channel.ports) {
if (port.getCheckAuth()) {
- TraceManager.addDev("Backtracing Authenticity proved but not satisfied / Found port with checkAuth");
- port.setStrongAuthStatus(3);
+ port.setStrongAuthStatus(2);
port.setMappingName(mappingName);
ProVerifResultTrace trace = pvoa.getResults().get(pragma).getTrace();
if (trace != null && !port.isOrigin()) {
@@ -924,10 +923,8 @@ public class TMLModeling<E> {
}
}
}
- } else {
- TraceManager.addDev("Backtracing Authenticity proved but not satisfied / NULL channel");
}
- signalName = s.toString().split("_reqData")[0];
+ signalName = s.split("_reqData")[0];
for (TMLTask t : getTasks()) {
if (signalName.contains(t.getName())) {
signalName = signalName.replace(t.getName() + "__", "");
@@ -937,12 +934,12 @@ public class TMLModeling<E> {
if (req != null) {
for (TMLPortWithSecurityInformation port : req.ports) {
if (port.getCheckAuth()) {
- port.setStrongAuthStatus(3);
+ port.setStrongAuthStatus(2);
port.setMappingName(mappingName);
}
}
}
- signalName = s.toString().split("_eventData")[0];
+ signalName = s.split("_eventData")[0];
for (TMLTask t : getTasks()) {
if (signalName.contains(t.getName())) {
signalName = signalName.replace(t.getName() + "__", "");
@@ -951,26 +948,34 @@ public class TMLModeling<E> {
TMLEvent ev = getEventByName(signalName);
if (ev != null) {
if (ev.port.checkAuth) {
- ev.port.checkStrongAuthStatus = 3;
+ ev.port.checkStrongAuthStatus = 2;
ev.port2.mappingName = mappingName;
}
if (ev.port2.checkAuth) {
- ev.port2.checkStrongAuthStatus = 3;
+ ev.port2.checkStrongAuthStatus = 2;
ev.port2.mappingName = mappingName;
}
}
signalName = s.split("__decrypt")[0];
+
+ /*for (TMLTask t: getTasks()){
+ if (signalName.contains(t.getName())){
+ signalName = signalName.replace(t.getName()+"__","");
+ }
+ }*/
+ signalName = signalName.split("__")[1];
+ // TraceManager.addDev("secpattern " + signalName);
List<String> channels = secChannelMap.get(signalName);
+ // TraceManager.addDev("secpattern channels " + channels);
if (channels != null) {
for (String channelName : channels) {
channel = getChannelByShortName(channelName);
if (channel != null) {
- TraceManager.addDev("Security ports: " + channel.getSecurityPorts());
for (TMLPortWithSecurityInformation port : channel.ports) {
- if (port.getCheckAuth() && port.getCheckStrongAuthStatus() == 1) {
- port.setStrongAuthStatus(3);
- TraceManager.addDev("Backtracing Authenticity not verified " + signalName);
+ // TraceManager.addDev("adding to port " + channelName);
+ if (port.getCheckAuth()) {
+ port.setStrongAuthStatus(2);
port.setSecName(signalName);
ProVerifResultTrace trace = pvoa.getResults().get(pragma).getTrace();
if (trace != null && !port.isOrigin()) {
@@ -1001,7 +1006,7 @@ public class TMLModeling<E> {
if (channel != null) {
for (TMLPortWithSecurityInformation port : channel.ports) {
if (port.getCheckAuth()) {
- port.setWeakAuthStatus(3);
+ port.setStrongAuthStatus(2);
port.setSecName(signalName);
ProVerifResultTrace trace = pvoa.getResults().get(pragma).getTrace();
if (trace != null && !port.isOrigin()) {
@@ -1014,9 +1019,7 @@ public class TMLModeling<E> {
}
}
}
- }
-
- if (result.isWeakProved() && result.isWeakSatisfied()) {
+ } else if (result.isWeakProved() && result.isWeakSatisfied()) {
TraceManager.addDev("Backtracing Authenticity weak proved and weak satisfied");
String signalName = s.split("_chData")[0];
signalName = signalName.split("__")[1];
@@ -1090,6 +1093,7 @@ public class TMLModeling<E> {
TraceManager.addDev("Security ports (2): " + channel.getSecurityPorts());
for (TMLPortWithSecurityInformation port : channel.ports) {
if (port.getCheckAuth()) {
+ port.setStrongAuthStatus(3);
port.setWeakAuthStatus(2);
port.setSecName(signalName);
ProVerifResultTrace trace = pvoa.getResults().get(pragma).getTrace();
@@ -1136,22 +1140,21 @@ public class TMLModeling<E> {
}
}
}
- }
+ } else if (result.isProved() && !result.isSatisfied()) {
+ TraceManager.addDev("Backtracing Authenticity proved but not satisfied");
+ String signalName = s.toString().split("_chData")[0];
+ signalName = signalName.split("__")[signalName.split("__").length - 1];
- if (result.isProved() && result.isSatisfied()) {
- TraceManager.addDev("Backtracing Authenticity proved and satisfied" );
- String signalName = s.split("_chData")[0];
- for (TMLTask t : getTasks()) {
- if (signalName.contains(t.getName())) {
- signalName = signalName.replace(t.getName() + "__", "");
- }
- }
- signalName = signalName.split("__")[1];
TMLChannel channel = getChannelByShortName(signalName);
+
+ if (channel == null) {
+ channel = getChannelByDestinationPortName(signalName);
+ }
if (channel != null) {
for (TMLPortWithSecurityInformation port : channel.ports) {
if (port.getCheckAuth()) {
- port.setStrongAuthStatus(2);
+ TraceManager.addDev("Backtracing Authenticity proved but not satisfied / Found port with checkAuth");
+ port.setStrongAuthStatus(3);
port.setMappingName(mappingName);
ProVerifResultTrace trace = pvoa.getResults().get(pragma).getTrace();
if (trace != null && !port.isOrigin()) {
@@ -1160,8 +1163,10 @@ public class TMLModeling<E> {
}
}
}
+ } else {
+ TraceManager.addDev("Backtracing Authenticity proved but not satisfied / NULL channel");
}
- signalName = s.split("_reqData")[0];
+ signalName = s.toString().split("_reqData")[0];
for (TMLTask t : getTasks()) {
if (signalName.contains(t.getName())) {
signalName = signalName.replace(t.getName() + "__", "");
@@ -1171,12 +1176,12 @@ public class TMLModeling<E> {
if (req != null) {
for (TMLPortWithSecurityInformation port : req.ports) {
if (port.getCheckAuth()) {
- port.setStrongAuthStatus(2);
+ port.setStrongAuthStatus(3);
port.setMappingName(mappingName);
}
}
}
- signalName = s.split("_eventData")[0];
+ signalName = s.toString().split("_eventData")[0];
for (TMLTask t : getTasks()) {
if (signalName.contains(t.getName())) {
signalName = signalName.replace(t.getName() + "__", "");
@@ -1185,33 +1190,30 @@ public class TMLModeling<E> {
TMLEvent ev = getEventByName(signalName);
if (ev != null) {
if (ev.port.checkAuth) {
- ev.port.checkStrongAuthStatus = 2;
+ ev.port.checkStrongAuthStatus = 3;
ev.port2.mappingName = mappingName;
}
if (ev.port2.checkAuth) {
- ev.port2.checkStrongAuthStatus = 2;
+ ev.port2.checkStrongAuthStatus = 3;
ev.port2.mappingName = mappingName;
}
}
signalName = s.split("__decrypt")[0];
- /*for (TMLTask t: getTasks()){
- if (signalName.contains(t.getName())){
- signalName = signalName.replace(t.getName()+"__","");
- }
- }*/
signalName = signalName.split("__")[1];
- // TraceManager.addDev("secpattern " + signalName);
List<String> channels = secChannelMap.get(signalName);
- // TraceManager.addDev("secpattern channels " + channels);
+ for (Map.Entry<String, List<String>> entry : secChannelMap.entrySet()) {
+ System.out.println(entry.getKey() + ":" + entry.getValue());
+ }
+
if (channels != null) {
for (String channelName : channels) {
channel = getChannelByShortName(channelName);
if (channel != null) {
for (TMLPortWithSecurityInformation port : channel.ports) {
- // TraceManager.addDev("adding to port " + channelName);
if (port.getCheckAuth()) {
- port.setStrongAuthStatus(2);
+ port.setStrongAuthStatus(3);
+ TraceManager.addDev("Backtracing Authenticity not verified " + signalName);
port.setSecName(signalName);
ProVerifResultTrace trace = pvoa.getResults().get(pragma).getTrace();
if (trace != null && !port.isOrigin()) {
@@ -1221,7 +1223,6 @@ public class TMLModeling<E> {
}
}
}
-
}
}
@@ -1243,7 +1244,7 @@ public class TMLModeling<E> {
if (channel != null) {
for (TMLPortWithSecurityInformation port : channel.ports) {
if (port.getCheckAuth()) {
- port.setStrongAuthStatus(2);
+ port.setWeakAuthStatus(3);
port.setSecName(signalName);
ProVerifResultTrace trace = pvoa.getResults().get(pragma).getTrace();
if (trace != null && !port.isOrigin()) {
@@ -1257,7 +1258,6 @@ public class TMLModeling<E> {
}
}
}
-
}
}
diff --git a/src/main/java/tmltranslator/toavatarsec/TML2Avatar.java b/src/main/java/tmltranslator/toavatarsec/TML2Avatar.java
index ffb204dd30a100fe50d963779cf879a585b8bbec..a82338ad9ba97bcc97d99d7a5304e0133609a56e 100644
--- a/src/main/java/tmltranslator/toavatarsec/TML2Avatar.java
+++ b/src/main/java/tmltranslator/toavatarsec/TML2Avatar.java
@@ -1183,7 +1183,7 @@ public class TML2Avatar {
afterSignalState.addNext(tran);
elementList.add(afterSignalState);
elementList.add(tran);
- if (autoAuthChans) {
+ if (autoAuthChans || ae.securityPattern == null) {
if (block.getAvatarAttributeWithName(getName(ch.getName()) + "_chData") == null) {
AvatarAttribute channelData = new AvatarAttribute(getName(ch.getName()) + "_chData", AvatarType.INTEGER, block, null);
block.addAttribute(channelData);
@@ -1250,7 +1250,7 @@ public class TML2Avatar {
// To be removed in case another authenticity pragma is used on the channel
// Also, to be duplicated for each send / receive
if (ch.checkAuth) {
- if (autoAuthChans) {
+ if (autoAuthChans || ae.securityPattern == null) {
if (block.getAvatarAttributeWithName(getName(ch.getName()) + "_chData") == null) {
AvatarAttribute channelData = new AvatarAttribute(getName(ch.getName()) + "_chData", AvatarType.INTEGER, block, null);
block.addAttribute(channelData);
diff --git a/src/main/java/ui/SecurityGeneration.java b/src/main/java/ui/SecurityGeneration.java
index 600f3cb93c48f85ec99b47a397ab709772075b4f..017c0c5400696530f062bc86c7abba46eaff7e4b 100644
--- a/src/main/java/ui/SecurityGeneration.java
+++ b/src/main/java/ui/SecurityGeneration.java
@@ -824,22 +824,33 @@ public class SecurityGeneration implements Runnable {
tcdp.addComponent(conn, 0, 0, false, true);
List<TMLChannel> chans2 = tmlmodel.getChannelsFromMe(task2);
- for (TGComponent comps : newarch.tmlap.getComponentList()) {
- if (comps instanceof TMLArchiMemoryNode) {
- TMLArchiMemoryNode compMem = (TMLArchiMemoryNode) comps;
+ int count_chans = 0;
+ TMLArchiCommunicationArtifact newChannelInMem = null;
+ TMLArchiMemoryNode compMemToPutChannel = null;
+ for (TGComponent comp : newarch.tmlap.getComponentList()) {
+ if (comp instanceof TMLArchiMemoryNode) {
+ TMLArchiMemoryNode compMem = (TMLArchiMemoryNode) comp;
for (TMLArchiCommunicationArtifact channelAtif : compMem.getChannelArtifactList()) {
for (TMLChannel chan : chans2) {
- if (chan.getName().split("__")[1].equals(channelAtif.getCommunicationName())) {
- TMLArchiCommunicationArtifact newChannelInMem = new TMLArchiCommunicationArtifact(compMem.getX(), (int)(compMem.getY()+compMem.getHeight()*(0.3+Math.random()/2)), compMem.getCurrentMinX(), compMem.getCurrentMaxX(), compMem.getCurrentMinY(), compMem.getCurrentMaxY(), true, comps, newarch.tmlap);
- newChannelInMem.setReferenceCommunicationName(channelAtif.getReferenceCommunicationName());
- newChannelInMem.setCommunicationName(destPort.commName);
- newChannelInMem.setOtherCommunicationNames(channelAtif.getOtherCommunicationNames());
- compMem.addInternalComponent(newChannelInMem, compMem.getNbInternalTGComponent());
+ if (chan.isCheckAuthChannel()) {
+ if (chan.getName().split("__")[1].equals(channelAtif.getCommunicationName())) {
+ count_chans +=1;
+ if (count_chans==1) {
+ compMemToPutChannel = compMem;
+ newChannelInMem = new TMLArchiCommunicationArtifact(compMem.getX(), (int)(compMem.getY()+compMem.getHeight()*(0.3+Math.random()/2)), compMem.getCurrentMinX(), compMem.getCurrentMaxX(), compMem.getCurrentMinY(), compMem.getCurrentMaxY(), true, comp, newarch.tmlap);
+ newChannelInMem.setCommunicationName(destPort.commName);
+ newChannelInMem.setReferenceCommunicationName(channelAtif.getReferenceCommunicationName());
+ }
+ newChannelInMem.addNewOtherCommunicationNames(channelAtif.getOtherCommunicationNames());
+ }
}
}
}
}
}
+ if (count_chans>0){
+ compMemToPutChannel.addInternalComponent(newChannelInMem, compMemToPutChannel.getNbInternalTGComponent());
+ }
}
}
}
diff --git a/src/main/java/ui/tmldd/TMLArchiCommunicationArtifact.java b/src/main/java/ui/tmldd/TMLArchiCommunicationArtifact.java
index ea036c374bb44f649e4bfc395688a6d6b90d97d2..5d21063c9b673ee913abbea91ee14d334ccab28e 100755
--- a/src/main/java/ui/tmldd/TMLArchiCommunicationArtifact.java
+++ b/src/main/java/ui/tmldd/TMLArchiCommunicationArtifact.java
@@ -386,8 +386,12 @@ public class TMLArchiCommunicationArtifact extends TGCWithoutInternalComponent i
return mappedElements;
}
- public void setOtherCommunicationNames(ArrayList<String> _mappedElements) {
- mappedElements = _mappedElements;
+ public void addNewOtherCommunicationNames(ArrayList<String> _mappedElements) {
+ for(String mappedElem: _mappedElements){
+ if (!mappedElements.contains(mappedElem)){
+ mappedElements.add(mappedElem);
+ }
+ }
makeFullValue();
}