diff --git a/src/main/java/tmltranslator/TMLTextSpecification.java b/src/main/java/tmltranslator/TMLTextSpecification.java
index 827bb057ef18130a2055637f94f8c47c529e3cd5..a7903cc125494afd77332b0699c5947ae159f4bc 100755
--- a/src/main/java/tmltranslator/TMLTextSpecification.java
+++ b/src/main/java/tmltranslator/TMLTextSpecification.java
@@ -2792,11 +2792,18 @@ public class TMLTextSpecification<E> {
TraceManager.addDev("Found security pattern: " + _split[2]);
TMLExecC execc = new TMLExecC("encrypt_" + _split[2], null);
execc.setAction(_split[1]);
- execc.setSecurityPattern(securityPatternMap.get(_split[2]));
+ 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>());
+ }
+ if (!tmlm.getSecurityTaskMap().get(sp).contains(task)) {
+ tmlm.getSecurityTaskMap().get(sp).add(task);
+ }
tmlae.addNext(execc);
task.getActivityDiagram().addElement(execc);
tmlae = execc;
diff --git a/src/main/java/tmltranslator/toavatarsec/TML2Avatar.java b/src/main/java/tmltranslator/toavatarsec/TML2Avatar.java
index 1d8e9bbc5c327cccdeb07b2e725aa9dc26100013..55028efdc1288acee37263f7d7854a428054c862 100644
--- a/src/main/java/tmltranslator/toavatarsec/TML2Avatar.java
+++ b/src/main/java/tmltranslator/toavatarsec/TML2Avatar.java
@@ -812,11 +812,8 @@ public class TML2Avatar {
} else if (ae instanceof TMLActivityElementWithAction) {
//Might be encrypt or decrypt
- AvatarState as = new AvatarState(ae.getValue().replaceAll(
- " ", "").replaceAll("\\*", "").replaceAll("\\+", "").replaceAll(
- "\\-", "") + "_" + ae.getName().replaceAll(" ", "").replaceAll(
- "\\*", "").replaceAll("\\+", "").replaceAll(
- "\\-", ""), ae.getReferenceObject(), block);
+ AvatarState as = new AvatarState(reNameStateWithAction(ae.getValue()) + "_" + reNameStateWithAction(ae.getName()),
+ ae.getReferenceObject(), block);
tran = new AvatarTransition(block, "__after_" + ae.getName(), ae.getReferenceObject());
as.addNext(tran);
elementList.add(as);
@@ -1748,6 +1745,7 @@ public class TML2Avatar {
// checkChannels();
distributeKeys();
+ createSecElements(tasks);
TraceManager.addDev("ALL KEYS " + accessKeys);
/*for (TMLTask t: accessKeys.keySet()){
@@ -1870,7 +1868,6 @@ public class TML2Avatar {
}
//AvatarTransition last;
AvatarStateMachine asm = block.getStateMachine();
- createSecElements(task.getActivityDiagram(), block);
//TODO: Create a fork with many requests. This looks terrible
if (tmlmodel.getRequestToMe(task) != null) {
//Create iteration attribute
@@ -2727,6 +2724,15 @@ public class TML2Avatar {
ret = ret.replaceAll("-", "");
return ret;
}
+
+ private String reNameStateWithAction(String _name) {
+ Set<String> symbols = new HashSet<>(Arrays.asList(" ", "\\*", "\\+", "\\-", "\\/", "=", "\\)", "\\("));
+ for (String symb : symbols) {
+ _name = _name.replaceAll(symb, "");
+ }
+ return _name;
+ }
+
private String setNewAttributeName(String _attributeName, AvatarBlock _block) {
String newAttributeName = _attributeName + "0";
int indexAttribute = 0;
@@ -2737,185 +2743,188 @@ public class TML2Avatar {
return newAttributeName;
}
- private void createSecElements(TMLActivity activityDiagram, AvatarBlock block) {
- for (TMLActivityElement ae : activityDiagram.getElements()) {
- if (ae instanceof TMLActivityElementWithAction) {
- if (ae.getSecurityPattern() != null && ae instanceof TMLExecC) {
- //If encryption
- if (!((TMLExecC) ae).isDecryptionProcess()) {
- if ((!ae.getSecurityPattern().getNonce().isEmpty() || ae.getSecurityPattern().getType().equals(SecurityPattern.MAC_PATTERN)) &&
- block.getAvatarMethodWithName("concat2") == null) {
- //Create concat2 method
- AvatarAttribute msg1 = new AvatarAttribute("msg1", AvatarType.INTEGER, block, null);
- AvatarAttribute msg2 = new AvatarAttribute("msg2", AvatarType.INTEGER, block, null);
- AvatarAttribute ConcatedMsg = new AvatarAttribute("ConcatedMsg", AvatarType.INTEGER, block, null);
- AvatarMethod concat2 = new AvatarMethod("concat2", ae);
- concat2.addParameter(msg1);
- concat2.addParameter(msg2);
- concat2.addReturnParameter(ConcatedMsg);
- block.addMethod(concat2);
- }
- switch (ae.getSecurityPattern().getType()) {
- case SecurityPattern.SYMMETRIC_ENC_PATTERN:
- //Type Symmetric Encryption
- if (block.getAvatarMethodWithName("sencrypt") == null) {
- AvatarMethod sencrypt = new AvatarMethod("sencrypt", ae);
- AvatarAttribute msg = new AvatarAttribute("msg", AvatarType.INTEGER, block, null);
- AvatarAttribute key = new AvatarAttribute("key", AvatarType.INTEGER, block, null);
- AvatarAttribute encryptedMsg = new AvatarAttribute("encryptedMsg", AvatarType.INTEGER, block, null);
- sencrypt.addParameter(msg);
- sencrypt.addParameter(key);
- sencrypt.addReturnParameter(encryptedMsg);
- block.addMethod(sencrypt);
- }
- if (!ae.getSecurityPattern().getKey().isEmpty()) {
- AvatarAttribute encryptedKey = new AvatarAttribute("encryptedKey_" + ae.getSecurityPattern().getKey(),
- AvatarType.INTEGER, block, null);
- block.addAttribute(encryptedKey);
- secPatternEncAttribute.put(ae.getSecurityPattern(), encryptedKey);
- } else {
+ private void createSecElements(List<TMLTask> _tasks) {
+ for (TMLTask task : _tasks) {
+ AvatarBlock block = taskBlockMap.get(task);
+ for (TMLActivityElement ae : task.getActivityDiagram().getElements()) {
+ if (ae instanceof TMLActivityElementWithAction) {
+ if (ae.getSecurityPattern() != null && ae instanceof TMLExecC) {
+ //If encryption
+ if (!((TMLExecC) ae).isDecryptionProcess()) {
+ if ((!ae.getSecurityPattern().getNonce().isEmpty() || ae.getSecurityPattern().getType().equals(SecurityPattern.MAC_PATTERN)) &&
+ block.getAvatarMethodWithName("concat2") == null) {
+ //Create concat2 method
+ AvatarAttribute msg1 = new AvatarAttribute("msg1", AvatarType.INTEGER, block, null);
+ AvatarAttribute msg2 = new AvatarAttribute("msg2", AvatarType.INTEGER, block, null);
+ AvatarAttribute ConcatedMsg = new AvatarAttribute("ConcatedMsg", AvatarType.INTEGER, block, null);
+ AvatarMethod concat2 = new AvatarMethod("concat2", ae);
+ concat2.addParameter(msg1);
+ concat2.addParameter(msg2);
+ concat2.addReturnParameter(ConcatedMsg);
+ block.addMethod(concat2);
+ }
+ switch (ae.getSecurityPattern().getType()) {
+ case SecurityPattern.SYMMETRIC_ENC_PATTERN:
+ //Type Symmetric Encryption
+ if (block.getAvatarMethodWithName("sencrypt") == null) {
+ AvatarMethod sencrypt = new AvatarMethod("sencrypt", ae);
+ AvatarAttribute msg = new AvatarAttribute("msg", AvatarType.INTEGER, block, null);
+ AvatarAttribute key = new AvatarAttribute("key", AvatarType.INTEGER, block, null);
+ AvatarAttribute encryptedMsg = new AvatarAttribute("encryptedMsg", AvatarType.INTEGER, block, null);
+ sencrypt.addParameter(msg);
+ sencrypt.addParameter(key);
+ sencrypt.addReturnParameter(encryptedMsg);
+ block.addMethod(sencrypt);
+ }
+ if (!ae.getSecurityPattern().getKey().isEmpty()) {
+ AvatarAttribute encryptedKey = new AvatarAttribute("encryptedKey_" + ae.getSecurityPattern().getKey(),
+ AvatarType.INTEGER, block, null);
+ block.addAttribute(encryptedKey);
+ secPatternEncAttribute.put(ae.getSecurityPattern(), encryptedKey);
+ } else {
+ AvatarAttribute msgEncrypted = new AvatarAttribute(ae.getSecurityPattern().getName() + "_encrypted", AvatarType.INTEGER
+ , block, null);
+ block.addAttribute(msgEncrypted);
+ secPatternEncAttribute.put(ae.getSecurityPattern(), msgEncrypted);
+ }
+ break;
+ case SecurityPattern.ASYMMETRIC_ENC_PATTERN:
+ if (block.getAvatarMethodWithName("aencrypt") == null) {
+ AvatarMethod aencrypt = new AvatarMethod("aencrypt", ae);
+ AvatarAttribute msg = new AvatarAttribute("msg", AvatarType.INTEGER, block, null);
+ AvatarAttribute pubKey = new AvatarAttribute("pubKey", AvatarType.INTEGER, block, null);
+ AvatarAttribute encryptedMsg = new AvatarAttribute("encryptedMsg", AvatarType.INTEGER, block, null);
+ aencrypt.addParameter(msg);
+ aencrypt.addParameter(pubKey);
+ aencrypt.addReturnParameter(encryptedMsg);
+ block.addMethod(aencrypt);
+ }
+ if (!ae.getSecurityPattern().getKey().isEmpty()) {
+ AvatarAttribute encryptedKey = new AvatarAttribute("encryptedKey_" + ae.getSecurityPattern().getKey(),
+ AvatarType.INTEGER, block, null);
+ block.addAttribute(encryptedKey);
+ secPatternEncAttribute.put(ae.getSecurityPattern(), encryptedKey);
+ } else {
+ AvatarAttribute msgEncrypted = new AvatarAttribute(ae.getSecurityPattern().getName() + "_encrypted", AvatarType.INTEGER
+ , block, null);
+ block.addAttribute(msgEncrypted);
+ secPatternEncAttribute.put(ae.getSecurityPattern(), msgEncrypted);
+ }
+ break;
+ case SecurityPattern.HASH_PATTERN: {
+ if (block.getAvatarMethodWithName("hash") == null) {
+ AvatarMethod hash = new AvatarMethod("hash", ae);
+ AvatarAttribute msg = new AvatarAttribute("msg", AvatarType.INTEGER, block, null);
+ AvatarAttribute res = new AvatarAttribute("res", AvatarType.INTEGER, block, null);
+ hash.addParameter(msg);
+ hash.addReturnParameter(res);
+ block.addMethod(hash);
+ }
AvatarAttribute msgEncrypted = new AvatarAttribute(ae.getSecurityPattern().getName() + "_encrypted", AvatarType.INTEGER
, block, null);
block.addAttribute(msgEncrypted);
secPatternEncAttribute.put(ae.getSecurityPattern(), msgEncrypted);
+ break;
}
- break;
- case SecurityPattern.ASYMMETRIC_ENC_PATTERN:
- if (block.getAvatarMethodWithName("aencrypt") == null) {
- AvatarMethod aencrypt = new AvatarMethod("aencrypt", ae);
- AvatarAttribute msg = new AvatarAttribute("msg", AvatarType.INTEGER, block, null);
- AvatarAttribute pubKey = new AvatarAttribute("pubKey", AvatarType.INTEGER, block, null);
- AvatarAttribute encryptedMsg = new AvatarAttribute("encryptedMsg", AvatarType.INTEGER, block, null);
- aencrypt.addParameter(msg);
- aencrypt.addParameter(pubKey);
- aencrypt.addReturnParameter(encryptedMsg);
- block.addMethod(aencrypt);
- }
- if (!ae.getSecurityPattern().getKey().isEmpty()) {
- AvatarAttribute encryptedKey = new AvatarAttribute("encryptedKey_" + ae.getSecurityPattern().getKey(),
- AvatarType.INTEGER, block, null);
- block.addAttribute(encryptedKey);
- secPatternEncAttribute.put(ae.getSecurityPattern(), encryptedKey);
- } else {
- AvatarAttribute msgEncrypted = new AvatarAttribute(ae.getSecurityPattern().getName() + "_encrypted", AvatarType.INTEGER
- , block, null);
+ case SecurityPattern.MAC_PATTERN: {
+ if (block.getAvatarMethodWithName("MAC") == null) {
+ AvatarMethod mac = new AvatarMethod("MAC", ae);
+ AvatarAttribute msg = new AvatarAttribute("msg", AvatarType.INTEGER, block, null);
+ AvatarAttribute key = new AvatarAttribute("key", AvatarType.INTEGER, block, null);
+ AvatarAttribute encryptedMsg = new AvatarAttribute("encryptedMsg", AvatarType.INTEGER, block, null);
+ mac.addParameter(msg);
+ mac.addParameter(key);
+ mac.addReturnParameter(encryptedMsg);
+ block.addMethod(mac);
+ }
+ AvatarAttribute msgEncrypted = new AvatarAttribute(ae.getSecurityPattern().getName() + "_encrypted", AvatarType.INTEGER,
+ block, null);
block.addAttribute(msgEncrypted);
secPatternEncAttribute.put(ae.getSecurityPattern(), msgEncrypted);
+ break;
}
- break;
- case SecurityPattern.HASH_PATTERN: {
- if (block.getAvatarMethodWithName("hash") == null) {
- AvatarMethod hash = new AvatarMethod("hash", ae);
- AvatarAttribute msg = new AvatarAttribute("msg", AvatarType.INTEGER, block, null);
- AvatarAttribute res = new AvatarAttribute("res", AvatarType.INTEGER, block, null);
- hash.addParameter(msg);
- hash.addReturnParameter(res);
- block.addMethod(hash);
- }
- AvatarAttribute msgEncrypted = new AvatarAttribute(ae.getSecurityPattern().getName() + "_encrypted", AvatarType.INTEGER
- , block, null);
- block.addAttribute(msgEncrypted);
- secPatternEncAttribute.put(ae.getSecurityPattern(), msgEncrypted);
- break;
}
- case SecurityPattern.MAC_PATTERN: {
- if (block.getAvatarMethodWithName("MAC") == null) {
- AvatarMethod mac = new AvatarMethod("MAC", ae);
- AvatarAttribute msg = new AvatarAttribute("msg", AvatarType.INTEGER, block, null);
- AvatarAttribute key = new AvatarAttribute("key", AvatarType.INTEGER, block, null);
- AvatarAttribute encryptedMsg = new AvatarAttribute("encryptedMsg", AvatarType.INTEGER, block, null);
- mac.addParameter(msg);
- mac.addParameter(key);
- mac.addReturnParameter(encryptedMsg);
- block.addMethod(mac);
- }
- AvatarAttribute msgEncrypted = new AvatarAttribute(ae.getSecurityPattern().getName() + "_encrypted", AvatarType.INTEGER,
- block, null);
- block.addAttribute(msgEncrypted);
- secPatternEncAttribute.put(ae.getSecurityPattern(), msgEncrypted);
- break;
+ } else {
+ //Decryption action
+ if ((!ae.getSecurityPattern().getNonce().isEmpty() || ae.getSecurityPattern().getType().equals(SecurityPattern.MAC_PATTERN))
+ && block.getAvatarMethodWithName("get2") == null) {
+ //Add get2 method
+ AvatarMethod get2 = new AvatarMethod("get2", ae);
+ AvatarAttribute msg = new AvatarAttribute("msg", AvatarType.INTEGER, block, null);
+ AvatarAttribute msg1 = new AvatarAttribute("msg1", AvatarType.INTEGER, block, null);
+ AvatarAttribute msg2 = new AvatarAttribute("msg2", AvatarType.INTEGER, block, null);
+ get2.addParameter(msg);
+ get2.addParameter(msg1);
+ get2.addParameter(msg2);
+ block.addMethod(get2);
}
- }
- } else {
- //Decryption action
- if ((!ae.getSecurityPattern().getNonce().isEmpty() || ae.getSecurityPattern().getType().equals(SecurityPattern.MAC_PATTERN))
- && block.getAvatarMethodWithName("get2") == null) {
- //Add get2 method
- AvatarMethod get2 = new AvatarMethod("get2", ae);
- AvatarAttribute msg = new AvatarAttribute("msg", AvatarType.INTEGER, block, null);
- AvatarAttribute msg1 = new AvatarAttribute("msg1", AvatarType.INTEGER, block, null);
- AvatarAttribute msg2 = new AvatarAttribute("msg2", AvatarType.INTEGER, block, null);
- get2.addParameter(msg);
- get2.addParameter(msg1);
- get2.addParameter(msg2);
- block.addMethod(get2);
- }
- switch (ae.getSecurityPattern().getType()) {
- case SecurityPattern.SYMMETRIC_ENC_PATTERN: {
- if (block.getAvatarMethodWithName("sdecrypt") == null) {
- AvatarMethod sdecrypt = new AvatarMethod("sdecrypt", ae);
- AvatarAttribute msgToDecrypt = new AvatarAttribute("msgToDecrypt", AvatarType.INTEGER, block, null);
- AvatarAttribute key = new AvatarAttribute("key", AvatarType.INTEGER, block, null);
- AvatarAttribute msgDecrypted = new AvatarAttribute("msgDecrypted", AvatarType.INTEGER, block, null);
- sdecrypt.addParameter(msgToDecrypt);
- sdecrypt.addParameter(key);
- sdecrypt.addReturnParameter(msgDecrypted);
- block.addMethod(sdecrypt);
- }
- if (!ae.getSecurityPattern().getKey().isEmpty()) {
- AvatarAttribute keyToDecrypt = new AvatarAttribute("encryptedKey_" + ae.getSecurityPattern().getKey(), AvatarType.INTEGER, block, null);
- block.addAttribute(keyToDecrypt);
- secPatternDecAttribute.put(ae.getSecurityPattern(), keyToDecrypt);
- } else {
- AvatarAttribute msgToDecrypt = new AvatarAttribute(ae.getSecurityPattern().getName() + "_encrypted", AvatarType.INTEGER, block, null);
- block.addAttribute(msgToDecrypt);
- secPatternDecAttribute.put(ae.getSecurityPattern(), msgToDecrypt);
+ switch (ae.getSecurityPattern().getType()) {
+ case SecurityPattern.SYMMETRIC_ENC_PATTERN: {
+ if (block.getAvatarMethodWithName("sdecrypt") == null) {
+ AvatarMethod sdecrypt = new AvatarMethod("sdecrypt", ae);
+ AvatarAttribute msgToDecrypt = new AvatarAttribute("msgToDecrypt", AvatarType.INTEGER, block, null);
+ AvatarAttribute key = new AvatarAttribute("key", AvatarType.INTEGER, block, null);
+ AvatarAttribute msgDecrypted = new AvatarAttribute("msgDecrypted", AvatarType.INTEGER, block, null);
+ sdecrypt.addParameter(msgToDecrypt);
+ sdecrypt.addParameter(key);
+ sdecrypt.addReturnParameter(msgDecrypted);
+ block.addMethod(sdecrypt);
+ }
+ if (!ae.getSecurityPattern().getKey().isEmpty()) {
+ AvatarAttribute keyToDecrypt = new AvatarAttribute("encryptedKey_" + ae.getSecurityPattern().getKey(), AvatarType.INTEGER, block, null);
+ block.addAttribute(keyToDecrypt);
+ secPatternDecAttribute.put(ae.getSecurityPattern(), keyToDecrypt);
+ } else {
+ AvatarAttribute msgToDecrypt = new AvatarAttribute(ae.getSecurityPattern().getName() + "_encrypted", AvatarType.INTEGER, block, null);
+ block.addAttribute(msgToDecrypt);
+ secPatternDecAttribute.put(ae.getSecurityPattern(), msgToDecrypt);
+ }
+ break;
}
- break;
- }
- case SecurityPattern.ASYMMETRIC_ENC_PATTERN: {
- if (block.getAvatarMethodWithName("adecrypt") == null) {
- AvatarMethod adecrypt = new AvatarMethod("adecrypt", ae);
- AvatarAttribute msgToDecrypt = new AvatarAttribute("msgToDecrypt", AvatarType.INTEGER, block, null);
- AvatarAttribute privKey = new AvatarAttribute("privKey", AvatarType.INTEGER, block, null);
- AvatarAttribute msgDecrypted = new AvatarAttribute("msgDecrypted", AvatarType.INTEGER, block, null);
- adecrypt.addParameter(msgToDecrypt);
- adecrypt.addParameter(privKey);
- adecrypt.addReturnParameter(msgDecrypted);
- block.addMethod(adecrypt);
+ case SecurityPattern.ASYMMETRIC_ENC_PATTERN: {
+ if (block.getAvatarMethodWithName("adecrypt") == null) {
+ AvatarMethod adecrypt = new AvatarMethod("adecrypt", ae);
+ AvatarAttribute msgToDecrypt = new AvatarAttribute("msgToDecrypt", AvatarType.INTEGER, block, null);
+ AvatarAttribute privKey = new AvatarAttribute("privKey", AvatarType.INTEGER, block, null);
+ AvatarAttribute msgDecrypted = new AvatarAttribute("msgDecrypted", AvatarType.INTEGER, block, null);
+ adecrypt.addParameter(msgToDecrypt);
+ adecrypt.addParameter(privKey);
+ adecrypt.addReturnParameter(msgDecrypted);
+ block.addMethod(adecrypt);
+ }
+ if (!ae.getSecurityPattern().getKey().isEmpty()) {
+ AvatarAttribute keyToDecrypt = new AvatarAttribute("encryptedKey_" + ae.getSecurityPattern().getKey(),
+ AvatarType.INTEGER, block, null);
+ block.addAttribute(keyToDecrypt);
+ secPatternDecAttribute.put(ae.getSecurityPattern(), keyToDecrypt);
+ } else {
+ AvatarAttribute msgToDecrypt = new AvatarAttribute(ae.getSecurityPattern().getName() + "_encrypted", AvatarType.INTEGER,
+ block, null);
+ block.addAttribute(msgToDecrypt);
+ secPatternDecAttribute.put(ae.getSecurityPattern(), msgToDecrypt);
+ }
+ break;
}
- if (!ae.getSecurityPattern().getKey().isEmpty()) {
- AvatarAttribute keyToDecrypt = new AvatarAttribute("encryptedKey_" + ae.getSecurityPattern().getKey(),
- AvatarType.INTEGER, block, null);
- block.addAttribute(keyToDecrypt);
- secPatternDecAttribute.put(ae.getSecurityPattern(), keyToDecrypt);
- } else {
+ case SecurityPattern.MAC_PATTERN: {
AvatarAttribute msgToDecrypt = new AvatarAttribute(ae.getSecurityPattern().getName() + "_encrypted", AvatarType.INTEGER,
block, null);
block.addAttribute(msgToDecrypt);
secPatternDecAttribute.put(ae.getSecurityPattern(), msgToDecrypt);
+ //Add verifymac method
+ if (block.getAvatarMethodWithName("verifyMAC") == null) {
+ AvatarMethod verifymac = new AvatarMethod("verifyMAC", ae);
+ AvatarAttribute msg = new AvatarAttribute("msg", AvatarType.INTEGER, block, null);
+ verifymac.addParameter(msg);
+ AvatarAttribute keyMAC = new AvatarAttribute("key", AvatarType.INTEGER, block, null);
+ verifymac.addParameter(keyMAC);
+ AvatarAttribute macMsg = new AvatarAttribute("mac", AvatarType.INTEGER, block, null);
+ verifymac.addParameter(macMsg);
+ AvatarAttribute testNonce = new AvatarAttribute("testNonce", AvatarType.BOOLEAN, block, null);
+ verifymac.addReturnParameter(testNonce);
+ block.addMethod(verifymac);
+ }
+ break;
}
- break;
- }
- case SecurityPattern.MAC_PATTERN: {
- AvatarAttribute msgToDecrypt = new AvatarAttribute(ae.getSecurityPattern().getName() + "_encrypted", AvatarType.INTEGER,
- block, null);
- block.addAttribute(msgToDecrypt);
- secPatternDecAttribute.put(ae.getSecurityPattern(), msgToDecrypt);
- //Add verifymac method
- if (block.getAvatarMethodWithName("verifyMAC") == null) {
- AvatarMethod verifymac = new AvatarMethod("verifyMAC", ae);
- AvatarAttribute msg = new AvatarAttribute("msg", AvatarType.INTEGER, block, null);
- verifymac.addParameter(msg);
- AvatarAttribute keyMAC = new AvatarAttribute("key", AvatarType.INTEGER, block, null);
- verifymac.addParameter(keyMAC);
- AvatarAttribute macMsg = new AvatarAttribute("mac", AvatarType.INTEGER, block, null);
- verifymac.addParameter(macMsg);
- AvatarAttribute testNonce = new AvatarAttribute("testNonce", AvatarType.BOOLEAN, block, null);
- verifymac.addReturnParameter(testNonce);
- block.addMethod(verifymac);
- }
- break;
}
}
}
diff --git a/ttool/src/test/java/test/AbstractTest.java b/ttool/src/test/java/test/AbstractTest.java
index 8916e05d54ec949901bb02d5f02411c6d6f67da1..e8f1a900bb4c658837606a179309f502ad5cbfcd 100644
--- a/ttool/src/test/java/test/AbstractTest.java
+++ b/ttool/src/test/java/test/AbstractTest.java
@@ -244,6 +244,7 @@ public abstract class AbstractTest {
if (summaryFound){
if (outputLine.startsWith(PROVERIF_QUERY_PREFIX)){
if (!idIssue) {
+ TraceManager.addDev("ProVerif Output : " + outputLine);
if (golden.contains(outputLine)) {
checked += 1;
} else {
diff --git a/ttool/src/test/java/tmltranslator/DiplodocusSecurityTest.java b/ttool/src/test/java/tmltranslator/DiplodocusSecurityTest.java
index 6495620d0713828b34b1c1d048ea0dc21d276ed9..b9c99314a85d4d18d08037831eeccbac0ecfbd42 100644
--- a/ttool/src/test/java/tmltranslator/DiplodocusSecurityTest.java
+++ b/ttool/src/test/java/tmltranslator/DiplodocusSecurityTest.java
@@ -62,12 +62,12 @@ public class DiplodocusSecurityTest extends AbstractTest {
public static Collection models() {
return Arrays.asList(new Object[][] {
//TODO : repair AliceAndBobHW pvspec generation
- //{"AliceAndBobHW", new ArrayList<>(Arrays.asList("SymmetricExchange", "Nonce", "KeyExchange", "Mac", "SampleAutoSec"))},
+ {"AliceAndBobHW", new ArrayList<>(Arrays.asList("SymmetricExchange", "Nonce", "KeyExchange", "Mac", "SampleAutoSec"))},
{"ITA01_v6", new ArrayList<>(Arrays.asList("mapAtt", "mapNoProtection"))},
- {"Rovers_SPARTA_DIPLO", new ArrayList<>(Arrays.asList("NoCountermeasureMapping", "MACMapping"))},
+ //{"Rovers_SPARTA_DIPLO", new ArrayList<>(Arrays.asList("NoCountermeasureMapping", "MACMapping"))},
// "SymmetricEncryptionNonceMapping" and "Rover" tabs give empty security pragmas from Rovers_SPARTA_DIPLO model
//TODO : repair ITSDemo model
- //{"ITSDemo", new ArrayList<>(Arrays.asList("Architecture_enc_or", "Architecture_hsm"))}
+ {"ITSDemo", new ArrayList<>(Arrays.asList("Architecture", "Architecture_hsm"))}
});
}
@@ -150,7 +150,7 @@ public class DiplodocusSecurityTest extends AbstractTest {
TraceManager.addDev("The golden for : " + tab + " is null");
fail();
}
- Assert.assertTrue(executeAndVerifyPvspec(PROVERIF_DIR + pvspecFilename, goldenMap.get(tab), true));
+ Assert.assertTrue(executeAndVerifyPvspec(PROVERIF_DIR + pvspecFilename, goldenMap.get(tab)));
TraceManager.addDev("Test for " + tab + " tab is ended");
}
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/KeyExchange/golden b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/KeyExchange/golden
index 91a14cab663acd08bc1b97a63eeef04d61927d14..8d545deb41fda10169d08559ea8164ac150e7bff 100644
--- a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/KeyExchange/golden
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/KeyExchange/golden
@@ -1,5 +1,4 @@
-Query not attacker(Alice___KeyExchange__comm_chData[!1 = v]) is true.
-Query not attacker(Alice___aenc[!1 = v]) is true.
+Query not attacker(Alice___symKey_encrypted0[!1 = v]) is true.
+Query not attacker(Alice___encryptedKey_symKey0[!1 = v]) is true.
Query not attacker(Alice___symKey[!1 = v]) is true.
-Query inj-event(authenticity___Bob___symKey___execc_dummy294(dummyM)) ==> inj-event(authenticity___Alice___symKey____execc222(dummyM)) is true.
-Query inj-event(authenticity___Bob___aenc___execc_dummy(dummyM)) ==> inj-event(authenticity___Alice___aenc____execc(dummyM)) is false.
+Query inj-event(authenticity___Bob___symKey___decrypt_symKey_dummy(dummyM)) ==> inj-event(authenticity___Alice___symKey____encrypt_symKey(dummyM)) is false.
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/Mac/golden b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/Mac/golden
index 628c9686ab48d2a7c2571d044d65ff4d1ff369f6..1dcbafbf38f4304d169b35f2b4099e6d97464d5c 100644
--- a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/Mac/golden
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/Mac/golden
@@ -1,3 +1,3 @@
-Query not attacker(Alice___MAC__comm_chData[!1 = v]) is true.
+Query not attacker(Alice___mac_encrypted0[!1 = v]) is true.
Query not attacker(Alice___mac[!1 = v]) is false.
-Query inj-event(authenticity___Bob___mac___execc_dummy(dummyM)) ==> inj-event(authenticity___Alice___mac____execc(dummyM)) is false.
+Query inj-event(authenticity___Bob___mac___decrypt_mac_dummy(dummyM)) ==> inj-event(authenticity___Alice___mac____encrypt_mac(dummyM)) is false.
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/Nonce/golden b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/Nonce/golden
index e1f3c9e0233198f5d07f377724c861407fbdfaf6..aef45a7b2f3c4fe345d0c7472ba88cb79543cdd0 100644
--- a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/Nonce/golden
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/Nonce/golden
@@ -1,3 +1,3 @@
-Query not attacker(Alice___nonce__comm_chData[!1 = v]) is true.
+Query not attacker(Alice___symN_encrypted0[!1 = v]) is true.
Query not attacker(Alice___symN[!1 = v]) is true.
-Query inj-event(authenticity___Bob___symN___execc_dummy(dummyM)) ==> inj-event(authenticity___Alice___symN____execc(dummyM)) is false.
+Query inj-event(authenticity___Bob___symN___decrypt_symN_dummy(dummyM)) ==> inj-event(authenticity___Alice___symN____encrypt_symN(dummyM)) is true.
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/SampleAutoSec/golden b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/SampleAutoSec/golden
index c2984028e52a3bb4da95bdbc6541d8901d6abb57..d88079628943f03466e01c4f2d0c697fb3ff70c0 100644
--- a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/SampleAutoSec/golden
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/SampleAutoSec/golden
@@ -1,2 +1,2 @@
-Query not attacker(Alice___sampleAutoSec__comm_chData[!1 = v]) is false.
-Query inj-event(authenticity___Bob___comm_chData___aftersignalstate_sampleAutoSec_comm_sampleAutoSec_comm(dummyM)) ==> inj-event(authenticity___Alice___comm_chData___signalstate_sampleAutoSec_comm_sampleAutoSec_comm(dummyM)) is false.
+Query not attacker(Alice___comm_chData0[!1 = v]) is false.
+Query inj-event(authenticity___Bob___comm_chData0___aftersignalstate_sampleAutoSec_comm_sampleAutoSec_comm(dummyM)) ==> inj-event(authenticity___Alice___comm_chData0___signalstate_sampleAutoSec_comm_sampleAutoSec_comm(dummyM)) is false.
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/SymmetricExchange/golden b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/SymmetricExchange/golden
index d56967036247800fb59e594c2999529c9a69f15f..6cfc6ccc3c7d84bc129bdeb238010719c8077222 100644
--- a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/SymmetricExchange/golden
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/SymmetricExchange/golden
@@ -1,3 +1,3 @@
-Query not attacker(Alice___SymmetricExchange__comm_chData[!1 = v]) is true.
+Query not attacker(Alice___sym_encrypted0[!1 = v]) is true.
Query not attacker(Alice___sym[!1 = v]) is true.
-Query inj-event(authenticity___Bob___sym___execc_dummy(dummyM)) ==> inj-event(authenticity___Alice___sym____execc(dummyM)) is false.
+Query inj-event(authenticity___Bob___sym___decrypt_sym_dummy(dummyM)) ==> inj-event(authenticity___Alice___sym____encrypt_sym(dummyM)) is false.
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v6/mapAtt/golden b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v6/mapAtt/golden
index 5ff21934da9d4ae8c04ab362881198e7f579ed1c..0dff9ba140518b8dd092bde29a76ea765e5e4178 100644
--- a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v6/mapAtt/golden
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v6/mapAtt/golden
@@ -1,7 +1,7 @@
-Query not attacker(BatterySensor___Application__battery_chData[!1 = v]) is true.
-Query not attacker(PumpController___Application__feedback4App_chData[!1 = v]) is true.
+Query not attacker(BatterySensor___battery_chData0[!1 = v]) is true.
+Query not attacker(PumpController___AES_CTRL_encrypted0[!1 = v]) is true.
Query not attacker(PumpController___AES_CTRL[!1 = v]) is true.
-Query not attacker(SmartphoneAppController___Application__emergencySign_chData[!1 = v]) is true.
+Query not attacker(SmartphoneAppController___AES_Emergency_encrypted0[!1 = v]) is true.
Query not attacker(SmartphoneAppController___AES_Emergency[!1 = v]) is true.
-Query inj-event(authenticity___MedicalInformationSystem___AES_Emergency___execc_dummy1224(dummyM)) ==> inj-event(authenticity___SmartphoneAppController___AES_Emergency____execc1077(dummyM)) is false.
-Query inj-event(authenticity___SmartphoneAppController___AES_CTRL___execc_dummy(dummyM)) ==> inj-event(authenticity___PumpController___AES_CTRL____execc(dummyM)) is false.
+Query inj-event(authenticity___MedicalInformationSystem___AES_Emergency___decrypt_AES_Emergency_dummy(dummyM)) ==> inj-event(authenticity___SmartphoneAppController___AES_Emergency____encrypt_AES_Emergency(dummyM)) is false.
+Query inj-event(authenticity___SmartphoneAppController___AES_CTRL___decrypt_AES_CTRL_dummy(dummyM)) ==> inj-event(authenticity___PumpController___AES_CTRL____encrypt_AES_CTRL(dummyM)) is false.
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v6/mapNoProtection/golden b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v6/mapNoProtection/golden
index 3970a75e07265469330b562168e49176d088a465..eee1ffc57ec7c55007be5fed8e8ef771018a072b 100644
--- a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v6/mapNoProtection/golden
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v6/mapNoProtection/golden
@@ -1,7 +1,7 @@
-Query not attacker(BatterySensor___Application__battery_chData[!1 = v]) is false.
-Query not attacker(PumpController___Application__feedback4App_chData[!1 = v]) is true.
-Query not attacker(PumpController___AES_CTRL[!1 = v]) is true.
-Query not attacker(SmartphoneAppController___Application__emergencySign_chData[!1 = v]) is true.
-Query not attacker(SmartphoneAppController___AES_Emergency[!1 = v]) is true.
-Query inj-event(authenticity___MedicalInformationSystem___AES_Emergency___execc_dummy2610(dummyM)) ==> inj-event(authenticity___SmartphoneAppController___AES_Emergency____execc2463(dummyM)) is true.
-Query inj-event(authenticity___SmartphoneAppController___AES_CTRL___execc_dummy(dummyM)) ==> inj-event(authenticity___PumpController___AES_CTRL____execc(dummyM)) is true.
+Query not attacker(BatterySensor___battery_chData0[!1 = v]) is false.
+Query not attacker(PumpController___AES_CTRL_encrypted0[!1 = v]) is true.
+Query not attacker(PumpController___AES_CTRL[!1 = v]) is false.
+Query not attacker(SmartphoneAppController___AES_Emergency_encrypted0[!1 = v]) is true.
+Query not attacker(SmartphoneAppController___AES_Emergency[!1 = v]) is false.
+Query inj-event(authenticity___MedicalInformationSystem___AES_Emergency___decrypt_AES_Emergency_dummy(dummyM)) ==> inj-event(authenticity___SmartphoneAppController___AES_Emergency____encrypt_AES_Emergency(dummyM)) is false.
+Query inj-event(authenticity___SmartphoneAppController___AES_CTRL___decrypt_AES_CTRL_dummy(dummyM)) ==> inj-event(authenticity___PumpController___AES_CTRL____encrypt_AES_CTRL(dummyM)) is false.
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture/golden b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture/golden
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..cd7595125c159429aadcbb50213af85cd5d1f2ed 100644
--- a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture/golden
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture/golden
@@ -0,0 +1,4 @@
+Query not attacker(GPSGateway___GPSdata_chData0[!1 = v]) is false.
+Query inj-event(authenticity___NavigationControl___GPSdata_chData0___aftersignalstate_App_GPSdata_App_GPSdata(dummyM)) ==> inj-event(authenticity___GPSGateway___GPSdata_chData0___signalstate_App_GPSdata_App_GPSdata(dummyM)) is false.
+Query inj-event(authenticity___vehicleControlGateway___vehData_chData0___aftersignalstate_App_vehData_App_vehData(dummyM)) ==> inj-event(authenticity___NavigationControl___vehData_chData0___signalstate_App_vehData_App_vehData(dummyM)) is false.
+Query inj-event(authenticity___NavigationControl___sensorData_chData0___aftersignalstate_App_sensorData_App_sensorData(dummyM)) ==> inj-event(authenticity___SensorUnit___sensorData_chData0___signalstate_App_sensorData_App_sensorData316(dummyM)) is false.
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture/spec.tarchi b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture/spec.tarchi
new file mode 100644
index 0000000000000000000000000000000000000000..0c680ed299a1f1b2118010b6ceaed4114c02986f
--- /dev/null
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture/spec.tarchi
@@ -0,0 +1,138 @@
+// Master clock frequency - in MHz
+MASTERCLOCKFREQUENCY 200
+
+NODE BRIDGE BridgeSensor
+SET BridgeSensor bufferByteSize 4
+SET BridgeSensor clockDivider 1
+
+NODE BRIDGE BridgeComm
+SET BridgeComm bufferByteSize 4
+SET BridgeComm clockDivider 1
+
+NODE BUS commBus
+SET commBus byteDataSize 4
+SET commBus pipelineSize 1
+SET commBus arbitration 0
+SET commBus sliceTime 10000
+SET commBus burstSize 100
+SET commBus privacy public
+SET commBus clockDivider 1
+
+NODE BUS InternalNavigationBus
+SET InternalNavigationBus byteDataSize 4
+SET InternalNavigationBus pipelineSize 1
+SET InternalNavigationBus arbitration 0
+SET InternalNavigationBus sliceTime 10000
+SET InternalNavigationBus burstSize 100
+SET InternalNavigationBus privacy private
+SET InternalNavigationBus clockDivider 1
+
+NODE CPU V2XCPU
+SET V2XCPU nbOfCores 1
+SET V2XCPU byteDataSize 4
+SET V2XCPU pipelineSize 5
+SET V2XCPU goIdleTime 10
+SET V2XCPU maxConsecutiveIdleCycles 10
+SET V2XCPU taskSwitchingTime 20
+SET V2XCPU branchingPredictionPenalty 2
+SET V2XCPU cacheMiss 5
+SET V2XCPU schedulingPolicy 0
+SET V2XCPU sliceTime 10000
+SET V2XCPU execiTime 1
+SET V2XCPU execcTime 1
+SET V2XCPU clockDivider 1
+
+NODE CPU controlCPU
+SET controlCPU nbOfCores 1
+SET controlCPU byteDataSize 4
+SET controlCPU pipelineSize 5
+SET controlCPU goIdleTime 10
+SET controlCPU maxConsecutiveIdleCycles 10
+SET controlCPU taskSwitchingTime 20
+SET controlCPU branchingPredictionPenalty 2
+SET controlCPU cacheMiss 5
+SET controlCPU schedulingPolicy 0
+SET controlCPU sliceTime 10000
+SET controlCPU execiTime 1
+SET controlCPU execcTime 1
+SET controlCPU clockDivider 1
+
+NODE CPU CPUSensor
+SET CPUSensor nbOfCores 1
+SET CPUSensor byteDataSize 4
+SET CPUSensor pipelineSize 5
+SET CPUSensor goIdleTime 10
+SET CPUSensor maxConsecutiveIdleCycles 10
+SET CPUSensor taskSwitchingTime 20
+SET CPUSensor branchingPredictionPenalty 2
+SET CPUSensor cacheMiss 5
+SET CPUSensor schedulingPolicy 0
+SET CPUSensor sliceTime 10000
+SET CPUSensor execiTime 1
+SET CPUSensor execcTime 1
+SET CPUSensor clockDivider 1
+
+NODE MEMORY MemoryNavigation
+SET MemoryNavigation byteDataSize 4
+SET MemoryNavigation clockDivider 1
+
+NODE BUS sensorBus
+SET sensorBus byteDataSize 4
+SET sensorBus pipelineSize 1
+SET sensorBus arbitration 1
+SET sensorBus sliceTime 10000
+SET sensorBus burstSize 100
+SET sensorBus privacy public
+SET sensorBus clockDivider 1
+
+NODE CPU CPU_Navigation
+SET CPU_Navigation nbOfCores 1
+SET CPU_Navigation byteDataSize 4
+SET CPU_Navigation pipelineSize 5
+SET CPU_Navigation goIdleTime 10
+SET CPU_Navigation maxConsecutiveIdleCycles 10
+SET CPU_Navigation taskSwitchingTime 20
+SET CPU_Navigation branchingPredictionPenalty 2
+SET CPU_Navigation cacheMiss 5
+SET CPU_Navigation schedulingPolicy 0
+SET CPU_Navigation sliceTime 10000
+SET CPU_Navigation execiTime 1
+SET CPU_Navigation execcTime 1
+SET CPU_Navigation clockDivider 1
+
+NODE LINK link_BridgeSensor_to_InternalNavigationBus
+SET link_BridgeSensor_to_InternalNavigationBus node BridgeSensor
+SET link_BridgeSensor_to_InternalNavigationBus bus InternalNavigationBus
+SET link_BridgeSensor_to_InternalNavigationBus priority 0
+NODE LINK link_BridgeSensor_to_sensorBus
+SET link_BridgeSensor_to_sensorBus node BridgeSensor
+SET link_BridgeSensor_to_sensorBus bus sensorBus
+SET link_BridgeSensor_to_sensorBus priority 0
+NODE LINK link_BridgeComm_to_commBus
+SET link_BridgeComm_to_commBus node BridgeComm
+SET link_BridgeComm_to_commBus bus commBus
+SET link_BridgeComm_to_commBus priority 0
+NODE LINK link_BridgeComm_to_InternalNavigationBus
+SET link_BridgeComm_to_InternalNavigationBus node BridgeComm
+SET link_BridgeComm_to_InternalNavigationBus bus InternalNavigationBus
+SET link_BridgeComm_to_InternalNavigationBus priority 0
+NODE LINK link_controlCPU_to_commBus
+SET link_controlCPU_to_commBus node controlCPU
+SET link_controlCPU_to_commBus bus commBus
+SET link_controlCPU_to_commBus priority 0
+NODE LINK link_MemoryNavigation_to_InternalNavigationBus
+SET link_MemoryNavigation_to_InternalNavigationBus node MemoryNavigation
+SET link_MemoryNavigation_to_InternalNavigationBus bus InternalNavigationBus
+SET link_MemoryNavigation_to_InternalNavigationBus priority 0
+NODE LINK link_CPU_Navigation_to_InternalNavigationBus
+SET link_CPU_Navigation_to_InternalNavigationBus node CPU_Navigation
+SET link_CPU_Navigation_to_InternalNavigationBus bus InternalNavigationBus
+SET link_CPU_Navigation_to_InternalNavigationBus priority 0
+NODE LINK link_V2XCPU_to_sensorBus
+SET link_V2XCPU_to_sensorBus node V2XCPU
+SET link_V2XCPU_to_sensorBus bus sensorBus
+SET link_V2XCPU_to_sensorBus priority 0
+NODE LINK link_CPUSensor_to_sensorBus
+SET link_CPUSensor_to_sensorBus node CPUSensor
+SET link_CPUSensor_to_sensorBus bus sensorBus
+SET link_CPUSensor_to_sensorBus priority 0
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture/spec.tmap b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture/spec.tmap
new file mode 100644
index 0000000000000000000000000000000000000000..d0248faf41144f37da8b128891728b8d6a07d07e
--- /dev/null
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture/spec.tmap
@@ -0,0 +1,44 @@
+TMLSPEC
+ #include "spec.tml"
+ENDTMLSPEC
+
+TMLARCHI
+ #include "spec.tarchi"
+ENDTMLARCHI
+
+TMLMAPPING
+ MAP V2XCPU App__V2XGateway
+ SET App__V2XGateway priority 0
+ MAP controlCPU App__vehicleControlGateway
+ SET App__vehicleControlGateway priority 0
+ MAP CPUSensor App__GPSGateway
+ SET App__GPSGateway priority 0
+ MAP CPUSensor App__SensorUnit
+ SET App__SensorUnit priority 0
+ MAP CPU_Navigation App__NavigationControl
+ SET App__NavigationControl priority 0
+ MAP MemoryNavigation App__GPSdata
+ SET App__GPSdata priority 5
+ MAP InternalNavigationBus App__GPSdata
+ SET App__GPSdata priority 5
+ MAP sensorBus App__GPSdata
+ SET App__GPSdata priority 5
+ MAP MemoryNavigation App__vehData
+ SET App__vehData priority 5
+ MAP InternalNavigationBus App__vehData
+ SET App__vehData priority 5
+ MAP commBus App__vehData
+ SET App__vehData priority 5
+ MAP MemoryNavigation App__V2Xdata
+ SET App__V2Xdata priority 5
+ MAP InternalNavigationBus App__V2Xdata
+ SET App__V2Xdata priority 5
+ MAP sensorBus App__V2Xdata
+ SET App__V2Xdata priority 5
+ MAP MemoryNavigation App__sensorData
+ SET App__sensorData priority 5
+ MAP InternalNavigationBus App__sensorData
+ SET App__sensorData priority 5
+ MAP sensorBus App__sensorData
+ SET App__sensorData priority 5
+ENDTMLMAPPING
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture/spec.tml b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture/spec.tml
new file mode 100644
index 0000000000000000000000000000000000000000..eb3f89445148c00550d4084ea533dba8ca081f5b
--- /dev/null
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture/spec.tml
@@ -0,0 +1,146 @@
+// TML Application - FORMAT 0.2
+// Generated: Tue Mar 26 18:11:43 CET 2024
+
+// PRAGMAS
+
+// Channels
+CHANNEL App__GPSdata NBRNBW 4 OUT App__GPSGateway IN App__NavigationControl
+VCCHANNEL App__GPSdata 0
+CONFCHANNEL App__GPSdata
+AUTHCHANNEL App__GPSdata
+CHANNEL App__V2Xdata NBRNBW 4 OUT App__V2XGateway IN App__NavigationControl
+VCCHANNEL App__V2Xdata 0
+CHANNEL App__sensorData NBRNBW 4 OUT App__SensorUnit IN App__NavigationControl
+VCCHANNEL App__sensorData 0
+AUTHCHANNEL App__sensorData
+CHANNEL App__vehData NBRNBW 4 OUT App__NavigationControl IN App__vehicleControlGateway
+VCCHANNEL App__vehData 0
+AUTHCHANNEL App__vehData
+
+// Events
+EVENT App__newV2X__App__newV2X() INF App__V2XGateway App__NavigationControl
+EVENT App__startGPS__App__startGPS() INF App__NavigationControl App__GPSGateway
+EVENT App__updateLoc__App__updateLoc() INF App__GPSGateway App__NavigationControl
+EVENT App__updateSensor__App__updateSensor() INF App__SensorUnit App__NavigationControl
+
+// Requests
+
+TASK App__GPSGateway
+ TASKOP
+ //Local variables
+ int processCommand = 100
+ int iteration
+ int loop_0 = 0
+
+ //Behavior
+ WAIT App__startGPS__App__startGPS
+ FOR(loop_0 = 0; loop_0<10; loop_0 = loop_0 + 1)
+ EXECI processCommand
+ NOTIFY App__updateLoc__App__updateLoc
+ WRITE App__GPSdata 1
+ ENDFOR
+ENDTASK
+
+TASK App__NavigationControl
+ TASKOP
+ //Local variables
+ int forgeCommand = 250
+ int calculateRoute
+ int calculateObstacle = 250
+ int initialize = 300
+ int updateTraffic
+ int i = 0
+ int processErr
+ int processV2X
+
+ //Behavior
+ EXECC initialize
+ NOTIFY App__startGPS__App__startGPS
+ FOR(i=0; i<10; i = i+1)
+ SELECTEVT
+ CASE App__newV2X__App__newV2X
+ READ App__V2Xdata 10
+ EXECI processV2X
+ ENDCASE
+ CASE App__updateLoc__App__updateLoc
+ READ App__GPSdata 1
+ EXECC calculateRoute
+ RAND
+ CASERAND 50
+ EXECC forgeCommand
+ WRITE App__vehData 10
+ ENDCASERAND
+ CASERAND 50
+ EXECC processErr
+ ENDCASERAND
+ ENDRAND
+ ENDCASE
+ CASE App__updateSensor__App__updateSensor
+ READ App__sensorData 1
+ EXECC calculateObstacle
+ ENDCASE
+ ENDSELECTEVT
+ ENDFOR
+ENDTASK
+
+TASK App__SensorUnit
+ TASKOP
+ //Local variables
+ int updateInterval
+ int sampleNum
+ int convert = 100
+ bool error
+ int plausibilityCheck = 150
+ int loop_0 = 0
+
+ //Behavior
+ FOR(loop_0 = 0; loop_0<10; loop_0 = loop_0 + 1)
+ EXECI (convert)+(plausibilityCheck)
+ RAND
+ CASERAND 50
+ NOTIFY App__updateSensor__App__updateSensor
+ WRITE App__sensorData 1
+ ENDCASERAND
+ CASERAND 50
+ error=true
+ ENDCASERAND
+ ENDRAND
+ ENDFOR
+ENDTASK
+
+TASK App__V2XGateway
+ TASKOP
+ //Local variables
+ int processCommand = 100
+ int loop_0 = 0
+
+ //Behavior
+ FOR(loop_0 = 0; loop_0<10; loop_0 = loop_0 + 1)
+ EXECI processCommand
+ NOTIFY App__newV2X__App__newV2X
+ WRITE App__V2Xdata 10
+ ENDFOR
+ENDTASK
+
+TASK App__vehicleControlGateway
+ TASKOP
+ //Local variables
+ int index
+ int calc = 100
+ int recalculate = 220
+ int loop_0 = 0
+
+ //Behavior
+ FOR(loop_0 = 0; loop_0<10; loop_0 = loop_0 + 1)
+ EXECI calc
+ RAND
+ CASERAND 50
+ READ App__vehData 1
+ ENDCASERAND
+ CASERAND 50
+ EXECI recalculate
+ ENDCASERAND
+ ENDRAND
+ ENDFOR
+ENDTASK
+
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture_enc_or/spec.tarchi b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture_enc_or/spec.tarchi
index eb91e80f96e2f0186d655907be76636d4155a94c..e9db433576d911bfbd8492d8d565b103abf50492 100644
--- a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture_enc_or/spec.tarchi
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture_enc_or/spec.tarchi
@@ -1,6 +1,14 @@
// Master clock frequency - in MHz
MASTERCLOCKFREQUENCY 200
+NODE BRIDGE BridgeComm
+SET BridgeComm bufferByteSize 4
+SET BridgeComm clockDivider 1
+
+NODE BRIDGE BridgeSensor
+SET BridgeSensor bufferByteSize 4
+SET BridgeSensor clockDivider 1
+
NODE MEMORY MemoryControl
SET MemoryControl byteDataSize 4
SET MemoryControl clockDivider 1
@@ -118,6 +126,22 @@ SET CPU_Navigation execiTime 1
SET CPU_Navigation execcTime 1
SET CPU_Navigation clockDivider 1
+NODE LINK link_BridgeComm_to_commBus
+SET link_BridgeComm_to_commBus node BridgeComm
+SET link_BridgeComm_to_commBus bus commBus
+SET link_BridgeComm_to_commBus priority 0
+NODE LINK link_BridgeComm_to_InternalNavigationBus
+SET link_BridgeComm_to_InternalNavigationBus node BridgeComm
+SET link_BridgeComm_to_InternalNavigationBus bus InternalNavigationBus
+SET link_BridgeComm_to_InternalNavigationBus priority 0
+NODE LINK link_BridgeSensor_to_InternalNavigationBus
+SET link_BridgeSensor_to_InternalNavigationBus node BridgeSensor
+SET link_BridgeSensor_to_InternalNavigationBus bus InternalNavigationBus
+SET link_BridgeSensor_to_InternalNavigationBus priority 0
+NODE LINK link_BridgeSensor_to_sensorBus
+SET link_BridgeSensor_to_sensorBus node BridgeSensor
+SET link_BridgeSensor_to_sensorBus bus sensorBus
+SET link_BridgeSensor_to_sensorBus priority 0
NODE LINK link_MemoryControl_to_privControlBus
SET link_MemoryControl_to_privControlBus node MemoryControl
SET link_MemoryControl_to_privControlBus bus privControlBus
@@ -138,10 +162,6 @@ NODE LINK link_controlCPU_to_commBus
SET link_controlCPU_to_commBus node controlCPU
SET link_controlCPU_to_commBus bus commBus
SET link_controlCPU_to_commBus priority 0
-NODE LINK link_CPU_Navigation_to_commBus
-SET link_CPU_Navigation_to_commBus node CPU_Navigation
-SET link_CPU_Navigation_to_commBus bus commBus
-SET link_CPU_Navigation_to_commBus priority 0
NODE LINK link_MemoryNavigation_to_InternalNavigationBus
SET link_MemoryNavigation_to_InternalNavigationBus node MemoryNavigation
SET link_MemoryNavigation_to_InternalNavigationBus bus InternalNavigationBus
@@ -150,10 +170,6 @@ NODE LINK link_CPU_Navigation_to_InternalNavigationBus
SET link_CPU_Navigation_to_InternalNavigationBus node CPU_Navigation
SET link_CPU_Navigation_to_InternalNavigationBus bus InternalNavigationBus
SET link_CPU_Navigation_to_InternalNavigationBus priority 0
-NODE LINK link_CPU_Navigation_to_sensorBus
-SET link_CPU_Navigation_to_sensorBus node CPU_Navigation
-SET link_CPU_Navigation_to_sensorBus bus sensorBus
-SET link_CPU_Navigation_to_sensorBus priority 0
NODE LINK link_V2XCPU_to_sensorBus
SET link_V2XCPU_to_sensorBus node V2XCPU
SET link_V2XCPU_to_sensorBus bus sensorBus
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture_enc_or/spec.tmap b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture_enc_or/spec.tmap
index ba7ce581e138f4f12f2323b892a3488e1048e171..a80f0e44f99f9fe2a8a096c31e8219e4c155ea91 100644
--- a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture_enc_or/spec.tmap
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture_enc_or/spec.tmap
@@ -17,10 +17,52 @@ TMLMAPPING
SET App_enc_or__GPSGateway priority 0
MAP CPU_Navigation App_enc_or__NavigationControl
SET App_enc_or__NavigationControl priority 0
- MAPSEC MemoryControl autoEncrypt_vehData
- MAPSEC MemoryNavigation autoEncrypt_vehData
- MAPSEC MemorySensor autoEncrypt_GPSdata
- MAPSEC MemoryNavigation autoEncrypt_GPSdata
+ MAP MemoryNavigation App_enc_or__sensorData
+ SET App_enc_or__sensorData priority 5
+ MAP InternalNavigationBus App_enc_or__sensorData
+ SET App_enc_or__sensorData priority 5
+ MAP sensorBus App_enc_or__sensorData
+ SET App_enc_or__sensorData priority 5
+ MAP MemoryNavigation App_enc_or__V2Xdata
+ SET App_enc_or__V2Xdata priority 5
+ MAP InternalNavigationBus App_enc_or__V2Xdata
+ SET App_enc_or__V2Xdata priority 5
+ MAP sensorBus App_enc_or__V2Xdata
+ SET App_enc_or__V2Xdata priority 5
+ MAP MemoryNavigation App_enc_or__vehData
+ SET App_enc_or__vehData priority 5
+ MAP commBus App_enc_or__vehData
+ SET App_enc_or__vehData priority 5
+ MAP InternalNavigationBus App_enc_or__vehData
+ SET App_enc_or__vehData priority 5
+ MAP MemoryNavigation App_enc_or__GPSdata
+ SET App_enc_or__GPSdata priority 5
+ MAP InternalNavigationBus App_enc_or__GPSdata
+ SET App_enc_or__GPSdata priority 5
+ MAP sensorBus App_enc_or__GPSdata
+ SET App_enc_or__GPSdata priority 5
+ MAP MemoryNavigation App_enc_or__nonceChvCG_NC
+ SET App_enc_or__nonceChvCG_NC priority 5
+ MAP InternalNavigationBus App_enc_or__nonceChvCG_NC
+ SET App_enc_or__nonceChvCG_NC priority 5
+ MAP commBus App_enc_or__nonceChvCG_NC
+ SET App_enc_or__nonceChvCG_NC priority 5
+ MAP MemoryNavigation App_enc_or__nonceChNC_GG
+ SET App_enc_or__nonceChNC_GG priority 5
+ MAP sensorBus App_enc_or__nonceChNC_GG
+ SET App_enc_or__nonceChNC_GG priority 5
+ MAP InternalNavigationBus App_enc_or__nonceChNC_GG
+ SET App_enc_or__nonceChNC_GG priority 5
+ MAP MemoryNavigation App_enc_or__nonceChNC_SU
+ SET App_enc_or__nonceChNC_SU priority 5
+ MAP sensorBus App_enc_or__nonceChNC_SU
+ SET App_enc_or__nonceChNC_SU priority 5
+ MAP InternalNavigationBus App_enc_or__nonceChNC_SU
+ SET App_enc_or__nonceChNC_SU priority 5
MAPSEC MemorySensor autoEncrypt_sensorData
MAPSEC MemoryNavigation autoEncrypt_sensorData
+ MAPSEC MemorySensor autoEncrypt_GPSdata
+ MAPSEC MemoryNavigation autoEncrypt_GPSdata
+ MAPSEC MemoryControl autoEncrypt_vehData
+ MAPSEC MemoryNavigation autoEncrypt_vehData
ENDTMLMAPPING
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture_enc_or/spec.tml b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture_enc_or/spec.tml
index 1e18208aeb3872ce9b21656ec33c85cdaae01ab5..179e1302d90d4bf24a011282b6c484a8ea602db5 100644
--- a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture_enc_or/spec.tml
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture_enc_or/spec.tml
@@ -1,6 +1,5 @@
// TML Application - FORMAT 0.2
-// Application: /home/kali/Documents/Eurecom/SemesterProject/TTool/modeling/ITSDemo.ttool/ITSDemo.xml
-// Generated: Sat Jan 20 17:18:05 EST 2024
+// Generated: Tue Mar 26 18:12:09 CET 2024
// PRAGMAS
@@ -44,7 +43,7 @@ TASK App_enc_or__GPSGateway
EXECI processCommand
NOTIFY App_enc_or__updateLoc__App_enc_or__updateLoc
READ App_enc_or__nonceChNC_GG 1+0 nonce_NavigationControl_GPSGateway
- EXECC 100 autoEncrypt_GPSdata SE 100 100 0 0 nonce_NavigationControl_GPSGateway nonce_NavigationControl_GPSGateway 1
+ EXECC 100 autoEncrypt_GPSdata SE 100 100 0 0 nonce_NavigationControl_GPSGateway - 1
WRITE App_enc_or__GPSdata 1+0 autoEncrypt_GPSdata
ENDFOR
ENDTASK
@@ -75,12 +74,12 @@ TASK App_enc_or__NavigationControl
EXECC 100 nonce_NavigationControl_GPSGateway NONCE 100 100 0 0 - - 1
WRITE App_enc_or__nonceChNC_GG 1+0 nonce_NavigationControl_GPSGateway
READ App_enc_or__GPSdata 1+0 autoEncrypt_GPSdata
- EXECC (100)+(calculateRoute) autoEncrypt_GPSdata SE 100 100 0 0 nonce_NavigationControl_GPSGateway nonce_NavigationControl_GPSGateway 2
+ EXECC (100)+(calculateRoute) autoEncrypt_GPSdata SE 100 100 0 0 nonce_NavigationControl_GPSGateway - 2
RAND
CASERAND 50
EXECC forgeCommand
READ App_enc_or__nonceChvCG_NC 1+0 nonce_vehicleControlGateway_NavigationControl
- EXECC 100 autoEncrypt_vehData MAC 100 100 0 0 nonce_vehicleControlGateway_NavigationControl nonce_vehicleControlGateway_NavigationControl 1
+ EXECC 100 autoEncrypt_vehData MAC 100 100 0 0 nonce_vehicleControlGateway_NavigationControl - 1
WRITE App_enc_or__vehData 10+0 autoEncrypt_vehData
ENDCASERAND
CASERAND 50
@@ -92,7 +91,7 @@ TASK App_enc_or__NavigationControl
EXECC 100 nonce_NavigationControl_SensorUnit NONCE 100 100 0 0 - - 1
WRITE App_enc_or__nonceChNC_SU 1+0 nonce_NavigationControl_SensorUnit
READ App_enc_or__sensorData 1+0 autoEncrypt_sensorData
- EXECC (100)+(calculateObstacle) autoEncrypt_sensorData MAC 100 100 0 0 nonce_NavigationControl_SensorUnit nonce_NavigationControl_SensorUnit 2
+ EXECC (100)+(calculateObstacle) autoEncrypt_sensorData MAC 100 100 0 0 nonce_NavigationControl_SensorUnit - 2
ENDCASE
ENDSELECTEVT
ENDFOR
@@ -114,7 +113,7 @@ TASK App_enc_or__SensorUnit
CASERAND 90
NOTIFY App_enc_or__updateSensor__App_enc_or__updateSensor
READ App_enc_or__nonceChNC_SU 1+0 nonce_NavigationControl_SensorUnit
- EXECC 100 autoEncrypt_sensorData MAC 100 100 0 0 nonce_NavigationControl_SensorUnit nonce_NavigationControl_SensorUnit 1
+ EXECC 100 autoEncrypt_sensorData MAC 100 100 0 0 nonce_NavigationControl_SensorUnit - 1
WRITE App_enc_or__sensorData 1+0 autoEncrypt_sensorData
ENDCASERAND
CASERAND 10
@@ -152,7 +151,7 @@ TASK App_enc_or__vehicleControlGateway
EXECC 100 nonce_vehicleControlGateway_NavigationControl NONCE 100 100 0 0 - - 1
WRITE App_enc_or__nonceChvCG_NC 1+0 nonce_vehicleControlGateway_NavigationControl
READ App_enc_or__vehData 1+0 autoEncrypt_vehData
- EXECC 100 autoEncrypt_vehData MAC 100 100 0 0 nonce_vehicleControlGateway_NavigationControl nonce_vehicleControlGateway_NavigationControl 2
+ EXECC 100 autoEncrypt_vehData MAC 100 100 0 0 nonce_vehicleControlGateway_NavigationControl - 2
ENDCASERAND
CASERAND 50
EXECI recalculate
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture_hsm/golden b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture_hsm/golden
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..f25a9a72733baff74c54ad148f7b9206250208b3 100644
--- a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture_hsm/golden
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture_hsm/golden
@@ -0,0 +1,5 @@
+Query not attacker(GPSGateway___hsmSec_GPSdata[!1 = v]) is true.
+Query not attacker(GPSGateway___hsmSec_GPSdata_encrypted0[!1 = v]) is true.
+Query inj-event(authenticity___vehicleControlGateway___hsmSec_vehData___decrypt_hsmSec_vehData_dummy(dummyM)) ==> inj-event(authenticity___HSM_CPU_Navigation___hsmSec_vehData____encrypt_hsmSec_vehData(dummyM)) is true.
+Query inj-event(authenticity___HSM_CPU_Navigation___hsmSec_sensorData___decrypt_hsmSec_sensorData_dummy(dummyM)) ==> inj-event(authenticity___SensorUnit___hsmSec_sensorData____encrypt_hsmSec_sensorData(dummyM)) is true.
+Query inj-event(authenticity___HSM_CPU_Navigation___hsmSec_GPSdata___decrypt_hsmSec_GPSdata_dummy(dummyM)) ==> inj-event(authenticity___GPSGateway___hsmSec_GPSdata____encrypt_hsmSec_GPSdata(dummyM)) is true.
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture_hsm/spec.tarchi b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture_hsm/spec.tarchi
index d3b6ccd8a9544ce1eb2e65ca8a80752efe201e4f..d61cf9f0caea5377eb6ccc30a826a7da3b67ee1f 100644
--- a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture_hsm/spec.tarchi
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture_hsm/spec.tarchi
@@ -1,6 +1,14 @@
// Master clock frequency - in MHz
MASTERCLOCKFREQUENCY 200
+NODE BRIDGE BridgeComm
+SET BridgeComm bufferByteSize 4
+SET BridgeComm clockDivider 1
+
+NODE BRIDGE BridgeSensor
+SET BridgeSensor bufferByteSize 4
+SET BridgeSensor clockDivider 1
+
NODE BUS BusControl
SET BusControl byteDataSize 4
SET BusControl pipelineSize 1
@@ -124,6 +132,22 @@ SET CPU_Navigation execiTime 1
SET CPU_Navigation execcTime 1
SET CPU_Navigation clockDivider 1
+NODE LINK link_BridgeComm_to_InternalNavigationBus
+SET link_BridgeComm_to_InternalNavigationBus node BridgeComm
+SET link_BridgeComm_to_InternalNavigationBus bus InternalNavigationBus
+SET link_BridgeComm_to_InternalNavigationBus priority 0
+NODE LINK link_BridgeComm_to_commBus
+SET link_BridgeComm_to_commBus node BridgeComm
+SET link_BridgeComm_to_commBus bus commBus
+SET link_BridgeComm_to_commBus priority 0
+NODE LINK link_BridgeSensor_to_sensorBus
+SET link_BridgeSensor_to_sensorBus node BridgeSensor
+SET link_BridgeSensor_to_sensorBus bus sensorBus
+SET link_BridgeSensor_to_sensorBus priority 0
+NODE LINK link_BridgeSensor_to_InternalNavigationBus
+SET link_BridgeSensor_to_InternalNavigationBus node BridgeSensor
+SET link_BridgeSensor_to_InternalNavigationBus bus InternalNavigationBus
+SET link_BridgeSensor_to_InternalNavigationBus priority 0
NODE LINK link_HSM_CPU_Navigation_to_InternalNavigationBus
SET link_HSM_CPU_Navigation_to_InternalNavigationBus node HSM_CPU_Navigation
SET link_HSM_CPU_Navigation_to_InternalNavigationBus bus InternalNavigationBus
@@ -148,10 +172,6 @@ NODE LINK link_controlCPU_to_commBus
SET link_controlCPU_to_commBus node controlCPU
SET link_controlCPU_to_commBus bus commBus
SET link_controlCPU_to_commBus priority 0
-NODE LINK link_CPU_Navigation_to_commBus
-SET link_CPU_Navigation_to_commBus node CPU_Navigation
-SET link_CPU_Navigation_to_commBus bus commBus
-SET link_CPU_Navigation_to_commBus priority 0
NODE LINK link_MemoryNavigation_to_InternalNavigationBus
SET link_MemoryNavigation_to_InternalNavigationBus node MemoryNavigation
SET link_MemoryNavigation_to_InternalNavigationBus bus InternalNavigationBus
@@ -160,10 +180,6 @@ NODE LINK link_CPU_Navigation_to_InternalNavigationBus
SET link_CPU_Navigation_to_InternalNavigationBus node CPU_Navigation
SET link_CPU_Navigation_to_InternalNavigationBus bus InternalNavigationBus
SET link_CPU_Navigation_to_InternalNavigationBus priority 0
-NODE LINK link_CPU_Navigation_to_sensorBus
-SET link_CPU_Navigation_to_sensorBus node CPU_Navigation
-SET link_CPU_Navigation_to_sensorBus bus sensorBus
-SET link_CPU_Navigation_to_sensorBus priority 0
NODE LINK link_V2XCPU_to_sensorBus
SET link_V2XCPU_to_sensorBus node V2XCPU
SET link_V2XCPU_to_sensorBus bus sensorBus
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture_hsm/spec.tmap b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture_hsm/spec.tmap
index 1c82a7730343f9190fecf1ee33775f2413192470..704fbee0e6d7f522155df6fae713ba359b3dac11 100644
--- a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture_hsm/spec.tmap
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture_hsm/spec.tmap
@@ -19,10 +19,88 @@ TMLMAPPING
SET App_hsm__GPSGateway priority 0
MAP CPU_Navigation App_hsm__NavigationControl
SET App_hsm__NavigationControl priority 0
- MAPSEC MemorySensor hsmSec_sensorData
- MAPSEC MemoryNavigation hsmSec_sensorData
- MAPSEC MemorySensor hsmSec_GPSdata
- MAPSEC MemoryNavigation hsmSec_GPSdata
+ MAP MemoryNavigation App_hsm__GPSdata
+ SET App_hsm__GPSdata priority 5
+ MAP InternalNavigationBus App_hsm__GPSdata
+ SET App_hsm__GPSdata priority 5
+ MAP sensorBus App_hsm__GPSdata
+ SET App_hsm__GPSdata priority 5
+ MAP MemoryNavigation App_hsm__vehData
+ SET App_hsm__vehData priority 5
+ MAP InternalNavigationBus App_hsm__vehData
+ SET App_hsm__vehData priority 5
+ MAP commBus App_hsm__vehData
+ SET App_hsm__vehData priority 5
+ MAP MemoryNavigation App_hsm__V2Xdata
+ SET App_hsm__V2Xdata priority 5
+ MAP sensorBus App_hsm__V2Xdata
+ SET App_hsm__V2Xdata priority 5
+ MAP InternalNavigationBus App_hsm__V2Xdata
+ SET App_hsm__V2Xdata priority 5
+ MAP MemoryNavigation App_hsm__data_GPSdata_NavigationControl
+ SET App_hsm__data_GPSdata_NavigationControl priority 5
+ MAP InternalNavigationBus App_hsm__data_GPSdata_NavigationControl
+ SET App_hsm__data_GPSdata_NavigationControl priority 5
+ MAP MemoryNavigation App_hsm__sensorData
+ SET App_hsm__sensorData priority 5
+ MAP sensorBus App_hsm__sensorData
+ SET App_hsm__sensorData priority 5
+ MAP InternalNavigationBus App_hsm__sensorData
+ SET App_hsm__sensorData priority 5
+ MAP MemoryNavigation App_hsm__data_sensorData_NavigationControl
+ SET App_hsm__data_sensorData_NavigationControl priority 5
+ MAP InternalNavigationBus App_hsm__data_sensorData_NavigationControl
+ SET App_hsm__data_sensorData_NavigationControl priority 5
+ MAP MemoryNavigation App_hsm__nonceChNC_SU
+ SET App_hsm__nonceChNC_SU priority 5
+ MAP sensorBus App_hsm__nonceChNC_SU
+ SET App_hsm__nonceChNC_SU priority 5
+ MAP InternalNavigationBus App_hsm__nonceChNC_SU
+ SET App_hsm__nonceChNC_SU priority 5
+ MAP MemoryNavigation App_hsm__data_vehData_NavigationControl
+ SET App_hsm__data_vehData_NavigationControl priority 5
+ MAP InternalNavigationBus App_hsm__data_vehData_NavigationControl
+ SET App_hsm__data_vehData_NavigationControl priority 5
+ MAP MemoryNavigation App_hsm__nonceChNC_GG
+ SET App_hsm__nonceChNC_GG priority 5
+ MAP sensorBus App_hsm__nonceChNC_GG
+ SET App_hsm__nonceChNC_GG priority 5
+ MAP InternalNavigationBus App_hsm__nonceChNC_GG
+ SET App_hsm__nonceChNC_GG priority 5
+ MAP MemoryNavigation App_hsm__nonceVehicle
+ SET App_hsm__nonceVehicle priority 5
+ MAP InternalNavigationBus App_hsm__nonceVehicle
+ SET App_hsm__nonceVehicle priority 5
+ MAP MemoryNavigation App_hsm__nonceChvCG_NC
+ SET App_hsm__nonceChvCG_NC priority 5
+ MAP InternalNavigationBus App_hsm__nonceChvCG_NC
+ SET App_hsm__nonceChvCG_NC priority 5
+ MAP commBus App_hsm__nonceChvCG_NC
+ SET App_hsm__nonceChvCG_NC priority 5
+ MAP MemoryNavigation App_hsm__nonceSensor
+ SET App_hsm__nonceSensor priority 5
+ MAP InternalNavigationBus App_hsm__nonceSensor
+ SET App_hsm__nonceSensor priority 5
+ MAP MemoryNavigation App_hsm__nonceGPS
+ SET App_hsm__nonceGPS priority 5
+ MAP InternalNavigationBus App_hsm__nonceGPS
+ SET App_hsm__nonceGPS priority 5
+ MAP MemoryNavigation App_hsm__retData_sensorData_NavigationControl
+ SET App_hsm__retData_sensorData_NavigationControl priority 5
+ MAP InternalNavigationBus App_hsm__retData_sensorData_NavigationControl
+ SET App_hsm__retData_sensorData_NavigationControl priority 5
+ MAP MemoryNavigation App_hsm__retData_GPSdata_NavigationControl
+ SET App_hsm__retData_GPSdata_NavigationControl priority 5
+ MAP InternalNavigationBus App_hsm__retData_GPSdata_NavigationControl
+ SET App_hsm__retData_GPSdata_NavigationControl priority 5
+ MAP MemoryNavigation App_hsm__retData_vehData_NavigationControl
+ SET App_hsm__retData_vehData_NavigationControl priority 5
+ MAP InternalNavigationBus App_hsm__retData_vehData_NavigationControl
+ SET App_hsm__retData_vehData_NavigationControl priority 5
MAPSEC MemoryControl hsmSec_vehData
MAPSEC MemoryNavigation hsmSec_vehData
+ MAPSEC MemorySensor hsmSec_GPSdata
+ MAPSEC MemoryNavigation hsmSec_GPSdata
+ MAPSEC MemorySensor hsmSec_sensorData
+ MAPSEC MemoryNavigation hsmSec_sensorData
ENDTMLMAPPING
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture_hsm/spec.tml b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture_hsm/spec.tml
index 3de69ff24e869fbdc44dab6fb517bd7b21518cce..2f54d42eb89b8b1374852f1fb853f68ef0a9409c 100644
--- a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture_hsm/spec.tml
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture_hsm/spec.tml
@@ -1,6 +1,6 @@
// TML Application - FORMAT 0.2
-// Application: /home/kali/Documents/Eurecom/SemesterProject/TTool/modeling/ITSDemo.ttool/ITSDemo.xml
-// Generated: Sat Jan 20 17:19:36 EST 2024
+// Application: /home/jawher/Jawher/TTool/TTool-orig/TTool/modeling/ITSDemo.ttool/ITSDemo.xml
+// Generated: Tue Mar 26 18:12:28 CET 2024
// PRAGMAS
@@ -62,7 +62,7 @@ TASK App_hsm__GPSGateway
EXECI processCommand
NOTIFY App_hsm__updateLoc__App_hsm__updateLoc
READ App_hsm__nonceChNC_GG 1+0 nonce_NavigationControl_GPSGateway
- EXECC 100 hsmSec_GPSdata SE 100 100 0 0 nonce_NavigationControl_GPSGateway nonce_NavigationControl_GPSGateway 1
+ EXECC 100 hsmSec_GPSdata SE 100 100 0 0 nonce_NavigationControl_GPSGateway - 1
WRITE App_hsm__GPSdata 1+0 hsmSec_GPSdata
ENDFOR
ENDTASK
@@ -90,18 +90,18 @@ TASK App_hsm__HSM_CPU_Navigation
RAND
CASERAND 33
READ App_hsm__data_sensorData_NavigationControl 1+0 hsmSec_sensorData
- EXECC 100 hsmSec_sensorData MAC 100 100 0 0 nonce_NavigationControl_SensorUnit nonce_NavigationControl_SensorUnit 2
+ EXECC 100 hsmSec_sensorData MAC 100 100 0 0 nonce_NavigationControl_SensorUnit - 2
WRITE App_hsm__retData_sensorData_NavigationControl 1+0 hsmSec_sensorData
ENDCASERAND
CASERAND 33
READ App_hsm__data_GPSdata_NavigationControl 1+0 hsmSec_GPSdata
- EXECC 100 hsmSec_GPSdata SE 100 100 0 0 nonce_NavigationControl_GPSGateway nonce_NavigationControl_GPSGateway 2
+ EXECC 100 hsmSec_GPSdata SE 100 100 0 0 nonce_NavigationControl_GPSGateway - 2
WRITE App_hsm__retData_GPSdata_NavigationControl 1+0 hsmSec_GPSdata
ENDCASERAND
CASERAND 33
READ App_hsm__nonceVehicle 1+0 nonce_vehicleControlGateway_NavigationControl
READ App_hsm__data_vehData_NavigationControl 1+0 hsmSec_vehData
- EXECC 100 hsmSec_vehData MAC 100 100 0 0 nonce_vehicleControlGateway_NavigationControl nonce_vehicleControlGateway_NavigationControl 1
+ EXECC 100 hsmSec_vehData MAC 100 100 0 0 nonce_vehicleControlGateway_NavigationControl - 1
WRITE App_hsm__retData_vehData_NavigationControl 1+0 hsmSec_vehData
ENDCASERAND
ENDRAND
@@ -181,7 +181,7 @@ TASK App_hsm__SensorUnit
CASERAND 50
NOTIFY App_hsm__updateSensor__App_hsm__updateSensor
READ App_hsm__nonceChNC_SU 1+0 nonce_NavigationControl_SensorUnit
- EXECC 100 hsmSec_sensorData MAC 100 100 0 0 nonce_NavigationControl_SensorUnit nonce_NavigationControl_SensorUnit 1
+ EXECC 100 hsmSec_sensorData MAC 100 100 0 0 nonce_NavigationControl_SensorUnit - 1
WRITE App_hsm__sensorData 1+0 hsmSec_sensorData
ENDCASERAND
CASERAND 50
@@ -219,7 +219,7 @@ TASK App_hsm__vehicleControlGateway
EXECC 100 nonce_vehicleControlGateway_NavigationControl NONCE 100 0 0 0 - - 1
WRITE App_hsm__nonceChvCG_NC 1+0 nonce_vehicleControlGateway_NavigationControl
READ App_hsm__vehData 1+0 hsmSec_vehData
- EXECC 100 hsmSec_vehData MAC 100 100 0 0 nonce_vehicleControlGateway_NavigationControl nonce_vehicleControlGateway_NavigationControl 2
+ EXECC 100 hsmSec_vehData MAC 100 100 0 0 nonce_vehicleControlGateway_NavigationControl - 2
ENDCASERAND
CASERAND 50
EXECI recalculate