From fce30a7e204bc0724e8f3fe08d70dbec1aea8002 Mon Sep 17 00:00:00 2001
From: Ludovic Apvrille <ludovic.apvrille@telecom-paris.fr>
Date: Mon, 22 May 2023 14:13:46 +0200
Subject: [PATCH] improving test on sec from diplo models
---
modeling/SysMLSec/AliceAndBobHW.xml | 18 +--
.../tmltranslator/DiplodocusSecurityTest.java | 17 ++-
.../keyexchange.tarchi | 116 ++++++++++++++++++
.../keyexchange.tmap | 24 ++++
.../keyexchange.tml | 38 ++++++
.../test_diplo_security_models/mac.tarchi | 116 ++++++++++++++++++
.../test_diplo_security_models/mac.tmap | 24 ++++
.../test_diplo_security_models/mac.tml | 34 +++++
8 files changed, 375 insertions(+), 12 deletions(-)
create mode 100644 ttool/src/test/resources/tmltranslator/test_diplo_security_models/keyexchange.tarchi
create mode 100644 ttool/src/test/resources/tmltranslator/test_diplo_security_models/keyexchange.tmap
create mode 100644 ttool/src/test/resources/tmltranslator/test_diplo_security_models/keyexchange.tml
create mode 100644 ttool/src/test/resources/tmltranslator/test_diplo_security_models/mac.tarchi
create mode 100644 ttool/src/test/resources/tmltranslator/test_diplo_security_models/mac.tmap
create mode 100644 ttool/src/test/resources/tmltranslator/test_diplo_security_models/mac.tml
diff --git a/modeling/SysMLSec/AliceAndBobHW.xml b/modeling/SysMLSec/AliceAndBobHW.xml
index 9c6a11bd43..4bbc4bde31 100644
--- a/modeling/SysMLSec/AliceAndBobHW.xml
+++ b/modeling/SysMLSec/AliceAndBobHW.xml
@@ -1,6 +1,6 @@
<?xml version="1.0" encoding="UTF-8"?>
-<TURTLEGMODELING version="1.0beta" ANIMATE_INTERACTIVE_SIMULATION="true" ACTIVATE_PENALTIES="true" UPDATE_INFORMATION_DIPLO_SIM="true" ANIMATE_WITH_INFO_DIPLO_SIM="true" OPEN_DIAG_DIPLO_SIM="false" LAST_SELECTED_MAIN_TAB="8" LAST_SELECTED_SUB_TAB="0">
+<TURTLEGMODELING version="1.0beta" ANIMATE_INTERACTIVE_SIMULATION="false" ACTIVATE_PENALTIES="true" UPDATE_INFORMATION_DIPLO_SIM="false" ANIMATE_WITH_INFO_DIPLO_SIM="false" OPEN_DIAG_DIPLO_SIM="false" LAST_SELECTED_MAIN_TAB="9" LAST_SELECTED_SUB_TAB="0">
<Modeling type="TML Component Design" nameTab="SymmetricExchange" tabs="TML Component Task Diagram$Bob$Alice" >
<TMLComponentTaskDiagramPanel name="TML Component Task Diagram" minX="10" maxX="2500" minY="10" maxY="1500" channels="true" events="true" requests="true" considerExecOperators="true" considerTimingOperators="true" zoom="1.0" >
@@ -8,8 +8,8 @@
<cdparam x="392" y="173" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector" value="Connector between ports" />
-<P1 x="412" y="187" id="13" />
-<P2 x="466" y="188" id="2" />
+<P1 x="399" y="174" id="13" />
+<P2 x="479" y="175" id="2" />
<AutomaticDrawing data="true" />
<new d="false" />
</CONNECTOR>
@@ -862,8 +862,8 @@
<cdparam x="578" y="303" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector" value="Connector between ports" />
-<P1 x="590" y="318" id="371" />
-<P2 x="659" y="318" id="358" />
+<P1 x="577" y="306" id="371" />
+<P2 x="671" y="306" id="358" />
<AutomaticDrawing data="true" />
<new d="false" />
</CONNECTOR>
@@ -871,8 +871,8 @@
<cdparam x="578" y="246" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector" value="Connector between ports" />
-<P1 x="590" y="275" id="369" />
-<P2 x="659" y="275" id="356" />
+<P1 x="577" y="263" id="369" />
+<P2 x="671" y="263" id="356" />
<AutomaticDrawing data="true" />
<new d="false" />
</CONNECTOR>
@@ -1853,8 +1853,8 @@
<cdparam x="404" y="206" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector" value="Connector between ports" />
-<P1 x="404" y="206" id="745" />
-<P2 x="480" y="206" id="734" />
+<P1 x="391" y="193" id="745" />
+<P2 x="493" y="193" id="734" />
<AutomaticDrawing data="true" />
<new d="false" />
</CONNECTOR>
diff --git a/ttool/src/test/java/tmltranslator/DiplodocusSecurityTest.java b/ttool/src/test/java/tmltranslator/DiplodocusSecurityTest.java
index cc0266ef04..dfe0bdd92b 100644
--- a/ttool/src/test/java/tmltranslator/DiplodocusSecurityTest.java
+++ b/ttool/src/test/java/tmltranslator/DiplodocusSecurityTest.java
@@ -43,13 +43,24 @@ import static org.junit.Assert.*;
public class DiplodocusSecurityTest extends AbstractTest {
final static String DIR_GEN = "tmltranslator/test_diplo_security/";
final static String DIR_MODELS = "tmltranslator/test_diplo_security_models/";
- final String [] MODELS_DIPLO_SECURITY = {"symetric", "nonce"};
+ final String [] MODELS_DIPLO_SECURITY = {"symetric", "nonce", "keyexchange", "mac"};
private static final List<List<String>> LIST_OF_LISTS_OF_QUERIES = Arrays.asList(
Arrays.asList("Query not attacker(Alice___SymmetricExchange__comm_chData[!1 = v]) is true.",
- "Query inj-event(authenticity___Bob___SymmetricExchange__comm_chData___aftersignalstate_SymmetricExchange_comm_SymmetricExchange_comm(dummyM)) ==> inj-event(authenticity___Alice___SymmetricExchange__comm_chData___signalstate_SymmetricExchange_comm_SymmetricExchange_comm(dummyM)) is false."),
+ "Query inj-event(authenticity___Bob___SymmetricExchange__comm_chData___aftersignalstate_SymmetricExchange_comm_" +
+ "SymmetricExchange_comm(dummyM)) ==> inj-event(authenticity___Alice___SymmetricExchange__comm_chData" +
+ "___signalstate_SymmetricExchange_comm_SymmetricExchange_comm(dummyM)) is false."),
Arrays.asList("Query not attacker(Alice___nonce__comm_chData[!1 = v]) is true.",
"Query inj-event(authenticity___Bob___nonce__comm_chData___aftersignalstate_nonce_comm_nonce_comm(dummyM)) ==> inj-event" +
- "(authenticity___Alice___nonce__comm_chData___signalstate_nonce_comm_nonce_comm(dummyM)) is false.")
+ "(authenticity___Alice___nonce__comm_chData___signalstate_nonce_comm_nonce_comm(dummyM)) is false."),
+ Arrays.asList("Query not attacker(Alice___KeyExchange__comm_chData[!1 = v]) is true.", "RESULT inj-event" +
+ "(authenticity___Bob___KeyExchange__comm_chData___aftersignalstate_KeyExchange_comm_KeyExchange_comm283" +
+ "(dummyM)) ==> inj-event(authenticity___Alice___KeyExchange__comm_chData___signalstate_KeyExchange_comm_KeyExchange_comm239" +
+ "(dummyM)) is true.", "Query inj-event(authenticity___Bob___KeyExchange__comm_chData___aftersignalstate_KeyExchange_comm" +
+ "_KeyExchange_comm283(dummyM)) ==> inj-event(authenticity___Alice___KeyExchange__comm_chData" +
+ "___signalstate_KeyExchange_comm_KeyExchange_comm239(dummyM)) is true."),
+ Arrays.asList("Query not attacker(Alice___MAC__comm_chData[!1 = v]) is true.",
+ "Query inj-event(authenticity___Bob___MAC__comm_chData___aftersignalstate_MAC_comm_MAC_comm(dummyM)) ==> inj-event(authenticity" +
+ "___Alice___MAC__comm_chData___signalstate_MAC_comm_MAC_comm(dummyM)) is false")
);
private static final String PROVERIF_SUMMARY = "Verification summary:";
private static final String PROVERIF_QUERY = "Query";
diff --git a/ttool/src/test/resources/tmltranslator/test_diplo_security_models/keyexchange.tarchi b/ttool/src/test/resources/tmltranslator/test_diplo_security_models/keyexchange.tarchi
new file mode 100644
index 0000000000..5b05969400
--- /dev/null
+++ b/ttool/src/test/resources/tmltranslator/test_diplo_security_models/keyexchange.tarchi
@@ -0,0 +1,116 @@
+// Master clock frequency - in MHz
+MASTERCLOCKFREQUENCY 200
+
+NODE BRIDGE BridgeAlice
+SET BridgeAlice bufferByteSize 4
+SET BridgeAlice clockDivider 1
+
+NODE BRIDGE BridgeBob
+SET BridgeBob bufferByteSize 4
+SET BridgeBob clockDivider 1
+
+NODE MEMORY ExternalMemory
+SET ExternalMemory byteDataSize 4
+SET ExternalMemory clockDivider 1
+
+NODE MEMORY MemoryAlice
+SET MemoryAlice byteDataSize 4
+SET MemoryAlice clockDivider 1
+
+NODE MEMORY MemoryBob
+SET MemoryBob byteDataSize 4
+SET MemoryBob clockDivider 1
+
+NODE BUS BusBob
+SET BusBob byteDataSize 4
+SET BusBob pipelineSize 1
+SET BusBob arbitration 0
+SET BusBob sliceTime 10000
+SET BusBob burstSize 100
+SET BusBob privacy private
+SET BusBob clockDivider 1
+
+NODE BUS BusAlice
+SET BusAlice byteDataSize 4
+SET BusAlice pipelineSize 1
+SET BusAlice arbitration 0
+SET BusAlice sliceTime 10000
+SET BusAlice burstSize 100
+SET BusAlice privacy private
+SET BusAlice clockDivider 1
+
+NODE BUS ExternalBus
+SET ExternalBus byteDataSize 4
+SET ExternalBus pipelineSize 1
+SET ExternalBus arbitration 0
+SET ExternalBus sliceTime 10000
+SET ExternalBus burstSize 100
+SET ExternalBus privacy public
+SET ExternalBus clockDivider 1
+
+NODE CPU CPUAlice
+SET CPUAlice nbOfCores 1
+SET CPUAlice byteDataSize 4
+SET CPUAlice pipelineSize 5
+SET CPUAlice goIdleTime 10
+SET CPUAlice maxConsecutiveIdleCycles 10
+SET CPUAlice taskSwitchingTime 20
+SET CPUAlice branchingPredictionPenalty 2
+SET CPUAlice cacheMiss 5
+SET CPUAlice schedulingPolicy 0
+SET CPUAlice sliceTime 10000
+SET CPUAlice execiTime 1
+SET CPUAlice execcTime 1
+SET CPUAlice clockDivider 1
+
+NODE CPU CPUBob
+SET CPUBob nbOfCores 1
+SET CPUBob byteDataSize 4
+SET CPUBob pipelineSize 5
+SET CPUBob goIdleTime 10
+SET CPUBob maxConsecutiveIdleCycles 10
+SET CPUBob taskSwitchingTime 20
+SET CPUBob branchingPredictionPenalty 2
+SET CPUBob cacheMiss 5
+SET CPUBob schedulingPolicy 0
+SET CPUBob sliceTime 10000
+SET CPUBob execiTime 1
+SET CPUBob execcTime 1
+SET CPUBob clockDivider 1
+
+NODE LINK link_BridgeBob_to_BusBob
+SET link_BridgeBob_to_BusBob node BridgeBob
+SET link_BridgeBob_to_BusBob bus BusBob
+SET link_BridgeBob_to_BusBob priority 0
+NODE LINK link_BridgeBob_to_ExternalBus
+SET link_BridgeBob_to_ExternalBus node BridgeBob
+SET link_BridgeBob_to_ExternalBus bus ExternalBus
+SET link_BridgeBob_to_ExternalBus priority 0
+NODE LINK link_BridgeAlice_to_ExternalBus
+SET link_BridgeAlice_to_ExternalBus node BridgeAlice
+SET link_BridgeAlice_to_ExternalBus bus ExternalBus
+SET link_BridgeAlice_to_ExternalBus priority 0
+NODE LINK link_BridgeAlice_to_BusAlice
+SET link_BridgeAlice_to_BusAlice node BridgeAlice
+SET link_BridgeAlice_to_BusAlice bus BusAlice
+SET link_BridgeAlice_to_BusAlice priority 0
+NODE LINK link_ExternalMemory_to_ExternalBus
+SET link_ExternalMemory_to_ExternalBus node ExternalMemory
+SET link_ExternalMemory_to_ExternalBus bus ExternalBus
+SET link_ExternalMemory_to_ExternalBus priority 0
+NODE LINK link_CPUAlice_to_BusAlice
+SET link_CPUAlice_to_BusAlice node CPUAlice
+SET link_CPUAlice_to_BusAlice bus BusAlice
+SET link_CPUAlice_to_BusAlice priority 0
+NODE LINK link_MemoryAlice_to_BusAlice
+SET link_MemoryAlice_to_BusAlice node MemoryAlice
+SET link_MemoryAlice_to_BusAlice bus BusAlice
+SET link_MemoryAlice_to_BusAlice priority 0
+NODE LINK link_MemoryBob_to_BusBob
+SET link_MemoryBob_to_BusBob node MemoryBob
+SET link_MemoryBob_to_BusBob bus BusBob
+SET link_MemoryBob_to_BusBob priority 0
+NODE LINK link_CPUBob_to_BusBob
+SET link_CPUBob_to_BusBob node CPUBob
+SET link_CPUBob_to_BusBob bus BusBob
+SET link_CPUBob_to_BusBob priority 0
diff --git a/ttool/src/test/resources/tmltranslator/test_diplo_security_models/keyexchange.tmap b/ttool/src/test/resources/tmltranslator/test_diplo_security_models/keyexchange.tmap
new file mode 100644
index 0000000000..d0d283372a
--- /dev/null
+++ b/ttool/src/test/resources/tmltranslator/test_diplo_security_models/keyexchange.tmap
@@ -0,0 +1,24 @@
+TMLSPEC
+ #include "keyexchange.tml"
+ENDTMLSPEC
+
+TMLARCHI
+ #include "keyexchange.tarchi"
+ENDTMLARCHI
+
+TMLMAPPING
+ MAP CPUAlice KeyExchange__Alice
+ SET KeyExchange__Alice priority 0
+ MAP CPUBob KeyExchange__Bob
+ SET KeyExchange__Bob priority 0
+ MAP ExternalMemory KeyExchange__comm
+ SET KeyExchange__comm priority 0
+ MAP ExternalBus KeyExchange__comm
+ SET KeyExchange__comm priority 0
+ MAP BusAlice KeyExchange__comm
+ SET KeyExchange__comm priority 0
+ MAP BusBob KeyExchange__comm
+ SET KeyExchange__comm priority 0
+ MAPSEC MemoryBob aenc
+ MAPSEC MemoryAlice symKey
+ENDTMLMAPPING
diff --git a/ttool/src/test/resources/tmltranslator/test_diplo_security_models/keyexchange.tml b/ttool/src/test/resources/tmltranslator/test_diplo_security_models/keyexchange.tml
new file mode 100644
index 0000000000..6de0229a51
--- /dev/null
+++ b/ttool/src/test/resources/tmltranslator/test_diplo_security_models/keyexchange.tml
@@ -0,0 +1,38 @@
+// TML Application - FORMAT 0.2
+// Application: /Users/ludovicapvrille/TTool/modeling/SysMLSec/AliceAndBobHW.xml
+// Generated: Mon May 22 13:40:05 CEST 2023
+
+// PRAGMAS
+
+// Channels
+CHANNEL KeyExchange__comm NBRNBW 4 OUT KeyExchange__Alice IN KeyExchange__Bob
+VCCHANNEL KeyExchange__comm 0
+CONFCHANNEL KeyExchange__comm
+AUTHCHANNEL KeyExchange__comm
+
+// Events
+
+// Requests
+
+TASK KeyExchange__Alice
+ TASKOP
+ //Local variables
+
+ //Behavior
+ EXECC 100 aenc AE 100 100 0 0 - - 1
+ WRITE KeyExchange__comm 1+0 aenc
+ EXECC 100 symKey SE 100 100 0 0 - - 1
+ WRITE KeyExchange__comm 1+0 symKey
+ENDTASK
+
+TASK KeyExchange__Bob
+ TASKOP
+ //Local variables
+
+ //Behavior
+ READ KeyExchange__comm 1+0 aenc
+ EXECC 100 aenc AE 100 100 0 0 - - 2
+ READ KeyExchange__comm 1+0 symKey
+ EXECC 100 symKey SE 100 100 0 0 - - 2
+ENDTASK
+
diff --git a/ttool/src/test/resources/tmltranslator/test_diplo_security_models/mac.tarchi b/ttool/src/test/resources/tmltranslator/test_diplo_security_models/mac.tarchi
new file mode 100644
index 0000000000..5b05969400
--- /dev/null
+++ b/ttool/src/test/resources/tmltranslator/test_diplo_security_models/mac.tarchi
@@ -0,0 +1,116 @@
+// Master clock frequency - in MHz
+MASTERCLOCKFREQUENCY 200
+
+NODE BRIDGE BridgeAlice
+SET BridgeAlice bufferByteSize 4
+SET BridgeAlice clockDivider 1
+
+NODE BRIDGE BridgeBob
+SET BridgeBob bufferByteSize 4
+SET BridgeBob clockDivider 1
+
+NODE MEMORY ExternalMemory
+SET ExternalMemory byteDataSize 4
+SET ExternalMemory clockDivider 1
+
+NODE MEMORY MemoryAlice
+SET MemoryAlice byteDataSize 4
+SET MemoryAlice clockDivider 1
+
+NODE MEMORY MemoryBob
+SET MemoryBob byteDataSize 4
+SET MemoryBob clockDivider 1
+
+NODE BUS BusBob
+SET BusBob byteDataSize 4
+SET BusBob pipelineSize 1
+SET BusBob arbitration 0
+SET BusBob sliceTime 10000
+SET BusBob burstSize 100
+SET BusBob privacy private
+SET BusBob clockDivider 1
+
+NODE BUS BusAlice
+SET BusAlice byteDataSize 4
+SET BusAlice pipelineSize 1
+SET BusAlice arbitration 0
+SET BusAlice sliceTime 10000
+SET BusAlice burstSize 100
+SET BusAlice privacy private
+SET BusAlice clockDivider 1
+
+NODE BUS ExternalBus
+SET ExternalBus byteDataSize 4
+SET ExternalBus pipelineSize 1
+SET ExternalBus arbitration 0
+SET ExternalBus sliceTime 10000
+SET ExternalBus burstSize 100
+SET ExternalBus privacy public
+SET ExternalBus clockDivider 1
+
+NODE CPU CPUAlice
+SET CPUAlice nbOfCores 1
+SET CPUAlice byteDataSize 4
+SET CPUAlice pipelineSize 5
+SET CPUAlice goIdleTime 10
+SET CPUAlice maxConsecutiveIdleCycles 10
+SET CPUAlice taskSwitchingTime 20
+SET CPUAlice branchingPredictionPenalty 2
+SET CPUAlice cacheMiss 5
+SET CPUAlice schedulingPolicy 0
+SET CPUAlice sliceTime 10000
+SET CPUAlice execiTime 1
+SET CPUAlice execcTime 1
+SET CPUAlice clockDivider 1
+
+NODE CPU CPUBob
+SET CPUBob nbOfCores 1
+SET CPUBob byteDataSize 4
+SET CPUBob pipelineSize 5
+SET CPUBob goIdleTime 10
+SET CPUBob maxConsecutiveIdleCycles 10
+SET CPUBob taskSwitchingTime 20
+SET CPUBob branchingPredictionPenalty 2
+SET CPUBob cacheMiss 5
+SET CPUBob schedulingPolicy 0
+SET CPUBob sliceTime 10000
+SET CPUBob execiTime 1
+SET CPUBob execcTime 1
+SET CPUBob clockDivider 1
+
+NODE LINK link_BridgeBob_to_BusBob
+SET link_BridgeBob_to_BusBob node BridgeBob
+SET link_BridgeBob_to_BusBob bus BusBob
+SET link_BridgeBob_to_BusBob priority 0
+NODE LINK link_BridgeBob_to_ExternalBus
+SET link_BridgeBob_to_ExternalBus node BridgeBob
+SET link_BridgeBob_to_ExternalBus bus ExternalBus
+SET link_BridgeBob_to_ExternalBus priority 0
+NODE LINK link_BridgeAlice_to_ExternalBus
+SET link_BridgeAlice_to_ExternalBus node BridgeAlice
+SET link_BridgeAlice_to_ExternalBus bus ExternalBus
+SET link_BridgeAlice_to_ExternalBus priority 0
+NODE LINK link_BridgeAlice_to_BusAlice
+SET link_BridgeAlice_to_BusAlice node BridgeAlice
+SET link_BridgeAlice_to_BusAlice bus BusAlice
+SET link_BridgeAlice_to_BusAlice priority 0
+NODE LINK link_ExternalMemory_to_ExternalBus
+SET link_ExternalMemory_to_ExternalBus node ExternalMemory
+SET link_ExternalMemory_to_ExternalBus bus ExternalBus
+SET link_ExternalMemory_to_ExternalBus priority 0
+NODE LINK link_CPUAlice_to_BusAlice
+SET link_CPUAlice_to_BusAlice node CPUAlice
+SET link_CPUAlice_to_BusAlice bus BusAlice
+SET link_CPUAlice_to_BusAlice priority 0
+NODE LINK link_MemoryAlice_to_BusAlice
+SET link_MemoryAlice_to_BusAlice node MemoryAlice
+SET link_MemoryAlice_to_BusAlice bus BusAlice
+SET link_MemoryAlice_to_BusAlice priority 0
+NODE LINK link_MemoryBob_to_BusBob
+SET link_MemoryBob_to_BusBob node MemoryBob
+SET link_MemoryBob_to_BusBob bus BusBob
+SET link_MemoryBob_to_BusBob priority 0
+NODE LINK link_CPUBob_to_BusBob
+SET link_CPUBob_to_BusBob node CPUBob
+SET link_CPUBob_to_BusBob bus BusBob
+SET link_CPUBob_to_BusBob priority 0
diff --git a/ttool/src/test/resources/tmltranslator/test_diplo_security_models/mac.tmap b/ttool/src/test/resources/tmltranslator/test_diplo_security_models/mac.tmap
new file mode 100644
index 0000000000..605264b48a
--- /dev/null
+++ b/ttool/src/test/resources/tmltranslator/test_diplo_security_models/mac.tmap
@@ -0,0 +1,24 @@
+TMLSPEC
+ #include "mac.tml"
+ENDTMLSPEC
+
+TMLARCHI
+ #include "mac.tarchi"
+ENDTMLARCHI
+
+TMLMAPPING
+ MAP CPUAlice MAC__Alice
+ SET MAC__Alice priority 0
+ MAP CPUBob MAC__Bob
+ SET MAC__Bob priority 0
+ MAP ExternalMemory MAC__comm
+ SET MAC__comm priority 0
+ MAP ExternalBus MAC__comm
+ SET MAC__comm priority 0
+ MAP BusAlice MAC__comm
+ SET MAC__comm priority 0
+ MAP BusBob MAC__comm
+ SET MAC__comm priority 0
+ MAPSEC MemoryAlice mac
+ MAPSEC MemoryBob mac
+ENDTMLMAPPING
diff --git a/ttool/src/test/resources/tmltranslator/test_diplo_security_models/mac.tml b/ttool/src/test/resources/tmltranslator/test_diplo_security_models/mac.tml
new file mode 100644
index 0000000000..01b38d3e83
--- /dev/null
+++ b/ttool/src/test/resources/tmltranslator/test_diplo_security_models/mac.tml
@@ -0,0 +1,34 @@
+// TML Application - FORMAT 0.2
+// Application: /Users/ludovicapvrille/TTool/modeling/SysMLSec/AliceAndBobHW.xml
+// Generated: Mon May 22 14:07:26 CEST 2023
+
+// PRAGMAS
+
+// Channels
+CHANNEL MAC__comm NBRNBW 4 OUT MAC__Alice IN MAC__Bob
+VCCHANNEL MAC__comm 0
+CONFCHANNEL MAC__comm
+AUTHCHANNEL MAC__comm
+
+// Events
+
+// Requests
+
+TASK MAC__Alice
+ TASKOP
+ //Local variables
+
+ //Behavior
+ EXECC 100 mac MAC 100 100 0 0 - - 1
+ WRITE MAC__comm 1+0 mac
+ENDTASK
+
+TASK MAC__Bob
+ TASKOP
+ //Local variables
+
+ //Behavior
+ READ MAC__comm 1+0 mac
+ EXECC 100 mac MAC 100 100 0 0 - - 2
+ENDTASK
+
--
GitLab