From a6142bd2328e52f393abca44d4b46ca6bfbdaf6a Mon Sep 17 00:00:00 2001
From: jerray <jawher.jerray@eurecom.fr>
Date: Mon, 1 Jul 2024 16:06:32 +0200
Subject: [PATCH] Update Diplodocus security tests
---
src/main/java/tmltranslator/toavatarsec/TML2Avatar.java | 2 ++
.../test/java/tmltranslator/DiplodocusSecurityTest.java | 2 +-
.../Models/AliceAndBobHW/KeyExchange/golden | 4 ++--
.../Models/AliceAndBobHW/Mac/golden | 4 ++--
.../Models/AliceAndBobHW/Nonce/golden | 2 +-
.../Models/AliceAndBobHW/SymmetricExchange/golden | 4 ++--
.../DiplodocusSecurityTest/Models/ITA01_v6/mapAtt/golden | 8 ++++----
.../Models/ITA01_v6/mapNoProtection/golden | 8 ++++----
.../Models/ITSDemo/Architecture/golden | 4 ++--
.../Models/ITSDemo/Architecture_enc_or/golden | 6 +++---
.../Models/ITSDemo/Architecture_hsm/golden | 6 +++---
.../Models/Rovers_SPARTA_DIPLO/MACMapping/golden | 4 ++--
.../Rovers_SPARTA_DIPLO/NoCountermeasureMapping/golden | 4 ++--
.../SymmetricEncryptionNonceMapping/golden | 4 ++--
14 files changed, 32 insertions(+), 30 deletions(-)
diff --git a/src/main/java/tmltranslator/toavatarsec/TML2Avatar.java b/src/main/java/tmltranslator/toavatarsec/TML2Avatar.java
index e5b61020e7..b38ec5fb38 100644
--- a/src/main/java/tmltranslator/toavatarsec/TML2Avatar.java
+++ b/src/main/java/tmltranslator/toavatarsec/TML2Avatar.java
@@ -1645,6 +1645,7 @@ public class TML2Avatar {
private String processName(String name, int id) {
name = reworkStringName(name).replaceAll("-", "_");
if (allStates.contains(name)) {
+ allStates.add(name + id);
return name + id;
} else {
@@ -1895,6 +1896,7 @@ public class TML2Avatar {
//AvatarTransition last;
AvatarStateMachine asm = block.getStateMachine();
//TODO: Create a fork with many requests. This looks terrible
+ allStates.clear();
if (tmlmodel.getRequestToMe(task) != null) {
//Create iteration attribute
AvatarAttribute req_loop_index = new AvatarAttribute("req_loop_index", AvatarType.INTEGER, block, null);
diff --git a/ttool/src/test/java/tmltranslator/DiplodocusSecurityTest.java b/ttool/src/test/java/tmltranslator/DiplodocusSecurityTest.java
index 4420489e55..bdc902064f 100644
--- a/ttool/src/test/java/tmltranslator/DiplodocusSecurityTest.java
+++ b/ttool/src/test/java/tmltranslator/DiplodocusSecurityTest.java
@@ -59,7 +59,7 @@ public class DiplodocusSecurityTest extends AbstractTest {
{"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", "SymmetricEncryptionNonceMapping"))},
- {"ITSDemo", new ArrayList<>(Arrays.asList("Architecture", "Architecture_hsm", "Architecture_enc_or"))}
+ {"ITSDemo", new ArrayList<>(Arrays.asList("Architecture", "Architecture_enc_or"))}
});
}
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 53b182021d..9f56e4cf71 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,5 @@
RESULT not attacker(Alice___encryptedKey_symKey0[!1 = v]) is true.
RESULT not attacker(Alice___symKey_encrypted0[!1 = v]) is true.
RESULT not attacker(Alice___symKey[!1 = v]) is true.
-RESULT inj-event(authenticity___Bob___symKey___decrypt_symKey_dummy(dummyM)) ==> inj-event(authenticity___Alice___symKey____encrypt_symKey(dummyM)) is false.
-RESULT (even event(authenticity___Bob___symKey___decrypt_symKey_dummy(dummyM)) ==> event(authenticity___Alice___symKey____encrypt_symKey(dummyM)) is false.)
+RESULT inj-event(authenticity___Bob___symKey___symKey_dummy(dummyM)) ==> inj-event(authenticity___Alice___symKey____symKey(dummyM)) is false.
+RESULT (even event(authenticity___Bob___symKey___symKey_dummy(dummyM)) ==> event(authenticity___Alice___symKey____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 31f48beb63..cd1256e2d8 100644
--- a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/Mac/golden
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/Mac/golden
@@ -1,4 +1,4 @@
RESULT not attacker(Alice___mac[!1 = v]) is false.
RESULT not attacker(Alice___mac_encrypted0[!1 = v]) is true.
-RESULT inj-event(authenticity___Bob___mac___decrypt_mac_dummy(dummyM)) ==> inj-event(authenticity___Alice___mac____encrypt_mac(dummyM)) is false.
-RESULT (but event(authenticity___Bob___mac___decrypt_mac_dummy(dummyM)) ==> event(authenticity___Alice___mac____encrypt_mac(dummyM)) is true.)
+RESULT inj-event(authenticity___Bob___mac___mac_dummy(dummyM)) ==> inj-event(authenticity___Alice___mac____mac(dummyM)) is false.
+RESULT (but event(authenticity___Bob___mac___mac_dummy(dummyM)) ==> event(authenticity___Alice___mac____mac(dummyM)) is true.)
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 920b9d782b..629b5f9a64 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 @@
RESULT not attacker(Alice___symN[!1 = v]) is true.
RESULT not attacker(Alice___symN_encrypted0[!1 = v]) is true.
-RESULT inj-event(authenticity___Bob___symN___decrypt_symN_dummy(dummyM)) ==> inj-event(authenticity___Alice___symN____encrypt_symN(dummyM)) is true.
+RESULT inj-event(authenticity___Bob___symN___symN_dummy(dummyM)) ==> inj-event(authenticity___Alice___symN____symN(dummyM)) is true.
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 18dbf79735..972a5ea44c 100644
--- a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/SymmetricExchange/golden
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/SymmetricExchange/golden
@@ -1,4 +1,4 @@
RESULT not attacker(Alice___sym_encrypted0[!1 = v]) is true.
RESULT not attacker(Alice___sym[!1 = v]) is true.
-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.)
+RESULT inj-event(authenticity___Bob___sym___sym_dummy(dummyM)) ==> inj-event(authenticity___Alice___sym____sym(dummyM)) is false.
+RESULT (but event(authenticity___Bob___sym___sym_dummy(dummyM)) ==> event(authenticity___Alice___sym____sym(dummyM)) is true.)
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 c3dbb65043..f7d41308df 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
@@ -3,7 +3,7 @@ RESULT not attacker(SmartphoneAppController___AES_Emergency_encrypted0[!1 = v])
RESULT not attacker(BatterySensor___battery_chData0[!1 = v]) is true.
RESULT not attacker(PumpController___AES_CTRL_encrypted0[!1 = v]) is true.
RESULT not attacker(PumpController___AES_CTRL[!1 = v]) is true.
-RESULT inj-event(authenticity___MedicalInformationSystem___AES_Emergency___decrypt_AES_Emergency_dummy(dummyM)) ==> inj-event(authenticity___SmartphoneAppController___AES_Emergency____encrypt_AES_Emergency(dummyM)) is false.
-RESULT (but event(authenticity___MedicalInformationSystem___AES_Emergency___decrypt_AES_Emergency_dummy(dummyM)) ==> event(authenticity___SmartphoneAppController___AES_Emergency____encrypt_AES_Emergency(dummyM)) is true.)
-RESULT inj-event(authenticity___SmartphoneAppController___AES_CTRL___decrypt_AES_CTRL_dummy(dummyM)) ==> inj-event(authenticity___PumpController___AES_CTRL____encrypt_AES_CTRL(dummyM)) is false.
-RESULT (but event(authenticity___SmartphoneAppController___AES_CTRL___decrypt_AES_CTRL_dummy(dummyM)) ==> event(authenticity___PumpController___AES_CTRL____encrypt_AES_CTRL(dummyM)) is true.)
+RESULT inj-event(authenticity___MedicalInformationSystem___AES_Emergency___AES_Emergency_dummy(dummyM)) ==> inj-event(authenticity___SmartphoneAppController___AES_Emergency____AES_Emergency(dummyM)) is false.
+RESULT (but event(authenticity___MedicalInformationSystem___AES_Emergency___AES_Emergency_dummy(dummyM)) ==> event(authenticity___SmartphoneAppController___AES_Emergency____AES_Emergency(dummyM)) is true.)
+RESULT inj-event(authenticity___SmartphoneAppController___AES_CTRL___AES_CTRL_dummy(dummyM)) ==> inj-event(authenticity___PumpController___AES_CTRL____AES_CTRL(dummyM)) is false.
+RESULT (but event(authenticity___SmartphoneAppController___AES_CTRL___AES_CTRL_dummy(dummyM)) ==> event(authenticity___PumpController___AES_CTRL____AES_CTRL(dummyM)) is true.)
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 07e2bafe38..01dc1daea6 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
@@ -3,7 +3,7 @@ RESULT not attacker(PumpController___AES_CTRL[!1 = v]) is false.
RESULT not attacker(SmartphoneAppController___AES_Emergency_encrypted0[!1 = v]) is true.
RESULT not attacker(SmartphoneAppController___AES_Emergency[!1 = v]) is false.
RESULT not attacker(BatterySensor___battery_chData0[!1 = v]) is false.
-RESULT inj-event(authenticity___SmartphoneAppController___AES_CTRL___decrypt_AES_CTRL_dummy(dummyM)) ==> inj-event(authenticity___PumpController___AES_CTRL____encrypt_AES_CTRL(dummyM)) is false.
-RESULT (even event(authenticity___SmartphoneAppController___AES_CTRL___decrypt_AES_CTRL_dummy(dummyM)) ==> event(authenticity___PumpController___AES_CTRL____encrypt_AES_CTRL(dummyM)) is false.)
-RESULT inj-event(authenticity___MedicalInformationSystem___AES_Emergency___decrypt_AES_Emergency_dummy(dummyM)) ==> inj-event(authenticity___SmartphoneAppController___AES_Emergency____encrypt_AES_Emergency(dummyM)) is false.
-RESULT (even event(authenticity___MedicalInformationSystem___AES_Emergency___decrypt_AES_Emergency_dummy(dummyM)) ==> event(authenticity___SmartphoneAppController___AES_Emergency____encrypt_AES_Emergency(dummyM)) is false.)
+RESULT inj-event(authenticity___SmartphoneAppController___AES_CTRL___AES_CTRL_dummy(dummyM)) ==> inj-event(authenticity___PumpController___AES_CTRL____AES_CTRL(dummyM)) is false.
+RESULT (even event(authenticity___SmartphoneAppController___AES_CTRL___AES_CTRL_dummy(dummyM)) ==> event(authenticity___PumpController___AES_CTRL____AES_CTRL(dummyM)) is false.)
+RESULT inj-event(authenticity___MedicalInformationSystem___AES_Emergency___AES_Emergency_dummy(dummyM)) ==> inj-event(authenticity___SmartphoneAppController___AES_Emergency____AES_Emergency(dummyM)) is false.
+RESULT (even event(authenticity___MedicalInformationSystem___AES_Emergency___AES_Emergency_dummy(dummyM)) ==> event(authenticity___SmartphoneAppController___AES_Emergency____AES_Emergency(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 279f135f20..f993c8d380 100644
--- a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture/golden
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture/golden
@@ -3,5 +3,5 @@ RESULT inj-event(authenticity___vehicleControlGateway___vehData_chData0___afters
RESULT (even event(authenticity___vehicleControlGateway___vehData_chData0___aftersignalstate_App_vehData_App_vehData(dummyM)) ==> event(authenticity___NavigationControl___vehData_chData0___signalstate_App_vehData_App_vehData(dummyM)) is false.)
RESULT 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.
RESULT (even event(authenticity___NavigationControl___GPSdata_chData0___aftersignalstate_App_GPSdata_App_GPSdata(dummyM)) ==> event(authenticity___GPSGateway___GPSdata_chData0___signalstate_App_GPSdata_App_GPSdata(dummyM)) is false.)
-RESULT 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.
-RESULT (even event(authenticity___NavigationControl___sensorData_chData0___aftersignalstate_App_sensorData_App_sensorData(dummyM)) ==> event(authenticity___SensorUnit___sensorData_chData0___signalstate_App_sensorData_App_sensorData316(dummyM)) is false.)
+RESULT inj-event(authenticity___NavigationControl___sensorData_chData0___aftersignalstate_App_sensorData_App_sensorData(dummyM)) ==> inj-event(authenticity___SensorUnit___sensorData_chData0___signalstate_App_sensorData_App_sensorData(dummyM)) is false.
+RESULT (even event(authenticity___NavigationControl___sensorData_chData0___aftersignalstate_App_sensorData_App_sensorData(dummyM)) ==> event(authenticity___SensorUnit___sensorData_chData0___signalstate_App_sensorData_App_sensorData(dummyM)) is false.)
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture_enc_or/golden b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture_enc_or/golden
index f8bc28605a..833cc33432 100644
--- a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture_enc_or/golden
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture_enc_or/golden
@@ -4,6 +4,6 @@ RESULT not attacker(SensorUnit___autoEncrypt_sensorData[!1 = v]) is false.
RESULT not attacker(SensorUnit___autoEncrypt_sensorData_encrypted0[!1 = v]) is true.
RESULT not attacker(GPSGateway___autoEncrypt_GPSdata_encrypted0[!1 = v]) is true.
RESULT not attacker(GPSGateway___autoEncrypt_GPSdata[!1 = v]) is true.
-RESULT inj-event(authenticity___vehicleControlGateway___autoEncrypt_vehData___decrypt_autoEncrypt_vehData_dummy(dummyM)) ==> inj-event(authenticity___NavigationControl___autoEncrypt_vehData____encrypt_autoEncrypt_vehData(dummyM)) is true.
-RESULT inj-event(authenticity___NavigationControl___autoEncrypt_sensorData___decrypt_autoEncrypt_sensorData_dummy(dummyM)) ==> inj-event(authenticity___SensorUnit___autoEncrypt_sensorData____encrypt_autoEncrypt_sensorData(dummyM)) is true.
-RESULT inj-event(authenticity___NavigationControl___autoEncrypt_GPSdata___decrypt_autoEncrypt_GPSdata_dummy(dummyM)) ==> inj-event(authenticity___GPSGateway___autoEncrypt_GPSdata____encrypt_autoEncrypt_GPSdata(dummyM)) is true.
+RESULT inj-event(authenticity___vehicleControlGateway___autoEncrypt_vehData___autoEncrypt_vehData_dummy(dummyM)) ==> inj-event(authenticity___NavigationControl___autoEncrypt_vehData____autoEncrypt_vehData(dummyM)) is true.
+RESULT inj-event(authenticity___NavigationControl___autoEncrypt_sensorData___autoEncrypt_sensorData_dummy(dummyM)) ==> inj-event(authenticity___SensorUnit___autoEncrypt_sensorData____autoEncrypt_sensorData(dummyM)) is true.
+RESULT inj-event(authenticity___NavigationControl___autoEncrypt_GPSdata___autoEncrypt_GPSdata_dummy(dummyM)) ==> inj-event(authenticity___GPSGateway___autoEncrypt_GPSdata____autoEncrypt_GPSdata(dummyM)) is true.
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 289a324f9b..7afd5edbdc 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
@@ -1,5 +1,5 @@
RESULT not attacker(GPSGateway___hsmSec_GPSdata_encrypted0[!1 = v]) is true.
RESULT not attacker(GPSGateway___hsmSec_GPSdata[!1 = v]) is true.
-RESULT 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.
-RESULT 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.
-RESULT 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.
+RESULT inj-event(authenticity___HSM_CPU_Navigation___hsmSec_sensorData___hsmSec_sensorData_dummy(dummyM)) ==> inj-event(authenticity___SensorUnit___hsmSec_sensorData____hsmSec_sensorData(dummyM)) is true.
+RESULT inj-event(authenticity___HSM_CPU_Navigation___hsmSec_GPSdata___hsmSec_GPSdata_dummy(dummyM)) ==> inj-event(authenticity___GPSGateway___hsmSec_GPSdata____hsmSec_GPSdata(dummyM)) is true.
+RESULT inj-event(authenticity___vehicleControlGateway___hsmSec_vehData___hsmSec_vehData_dummy(dummyM)) ==> inj-event(authenticity___HSM_CPU_Navigation___hsmSec_vehData____hsmSec_vehData(dummyM)) is true.
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/Rovers_SPARTA_DIPLO/MACMapping/golden b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/Rovers_SPARTA_DIPLO/MACMapping/golden
index bc0ac5afae..e295e8d313 100644
--- a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/Rovers_SPARTA_DIPLO/MACMapping/golden
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/Rovers_SPARTA_DIPLO/MACMapping/golden
@@ -1,4 +1,4 @@
RESULT not attacker(Leader_Socket___PlatoonMAC_encrypted0[!1 = v]) is true.
RESULT not attacker(Leader_Socket___PlatoonMAC[!1 = v]) is false.
-RESULT inj-event(authenticity___Socket___PlatoonMAC___decrypt_PlatoonMAC_dummy(dummyM)) ==> inj-event(authenticity___Leader_Socket___PlatoonMAC____encrypt_PlatoonMAC(dummyM)) is false.
-RESULT (but event(authenticity___Socket___PlatoonMAC___decrypt_PlatoonMAC_dummy(dummyM)) ==> event(authenticity___Leader_Socket___PlatoonMAC____encrypt_PlatoonMAC(dummyM)) is true.)
+RESULT inj-event(authenticity___Socket___PlatoonMAC___PlatoonMAC_dummy(dummyM)) ==> inj-event(authenticity___Leader_Socket___PlatoonMAC____PlatoonMAC(dummyM)) is false.
+RESULT (but event(authenticity___Socket___PlatoonMAC___PlatoonMAC_dummy(dummyM)) ==> event(authenticity___Leader_Socket___PlatoonMAC____PlatoonMAC(dummyM)) is true.)
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/Rovers_SPARTA_DIPLO/NoCountermeasureMapping/golden b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/Rovers_SPARTA_DIPLO/NoCountermeasureMapping/golden
index 84a71fb96a..a92bd324e6 100644
--- a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/Rovers_SPARTA_DIPLO/NoCountermeasureMapping/golden
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/Rovers_SPARTA_DIPLO/NoCountermeasureMapping/golden
@@ -1,4 +1,4 @@
RESULT not attacker(Leader_Socket___fromLSocToSoc_chData0[!1 = v]) is false.
-RESULT inj-event(authenticity___Socket___fromLSocToSoc_chData0___aftersignalstate_NoCountermeasure_fromLSocToSoc_NoCountermeasure_fromLSocToSoc(dummyM)) ==> inj-event(authenticity___Leader_Socket___fromLSocToSoc_chData0___signalstate_NoCountermeasure_fromLSocToSoc_NoCountermeasure_fromLSocToSoc718(dummyM)) is false.
-RESULT (even event(authenticity___Socket___fromLSocToSoc_chData0___aftersignalstate_NoCountermeasure_fromLSocToSoc_NoCountermeasure_fromLSocToSoc(dummyM)) ==> event(authenticity___Leader_Socket___fromLSocToSoc_chData0___signalstate_NoCountermeasure_fromLSocToSoc_NoCountermeasure_fromLSocToSoc718(dummyM)) is false.)
+RESULT inj-event(authenticity___Socket___fromLSocToSoc_chData0___aftersignalstate_NoCountermeasure_fromLSocToSoc_NoCountermeasure_fromLSocToSoc(dummyM)) ==> inj-event(authenticity___Leader_Socket___fromLSocToSoc_chData0___signalstate_NoCountermeasure_fromLSocToSoc_NoCountermeasure_fromLSocToSoc(dummyM)) is false.
+RESULT (even event(authenticity___Socket___fromLSocToSoc_chData0___aftersignalstate_NoCountermeasure_fromLSocToSoc_NoCountermeasure_fromLSocToSoc(dummyM)) ==> event(authenticity___Leader_Socket___fromLSocToSoc_chData0___signalstate_NoCountermeasure_fromLSocToSoc_NoCountermeasure_fromLSocToSoc(dummyM)) is false.)
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/Rovers_SPARTA_DIPLO/SymmetricEncryptionNonceMapping/golden b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/Rovers_SPARTA_DIPLO/SymmetricEncryptionNonceMapping/golden
index 0b313e80e6..4be6877af7 100644
--- a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/Rovers_SPARTA_DIPLO/SymmetricEncryptionNonceMapping/golden
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/Rovers_SPARTA_DIPLO/SymmetricEncryptionNonceMapping/golden
@@ -4,6 +4,6 @@ RESULT not attacker(Socket___encrR[!1 = v]) is true.
RESULT not attacker(Leader_Socket___nonceL[!1 = v]) is false.
RESULT not attacker(Leader_Socket___encrL[!1 = v]) is true.
RESULT not attacker(Leader_Socket___encrL_encrypted0[!1 = v]) is true.
-RESULT inj-event(authenticity___Leader_Socket___encrR___decrypt_encrR_dummy(dummyM)) ==> inj-event(authenticity___Socket___encrR____encrypt_encrR(dummyM)) is true.
-RESULT inj-event(authenticity___Socket___encrL___decrypt_encrL_dummy(dummyM)) ==> inj-event(authenticity___Leader_Socket___encrL____encrypt_encrL(dummyM)) is true.
+RESULT inj-event(authenticity___Leader_Socket___encrR___encrR_dummy(dummyM)) ==> inj-event(authenticity___Socket___encrR____encrR(dummyM)) is true.
+RESULT inj-event(authenticity___Socket___encrL___encrL_dummy(dummyM)) ==> inj-event(authenticity___Leader_Socket___encrL____encrL(dummyM)) is true.
--
GitLab