From 2fa2b166ef861e791d7df6f34426caccf5b690b3 Mon Sep 17 00:00:00 2001
From: dontenvi <pierre.dontenville@eurecom.fr>
Date: Sat, 20 Jan 2024 19:49:29 -0500
Subject: [PATCH] new golden, without autoAuthChan
---
.../tmltranslator/DiplodocusSecurityTest.java | 15 ++++++++-------
.../Models/AliceAndBobHW/KeyExchange/golden | 4 ----
.../Models/AliceAndBobHW/Mac/golden | 1 -
.../Models/AliceAndBobHW/Nonce/golden | 1 -
.../Models/AliceAndBobHW/SymmetricExchange/golden | 1 -
.../Models/ITA01_v6/mapAtt/golden | 2 --
.../Models/ITA01_v6/mapNoProtection/golden | 2 --
.../Models/ITSDemo/Architecture_enc_or/golden | 3 ---
.../Models/ITSDemo/Architecture_hsm/golden | 3 ---
.../Models/Rovers_SPARTA_DIPLO/MACMapping/golden | 1 -
.../NoCountermeasureMapping/golden | 2 +-
.../SymmetricEncryptionNonceMapping/golden | 4 ----
12 files changed, 9 insertions(+), 30 deletions(-)
diff --git a/ttool/src/test/java/tmltranslator/DiplodocusSecurityTest.java b/ttool/src/test/java/tmltranslator/DiplodocusSecurityTest.java
index 2ac98b175b..995286d9b6 100644
--- a/ttool/src/test/java/tmltranslator/DiplodocusSecurityTest.java
+++ b/ttool/src/test/java/tmltranslator/DiplodocusSecurityTest.java
@@ -72,10 +72,10 @@ public class DiplodocusSecurityTest extends AbstractTest {
return Arrays.asList(new Object[][] {
// {"AliceAndBobHW", new ArrayList<>(Arrays.asList("KeyExchange"))}, //the tab which include ID issue in golden
{"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",
-// "Rover"))},
-// {"ITSDemo", new ArrayList<>(Arrays.asList("Architecture_enc_or", "Architecture_hsm"))}
+ {"ITA01_v6", new ArrayList<>(Arrays.asList("mapAtt", "mapNoProtection"))},
+ {"Rovers_SPARTA_DIPLO", new ArrayList<>(Arrays.asList("NoCountermeasureMapping", "MACMapping","SymmetricEncryptionNonceMapping",
+ "Rover"))},
+ {"ITSDemo", new ArrayList<>(Arrays.asList("Architecture_enc_or", "Architecture_hsm"))}
});
}
@@ -145,9 +145,9 @@ public class DiplodocusSecurityTest extends AbstractTest {
System.out.println("Generating ProVerif code for " + tab);
TML2Avatar t2a = new TML2Avatar(tmap, false, true, null);
- AvatarSpecification avatarspec = t2a.generateAvatarSpec("1", true);
+ AvatarSpecification avatarspec = t2a.generateAvatarSpec("1", false);
AVATAR2ProVerif avatar2proverif = new AVATAR2ProVerif(avatarspec);
- ProVerifSpec proverif = avatar2proverif.generateProVerif(true, true, 0, true,
+ ProVerifSpec proverif = avatar2proverif.generateProVerif(true, true, 3, true,
true);
String pvspecFilename = currentModel + "_" + tab;
@@ -177,9 +177,10 @@ public class DiplodocusSecurityTest extends AbstractTest {
while ((str = proc_in.readLine()) != null) {
// TraceManager.addDev( "Sending " + str + " from " + port + " to client..." );
bw.write(str + "\n");
- System.out.println("Output from ProVerif: " + str);
+// System.out.println("Output from ProVerif: " + str);
if (summaryFound && (str.contains(PROVERIF_QUERY))) {
+ System.out.println(str);
// assertTrue(goldenMap.get(tab).length > nbLines);
// assertTrue(equals(goldenMap.get(tab)[nbLines], str));
nbLines++;
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 d6f0cf9946..59fed64c69 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 @@
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/DiplodocusSecurityTest/Models/AliceAndBobHW/Mac/golden b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/Mac/golden
index 4436f6f06d..41f3a49a94 100644
--- a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/Mac/golden
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/Mac/golden
@@ -1,2 +1 @@
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/DiplodocusSecurityTest/Models/AliceAndBobHW/Nonce/golden b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/Nonce/golden
index 6777b481ce..bd548d626c 100644
--- a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/Nonce/golden
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/Nonce/golden
@@ -1,2 +1 @@
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/DiplodocusSecurityTest/Models/AliceAndBobHW/SymmetricExchange/golden b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/SymmetricExchange/golden
index 5e788c2fbc..88a800096b 100644
--- a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/SymmetricExchange/golden
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/SymmetricExchange/golden
@@ -1,2 +1 @@
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/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v6/mapAtt/golden b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v6/mapAtt/golden
index 145f3ec93b..d692c30a92 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,5 +1,3 @@
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(SmartphoneAppController___Application__emergencySign_chData[!1 = v]) is true.
-Query inj-event(authenticity___MedicalInformationSystem___emergencySign_chData___aftersignalstate_Application_emergencySign_Application_emergencySign(dummyM)) ==> inj-event(authenticity___SmartphoneAppController___emergencySign_chData___signalstate_Application_emergencySign_Application_emergencySign(dummyM)) is false.
-Query inj-event(authenticity___SmartphoneAppController___feedback4App_chData___aftersignalstate_Application_feedback4App_Application_feedback4App(dummyM)) ==> inj-event(authenticity___PumpController___feedback4App_chData___signalstate_Application_feedback4App_Application_feedback4App(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 04b400fddd..b3c4c7afca 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,5 +1,3 @@
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(SmartphoneAppController___Application__emergencySign_chData[!1 = v]) is true.
-Query inj-event(authenticity___MedicalInformationSystem___emergencySign_chData___aftersignalstate_Application_emergencySign_Application_emergencySign(dummyM)) ==> inj-event(authenticity___SmartphoneAppController___emergencySign_chData___signalstate_Application_emergencySign_Application_emergencySign(dummyM)) is true.
-Query inj-event(authenticity___SmartphoneAppController___feedback4App_chData___aftersignalstate_Application_feedback4App_Application_feedback4App(dummyM)) ==> inj-event(authenticity___PumpController___feedback4App_chData___signalstate_Application_feedback4App_Application_feedback4App(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 147d4b399c..4752753d98 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
@@ -1,4 +1 @@
Query not attacker(GPSGateway___App_enc_or__GPSdata_chData[!1 = v]) is true.
-Query inj-event(authenticity___NavigationControl___GPSdata_chData___aftersignalstate_App_enc_or_GPSdata_App_enc_or_GPSdata(dummyM)) ==> inj-event(authenticity___GPSGateway___GPSdata_chData___signalstate_App_enc_or_GPSdata_App_enc_or_GPSdata(dummyM)) is false.
-Query inj-event(authenticity___NavigationControl___sensorData_chData___aftersignalstate_App_enc_or_sensorData_App_enc_or_sensorData(dummyM)) ==> inj-event(authenticity___SensorUnit___sensorData_chData___signalstate_App_enc_or_sensorData_App_enc_or_sensorData3304(dummyM)) is false.
-Query inj-event(authenticity___vehicleControlGateway___vehData_chData___aftersignalstate_App_enc_or_vehData_App_enc_or_vehData(dummyM)) ==> inj-event(authenticity___NavigationControl___vehData_chData___signalstate_App_enc_or_vehData_App_enc_or_vehData(dummyM)) is false.
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 adf6224222..265208ad53 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,4 +1 @@
Query not attacker(GPSGateway___App_hsm__GPSdata_chData[!1 = v]) is true.
-Query inj-event(authenticity___NavigationControl___sensorData_chData___aftersignalstate_App_hsm_sensorData_App_hsm_sensorData(dummyM)) ==> inj-event(authenticity___SensorUnit___sensorData_chData___signalstate_App_hsm_sensorData_App_hsm_sensorData4191(dummyM)) is false.
-Query inj-event(authenticity___vehicleControlGateway___vehData_chData___aftersignalstate_App_hsm_vehData_App_hsm_vehData(dummyM)) ==> inj-event(authenticity___NavigationControl___vehData_chData___signalstate_App_hsm_vehData_App_hsm_vehData(dummyM)) is false.
-Query inj-event(authenticity___NavigationControl___GPSdata_chData___aftersignalstate_App_hsm_GPSdata_App_hsm_GPSdata(dummyM)) ==> inj-event(authenticity___GPSGateway___GPSdata_chData___signalstate_App_hsm_GPSdata_App_hsm_GPSdata(dummyM)) is false.
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 436b4bef6f..e69de29bb2 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 +0,0 @@
-Query inj-event(authenticity___Socket___fromLSocToSoc_chData___aftersignalstate_MAC_fromLSocToSoc_MAC_fromLSocToSoc(dummyM)) ==> inj-event(authenticity___Leader_Socket___fromLSocToSoc_chData___signalstate_MAC_fromLSocToSoc_MAC_fromLSocToSoc1753(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 bf1534064c..c458131e69 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 +1 @@
-Query inj-event(authenticity___Socket___fromLSocToSoc_chData___aftersignalstate_NoCountermeasure_fromLSocToSoc_NoCountermeasure_fromLSocToSoc(dummyM)) ==> inj-event(authenticity___Leader_Socket___fromLSocToSoc_chData___signalstate_NoCountermeasure_fromLSocToSoc_NoCountermeasure_fromLSocToSoc693(dummyM)) is false.
+Query inj-event(authenticity___Socket___fromLSocToSoc_chData___aftersignalstate_NoCountermeasure_fromLSocToSoc_NoCountermeasure_fromLSocToSoc(dummyM)) ==> inj-event(authenticity___Leader_Socket___fromLSocToSoc_chData___signalstate_NoCountermeasure_fromLSocToSoc_NoCountermeasure_fromLSocToSoc3934(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 5ee10f1144..e69de29bb2 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
@@ -1,4 +0,0 @@
-Query inj-event(authenticity___Socket___fromLSocToSoc_chData___aftersignalstate_SymmetricEncryptionNonce_fromLSocToSoc_SymmetricEncryptionNonce_fromLSocToSoc(dummyM)) ==> inj-event(authenticity___Leader_Socket___fromLSocToSoc_chData___signalstate_SymmetricEncryptionNonce_fromLSocToSoc_SymmetricEncryptionNonce_fromLSocToSoc2856(dummyM)) is true.
-Query inj-event(authenticity___Socket___fromLSocToSoc_chData___aftersignalstate_SymmetricEncryptionNonce_fromLSocToSoc_SymmetricEncryptionNonce_fromLSocToSoc2450(dummyM)) ==> inj-event(authenticity___Leader_Socket___fromLSocToSoc_chData___signalstate_SymmetricEncryptionNonce_fromLSocToSoc_SymmetricEncryptionNonce_fromLSocToSoc2856(dummyM)) is true.
-Query inj-event(authenticity___Socket___fromLSocToSoc_chData___aftersignalstate_SymmetricEncryptionNonce_fromLSocToSoc_SymmetricEncryptionNonce_fromLSocToSoc(dummyM)) ==> inj-event(authenticity___Leader_Socket___fromLSocToSoc_chData___signalstate_SymmetricEncryptionNonce_fromLSocToSoc_SymmetricEncryptionNonce_fromLSocToSoc2872(dummyM)) is true.
-Query inj-event(authenticity___Socket___fromLSocToSoc_chData___aftersignalstate_SymmetricEncryptionNonce_fromLSocToSoc_SymmetricEncryptionNonce_fromLSocToSoc2450(dummyM)) ==> inj-event(authenticity___Leader_Socket___fromLSocToSoc_chData___signalstate_SymmetricEncryptionNonce_fromLSocToSoc_SymmetricEncryptionNonce_fromLSocToSoc2872(dummyM)) is true.
--
GitLab