diff --git a/src/main/java/tmltranslator/TMLComparingMethod.java b/src/main/java/tmltranslator/TMLComparingMethod.java
index f6c1bbddaa2196060e72bb056ef77ec8e49f05e0..29f4c3154dbd3b8580f7e8e5ad756e82e93858cb 100644
--- a/src/main/java/tmltranslator/TMLComparingMethod.java
+++ b/src/main/java/tmltranslator/TMLComparingMethod.java
@@ -55,8 +55,8 @@ public class TMLComparingMethod {
list1 = new ArrayList<>(list1);
list2 = new ArrayList<>(list2);
- Collections.sort(list1, Comparator.comparing(TMLElement::getID));
- Collections.sort(list2, Comparator.comparing(TMLElement::getID));
+ Collections.sort(list1, Comparator.comparing(TMLElement::getName));
+ Collections.sort(list2, Comparator.comparing(TMLElement::getName));
boolean test;
@@ -192,9 +192,14 @@ public class TMLComparingMethod {
}
boolean test;
- for (SecurityPattern sp : map1.keySet()) {
- test = isHwMemoryListEquals(map1.get(sp), map2.get(sp));
- if (!test) return false;
+ for (SecurityPattern spMap1 : map1.keySet()) {
+ for (SecurityPattern spMap2 : map2.keySet()) {
+ if (spMap1.getName().equals(spMap2.getName())) {
+ test = isHwMemoryListEquals(map1.get(spMap1), map2.get(spMap2));
+ if (!test) return false;
+ break;
+ }
+ }
}
return true;
@@ -250,8 +255,22 @@ public class TMLComparingMethod {
boolean test;
- for (int i = 0; i < list1.size(); i++) {
- test = list1.get(i).equalSpec(list2.get(i));
+ for (TMLActivityElement tmlActivityElement : list1) {
+ test = tmlActivityElement.equalSpec(list2.get(0));
+ if (test) {
+ list2.remove(0);
+ } else if (list2.size() > 1) {
+ int comp = 1;
+ while (tmlActivityElement.getName().equals(list2.get(comp).getName())) {
+ test = tmlActivityElement.equalSpec(list2.get(comp));
+ if (test) {
+ list2.remove(comp);
+ break;
+ } else {
+ comp += 1;
+ }
+ }
+ }
if (!test) return false;
}
diff --git a/src/main/java/tmltranslator/TMLTextSpecification.java b/src/main/java/tmltranslator/TMLTextSpecification.java
index a7903cc125494afd77332b0699c5947ae159f4bc..ecc268ef908fb346170f516c46113d7938b2f2ca 100755
--- a/src/main/java/tmltranslator/TMLTextSpecification.java
+++ b/src/main/java/tmltranslator/TMLTextSpecification.java
@@ -2790,13 +2790,12 @@ public class TMLTextSpecification<E> {
if ((_split[10].compareTo("" + DECRYPTION_PROCESS) == 0) || (_split[10].compareTo("" + ENCRYPTION_PROCESS) == 0)) {
//Security operation
TraceManager.addDev("Found security pattern: " + _split[2]);
- TMLExecC execc = new TMLExecC("encrypt_" + _split[2], null);
+ TMLExecC execc = new TMLExecC(_split[2], null);
execc.setAction(_split[1]);
SecurityPattern sp = securityPatternMap.get(_split[2]);
execc.setSecurityPattern(sp);
if (_split[10].compareTo("" + DECRYPTION_PROCESS) == 0) {
execc.setDecryptionProcess(true);
- execc.setName("decrypt_" + _split[2]);
}
if (!tmlm.getSecurityTaskMap().containsKey(sp)) {
tmlm.getSecurityTaskMap().put(sp, new ArrayList<TMLTask>());
diff --git a/src/main/java/tmltranslator/patternhandling/PatternIntegration.java b/src/main/java/tmltranslator/patternhandling/PatternIntegration.java
index a5813c0478395e56327eb8562856a1b1c93483f2..2b26dba8fc744049977ac11a72c3553fab279313 100644
--- a/src/main/java/tmltranslator/patternhandling/PatternIntegration.java
+++ b/src/main/java/tmltranslator/patternhandling/PatternIntegration.java
@@ -1855,8 +1855,8 @@ public class PatternIntegration implements Runnable {
if (_appTabName != "") {
_tmapModel = putBackPrefixNames(_tmapModel, _appTabName);
- SecurityGenerationForTMAP secgen = new SecurityGenerationForTMAP(_appTabName, _tmapModel, "100", "0", "100", new HashMap<String,
- java.util.List<String>>(), false);
+ SecurityGenerationForTMAP secgen = new SecurityGenerationForTMAP(_appTabName, _tmapModel, "100", "0", "100", new ArrayList<>(),
+ false);
_tmapModel = secgen.startThread();
_tmapModel = secgen.autoMapKeys();
_tmapModel = removePrefixNames(_tmapModel);
diff --git a/src/main/java/tmltranslator/patternhandling/SecurityGenerationForTMAP.java b/src/main/java/tmltranslator/patternhandling/SecurityGenerationForTMAP.java
index 59b9d81e7199f90ab84ea4d3e5036a0165c64b26..46ef82b662cd127cb530651460ae5adf47ab941b 100644
--- a/src/main/java/tmltranslator/patternhandling/SecurityGenerationForTMAP.java
+++ b/src/main/java/tmltranslator/patternhandling/SecurityGenerationForTMAP.java
@@ -54,6 +54,7 @@ import avatartranslator.AvatarSpecification;
import avatartranslator.toproverif.AVATAR2ProVerif;
import common.ConfigurationTTool;
import launcher.RshClient;
+import myutil.FileUtils;
import myutil.TraceManager;
import org.apache.commons.math3.util.Pair;
import proverifspec.*;
@@ -73,7 +74,7 @@ public class SecurityGenerationForTMAP implements Runnable {
private final String encComp;
private final String overhead;
private final String decComp;
- private final Map<String, List<String>> selectedCPUTasks;
+ private final List<String> selectedTasks;
private final boolean linkedHSMs;
private final Map<TMLTask, List<TMLTask>> taskAndItsHSMMap = new HashMap<>();
@@ -89,13 +90,13 @@ public class SecurityGenerationForTMAP implements Runnable {
private final Map<Pair<TMLTask, TMLChannel>, TMLChannel> channelFromHsmMap = new HashMap<>();
public SecurityGenerationForTMAP(String appName, TMLMapping<?> tmap, String encComp, String overhead, String decComp,
- Map<String, List<String>> selectedCPUTasks, boolean isLinkedHSMs) {
+ List<String> selectedTasks, boolean isLinkedHSMs) {
this.appName = appName;
this.tmap = tmap;
this.overhead = overhead;
this.decComp = decComp;
this.encComp = encComp;
- this.selectedCPUTasks = selectedCPUTasks;
+ this.selectedTasks = selectedTasks;
this.linkedHSMs = isLinkedHSMs;
}
@@ -121,16 +122,14 @@ public class SecurityGenerationForTMAP implements Runnable {
AVATAR2ProVerif avatar2proverif = new AVATAR2ProVerif(avatarspec);
try {
- avatar2proverif.generateProVerif(true, true, 3, true, true);
- //warnings = avatar2proverif.getWarnings();
+ ProVerifSpec proverifSpec =avatar2proverif.generateProVerif(true, true, 3, true, true);
- if (!avatar2proverif.saveInFile("pvspec")) {
- return;
- }
+ FileUtils.saveFile(ConfigurationTTool.ProVerifCodeDirectory + "pvspec", proverifSpec.getStringSpec());
RshClient rshc = new RshClient(ConfigurationTTool.ProVerifVerifierHost);
- rshc.setCmd(ConfigurationTTool.ProVerifVerifierPath + " -in pitype pvspec");
+ rshc.setCmd(ConfigurationTTool.ProVerifVerifierPath + " -in pitype " + ConfigurationTTool.ProVerifCodeDirectory + "pvspec");
+ TraceManager.addDev(ConfigurationTTool.ProVerifVerifierPath + " -in pitype " + ConfigurationTTool.ProVerifCodeDirectory + "pvspec");
rshc.sendExecuteCommandRequest();
Reader data = rshc.getDataReaderFromProcess();
@@ -265,33 +264,18 @@ public class SecurityGenerationForTMAP implements Runnable {
proverifAnalysis(tmap, nonConfChans, nonWeakAuthChans, nonStrongAuthChans);
- for (String cpuName : selectedCPUTasks.keySet()) {
- for (String task : selectedCPUTasks.get(cpuName)) {
- String taskLongName = appName + "__" + task;
- initHSMArchDiagram(tmap.getTaskByName(taskLongName));
- }
+ for (String task : selectedTasks) {
+ String taskLongName = appName + "__" + task;
+ initHSMArchDiagram(tmap.getTaskByName(taskLongName));
}
- //ToSecure keeps a tmap of origin task: {dest task} for which security operators need to be added
- //ToSecureRev keeps a tmap of dest task: {origin task} for which security operators need to be added
-
- //SecOutChannels are channels which need symmetric encryption operators added
- //SecInChannels are channels which need sym decryption operators added
- //nonceInChannels are channels which need to send a nonce before receiving the channel data
- //nonceOutChannels are channels which need to receive a nonce before sending the channel data
- //macInChannels are channels which need verifymac operators added
- //macOutChannels are channels which need mac operators added
-
- //hsmSecInChannels need to send data to the hsm to decrypt after receiving channel data
- //hsmSecOutChannels need to send data to the hsm to encrypt before sending channel data
-
//With the proverif results, check which channels need to be secured
- HashSet<TMLChannel> chAddCSA = new HashSet<>();
- HashSet<TMLChannel> chAddCWA = new HashSet<>();
- HashSet<TMLChannel> chAddSA = new HashSet<>();
- HashSet<TMLChannel> chAddWA = new HashSet<>();
- HashSet<TMLChannel> chAddC = new HashSet<>();
+ LinkedHashSet<TMLChannel> chAddCSA = new LinkedHashSet<>();
+ LinkedHashSet<TMLChannel> chAddCWA = new LinkedHashSet<>();
+ LinkedHashSet<TMLChannel> chAddSA = new LinkedHashSet<>();
+ LinkedHashSet<TMLChannel> chAddWA = new LinkedHashSet<>();
+ LinkedHashSet<TMLChannel> chAddC = new LinkedHashSet<>();
for (TMLChannel chan : tmlmodel.getChannels()) {
boolean nonConf = nonConfChans.contains(chan);
@@ -319,7 +303,6 @@ public class SecurityGenerationForTMAP implements Runnable {
}
}
for (TMLChannel ch : chAddCSA) {
- //SecurityPattern spNonce = FindOrCreateNonceSecurityPattern(ch.getOriginTask(), ch.getDestinationTask());
SecurityPattern spNonce = findOrCreateNonceSecurityPattern(ch);
boolean nonceChannelExist = nonceChannelIsCreated(ch);
TMLChannel chNonce = findOrCreateNonceChannel(ch);
@@ -335,7 +318,7 @@ public class SecurityGenerationForTMAP implements Runnable {
encComp, decComp, spNonce.getName(), "", "");
handleSecurityGoalsForChannels(tmlmodel, ch, secPattern, !nonceChannelExist, spNonce, chNonce, linkedHSMs);
}
- HashSet<TMLChannel> chAddCAndCWA = new HashSet<>(chAddCWA);
+ LinkedHashSet<TMLChannel> chAddCAndCWA = new LinkedHashSet<>(chAddCWA);
chAddCAndCWA.addAll(chAddC);
for (TMLChannel ch : chAddCAndCWA) {
@@ -386,17 +369,6 @@ public class SecurityGenerationForTMAP implements Runnable {
for (TMLTask hsmTask : hsmTaskOperationMap.keySet()) {
buildHSMActivityDiagram(hsmTask, hsmTaskOperationMap.get(hsmTask));
TMLTask taskOfHSM = hsmTaskRequestMap.get(hsmTask).getOriginTasks().get(0);
-// for (TMLChannel ch : tmlmodel.getChannels(hsmTask)) {
-// boolean isMappedToMem = false;
-// for (HwCommunicationNode commNode : taskHSMCommunicationNodesMap.get(taskOfHSM)) {
-// if (!isMappedToMem || !(commNode instanceof HwMemory)) {
-// tmap.addCommToHwCommNode(ch, commNode);
-// }
-// if (commNode instanceof HwMemory) {
-// isMappedToMem = true;
-// }
-// }
-// }
updateHSMArchDiagram(hsmTask, taskAndHSMBusMap.get(taskOfHSM));
}
}
@@ -408,12 +380,12 @@ public class SecurityGenerationForTMAP implements Runnable {
List<TMLReadChannel> listRd = readOperatorsOfChannel(ch.getDestinationTask(), ch);
TMLTask hsmTaskForOriginTask = null;
TMLTask hsmTaskForDestinationTask = null;
- TMLChannel chToHSM = null;
- TMLChannel chFromHSM = null;
+ TMLChannel chToHSM;
+ TMLChannel chFromHSM;
TMLChannel chToDestinationHSM = null;
TMLChannel chFromOriginHSM = null;
- TMLChannel chSendNonceToHSM = null;
- TMLChannel chReceiveNonceFromHSM = null;
+ TMLChannel chSendNonceToHSM;
+ TMLChannel chReceiveNonceFromHSM;
if (taskAndItsHSMMap.containsKey(ch.getOriginTask())) {
hsmTaskForOriginTask = initHSMTaskDiagram(ch.getOriginTask(), "Encrypt_" + ch.getChannelName());
}
@@ -439,6 +411,7 @@ public class SecurityGenerationForTMAP implements Runnable {
chFromHSM = findOrCreateChannelFromHSM(hsmTaskForOriginTask, ch.getDestinationTask(), ch);
chFromHSM.checkConf = true;
chFromHSM.checkAuth = true;
+ chFromHSM.setDestinationTask(ch.getDestinationTask());
chFromOriginHSM = chFromHSM;
}
}
@@ -555,7 +528,7 @@ public class SecurityGenerationForTMAP implements Runnable {
}
try {
if (chFromOriginHSM != null) {
- addDecryptionADConnectedToOtherHSM(ch.getOriginTask(), listRd, secPattern, chFromOriginHSM);
+ addDecryptionADConnectedToOtherHSM(ch.getDestinationTask(), listRd, secPattern, chFromOriginHSM);
} else {
addDecryptionAD(ch.getDestinationTask(), listRd, secPattern);
}
@@ -585,102 +558,135 @@ public class SecurityGenerationForTMAP implements Runnable {
}
}
- private void mergeToCommNodeList(List<HwCommunicationNode> listCommNode, Map<TMLChannel, Set<HwCommunicationNode>> chCommNodesMap, TMLChannel ch) {
+ private void mergeBusToCommNodeList(List<HwCommunicationNode> listCommNode, Map<TMLChannel, Set<HwCommunicationNode>> chCommNodesMap,
+ TMLChannel ch) {
+ for (HwCommunicationNode commNode : listCommNode) {
+ if (!(commNode instanceof HwMemory)) {
+ chCommNodesMap.get(ch).add(commNode);
+ }
+ }
+ }
+
+ private void mergeMemoryToCommNodeList(List<HwCommunicationNode> listCommNode, Map<TMLChannel, Set<HwCommunicationNode>> chCommNodesMap,
+ TMLChannel ch) {
for (HwCommunicationNode commNode : listCommNode) {
- if (!(commNode instanceof HwMemory) || chCommNodesMap.get(ch).stream().noneMatch(c -> c instanceof HwMemory)) {
- TraceManager.addDev("add : " + commNode.getName() + " To : " + ch.getChannelName());
+ if ((commNode instanceof HwMemory) || chCommNodesMap.get(ch).stream().noneMatch(c -> c instanceof HwMemory)) {
chCommNodesMap.get(ch).add(commNode);
}
}
}
+ private HwBus getAssociatedBusOfTask(TMLTask task) {
+ HwExecutionNode execNode = tmap.getHwNodeOf(task);
+ for (HwLink link : tmap.getArch().getHwLinks()) {
+ if (link.hwnode == execNode) {
+ return link.bus;
+ }
+ }
+ return null;
+ }
+
+ private HwMemory getAssociatedMemoryOfBus(HwBus bus) {
+ for (HwLink link : tmap.getArch().getHwLinks()) {
+ if (link.bus == bus && link.hwnode instanceof HwMemory) {
+ return (HwMemory) link.hwnode;
+ }
+ }
+ return null;
+ }
+
private Map<TMLChannel, Set<HwCommunicationNode>> mapHSMChannelsInCommunicationNodes(TMLTask hsmTaskForOriginTask,
TMLTask hsmTaskForDestinationTask, TMLChannel ch) {
Map<TMLChannel, Set<HwCommunicationNode>> chCommNodesMap = new HashMap<>();
TMLModeling<?> tmlmodel = tmap.getTMLModeling();
if (hsmTaskForOriginTask != null) {
- TraceManager.addDev("hsmTaskForOriginTask = " + hsmTaskForOriginTask.getTaskName());
TMLTask taskOfHSM = hsmTaskRequestMap.get(hsmTaskForOriginTask).getOriginTasks().get(0);
for (TMLChannel chHSMOrigin : tmlmodel.getChannelsFromMe(hsmTaskForOriginTask)) {
if (!chCommNodesMap.containsKey(chHSMOrigin)) {
- chCommNodesMap.put(chHSMOrigin, new HashSet<>());
+ chCommNodesMap.put(chHSMOrigin, new LinkedHashSet<>());
}
if (taskHSMCommunicationNodesMap.containsKey(taskOfHSM)) {
- mergeToCommNodeList(taskHSMCommunicationNodesMap.get(taskOfHSM), chCommNodesMap, chHSMOrigin);
+ mergeBusToCommNodeList(taskHSMCommunicationNodesMap.get(taskOfHSM), chCommNodesMap, chHSMOrigin);
+ mergeMemoryToCommNodeList(taskHSMCommunicationNodesMap.get(taskOfHSM), chCommNodesMap, chHSMOrigin);
}
TMLTask corresTask = null;
if (hsmTaskRequestMap.containsKey(chHSMOrigin.getDestinationTask())) {
corresTask = hsmTaskRequestMap.get(chHSMOrigin.getDestinationTask()).getOriginTasks().get(0);
}
if (corresTask != null && taskHSMCommunicationNodesMap.containsKey(corresTask)) {
- mergeToCommNodeList(taskHSMCommunicationNodesMap.get(corresTask), chCommNodesMap, chHSMOrigin);
- mergeToCommNodeList(tmap.getAllCommunicationNodesOfChannel(ch), chCommNodesMap, chHSMOrigin);
- } else if (!chHSMOrigin.getDestinationTask().equals(ch.getOriginTask())) {
- mergeToCommNodeList(tmap.getAllCommunicationNodesOfChannel(ch), chCommNodesMap, chHSMOrigin);
+ mergeBusToCommNodeList(taskHSMCommunicationNodesMap.get(corresTask), chCommNodesMap, chHSMOrigin);
+ mergeBusToCommNodeList(tmap.getAllCommunicationNodesOfChannel(ch), chCommNodesMap, chHSMOrigin);
+ } else if (chHSMOrigin.getDestinationTask().equals(ch.getOriginTask())) {
+ chCommNodesMap.get(chHSMOrigin).add(getAssociatedBusOfTask(chHSMOrigin.getDestinationTask()));
+ } else {
+ mergeBusToCommNodeList(tmap.getAllCommunicationNodesOfChannel(ch), chCommNodesMap, chHSMOrigin);
}
}
for (TMLChannel chHSMOrigin : tmlmodel.getChannelsToMe(hsmTaskForOriginTask)) {
- TraceManager.addDev("chHSMOrigin = " + chHSMOrigin.getChannelName());
if (!chCommNodesMap.containsKey(chHSMOrigin)) {
- chCommNodesMap.put(chHSMOrigin, new HashSet<>());
+ chCommNodesMap.put(chHSMOrigin, new LinkedHashSet<>());
}
if (taskHSMCommunicationNodesMap.containsKey(taskOfHSM)) {
- TraceManager.addDev("containsKey(hsmTaskForOriginTask)");
- mergeToCommNodeList(taskHSMCommunicationNodesMap.get(taskOfHSM), chCommNodesMap, chHSMOrigin);
+ mergeBusToCommNodeList(taskHSMCommunicationNodesMap.get(taskOfHSM), chCommNodesMap, chHSMOrigin);
}
TMLTask corresTask = null;
if (hsmTaskRequestMap.containsKey(chHSMOrigin.getOriginTask())) {
corresTask = hsmTaskRequestMap.get(chHSMOrigin.getOriginTask()).getOriginTasks().get(0);
}
if (corresTask != null && taskHSMCommunicationNodesMap.containsKey(corresTask)) {
- TraceManager.addDev("containsKey(chHSMOrigin.getOriginTask()) = " + corresTask.getTaskName());
- mergeToCommNodeList(taskHSMCommunicationNodesMap.get(corresTask), chCommNodesMap, chHSMOrigin);
- mergeToCommNodeList(tmap.getAllCommunicationNodesOfChannel(ch), chCommNodesMap, chHSMOrigin);
- } else if (!chHSMOrigin.getOriginTask().equals(ch.getOriginTask())) {
- TraceManager.addDev("chHSMOrigin.getOriginTask() != ch.getOriginTask()");
- TraceManager.addDev("chHSMOrigin.getOriginTask() = " + chHSMOrigin.getOriginTask().getTaskName());
- TraceManager.addDev("ch.getOriginTask() = " + ch.getOriginTask().getTaskName());
- mergeToCommNodeList(tmap.getAllCommunicationNodesOfChannel(ch), chCommNodesMap, chHSMOrigin);
+ mergeBusToCommNodeList(taskHSMCommunicationNodesMap.get(corresTask), chCommNodesMap, chHSMOrigin);
+ mergeBusToCommNodeList(tmap.getAllCommunicationNodesOfChannel(ch), chCommNodesMap, chHSMOrigin);
+ } else if (chHSMOrigin.getOriginTask().equals(ch.getOriginTask())) {
+ mapChannelsInArch(chCommNodesMap, taskOfHSM, chHSMOrigin);
+ } else {
+ mergeBusToCommNodeList(tmap.getAllCommunicationNodesOfChannel(ch), chCommNodesMap, chHSMOrigin);
+ mapChannelsInArch(chCommNodesMap, taskOfHSM, chHSMOrigin);
}
}
}
if (hsmTaskForDestinationTask != null) {
- TMLTask taskOfHSM = hsmTaskRequestMap.get(hsmTaskForOriginTask).getOriginTasks().get(0);
+ TMLTask taskOfHSM = hsmTaskRequestMap.get(hsmTaskForDestinationTask).getOriginTasks().get(0);
for (TMLChannel chHSMDestination : tmlmodel.getChannelsFromMe(hsmTaskForDestinationTask)) {
if (!chCommNodesMap.containsKey(chHSMDestination)) {
- chCommNodesMap.put(chHSMDestination, new HashSet<>());
+ chCommNodesMap.put(chHSMDestination, new LinkedHashSet<>());
}
if (taskHSMCommunicationNodesMap.containsKey(taskOfHSM)) {
- mergeToCommNodeList(taskHSMCommunicationNodesMap.get(taskOfHSM), chCommNodesMap, chHSMDestination);
+ mergeBusToCommNodeList(taskHSMCommunicationNodesMap.get(taskOfHSM), chCommNodesMap, chHSMDestination);
+ mergeMemoryToCommNodeList(taskHSMCommunicationNodesMap.get(taskOfHSM), chCommNodesMap, chHSMDestination);
}
TMLTask corresTask = null;
if (hsmTaskRequestMap.containsKey(chHSMDestination.getDestinationTask())) {
corresTask = hsmTaskRequestMap.get(chHSMDestination.getDestinationTask()).getOriginTasks().get(0);
}
if (corresTask != null && taskHSMCommunicationNodesMap.containsKey(corresTask)) {
- mergeToCommNodeList(taskHSMCommunicationNodesMap.get(corresTask), chCommNodesMap, chHSMDestination);
- mergeToCommNodeList(tmap.getAllCommunicationNodesOfChannel(ch), chCommNodesMap, chHSMDestination);
- } else if (!chHSMDestination.getDestinationTask().equals(ch.getDestinationTask())) {
- mergeToCommNodeList(tmap.getAllCommunicationNodesOfChannel(ch), chCommNodesMap, chHSMDestination);
+ mergeBusToCommNodeList(taskHSMCommunicationNodesMap.get(corresTask), chCommNodesMap, chHSMDestination);
+ mergeBusToCommNodeList(tmap.getAllCommunicationNodesOfChannel(ch), chCommNodesMap, chHSMDestination);
+ } else if (chHSMDestination.getDestinationTask().equals(ch.getDestinationTask())) {
+ chCommNodesMap.get(chHSMDestination).add(getAssociatedBusOfTask(chHSMDestination.getDestinationTask()));
+ } else {
+ mergeBusToCommNodeList(tmap.getAllCommunicationNodesOfChannel(ch), chCommNodesMap, chHSMDestination);
}
}
for (TMLChannel chHSMDestination : tmlmodel.getChannelsToMe(hsmTaskForDestinationTask)) {
if (!chCommNodesMap.containsKey(chHSMDestination)) {
- chCommNodesMap.put(chHSMDestination, new HashSet<>());
+ chCommNodesMap.put(chHSMDestination, new LinkedHashSet<>());
}
if (taskHSMCommunicationNodesMap.containsKey(taskOfHSM)) {
- mergeToCommNodeList(taskHSMCommunicationNodesMap.get(taskOfHSM), chCommNodesMap, chHSMDestination);
+ mergeBusToCommNodeList(taskHSMCommunicationNodesMap.get(taskOfHSM), chCommNodesMap, chHSMDestination);
}
TMLTask corresTask = null;
if (hsmTaskRequestMap.containsKey(chHSMDestination.getOriginTask())) {
corresTask = hsmTaskRequestMap.get(chHSMDestination.getOriginTask()).getOriginTasks().get(0);
}
if (corresTask != null && taskHSMCommunicationNodesMap.containsKey(corresTask)) {
- mergeToCommNodeList(taskHSMCommunicationNodesMap.get(corresTask), chCommNodesMap, chHSMDestination);
- mergeToCommNodeList(tmap.getAllCommunicationNodesOfChannel(ch), chCommNodesMap, chHSMDestination);
- } else if (!chHSMDestination.getOriginTask().equals(ch.getDestinationTask())) {
- mergeToCommNodeList(tmap.getAllCommunicationNodesOfChannel(ch), chCommNodesMap, chHSMDestination);
+ mergeBusToCommNodeList(taskHSMCommunicationNodesMap.get(corresTask), chCommNodesMap, chHSMDestination);
+ mergeBusToCommNodeList(tmap.getAllCommunicationNodesOfChannel(ch), chCommNodesMap, chHSMDestination);
+ } else if (chHSMDestination.getOriginTask().equals(ch.getDestinationTask())) {
+ mapChannelsInArch(chCommNodesMap, taskOfHSM, chHSMDestination);
+ } else {
+ mergeBusToCommNodeList(tmap.getAllCommunicationNodesOfChannel(ch), chCommNodesMap, chHSMDestination);
+ mapChannelsInArch(chCommNodesMap, taskOfHSM, chHSMDestination);
}
}
}
@@ -688,6 +694,23 @@ public class SecurityGenerationForTMAP implements Runnable {
return chCommNodesMap;
}
+ private void mapChannelsInArch(Map<TMLChannel, Set<HwCommunicationNode>> chCommNodesMap, TMLTask taskOfHSM, TMLChannel chHSMDestination) {
+ List<HwCommunicationNode> listCommNode = new ArrayList<>();
+ HwBus bus = getAssociatedBusOfTask(chHSMDestination.getOriginTask());
+ if (bus != null) {
+ listCommNode.add(bus);
+ mergeBusToCommNodeList(listCommNode, chCommNodesMap, chHSMDestination);
+ HwMemory mem = getAssociatedMemoryOfBus(bus);
+ if (mem != null) {
+ listCommNode.clear();
+ listCommNode.add(mem);
+ mergeMemoryToCommNodeList(listCommNode, chCommNodesMap, chHSMDestination);
+ } else {
+ mergeMemoryToCommNodeList(taskHSMCommunicationNodesMap.get(taskOfHSM), chCommNodesMap, chHSMDestination);
+ }
+ }
+ }
+
private TMLTask initHSMTaskDiagram(TMLTask task, String nameHSM) {
String hsmTaskNameInit = appName + "__" + "HSM_" + task.getTaskName() + "_" + nameHSM;
int index = 0;
@@ -706,7 +729,7 @@ public class SecurityGenerationForTMAP implements Runnable {
}
}
- String hsmRequestNameInit = "req_" + hsm.getTaskName();
+ String hsmRequestNameInit = appName + "__" + "req_" + hsm.getTaskName();
int indexRequest = 0;
String hsmRequestName = hsmRequestNameInit;
while (tmap.getTMLModeling().getRequestByName(hsmRequestName) != null) {
@@ -717,6 +740,7 @@ public class SecurityGenerationForTMAP implements Runnable {
request.addOriginTask(task);
request.setDestinationTask(hsm);
hsm.setRequest(request);
+ hsm.setRequested(true);
//task.setRequest(request);
// request.addParam(new TMLType(TMLType.NATURAL));
tmap.getTMLModeling().addRequest(request);
@@ -813,7 +837,7 @@ public class SecurityGenerationForTMAP implements Runnable {
private TMLActivityElement addBranchHSM(TMLTask hsmTask, TMLChannel dataCh, TMLChannel retrieveDataCh, SecurityPattern sp,
boolean isEncryption) throws TMLCheckingError {
TMLActivity hsmTaskAD = hsmTask.getActivityDiagram();
- TMLReadChannel rd = new TMLReadChannel(dataCh.getChannelName(), hsmTaskAD.getReferenceObject());
+ TMLReadChannel rd = new TMLReadChannel(dataCh.getName(), hsmTaskAD.getReferenceObject());
rd.addChannel(dataCh);
rd.setNbOfSamples("1");
if (!isEncryption) {
@@ -828,7 +852,7 @@ public class SecurityGenerationForTMAP implements Runnable {
hsmTaskAD.addElement(exec);
rd.addNext(exec);
- TMLWriteChannel wr = new TMLWriteChannel(retrieveDataCh.getChannelName(), hsmTaskAD.getReferenceObject());
+ TMLWriteChannel wr = new TMLWriteChannel(retrieveDataCh.getName(), hsmTaskAD.getReferenceObject());
wr.addChannel(retrieveDataCh);
hsmTaskAD.addElement(wr);
wr.setNbOfSamples("1");
@@ -849,7 +873,7 @@ public class SecurityGenerationForTMAP implements Runnable {
boolean isEncryption, TMLActivityElement header, TMLActivityElement bottom) throws TMLCheckingError {
TMLActivity hsmTaskAD = hsmTask.getActivityDiagram();
- TMLReadChannel rd = new TMLReadChannel(dataCh.getChannelName(), hsmTaskAD.getReferenceObject());
+ TMLReadChannel rd = new TMLReadChannel(dataCh.getName(), hsmTaskAD.getReferenceObject());
rd.addChannel(dataCh);
rd.setNbOfSamples("1");
if (!isEncryption) {
@@ -865,7 +889,7 @@ public class SecurityGenerationForTMAP implements Runnable {
hsmTaskAD.addElement(exec);
rd.addNext(exec);
- TMLWriteChannel wr = new TMLWriteChannel(retrieveDataCh.getChannelName(), hsmTaskAD.getReferenceObject());
+ TMLWriteChannel wr = new TMLWriteChannel(retrieveDataCh.getName(), hsmTaskAD.getReferenceObject());
wr.addChannel(retrieveDataCh);
hsmTaskAD.addElement(wr);
wr.setNbOfSamples("1");
@@ -891,7 +915,7 @@ public class SecurityGenerationForTMAP implements Runnable {
exec.setAction(Integer.toString(sp.getEncTime()));
hsmTaskAD.addElement(exec);
- TMLWriteChannel wr = new TMLWriteChannel(nonceCh.getChannelName(), hsmTaskAD.getReferenceObject());
+ TMLWriteChannel wr = new TMLWriteChannel(nonceCh.getName(), hsmTaskAD.getReferenceObject());
wr.addChannel(nonceCh);
hsmTaskAD.addElement(wr);
wr.setNbOfSamples("1");
@@ -900,7 +924,7 @@ public class SecurityGenerationForTMAP implements Runnable {
return new Pair<>(exec, wr);
} else {
- TMLReadChannel rd = new TMLReadChannel(nonceCh.getChannelName(), hsmTaskAD.getReferenceObject());
+ TMLReadChannel rd = new TMLReadChannel(nonceCh.getName(), hsmTaskAD.getReferenceObject());
rd.addChannel(nonceCh);
rd.setSecurityPattern(sp);
rd.setNbOfSamples("1");
@@ -918,12 +942,12 @@ public class SecurityGenerationForTMAP implements Runnable {
//reqSend.addParam(Integer.toString(indexRequest));
taskAD.addElement(reqSend);
- TMLWriteChannel wr = new TMLWriteChannel(dataCh.getChannelName(), taskAD.getReferenceObject());
+ TMLWriteChannel wr = new TMLWriteChannel(dataCh.getName(), taskAD.getReferenceObject());
wr.addChannel(dataCh);
wr.setNbOfSamples(comm.getNbOfSamples());
taskAD.addElement(wr);
- TMLReadChannel rd = new TMLReadChannel(retrieveDataCh.getChannelName(), taskAD.getReferenceObject());
+ TMLReadChannel rd = new TMLReadChannel(retrieveDataCh.getName(), taskAD.getReferenceObject());
rd.addChannel(retrieveDataCh);
rd.setNbOfSamples(comm.getNbOfSamples());
taskAD.addElement(rd);
@@ -933,13 +957,13 @@ public class SecurityGenerationForTMAP implements Runnable {
comm.setSecurityPattern(sp);
if (comm instanceof TMLWriteChannel) {
- TMLWriteChannel wrNonceToHSM = new TMLWriteChannel(chNonceWithHSM.getChannelName(), taskAD.getReferenceObject());
+ TMLWriteChannel wrNonceToHSM = new TMLWriteChannel(chNonceWithHSM.getName(), taskAD.getReferenceObject());
wrNonceToHSM.addChannel(chNonceWithHSM);
wrNonceToHSM.setNbOfSamples("1");
wrNonceToHSM.setSecurityPattern(spNonce);
taskAD.addElement(wrNonceToHSM);
- TMLReadChannel rdNonce = new TMLReadChannel(chNonce.getChannelName(), taskAD.getReferenceObject());
+ TMLReadChannel rdNonce = new TMLReadChannel(chNonce.getName(), taskAD.getReferenceObject());
rdNonce.addChannel(chNonce);
rdNonce.setNbOfSamples("1");
rdNonce.setSecurityPattern(spNonce);
@@ -955,13 +979,13 @@ public class SecurityGenerationForTMAP implements Runnable {
rd.addNext(comm);
} else if (comm instanceof TMLReadChannel) {
- TMLReadChannel rdNonceFromHSM = new TMLReadChannel(chNonceWithHSM.getChannelName(), taskAD.getReferenceObject());
+ TMLReadChannel rdNonceFromHSM = new TMLReadChannel(chNonceWithHSM.getName(), taskAD.getReferenceObject());
rdNonceFromHSM.addChannel(chNonceWithHSM);
rdNonceFromHSM.setNbOfSamples("1");
rdNonceFromHSM.setSecurityPattern(spNonce);
taskAD.addElement(rdNonceFromHSM);
- TMLWriteChannel wrNonce = new TMLWriteChannel(chNonce.getChannelName(), taskAD.getReferenceObject());
+ TMLWriteChannel wrNonce = new TMLWriteChannel(chNonce.getName(), taskAD.getReferenceObject());
wrNonce.addChannel(chNonce);
wrNonce.setNbOfSamples("1");
wrNonce.setSecurityPattern(spNonce);
@@ -989,12 +1013,12 @@ public class SecurityGenerationForTMAP implements Runnable {
//reqSend.addParam(Integer.toString(indexRequest));
taskAD.addElement(reqSend);
- TMLWriteChannel wr = new TMLWriteChannel(dataCh.getChannelName(), taskAD.getReferenceObject());
+ TMLWriteChannel wr = new TMLWriteChannel(dataCh.getName(), taskAD.getReferenceObject());
wr.addChannel(dataCh);
wr.setNbOfSamples(comm.getNbOfSamples());
taskAD.addElement(wr);
- TMLReadChannel rd = new TMLReadChannel(retrieveDataCh.getChannelName(), taskAD.getReferenceObject());
+ TMLReadChannel rd = new TMLReadChannel(retrieveDataCh.getName(), taskAD.getReferenceObject());
rd.addChannel(retrieveDataCh);
rd.setNbOfSamples(comm.getNbOfSamples());
taskAD.addElement(rd);
@@ -1029,7 +1053,7 @@ public class SecurityGenerationForTMAP implements Runnable {
TMLActivityElement origNextComm = comm.getNextElement(0);
if (comm instanceof TMLWriteChannel) {
- TMLWriteChannel wr = new TMLWriteChannel(dataCh.getChannelName(), taskAD.getReferenceObject());
+ TMLWriteChannel wr = new TMLWriteChannel(dataCh.getName(), taskAD.getReferenceObject());
wr.addChannel(dataCh);
wr.setNbOfSamples(comm.getNbOfSamples());
taskAD.addElement(wr);
@@ -1038,7 +1062,7 @@ public class SecurityGenerationForTMAP implements Runnable {
taskAD.removeElement(comm);
wr.addNext(origNextComm);
} else if (comm instanceof TMLReadChannel) {
- TMLReadChannel rd = new TMLReadChannel(dataCh.getChannelName(), taskAD.getReferenceObject());
+ TMLReadChannel rd = new TMLReadChannel(dataCh.getName(), taskAD.getReferenceObject());
rd.addChannel(dataCh);
rd.setNbOfSamples(comm.getNbOfSamples());
taskAD.addElement(rd);
@@ -1076,7 +1100,7 @@ public class SecurityGenerationForTMAP implements Runnable {
taskAD.addElement(exec);
readComm.replaceChannelWith(readComm.getChannel(0), chToDestHSM);
-
+ readComm.setName(chToDestHSM.getName());
readComm.setSecurityPattern(sp);
TMLActivityElement origNextComm = readComm.getNextElement(0);
readComm.setNewNext(origNextComm, exec);
@@ -1093,7 +1117,7 @@ public class SecurityGenerationForTMAP implements Runnable {
exec.setAction(Integer.toString(spNonce.getEncTime()));
taskAD.addElement(exec);
for (TMLReadChannel readComm : readComms) {
- TMLWriteChannel wrNonce = new TMLWriteChannel(nonceCh.getChannelName(), taskAD.getReferenceObject());
+ TMLWriteChannel wrNonce = new TMLWriteChannel(nonceCh.getName(), taskAD.getReferenceObject());
wrNonce.addChannel(nonceCh);
wrNonce.setNbOfSamples("1");
wrNonce.setSecurityPattern(spNonce);
@@ -1113,7 +1137,7 @@ public class SecurityGenerationForTMAP implements Runnable {
headerElement.setNewNext(origNextComm, exec);
exec.addNext(origNextComm);
} else {
- TMLWriteChannel wrNonce = new TMLWriteChannel(nonceCh.getChannelName(), taskAD.getReferenceObject());
+ TMLWriteChannel wrNonce = new TMLWriteChannel(nonceCh.getName(), taskAD.getReferenceObject());
wrNonce.addChannel(nonceCh);
wrNonce.setNbOfSamples("1");
wrNonce.setSecurityPattern(spNonce);
@@ -1133,7 +1157,7 @@ public class SecurityGenerationForTMAP implements Runnable {
TMLActivityElement headerElement) {
TMLActivity taskAD = task.getActivityDiagram();
for(TMLWriteChannel writeCh : writeComms) {
- TMLReadChannel rdNonce = new TMLReadChannel(nonceCh.getChannelName(), taskAD.getReferenceObject());
+ TMLReadChannel rdNonce = new TMLReadChannel(nonceCh.getName(), taskAD.getReferenceObject());
rdNonce.addChannel(nonceCh);
rdNonce.setNbOfSamples("1");
rdNonce.setSecurityPattern(spNonce);
@@ -1143,7 +1167,7 @@ public class SecurityGenerationForTMAP implements Runnable {
rdNonce.addNext(writeCh);
}
if (writeComms.size() > 1) {
- TMLReadChannel rdNonce = new TMLReadChannel(nonceCh.getChannelName(), taskAD.getReferenceObject());
+ TMLReadChannel rdNonce = new TMLReadChannel(nonceCh.getName(), taskAD.getReferenceObject());
rdNonce.addChannel(nonceCh);
rdNonce.setNbOfSamples("1");
rdNonce.setSecurityPattern(spNonce);
@@ -1189,6 +1213,7 @@ public class SecurityGenerationForTMAP implements Runnable {
taskAD.addElement(exec);
if (writeComms.size() == 1) {
writeComms.get(0).replaceChannelWith(writeComms.get(0).getChannel(0), chToDestHSM);
+ writeComms.get(0).setName(chToDestHSM.getName());
TMLActivityElement prevOfWrite = taskAD.getPrevious(writeComms.get(0));
prevOfWrite.setNewNext(writeComms.get(0), exec);
exec.addNext(writeComms.get(0));
@@ -1199,6 +1224,7 @@ public class SecurityGenerationForTMAP implements Runnable {
exec.addNext(origNextHeader);
for (TMLWriteChannel writeComm : writeComms) {
writeComm.replaceChannelWith(writeComm.getChannel(0), chToDestHSM);
+ writeComm.setName(chToDestHSM.getName());
writeComm.setSecurityPattern(sp);
}
}
@@ -1255,7 +1281,8 @@ public class SecurityGenerationForTMAP implements Runnable {
return channelTochannelNonceMap.get(ch);
}
- String channelNameInit = "nonceCh" + ch.getDestinationTask().getTaskName() + "_" + ch.getOriginTask().getTaskName() + "_" + ch.getChannelName();
+ String channelNameInit =
+ appName + "__" + "nonceCh" + ch.getDestinationTask().getTaskName() + "_" + ch.getOriginTask().getTaskName() + "_" + ch.getChannelName();
int index = 0;
String channelName = channelNameInit;
while (tmap.getChannelByName(channelName) != null) {
@@ -1279,7 +1306,7 @@ public class SecurityGenerationForTMAP implements Runnable {
}
TMLTask originTaskOfNonce = chNonce.getOriginTask();
TMLTask destinationTaskOfNonce = chNonce.getDestinationTask();
- String channelNameHSMInit = "dataNonceCh" + destinationTaskOfNonce.getTaskName() + "_" + originTaskOfNonce.getTaskName();
+ String channelNameHSMInit = appName + "__" + "dataNonceCh" + destinationTaskOfNonce.getTaskName() + "_" + originTaskOfNonce.getTaskName();
int indexHSM = 0;
String channelNameHSM = channelNameHSMInit;
while (tmap.getChannelByName(channelNameHSM) != null) {
@@ -1302,7 +1329,7 @@ public class SecurityGenerationForTMAP implements Runnable {
}
TMLTask originTaskOfNonce = chNonce.getOriginTask(); ;
TMLTask destinationTaskOfNonce = chNonce.getDestinationTask();
- String channelNameHSMInit = "retDataNonceCh" + destinationTaskOfNonce.getTaskName() + "_" + originTaskOfNonce.getTaskName();
+ String channelNameHSMInit = appName + "__" + "retDataNonceCh" + destinationTaskOfNonce.getTaskName() + "_" + originTaskOfNonce.getTaskName();
int indexHSM = 0;
String channelNameHSM = channelNameHSMInit;
while (tmap.getChannelByName(channelNameHSM) != null) {
@@ -1325,7 +1352,7 @@ public class SecurityGenerationForTMAP implements Runnable {
if (channelToHsmMap.containsKey(taskChannelPair)) {
return channelToHsmMap.get(taskChannelPair);
}
- String channelNameHSMInit = "dataCh_" + task.getTaskName() + "_" + ch.getChannelName();
+ String channelNameHSMInit = appName + "__" + "dataCh_" + task.getTaskName() + "_" + ch.getChannelName();
int indexHSM = 0;
String channelNameHSM = channelNameHSMInit;
while (tmap.getChannelByName(channelNameHSM) != null) {
@@ -1348,7 +1375,7 @@ public class SecurityGenerationForTMAP implements Runnable {
if (channelFromHsmMap.containsKey(taskChannelPair)) {
return channelFromHsmMap.get(taskChannelPair);
}
- String channelNameHSMInit = "retDataCh_" + task.getTaskName() + "_" + ch.getChannelName();
+ String channelNameHSMInit = appName + "__" + "retDataCh_" + task.getTaskName() + "_" + ch.getChannelName();
int indexHSM = 0;
String channelNameHSM = channelNameHSMInit;
while (tmap.getChannelByName(channelNameHSM) != null) {
diff --git a/src/main/java/ui/GTURTLEModeling.java b/src/main/java/ui/GTURTLEModeling.java
index 31c433f3b33aa83f03263006339a821f5137e754..478a8a618c6f3e64a55e82342f47af11cc8aa770 100644
--- a/src/main/java/ui/GTURTLEModeling.java
+++ b/src/main/java/ui/GTURTLEModeling.java
@@ -1788,7 +1788,7 @@ public class GTURTLEModeling {
@SuppressWarnings("unchecked")
public void autoSecure(MainGUI gui, String encComp, String overhead, String decComp, Vector<String> channelsToAddSec,
- Map<String, List<String>> selectedCpuTasks, boolean isLinkedHsm) {
+ List<String> selectedCpuTasks, boolean isLinkedHsm) {
if (tmap == null) {
return;
}
diff --git a/src/main/java/ui/tmldd/TMLArchiCommunicationArtifact.java b/src/main/java/ui/tmldd/TMLArchiCommunicationArtifact.java
index e913f9f1c536fa6c36edbfd57dd5e94d220319e1..024ef4ee6a8c69bc2205d2335d256fec517e19bf 100755
--- a/src/main/java/ui/tmldd/TMLArchiCommunicationArtifact.java
+++ b/src/main/java/ui/tmldd/TMLArchiCommunicationArtifact.java
@@ -73,7 +73,7 @@ public class TMLArchiCommunicationArtifact extends TGCWithoutInternalComponent i
protected String referenceCommunicationName = "TMLCommunication";
protected String communicationName = "name";
protected String typeName = "channel";
- protected int priority = 5; // Between 0 and 10
+ protected int priority = 0; // Between 0 and 10
protected ArrayList<String> mappedElements = new ArrayList<>();
public TMLArchiCommunicationArtifact(int _x, int _y, int _minX, int _maxX, int _minY, int _maxY, boolean _pos, TGComponent _father,
diff --git a/src/main/java/ui/tmldd/TMLArchiEventArtifact.java b/src/main/java/ui/tmldd/TMLArchiEventArtifact.java
index 4ca1529387d58a4c5b0e81e6986b13a294f13f54..c052fbe474cb533b57a72793f7639e3ebcceedf0 100755
--- a/src/main/java/ui/tmldd/TMLArchiEventArtifact.java
+++ b/src/main/java/ui/tmldd/TMLArchiEventArtifact.java
@@ -69,7 +69,7 @@ public class TMLArchiEventArtifact extends TGCWithoutInternalComponent implement
protected String referenceEventName = "TMLEvent";
protected String eventName = "name";
protected String typeName = "event";
- protected int priority = 5; // Between 0 and 10
+ protected int priority = 0; // Between 0 and 10
public TMLArchiEventArtifact(
int _x, int _y, int _minX, int _maxX, int _minY, int _maxY, boolean _pos, TGComponent _father, TDiagramPanel _tdp) {
diff --git a/src/main/java/ui/tmldd/TMLArchiKey.java b/src/main/java/ui/tmldd/TMLArchiKey.java
index df0b12822cbd74551d1eb9b997a6559ac6144244..66304079015e697e73d805efe4d4d882267450d3 100755
--- a/src/main/java/ui/tmldd/TMLArchiKey.java
+++ b/src/main/java/ui/tmldd/TMLArchiKey.java
@@ -74,7 +74,7 @@ public class TMLArchiKey extends TGCWithoutInternalComponent implements Swallowe
protected String oldValue = "";
protected String referenceKey = "TMLKey";
protected String typeName = "key";
- protected int priority = 5; // Between 0 and 10
+ protected int priority = 0; // Between 0 and 10
public TMLArchiKey(int _x, int _y, int _minX, int _maxX, int _minY, int _maxY, boolean _pos, TGComponent _father, TDiagramPanel _tdp) {
super(_x, _y, _minX, _maxX, _minY, _maxY, _pos, _father, _tdp);
diff --git a/src/main/java/ui/tmldd/TMLArchiPortArtifact.java b/src/main/java/ui/tmldd/TMLArchiPortArtifact.java
index ecc0ba86a43063bd2bcae768223819fea1e9560c..b7d0d73292b3ef17913b5aab758938c15a07b3ed 100644
--- a/src/main/java/ui/tmldd/TMLArchiPortArtifact.java
+++ b/src/main/java/ui/tmldd/TMLArchiPortArtifact.java
@@ -104,7 +104,7 @@ public class TMLArchiPortArtifact extends TGCWithoutInternalComponent implements
protected String endAddress = "";
protected List<String> bufferParameters = new ArrayList<String>();
protected String bufferType = "noBuffer";
- protected int priority = 5; // Between 0 and 10
+ protected int priority = 0; // Between 0 and 10
public TMLArchiPortArtifact(int _x, int _y, int _minX, int _maxX, int _minY, int _maxY, boolean _pos, TGComponent _father, TDiagramPanel _tdp) {
super(_x, _y, _minX, _maxX, _minY, _maxY, _pos, _father, _tdp);
diff --git a/src/main/java/ui/window/JDialogProverifVerification.java b/src/main/java/ui/window/JDialogProverifVerification.java
index 8e32b33d45cab8f30fe386227a5665bbf96fe07c..44b731c08c92fa23d941dd766f52d4eb5aeb33a6 100644
--- a/src/main/java/ui/window/JDialogProverifVerification.java
+++ b/src/main/java/ui/window/JDialogProverifVerification.java
@@ -57,7 +57,6 @@ import java.io.InputStreamReader;
import java.io.OutputStreamWriter;
import java.io.PipedInputStream;
import java.io.PipedOutputStream;
-import java.util.ArrayList;
import java.util.Arrays;
import java.util.Collection;
import java.util.Collections;
@@ -87,7 +86,6 @@ import proverifspec.ProVerifOutputListener;
import proverifspec.ProVerifQueryAuthResult;
import proverifspec.ProVerifQueryResult;
import proverifspec.ProVerifResultTraceStep;
-import tmltranslator.TMLMapping;
import ui.*;
import ui.interactivesimulation.JFrameSimulationSDPanel;
import ui.util.IconManager;
@@ -125,8 +123,6 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
private static boolean DRAW_AVATAR = false;
- private JLabel labelError;
-
protected MainGUI mgui;
private AvatarDesignPanel adp;
@@ -1574,7 +1570,6 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
public void run() {
TraceManager.addDev("Thread started");
File testFile;
- Map<String, List<String>> selectedCpuTasks = new HashMap<String, java.util.List<String>>();
int currentPosY = 0;
int stepY = 10;
if (jp1.getSelectedIndex() == 2) {
@@ -1700,31 +1695,8 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
encCC = encTime.getText();
decCC = decTime.getText();
secOv = secOverhead.getText();
- TMLMapping map;
- if (addHSM.isSelected() && selectedTasks.size()>0) {
-
-
- for (String task : selectedTasks) {
- String cpu = taskCpuMap.get(task);
- if (selectedCpuTasks.containsKey(cpu)) {
- selectedCpuTasks.get(cpu).add(task);
- } else {
- ArrayList<String> tasks = new ArrayList<String>();
- tasks.add(task);
- selectedCpuTasks.put(cpu, tasks);
- }
- }
- //mgui.gtm.addHSM(mgui, selectedCpuTasks);
- }
if (autoConf.isSelected() || autoWeakAuth.isSelected() || autoStrongAuth.isSelected()) {
- /*if (custom.isSelected()) {
- map = mgui.gtm.autoSecure(mgui, encCC, secOv, decCC, autoConf.isSelected(), autoWeakAuth.isSelected(),
- autoStrongAuth.isSelected(), selectedCpuTasks);
- } else {
- map = mgui.gtm.autoSecure(mgui, "100", "0", "100", autoConf.isSelected(),
- autoWeakAuth.isSelected(), autoStrongAuth.isSelected(), selectedCpuTasks);
- }*/
- mgui.gtm.autoSecure(mgui, encCC, secOv, decCC, selectedChannelsToAddSec, selectedCpuTasks, linkHSMs.isSelected());
+ mgui.gtm.autoSecure(mgui, encCC, secOv, decCC, selectedChannelsToAddSec, selectedTasks, linkHSMs.isSelected());
}
}
else if (autoMapKeys.isSelected()) {