diff --git a/ttool/src/test/java/pragmasmodel/AliceAndBobPragmasTest.java b/ttool/src/test/java/pragmasmodel/AliceAndBobPragmasTest.java
deleted file mode 100644
index 8b85ed7df0896607242415be2bb7764fa25266d0..0000000000000000000000000000000000000000
--- a/ttool/src/test/java/pragmasmodel/AliceAndBobPragmasTest.java
+++ /dev/null
@@ -1,81 +0,0 @@
-package pragmasmodel;
-
-import myutil.FileException;
-import myutil.FileUtils;
-import myutil.TraceManager;
-import org.junit.Assert;
-import org.junit.Before;
-import org.junit.BeforeClass;
-import org.junit.Test;
-
-import java.util.ArrayList;
-import java.util.Arrays;
-import java.util.HashMap;
-
-public class AliceAndBobPragmasTest {
-
- private static AvatarNetworkProjectPragmaTests parent;
-
- private static HashMap<String, String[]> goldenList;
-
- private static ArrayList<String> resultsToBeChecked;
-
- private static final ArrayList<String> tabbedPanes = new ArrayList<>(Arrays.asList("SymExchangeArch"));;
-
- private static int currentIdxTabbedPane = -1;
-
-
- @BeforeClass
- public static void setUp() {
- parent = new AvatarNetworkProjectPragmaTests();
- parent.setProjectName("AliceAndBobHW");
- goldenList = new HashMap<String, String[]>();
- resultsToBeChecked = new ArrayList<>();
-
- }
-
- @BeforeClass
- public static void setUpGolden() throws FileException {
-
- String path = "test/resources/pragmasmodel/AliceAndBobHW/";
-
- for (String tabbedPane : tabbedPanes){
-
- TraceManager.addDev("tabbedPane : " + tabbedPane);
- String fileContent = FileUtils.loadFile(path + tabbedPane + "/golden");
-
- goldenList.put(tabbedPane,fileContent.split("\n"));
-
- }
-
- }
-
- @Before
- public void switchTabbedPane() throws Exception {
- //no index out of bounds because runs x times if x @Test. x Must be same length as tabbedPanes.size()
- currentIdxTabbedPane+=1;
-
- parent.buildPvspec(tabbedPanes.get(currentIdxTabbedPane));
- parent.runProverif();
-
- resultsToBeChecked = parent.getResultsToBeChecked();
-
- }
-
- @Test
- public void testPragmaResult_1(){
- iterateOverArrayList(tabbedPanes.get(currentIdxTabbedPane));
- }
-
-
- public void iterateOverArrayList(String key){
- String[] golden = goldenList.get(key);
-
- Assert.assertEquals(golden.length, resultsToBeChecked.size());
-
- for (int i = 0; i < golden.length; i++) {
- Assert.assertEquals(golden[i],resultsToBeChecked.get(i));
- }
-
- }
-}
diff --git a/ttool/src/test/java/pragmasmodel/AvatarNetworkProjectPragmaTests.java b/ttool/src/test/java/pragmasmodel/AvatarNetworkProjectPragmaTests.java
deleted file mode 100644
index 5c97666e122b10568891b7c7e1458ddaae1de356..0000000000000000000000000000000000000000
--- a/ttool/src/test/java/pragmasmodel/AvatarNetworkProjectPragmaTests.java
+++ /dev/null
@@ -1,153 +0,0 @@
-package pragmasmodel;
-
-import avatartranslator.AvatarSpecification;
-import avatartranslator.toproverif.AVATAR2ProVerif;
-import common.ConfigurationTTool;
-import common.SpecConfigTTool;
-import launcher.LauncherException;
-import launcher.RshClient;
-import launcher.RshClientReader;
-import myutil.FileException;
-import myutil.FileUtils;
-import myutil.MalformedConfigurationException;
-import myutil.TraceManager;
-import proverifspec.ProVerifOutputAnalyzer;
-import proverifspec.ProVerifSpec;
-import tmltranslator.TMLError;
-import tmltranslator.TMLMapping;
-import tmltranslator.TMLMappingTextSpecification;
-import tmltranslator.TMLSyntaxChecking;
-import tmltranslator.patternhandling.PatternIntegration;
-import tmltranslator.toavatarsec.TML2Avatar;
-import ui.AbstractUITest;
-import ui.AvatarDesignPanel;
-import ui.TGComponent;
-import ui.TGUIAction;
-import ui.networkmodelloader.NetworkModel;
-
-import java.io.BufferedReader;
-import java.io.File;
-import java.io.IOException;
-import java.io.InputStreamReader;
-import java.util.ArrayList;
-
-import static org.junit.Assert.assertTrue;
-
-public class AvatarNetworkProjectPragmaTests {
-
-
- protected static String PROJECT_NAME="";
-
- protected static ArrayList<String> resultsToBeChecked;
-
- protected static String pvspecPath;
-
- protected RshClient rshc;
-
- private ProVerifOutputAnalyzer pvoa;
-
- protected static String currentTabbedPane;
-
- protected static String currentFolderPath;
-
-
- public AvatarNetworkProjectPragmaTests() {}
-
-
- private TMLMapping<?> buildTMAPPattern() {
- resultsToBeChecked = new ArrayList<>();
- currentFolderPath = "test/resources/pragmasmodel/" + PROJECT_NAME + "/" + currentTabbedPane + "/";
- String filename = "spec";
- TMLMappingTextSpecification<Class<?>> tmts = new TMLMappingTextSpecification<Class<?>>(filename);
- File f = new File(currentFolderPath + filename + ".tmap");
- String spec = null;
- try {
- spec = FileUtils.loadFileData(f);
- } catch (Exception e) {
- System.out.println("Exception executing: loading " + currentTabbedPane);
- }
- boolean parsed = tmts.makeTMLMapping(spec, currentFolderPath);
- TMLMapping<?> _tmapPattern = tmts.getTMLMapping();
- // Checking syntax
- TMLSyntaxChecking syntax = new TMLSyntaxChecking(_tmapPattern);
- syntax.checkSyntax();
-
- if (syntax.hasErrors() > 0) {
- for (TMLError error: syntax.getErrors()) {
- TraceManager.addDev("Error: " + error.toString());
- }
-
- }
- return _tmapPattern;
- }
-
- public void buildPvspec(String _currentTabbedPane) throws FileException {
-
- currentTabbedPane = _currentTabbedPane;
- TMLMapping<?> _tmapPattern = buildTMAPPattern();
- //null for _referenceObject ? => getReferenceObject null
- Object o = null;
- TraceManager.addDev("getReference ? : " + _tmapPattern.getTMLModeling().getTasks().get(0).toString());
- if (_tmapPattern.getTMLModeling().getReference() instanceof TGComponent) {
- o = ((TGComponent)(_tmapPattern.getTMLModeling().getReference())).getTDiagramPanel().tp;
- }
- TML2Avatar tml2Avatar = new TML2Avatar(_tmapPattern,false,true,o);
- AvatarSpecification avatarspec = tml2Avatar.generateAvatarSpec("1",true);
- AVATAR2ProVerif avatar2proverif = new AVATAR2ProVerif(avatarspec);
- ProVerifSpec proverif = avatar2proverif.generateProVerif(true, true, 1, true,
- true);
-
- String filename = currentFolderPath + "pvspec";
- FileUtils.saveFile(filename, proverif.getStringSpec());
-
- }
-
- public void setProjectName(String projectName){
- PROJECT_NAME=projectName;
- }
-
-
- public void runProverif() throws MalformedConfigurationException {
-
- String filename = currentFolderPath + "pvspec";
- String str;
- ConfigurationTTool.loadConfiguration("/home/kali/Documents/Eurecom/SemesterProject/TTool/bin/config.xml",false);
- String cmd = "/bin/bash -c \'" + ConfigurationTTool.ProVerifVerifierPath + " -in pitype " + filename + " |grep RESULT\'";
-
-
- TraceManager.addDev("proverif path : " + ConfigurationTTool.ProVerifVerifierPath);
- TraceManager.addDev("Executing command " + cmd);
-
- try {
- ProcessBuilder processBuilder = new ProcessBuilder("/bin/bash", "-c", cmd);
- processBuilder.redirectErrorStream(true);
- Process process = processBuilder.start();
- BufferedReader process_in = new BufferedReader(new InputStreamReader(process.getInputStream()));
-
- while ((str = process_in.readLine()) != null) {
- TraceManager.addDev("Output proverif : " + str);
- resultsToBeChecked.add(str);
-
- }
- } catch (Exception e) {
- TraceManager.addDev("FAILED: executing: " + cmd + ": " + e.getMessage());
- }
-
- }
-
- public void generatePvspec(){
-
- pvspecPath = SpecConfigTTool.ProVerifCodeDirectory += "pvspec";
-
- }
-
- public void checkPragmas() throws Exception {
-
- }
-
- public ArrayList<String> getResultsToBeChecked(){
- return resultsToBeChecked;
- }
-
-}
-
diff --git a/ttool/src/test/java/tmltranslator/DiplodocusSecurityTest.java b/ttool/src/test/java/tmltranslator/DiplodocusSecurityTest.java
index d7d0e55841e9620e3ebefd4bd216ba225d3b4352..839897e7751493b26f0de1e6749d925c66dd1ae0 100644
--- a/ttool/src/test/java/tmltranslator/DiplodocusSecurityTest.java
+++ b/ttool/src/test/java/tmltranslator/DiplodocusSecurityTest.java
@@ -10,6 +10,8 @@ import myutil.TraceManager;
import org.junit.Before;
import org.junit.BeforeClass;
import org.junit.Test;
+import org.junit.runner.RunWith;
+import org.junit.runners.Parameterized;
import proverifspec.ProVerifSpec;
import req.ebrdd.EBRDD;
import tepe.TEPE;
@@ -31,47 +33,23 @@ import java.io.InputStreamReader;
import java.nio.file.Files;
import java.nio.file.Path;
import java.nio.file.Paths;
-import java.util.ArrayList;
-import java.util.Arrays;
-import java.util.List;
+import java.util.*;
import static org.junit.Assert.*;
-
+@RunWith(Parameterized.class)
public class DiplodocusSecurityTest extends AbstractTest {
- final static String DIR_GEN = "tmltranslator/test_diplo_security/";
- final static String DIR_MODELS = "tmltranslator/test_diplo_security_models/";
- final String [] MODELS_DIPLO_SECURITY = {"symetric", "nonce", "keyexchange", "mac"};
-
- private static final List<List<String>> LIST_OF_LISTS_OF_QUERIES = Arrays.asList(
- Arrays.asList("Query not attacker(Alice___SymmetricExchange__comm_chData[!1 = v]) is true.",
- "Query inj-event(authenticity___Bob___SymmetricExchange__comm_chData___aftersignalstate_SymmetricExchange_comm_" +
- "SymmetricExchange_comm(dummyM)) ==> inj-event(authenticity___Alice___SymmetricExchange__comm_chData" +
- "___signalstate_SymmetricExchange_comm_SymmetricExchange_comm(dummyM)) is false."),
- Arrays.asList("Query not attacker(Alice___nonce__comm_chData[!1 = v]) is true.",
- "Query inj-event(authenticity___Bob___nonce__comm_chData___aftersignalstate_nonce_comm_nonce_comm(dummyM)) ==> inj-event" +
- "(authenticity___Alice___nonce__comm_chData___signalstate_nonce_comm_nonce_comm(dummyM)) is false."),
- Arrays.asList("Query not attacker(Alice___KeyExchange__comm_chData[!1 = v]) is true.", "RESULT inj-event" +
- "(authenticity___Bob___KeyExchange__comm_chData___aftersignalstate_KeyExchange_comm_KeyExchange_comm283" +
- "(dummyM)) ==> inj-event(authenticity___Alice___KeyExchange__comm_chData___signalstate_KeyExchange_comm_KeyExchange_comm239" +
- "(dummyM)) is true.", "Query inj-event(authenticity___Bob___KeyExchange__comm_chData___aftersignalstate_KeyExchange_comm" +
- "_KeyExchange_comm283(dummyM)) ==> inj-event(authenticity___Alice___KeyExchange__comm_chData" +
- "___signalstate_KeyExchange_comm_KeyExchange_comm239(dummyM)) is true.",
- "Query inj-event(authenticity___Bob___KeyExchange__comm_chData___aftersignalstate_KeyExchange_comm_KeyExchange_",
- "Query inj-event(authenticity___Bob___KeyExchange__comm_chData___aftersignalstate_KeyExchange_comm_KeyExchange_comm(dummyM)) " +
- "==> inj-event(authenticity___Alice___KeyExchange__comm_chData___signalstate_KeyExchange_comm_KeyExchange_comm(dummyM)) is false"),
- Arrays.asList("Query not attacker(Alice___MAC__comm_chData[!1 = v]) is true.",
- "Query inj-event(authenticity___Bob___MAC__comm_chData___aftersignalstate_MAC_comm_MAC_comm(dummyM)) ==> inj-event(authenticity" +
- "___Alice___MAC__comm_chData___signalstate_MAC_comm_MAC_comm(dummyM)) is false")
- );
+ final static String DIR_GEN = "tmltranslator/DiplodocusSecurityTest/";
+ final static String DIR_MODELS = "tmltranslator/DiplodocusSecurityTest/Models/";
+ final static String PVSPEC_FILENAME = "generatedPvspec";
+ private static String currentModel;
+ private static ArrayList<String> currentTabs;
+ private static HashMap<String, String[]> goldenMap;
+
private static final String PROVERIF_SUMMARY = "Verification summary:";
private static final String PROVERIF_QUERY = "Query";
-
-
static String PROVERIF_DIR;
static String MODELS_DIR;
-
-
@BeforeClass
public static void setUpBeforeClass() throws Exception {
PROVERIF_DIR = getBaseResourcesDir() + DIR_GEN;
@@ -79,18 +57,41 @@ public class DiplodocusSecurityTest extends AbstractTest {
RESOURCES_DIR = getBaseResourcesDir() + DIR_MODELS;
}
- public DiplodocusSecurityTest() {
+ //arguments are defined in @Parameterized.Parameters
+ public DiplodocusSecurityTest(String model, ArrayList<String> tabs){
super();
+ currentModel = model;
+ currentTabs = tabs;
+ goldenMap = new HashMap<String, String[]>();
+ }
+
+ @Parameterized.Parameters(name = "{index}: {0}")
+ public static Collection models(){
+ return Arrays.asList(new Object[][] {
+ {"AliceAndBobHW", new ArrayList<>(Arrays.asList("SymmetricExchange", "Nonce", "KeyExchange", "Mac"))},
+ {"AliceAndBobHW", new ArrayList<>(Arrays.asList("SymmetricExchange", "Nonce", "KeyExchange", "Mac"))},
+// {"AliceAndBobHW", new ArrayList<>(Arrays.asList("SymmetricExchange", "Nonce", "KeyExchange", "Mac", "SampleAutoSec"))}
+ });
}
+
@Before
public void setUp() throws Exception {
TraceManager.devPolicy = TraceManager.TO_CONSOLE;
+
+ TraceManager.addDev("Starting test for " + currentModel + " model");
Path path = Paths.get(PROVERIF_DIR);
if (!Files.exists(path)) {
Files.createDirectory(path);
}
+ goldenMap.clear();
+ //Load current golden map, which is map a tab with its golden pvspec
+ for (String tab : currentTabs){
+ TraceManager.addDev("tab : " + tab);
+ String fileContent = FileUtils.loadFile(RESOURCES_DIR + currentModel + "/" + tab + "/golden");
+ goldenMap.put(tab,fileContent.split("\n"));
+ }
}
@Test
@@ -102,27 +103,25 @@ public class DiplodocusSecurityTest extends AbstractTest {
return;
}
-
- for (int i = 0; i < MODELS_DIPLO_SECURITY.length; i++) {
- String s = MODELS_DIPLO_SECURITY[i];
- System.out.println("\n\n********** Checking the security of " + s + " ********\n");
- TMLMappingTextSpecification tmts = new TMLMappingTextSpecification(s);
- File f = new File(RESOURCES_DIR + s + ".tmap");
+ for (String tab : currentTabs){
+ System.out.println("\n\n********** Checking the security of " + tab + " ********\n");
+ TMLMappingTextSpecification tmts = new TMLMappingTextSpecification(tab);
+ File f = new File(RESOURCES_DIR + currentModel + "/" + tab + "/spec.tmap");
System.out.println("Loading file: " + f.getAbsolutePath());
String spec = null;
try {
spec = FileUtils.loadFileData(f);
} catch (Exception e) {
- System.out.println("Exception executing: loading " + s);
+ System.out.println("Exception executing: loading " + tab);
assertTrue(false);
}
- System.out.println("Testing spec " + s);
+ System.out.println("Testing spec " + tab);
assertTrue(spec != null);
- System.out.println("Going to parse " + s);
- boolean parsed = tmts.makeTMLMapping(spec, RESOURCES_DIR);
+ System.out.println("Going to parse " + tab);
+ boolean parsed = tmts.makeTMLMapping(spec, RESOURCES_DIR + currentModel + "/" + tab + "/");
assertTrue(parsed);
- System.out.println("Checking syntax " + s);
+ System.out.println("Checking syntax " + tab);
// Checking syntax
TMLMapping tmap = tmts.getTMLMapping();
@@ -139,7 +138,7 @@ public class DiplodocusSecurityTest extends AbstractTest {
assertTrue(syntax.hasErrors() == 0);
// Generate ProVerif code
- System.out.println("Generating ProVerif code for " + s);
+ System.out.println("Generating ProVerif code for " + tab);
Object o = null;
if (tmap.getTMLModeling().getReference() instanceof TGComponent) {
o = ((TGComponent)(tmap.getTMLModeling().getReference())).getTDiagramPanel().tp;
@@ -150,14 +149,14 @@ public class DiplodocusSecurityTest extends AbstractTest {
ProVerifSpec proverif = avatar2proverif.generateProVerif(true, true, 0, true,
true);
- TraceManager.addDev("Saving spec in " + PROVERIF_DIR + s);
- FileUtils.saveFile(PROVERIF_DIR + s, proverif.getStringSpec());
+ TraceManager.addDev("Saving spec in " + PROVERIF_DIR + PVSPEC_FILENAME);
+ FileUtils.saveFile(PROVERIF_DIR + PVSPEC_FILENAME, proverif.getStringSpec());
TraceManager.addDev("Running Proverif");
Process proc;
BufferedReader proc_in;
String str;
- String cmd = "proverif -in pitype " + PROVERIF_DIR + s;
+ String cmd = "proverif -in pitype " + PROVERIF_DIR + PVSPEC_FILENAME;
boolean summaryFound = false;
try {
@@ -169,7 +168,7 @@ public class DiplodocusSecurityTest extends AbstractTest {
System.out.println("Output from ProVerif: " + str);
if (summaryFound && (str.contains(PROVERIF_QUERY))) {
- assertTrue(contains(i, str));
+ assertTrue(contains(tab, str));
}
if (str.contains(PROVERIF_SUMMARY)) {
@@ -181,18 +180,24 @@ public class DiplodocusSecurityTest extends AbstractTest {
System.out.println("FAILED: executing: " + cmd + ": " + e.getMessage());
return;
}
-
+ TraceManager.addDev("Test for " + tab + " tab is ended");
}
+ TraceManager.addDev("Test for " + currentModel + " model is ended");
}
- private boolean contains(int index, String str) {
+ private boolean contains(String tab, String str) {
str = str.trim();
- for(String s: LIST_OF_LISTS_OF_QUERIES.get(index)) {
- if (str.startsWith(s.trim())) {
- TraceManager.addDev("Query: " + s + " is correct");
+ if (goldenMap.get(tab) == null){
+ TraceManager.addDev("The golden for : " + tab + " is null");
+ return false;
+ }
+ for(String s: goldenMap.get(tab)) {
+ if (str.startsWith(s.trim())&& !s.trim().isEmpty()) {
+ TraceManager.addDev( "\"" + str + "\"" + " is in golden");
return true;
}
}
+ TraceManager.addDev("\"" + str + "\"" + " not in golden");
return false;
}
}
diff --git a/ttool/src/test/resources/pragmasmodel/AliceAndBobHW/SymExchangeArch/golden b/ttool/src/test/resources/pragmasmodel/AliceAndBobHW/SymExchangeArch/golden
deleted file mode 100644
index 5f304fb980b4df75047ef2ddf6a92459166921fb..0000000000000000000000000000000000000000
--- a/ttool/src/test/resources/pragmasmodel/AliceAndBobHW/SymExchangeArch/golden
+++ /dev/null
@@ -1,10 +0,0 @@
-RESULT not attacker(Alice___comm_chData[!1 = v]) is true.
-RESULT not attacker(Alice___sym[!1 = v]) is true.
-RESULT not event(enteringState___Alice____encrypt_sym) is false.
-RESULT not event(enteringState___Alice___signalstate_writechannel_SymmetricExchange_comm) is false.
-RESULT not event(enteringState___Bob___signalstate_readchannel_SymmetricExchange_comm) is false.
-RESULT not event(enteringState___Bob___aftersignalstate_readchannel_SymmetricExchange_comm) is false.
-RESULT not event(enteringState___Bob____decrypt_sym) is false.
-RESULT not event(enteringState___Bob___decrypt_sym_dummy) is false.
-RESULT inj-event(authenticity___Bob___sym___decrypt_sym_dummy(dummyM)) ==> inj-event(authenticity___Alice___sym____encrypt_sym(dummyM)) is false.
-RESULT (but event(authenticity___Bob___sym___decrypt_sym_dummy(dummyM)) ==> event(authenticity___Alice___sym____encrypt_sym(dummyM)) is true.)
diff --git a/ttool/src/test/resources/pragmasmodel/AliceAndBobHW/SymExchangeArch/spec.tml b/ttool/src/test/resources/pragmasmodel/AliceAndBobHW/SymExchangeArch/spec.tml
deleted file mode 100644
index 66d2c62a31c10a5b6e3f3ac1f8c0a44ccaf5126d..0000000000000000000000000000000000000000
--- a/ttool/src/test/resources/pragmasmodel/AliceAndBobHW/SymExchangeArch/spec.tml
+++ /dev/null
@@ -1,34 +0,0 @@
-// TML Application - FORMAT 0.2
-// Application: /home/kali/Documents/Eurecom/SemesterProject/TTool/modeling/AliceAndBobHW.ttool/AliceAndBobHW.xml
-// Generated: Tue Dec 05 15:15:11 EST 2023
-
-// PRAGMAS
-
-// Channels
-CHANNEL SymmetricExchange__comm NBRNBW 4 OUT SymmetricExchange__Alice IN SymmetricExchange__Bob
-VCCHANNEL SymmetricExchange__comm 0
-CONFCHANNEL SymmetricExchange__comm
-AUTHCHANNEL SymmetricExchange__comm
-
-// Events
-
-// Requests
-
-TASK SymmetricExchange__Alice
- TASKOP
- //Local variables
-
- //Behavior
- EXECC 100 sym SE 100 100 0 0 - - 1
- WRITE SymmetricExchange__comm 1+0 sym
-ENDTASK
-
-TASK SymmetricExchange__Bob
- TASKOP
- //Local variables
-
- //Behavior
- READ SymmetricExchange__comm 1+0 sym
- EXECC 100 sym SE 100 100 0 0 - - 2
-ENDTASK
-
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/KeyExchange/golden b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/KeyExchange/golden
new file mode 100644
index 0000000000000000000000000000000000000000..d6f0cf9946185bb9d8588e8e14235fd080915451
--- /dev/null
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/KeyExchange/golden
@@ -0,0 +1,5 @@
+Query not attacker(Alice___KeyExchange__comm_chData[!1 = v]) is true.
+Query inj-event(authenticity___Bob___comm_chData___aftersignalstate_KeyExchange_comm_KeyExchange_comm(dummyM)) ==> inj-event(authenticity___Alice___comm_chData___signalstate_KeyExchange_comm_KeyExchange_comm(dummyM)) is false.
+Query inj-event(authenticity___Bob___comm_chData___aftersignalstate_KeyExchange_comm_KeyExchange_comm297(dummyM)) ==> inj-event(authenticity___Alice___comm_chData___signalstate_KeyExchange_comm_KeyExchange_comm(dummyM)) is false.
+Query inj-event(authenticity___Bob___comm_chData___aftersignalstate_KeyExchange_comm_KeyExchange_comm(dummyM)) ==> inj-event(authenticity___Alice___comm_chData___signalstate_KeyExchange_comm_KeyExchange_comm251(dummyM)) is false.
+Query inj-event(authenticity___Bob___comm_chData___aftersignalstate_KeyExchange_comm_KeyExchange_comm297(dummyM)) ==> inj-event(authenticity___Alice___comm_chData___signalstate_KeyExchange_comm_KeyExchange_comm251(dummyM)) is false.
diff --git a/ttool/src/test/resources/tmltranslator/test_diplo_security_models/keyexchange.tarchi b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/KeyExchange/spec.tarchi
similarity index 100%
rename from ttool/src/test/resources/tmltranslator/test_diplo_security_models/keyexchange.tarchi
rename to ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/KeyExchange/spec.tarchi
diff --git a/ttool/src/test/resources/tmltranslator/test_diplo_security_models/keyexchange.tmap b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/KeyExchange/spec.tmap
similarity index 89%
rename from ttool/src/test/resources/tmltranslator/test_diplo_security_models/keyexchange.tmap
rename to ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/KeyExchange/spec.tmap
index d0d283372a25d887224c4b5f6926553ddfeff095..ef6c52762910f9aba6f97cbc152775cde7d59e7a 100644
--- a/ttool/src/test/resources/tmltranslator/test_diplo_security_models/keyexchange.tmap
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/KeyExchange/spec.tmap
@@ -1,9 +1,9 @@
TMLSPEC
- #include "keyexchange.tml"
+ #include "spec.tml"
ENDTMLSPEC
TMLARCHI
- #include "keyexchange.tarchi"
+ #include "spec.tarchi"
ENDTMLARCHI
TMLMAPPING
diff --git a/ttool/src/test/resources/tmltranslator/test_diplo_security_models/keyexchange.tml b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/KeyExchange/spec.tml
similarity index 100%
rename from ttool/src/test/resources/tmltranslator/test_diplo_security_models/keyexchange.tml
rename to ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/KeyExchange/spec.tml
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/Mac/golden b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/Mac/golden
new file mode 100644
index 0000000000000000000000000000000000000000..4436f6f06de60abe6270d7e515aa72d579bab805
--- /dev/null
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/Mac/golden
@@ -0,0 +1,2 @@
+Query not attacker(Alice___MAC__comm_chData[!1 = v]) is true.
+Query inj-event(authenticity___Bob___comm_chData___aftersignalstate_MAC_comm_MAC_comm(dummyM)) ==> inj-event(authenticity___Alice___comm_chData___signalstate_MAC_comm_MAC_comm(dummyM)) is false.
diff --git a/ttool/src/test/resources/tmltranslator/test_diplo_security_models/mac.tarchi b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/Mac/spec.tarchi
similarity index 100%
rename from ttool/src/test/resources/tmltranslator/test_diplo_security_models/mac.tarchi
rename to ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/Mac/spec.tarchi
diff --git a/ttool/src/test/resources/tmltranslator/test_diplo_security_models/mac.tmap b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/Mac/spec.tmap
similarity index 90%
rename from ttool/src/test/resources/tmltranslator/test_diplo_security_models/mac.tmap
rename to ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/Mac/spec.tmap
index 605264b48af898a235b20114d26388677db326da..882d0eba991bb950821be439dfb86ff177fd7b7b 100644
--- a/ttool/src/test/resources/tmltranslator/test_diplo_security_models/mac.tmap
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/Mac/spec.tmap
@@ -1,9 +1,9 @@
TMLSPEC
- #include "mac.tml"
+ #include "spec.tml"
ENDTMLSPEC
TMLARCHI
- #include "mac.tarchi"
+ #include "spec.tarchi"
ENDTMLARCHI
TMLMAPPING
diff --git a/ttool/src/test/resources/tmltranslator/test_diplo_security_models/mac.tml b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/Mac/spec.tml
similarity index 100%
rename from ttool/src/test/resources/tmltranslator/test_diplo_security_models/mac.tml
rename to ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/Mac/spec.tml
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/Nonce/golden b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/Nonce/golden
new file mode 100644
index 0000000000000000000000000000000000000000..6777b481cefc1e86564ed458e77d57f332268340
--- /dev/null
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/Nonce/golden
@@ -0,0 +1,2 @@
+Query not attacker(Alice___nonce__comm_chData[!1 = v]) is true.
+Query inj-event(authenticity___Bob___comm_chData___aftersignalstate_nonce_comm_nonce_comm(dummyM)) ==> inj-event(authenticity___Alice___comm_chData___signalstate_nonce_comm_nonce_comm(dummyM)) is false.
diff --git a/ttool/src/test/resources/tmltranslator/test_diplo_security_models/nonce.tarchi b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/Nonce/spec.tarchi
similarity index 100%
rename from ttool/src/test/resources/tmltranslator/test_diplo_security_models/nonce.tarchi
rename to ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/Nonce/spec.tarchi
diff --git a/ttool/src/test/resources/tmltranslator/test_diplo_security_models/nonce.tmap b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/Nonce/spec.tmap
similarity index 93%
rename from ttool/src/test/resources/tmltranslator/test_diplo_security_models/nonce.tmap
rename to ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/Nonce/spec.tmap
index dd190afbba4350ae50ab4eb6262748b940f7e5e5..603187e9ebcc069a48d29337b927b76b510a3d4d 100644
--- a/ttool/src/test/resources/tmltranslator/test_diplo_security_models/nonce.tmap
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/Nonce/spec.tmap
@@ -1,9 +1,9 @@
TMLSPEC
- #include "nonce.tml"
+ #include "spec.tml"
ENDTMLSPEC
TMLARCHI
- #include "nonce.tarchi"
+ #include "spec.tarchi"
ENDTMLARCHI
TMLMAPPING
diff --git a/ttool/src/test/resources/tmltranslator/test_diplo_security_models/nonce.tml b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/Nonce/spec.tml
similarity index 100%
rename from ttool/src/test/resources/tmltranslator/test_diplo_security_models/nonce.tml
rename to ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/Nonce/spec.tml
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/SymmetricExchange/golden b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/SymmetricExchange/golden
new file mode 100644
index 0000000000000000000000000000000000000000..5e788c2fbc639f17e05a3b60a7cacf8f58838b6c
--- /dev/null
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/SymmetricExchange/golden
@@ -0,0 +1,2 @@
+Query not attacker(Alice___SymmetricExchange__comm_chData[!1 = v]) is true.
+Query inj-event(authenticity___Bob___comm_chData___aftersignalstate_SymmetricExchange_comm_SymmetricExchange_comm(dummyM)) ==> inj-event(authenticity___Alice___comm_chData___signalstate_SymmetricExchange_comm_SymmetricExchange_comm(dummyM)) is false.
diff --git a/ttool/src/test/resources/pragmasmodel/AliceAndBobHW/SymExchangeArch/spec.tarchi b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/SymmetricExchange/spec.tarchi
similarity index 100%
rename from ttool/src/test/resources/pragmasmodel/AliceAndBobHW/SymExchangeArch/spec.tarchi
rename to ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/SymmetricExchange/spec.tarchi
diff --git a/ttool/src/test/resources/pragmasmodel/AliceAndBobHW/SymExchangeArch/spec.tmap b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/SymmetricExchange/spec.tmap
similarity index 100%
rename from ttool/src/test/resources/pragmasmodel/AliceAndBobHW/SymExchangeArch/spec.tmap
rename to ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/SymmetricExchange/spec.tmap
diff --git a/ttool/src/test/resources/tmltranslator/test_diplo_security_models/symetric.tml b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/SymmetricExchange/spec.tml
similarity index 100%
rename from ttool/src/test/resources/tmltranslator/test_diplo_security_models/symetric.tml
rename to ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/SymmetricExchange/spec.tml
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/generatedPvspec b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/generatedPvspec
new file mode 100644
index 0000000000000000000000000000000000000000..d3667333e5e28cddc53d770758b63b642e6065c1
--- /dev/null
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/generatedPvspec
@@ -0,0 +1,153 @@
+
+
+(* Generated ProVerif specification *)
+set abbreviateDerivation = false.
+
+(* Boolean return types *)
+const TRUE: bitstring [data].
+const FALSE: bitstring [data].
+
+(* Functions data *)
+const UNKNOWN: bitstring [data].
+
+(* Public key cryptography *)
+fun pk (bitstring): bitstring.
+fun aencrypt (bitstring, bitstring): bitstring.
+reduc forall x: bitstring, y: bitstring; adecrypt (aencrypt (x, pk (y)), y) = x.
+fun sign (bitstring, bitstring): bitstring.
+fun verifySign (bitstring, bitstring, bitstring): bitstring
+ reduc forall m: bitstring, sk: bitstring; verifySign (m, sign (m, sk), pk (sk)) = TRUE
+ otherwise forall m: bitstring, m2: bitstring, ppk: bitstring; verifySign (m, m2, ppk) = FALSE.
+
+(* Certificates *)
+fun cert (bitstring, bitstring): bitstring.
+fun verifyCert (bitstring, bitstring): bitstring
+ reduc forall epk: bitstring, sk: bitstring; verifyCert (cert (epk, sign (epk, sk)), pk (sk)) = TRUE
+ otherwise forall m: bitstring, ppk: bitstring; verifyCert (m, ppk) = FALSE.
+reduc forall epk: bitstring, sk: bitstring; getpk (cert (epk, sign (epk,sk))) = epk.
+
+(* Symmetric key cryptography *)
+fun sencrypt (bitstring, bitstring): bitstring.
+reduc forall x: bitstring, k: bitstring; sdecrypt (sencrypt (x, k), k) = x.
+
+(* Diffie-Hellman *)
+fun DH (bitstring, bitstring): bitstring.
+equation forall x: bitstring, y: bitstring; DH (pk (x), y) = DH (pk (y), x).
+
+(* MAC *)
+fun MAC (bitstring, bitstring): bitstring.
+fun verifyMAC (bitstring, bitstring, bitstring): bitstring
+ reduc forall m: bitstring, k: bitstring; verifyMAC (m, k, MAC (m, k)) = TRUE
+ otherwise forall m: bitstring, m2: bitstring, k: bitstring; verifyMAC (m, k, m2) = FALSE.
+
+(* HASH *)
+fun hash (bitstring): bitstring.
+
+(* Key and host *)
+fun host (bitstring): bitstring.
+reduc forall x: bitstring; getKey (host (x)) = x.
+
+(* Channel *)
+free ch: channel.
+
+(* Control Channel *)
+free chControl: channel.
+fun chControlEnc (bitstring): bitstring [private].
+reduc forall x: bitstring; chControlDec (chControlEnc (x)) = x [private].
+
+(* Basic Peano Arithmetic *)
+const O: bitstring [data].
+fun N (bitstring): bitstring.
+free call___Alice___0: bitstring [private].
+free call___Bob___0: bitstring [private].
+
+(* Constants *)
+
+(* Secrecy Assumptions *)
+
+(* Queries Secret *)
+query attacker(new Alice___KeyExchange__comm_chData).
+
+(* Queries Event *)
+
+(* Authenticity *)
+event authenticity___Alice___comm_chData___signalstate_KeyExchange_comm_KeyExchange_comm(bitstring).
+event authenticity___Bob___comm_chData___aftersignalstate_KeyExchange_comm_KeyExchange_comm(bitstring).
+query dummyM: bitstring; inj-event(authenticity___Bob___comm_chData___aftersignalstate_KeyExchange_comm_KeyExchange_comm (dummyM)) ==> inj-event(authenticity___Alice___comm_chData___signalstate_KeyExchange_comm_KeyExchange_comm (dummyM)).
+event authenticity___Bob___comm_chData___aftersignalstate_KeyExchange_comm_KeyExchange_comm727(bitstring).
+query dummyM: bitstring; inj-event(authenticity___Bob___comm_chData___aftersignalstate_KeyExchange_comm_KeyExchange_comm727 (dummyM)) ==> inj-event(authenticity___Alice___comm_chData___signalstate_KeyExchange_comm_KeyExchange_comm (dummyM)).
+event authenticity___Alice___comm_chData___signalstate_KeyExchange_comm_KeyExchange_comm681(bitstring).
+query dummyM: bitstring; inj-event(authenticity___Bob___comm_chData___aftersignalstate_KeyExchange_comm_KeyExchange_comm (dummyM)) ==> inj-event(authenticity___Alice___comm_chData___signalstate_KeyExchange_comm_KeyExchange_comm681 (dummyM)).
+query dummyM: bitstring; inj-event(authenticity___Bob___comm_chData___aftersignalstate_KeyExchange_comm_KeyExchange_comm727 (dummyM)) ==> inj-event(authenticity___Alice___comm_chData___signalstate_KeyExchange_comm_KeyExchange_comm681 (dummyM)).
+
+let Alice___start (sessionID: bitstring) =
+ new Alice___key_symKey[]: bitstring;
+ new Alice___pubKey_aenc[]: bitstring;
+ new Alice___KeyExchange__comm_chData[]: bitstring;
+ new Alice___tmp[]: bitstring;
+ new Alice___loop_index[]: bitstring;
+ new Alice___aenc_encrypted[]: bitstring;
+ new Alice___aenc[]: bitstring;
+ new Alice___privKey_aenc[]: bitstring;
+ new Alice___comm_chData[]: bitstring;
+ new Alice___symKey[]: bitstring;
+ new Alice___symKey_encrypted[]: bitstring;
+ in (chControl, strong___Alice___01: bitstring);
+ out (chControl, chControlEnc ((sessionID, call___Alice___0, strong___Alice___01, Alice___key_symKey, Alice___pubKey_aenc, Alice___KeyExchange__comm_chData, Alice___tmp, Alice___loop_index, Alice___aenc_encrypted, Alice___aenc, Alice___privKey_aenc, Alice___comm_chData, Alice___symKey, Alice___symKey_encrypted))).
+
+let Alice___0 (sessionID: bitstring) =
+ new strong___Alice___02[]: bitstring;
+ out (chControl, strong___Alice___02);
+ in (chControl, chControlData: bitstring);
+ let (=sessionID, =call___Alice___0, =strong___Alice___02, Alice___key_symKey___1: bitstring, Alice___pubKey_aenc___1: bitstring, Alice___KeyExchange__comm_chData___1: bitstring, Alice___tmp___1: bitstring, Alice___loop_index___1: bitstring, Alice___aenc_encrypted___1: bitstring, Alice___aenc___1: bitstring, Alice___privKey_aenc___1: bitstring, Alice___comm_chData___1: bitstring, Alice___symKey___1: bitstring, Alice___symKey_encrypted___1: bitstring) = chControlDec (chControlData) in
+ let Alice___aenc___2: bitstring = adecrypt (Alice___aenc_encrypted___1, Alice___privKey_aenc___1) in
+ event authenticity___Alice___comm_chData___signalstate_KeyExchange_comm_KeyExchange_comm (Alice___comm_chData___1);
+ out (ch, Alice___aenc_encrypted___1);
+ let Alice___symKey___2: bitstring = sdecrypt (Alice___symKey_encrypted___1, Alice___key_symKey___1) in
+ event authenticity___Alice___comm_chData___signalstate_KeyExchange_comm_KeyExchange_comm681 (Alice___comm_chData___1);
+ out (ch, Alice___symKey_encrypted___1).
+
+let Bob___start (sessionID: bitstring) =
+ new Bob___privKey_aenc[]: bitstring;
+ let Bob___pubKey_aenc: bitstring = pk(Bob___privKey_aenc) in
+ out (ch, Bob___pubKey_aenc);
+ new Bob___KeyExchange__comm_chData[]: bitstring;
+ new Bob___tmp[]: bitstring;
+ new Bob___loop_index[]: bitstring;
+ new Bob___aenc_encrypted[]: bitstring;
+ new Bob___comm_chData[]: bitstring;
+ new Bob___aenc[]: bitstring;
+ new Bob___symKey_encrypted[]: bitstring;
+ new Bob___symKey[]: bitstring;
+ new Bob___key_symKey[]: bitstring;
+ in (chControl, strong___Bob___03: bitstring);
+ out (chControl, chControlEnc ((sessionID, call___Bob___0, strong___Bob___03, Bob___pubKey_aenc, Bob___privKey_aenc, Bob___KeyExchange__comm_chData, Bob___tmp, Bob___loop_index, Bob___aenc_encrypted, Bob___comm_chData, Bob___aenc, Bob___symKey_encrypted, Bob___symKey, Bob___key_symKey))).
+
+let Bob___0 (sessionID: bitstring) =
+ new strong___Bob___04[]: bitstring;
+ out (chControl, strong___Bob___04);
+ in (chControl, chControlData: bitstring);
+ let (=sessionID, =call___Bob___0, =strong___Bob___04, Bob___pubKey_aenc___1: bitstring, Bob___privKey_aenc___1: bitstring, Bob___KeyExchange__comm_chData___1: bitstring, Bob___tmp___1: bitstring, Bob___loop_index___1: bitstring, Bob___aenc_encrypted___1: bitstring, Bob___comm_chData___1: bitstring, Bob___aenc___1: bitstring, Bob___symKey_encrypted___1: bitstring, Bob___symKey___1: bitstring, Bob___key_symKey___1: bitstring) = chControlDec (chControlData) in
+ in (ch, Bob___aenc_encrypted___2: bitstring);
+ event authenticity___Bob___comm_chData___aftersignalstate_KeyExchange_comm_KeyExchange_comm (Bob___comm_chData___1);
+ let Bob___aenc___2: bitstring = adecrypt (Bob___aenc_encrypted___2, Bob___privKey_aenc___1) in
+ in (ch, Bob___symKey_encrypted___2: bitstring);
+ event authenticity___Bob___comm_chData___aftersignalstate_KeyExchange_comm_KeyExchange_comm727 (Bob___comm_chData___1);
+ let Bob___symKey___2: bitstring = sdecrypt (Bob___symKey_encrypted___2, Bob___key_symKey___1) in
+ 0.
+
+process
+ ! (
+ new sessionID[]: bitstring;
+ ((
+ Alice___0 (sessionID)
+ ) | (
+ Bob___0 (sessionID)
+ ) | (
+ (
+ ((
+ Alice___start (sessionID)
+ ) | (
+ Bob___start (sessionID)
+ )))
+ )))
\ No newline at end of file
diff --git a/ttool/src/test/resources/tmltranslator/test_diplo_security_models/symetric.tarchi b/ttool/src/test/resources/tmltranslator/test_diplo_security_models/symetric.tarchi
deleted file mode 100644
index 8013dbe04a245b2e9b40483231470468045e0dcd..0000000000000000000000000000000000000000
--- a/ttool/src/test/resources/tmltranslator/test_diplo_security_models/symetric.tarchi
+++ /dev/null
@@ -1,116 +0,0 @@
-// Master clock frequency - in MHz
-MASTERCLOCKFREQUENCY 200
-
-NODE BRIDGE BridgeAlice
-SET BridgeAlice bufferByteSize 4
-SET BridgeAlice clockDivider 1
-
-NODE BRIDGE BridgeBob
-SET BridgeBob bufferByteSize 4
-SET BridgeBob clockDivider 1
-
-NODE MEMORY ExternalMemory
-SET ExternalMemory byteDataSize 4
-SET ExternalMemory clockDivider 1
-
-NODE MEMORY MemoryAlice
-SET MemoryAlice byteDataSize 4
-SET MemoryAlice clockDivider 1
-
-NODE MEMORY MemoryBob
-SET MemoryBob byteDataSize 4
-SET MemoryBob clockDivider 1
-
-NODE BUS BusBob
-SET BusBob byteDataSize 4
-SET BusBob pipelineSize 1
-SET BusBob arbitration 0
-SET BusBob sliceTime 10000
-SET BusBob burstSize 100
-SET BusBob privacy private
-SET BusBob clockDivider 1
-
-NODE BUS BusAlice
-SET BusAlice byteDataSize 4
-SET BusAlice pipelineSize 1
-SET BusAlice arbitration 0
-SET BusAlice sliceTime 10000
-SET BusAlice burstSize 100
-SET BusAlice privacy private
-SET BusAlice clockDivider 1
-
-NODE BUS ExternalBus
-SET ExternalBus byteDataSize 4
-SET ExternalBus pipelineSize 1
-SET ExternalBus arbitration 0
-SET ExternalBus sliceTime 10000
-SET ExternalBus burstSize 100
-SET ExternalBus privacy public
-SET ExternalBus clockDivider 1
-
-NODE CPU CPUAlice
-SET CPUAlice nbOfCores 1
-SET CPUAlice byteDataSize 4
-SET CPUAlice pipelineSize 5
-SET CPUAlice goIdleTime 10
-SET CPUAlice maxConsecutiveIdleCycles 10
-SET CPUAlice taskSwitchingTime 20
-SET CPUAlice branchingPredictionPenalty 2
-SET CPUAlice cacheMiss 5
-SET CPUAlice schedulingPolicy 0
-SET CPUAlice sliceTime 10000
-SET CPUAlice execiTime 1
-SET CPUAlice execcTime 1
-SET CPUAlice clockDivider 1
-
-NODE CPU CPUBob
-SET CPUBob nbOfCores 1
-SET CPUBob byteDataSize 4
-SET CPUBob pipelineSize 5
-SET CPUBob goIdleTime 10
-SET CPUBob maxConsecutiveIdleCycles 10
-SET CPUBob taskSwitchingTime 20
-SET CPUBob branchingPredictionPenalty 2
-SET CPUBob cacheMiss 5
-SET CPUBob schedulingPolicy 0
-SET CPUBob sliceTime 10000
-SET CPUBob execiTime 1
-SET CPUBob execcTime 1
-SET CPUBob clockDivider 1
-
-NODE LINK link_CPUBob_to_BusBob
-SET link_CPUBob_to_BusBob node CPUBob
-SET link_CPUBob_to_BusBob bus BusBob
-SET link_CPUBob_to_BusBob priority 0
-NODE LINK link_CPUAlice_to_BusAlice
-SET link_CPUAlice_to_BusAlice node CPUAlice
-SET link_CPUAlice_to_BusAlice bus BusAlice
-SET link_CPUAlice_to_BusAlice priority 0
-NODE LINK link_BridgeBob_to_BusBob
-SET link_BridgeBob_to_BusBob node BridgeBob
-SET link_BridgeBob_to_BusBob bus BusBob
-SET link_BridgeBob_to_BusBob priority 0
-NODE LINK link_BridgeBob_to_ExternalBus
-SET link_BridgeBob_to_ExternalBus node BridgeBob
-SET link_BridgeBob_to_ExternalBus bus ExternalBus
-SET link_BridgeBob_to_ExternalBus priority 0
-NODE LINK link_BridgeAlice_to_ExternalBus
-SET link_BridgeAlice_to_ExternalBus node BridgeAlice
-SET link_BridgeAlice_to_ExternalBus bus ExternalBus
-SET link_BridgeAlice_to_ExternalBus priority 0
-NODE LINK link_BridgeAlice_to_BusAlice
-SET link_BridgeAlice_to_BusAlice node BridgeAlice
-SET link_BridgeAlice_to_BusAlice bus BusAlice
-SET link_BridgeAlice_to_BusAlice priority 0
-NODE LINK link_ExternalMemory_to_ExternalBus
-SET link_ExternalMemory_to_ExternalBus node ExternalMemory
-SET link_ExternalMemory_to_ExternalBus bus ExternalBus
-SET link_ExternalMemory_to_ExternalBus priority 0
-NODE LINK link_MemoryAlice_to_BusAlice
-SET link_MemoryAlice_to_BusAlice node MemoryAlice
-SET link_MemoryAlice_to_BusAlice bus BusAlice
-SET link_MemoryAlice_to_BusAlice priority 0
-NODE LINK link_MemoryBob_to_BusBob
-SET link_MemoryBob_to_BusBob node MemoryBob
-SET link_MemoryBob_to_BusBob bus BusBob
-SET link_MemoryBob_to_BusBob priority 0
diff --git a/ttool/src/test/resources/tmltranslator/test_diplo_security_models/symetric.tmap b/ttool/src/test/resources/tmltranslator/test_diplo_security_models/symetric.tmap
deleted file mode 100644
index 66914329ce8183adb0922d584a603a485734f3be..0000000000000000000000000000000000000000
--- a/ttool/src/test/resources/tmltranslator/test_diplo_security_models/symetric.tmap
+++ /dev/null
@@ -1,24 +0,0 @@
-TMLSPEC
- #include "symetric.tml"
-ENDTMLSPEC
-
-TMLARCHI
- #include "symetric.tarchi"
-ENDTMLARCHI
-
-TMLMAPPING
- MAP CPUAlice SymmetricExchange__Alice
- SET SymmetricExchange__Alice priority 0
- MAP CPUBob SymmetricExchange__Bob
- SET SymmetricExchange__Bob priority 0
- MAP ExternalMemory SymmetricExchange__comm
- SET SymmetricExchange__comm priority 0
- MAP ExternalBus SymmetricExchange__comm
- SET SymmetricExchange__comm priority 0
- MAP BusAlice SymmetricExchange__comm
- SET SymmetricExchange__comm priority 0
- MAP BusBob SymmetricExchange__comm
- SET SymmetricExchange__comm priority 0
- MAPSEC MemoryAlice sym
- MAPSEC MemoryBob sym
-ENDTMLMAPPING