diff --git a/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bcm b/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bcm
index 7823a6793f6a585f815f5844d7935ff3c11a7bda..e11b278ca8d3667a1c0c7a62e9b4f382e8a515b2 100644
--- a/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bcm
+++ b/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bcm
@@ -64,9 +64,9 @@
         <org.eventb.core.scAction name=")" org.eventb.core.assignment="subscriptions ≔ ∅ ⦂ ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)" org.eventb.core.label="act3" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_zpBzkcQ4Ee609fto5wotHA"/>
         <org.eventb.core.scAction name="*" org.eventb.core.assignment="gateway_pending_events ≔ ∅ ⦂ ℙ(GATEWAYS×TARGET_TRANSACTIONS)" org.eventb.core.label="act4" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_zpBzksQ4Ee609fto5wotHA"/>
         <org.eventb.core.scAction name="+" org.eventb.core.assignment="received_target_transactions ≔ ∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS)" org.eventb.core.label="act6" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_zpCaoMQ4Ee609fto5wotHA"/>
-        <org.eventb.core.scAction name="," org.eventb.core.assignment="authenticated_users ≔ ∅ ⦂ ℙ(USERS)" org.eventb.core.label="act11" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_jV8FAMEWEe6yC4BToIaAqA"/>
-        <org.eventb.core.scAction name="-" org.eventb.core.assignment="authenticated_transactions ≔ ∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS×USERS)" org.eventb.core.label="act12" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_jV8FAcEWEe6yC4BToIaAqA"/>
-        <org.eventb.core.scAction name="." org.eventb.core.assignment="grants ≔ ∅ ⦂ ℙ(USERS×PERMISSIONS)" org.eventb.core.label="act14" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_0oC5cMErEe6yC4BToIaAqA"/>
+        <org.eventb.core.scAction name="," org.eventb.core.assignment="authenticated_users ≔ ∅ ⦂ ℙ(USERS)" org.eventb.core.label="act11" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_CJbpkPRrEe60CqkwWvstGA|org.eventb.core.action#_jV8FAMEWEe6yC4BToIaAqA"/>
+        <org.eventb.core.scAction name="-" org.eventb.core.assignment="authenticated_transactions ≔ ∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS×USERS)" org.eventb.core.label="act12" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_CJbpkPRrEe60CqkwWvstGA|org.eventb.core.action#_jV8FAcEWEe6yC4BToIaAqA"/>
+        <org.eventb.core.scAction name="." org.eventb.core.assignment="grants ≔ ∅ ⦂ ℙ(USERS×PERMISSIONS)" org.eventb.core.label="act14" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_CJbpkPRrEe60CqkwWvstGA|org.eventb.core.action#_0oC5cMErEe6yC4BToIaAqA"/>
         <org.eventb.core.scAction name="/" org.eventb.core.assignment="subscribed ≔ 0" org.eventb.core.label="act31" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_FVN5wMHOEe609fto5wotHA"/>
         <org.eventb.core.scAction name="0" org.eventb.core.assignment="initiated ≔ 0" org.eventb.core.label="act32" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_FVN5wcHOEe609fto5wotHA"/>
         <org.eventb.core.scAction name="1" org.eventb.core.assignment="emitted ≔ 0" org.eventb.core.label="act33" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_FVOg0MHOEe609fto5wotHA"/>
diff --git a/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo b/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo
index 3db49db70912b9dbffdf5d0ced987e4f06c44bf7..2f2c9d560534e03eb6cb453796493613f220cb44 100644
--- a/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo
+++ b/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo
@@ -1,5 +1,5 @@
 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
-<org.eventb.core.poFile org.eventb.core.poStamp="11">
+<org.eventb.core.poFile org.eventb.core.poStamp="12">
     <org.eventb.core.poPredicateSet name="CTXHYP" org.eventb.core.poStamp="11">
         <org.eventb.core.poIdentifier name="TARGET_TRANSACTIONS" org.eventb.core.type="ℙ(TARGET_TRANSACTIONS)"/>
         <org.eventb.core.poIdentifier name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
@@ -47,64 +47,64 @@
         <org.eventb.core.poPredicate name="received_target_transaction|" org.eventb.core.predicate="grants∈authenticated_users ↔ PERMISSIONS" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_OTstIMHNEe609fto5wotHA"/>
         <org.eventb.core.poPredicate name="received_target_transaction}" org.eventb.core.predicate="∀u⦂USERS·u∈authenticated_transactions[received_target_transactions]⇒u ↦ write∈grants" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_jCLrMcHJEe6yC4BToIaAqA"/>
     </org.eventb.core.poPredicateSet>
-    <org.eventb.core.poSequent name="INITIALISATION/inv11/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="11">
+    <org.eventb.core.poSequent name="INITIALISATION/inv11/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="12">
         <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiont"/>
         <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_DmAl8MHOEe609fto5wotHA"/>
-        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_CJbpkPRrEe60CqkwWvstGA"/>
         <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/>
         <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_DmAl8MHOEe609fto5wotHA"/>
         <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poSequent#INITIALISATION\/inv11\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
         <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD0"/>
     </org.eventb.core.poSequent>
-    <org.eventb.core.poSequent name="INITIALISATION/inv12/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="11">
+    <org.eventb.core.poSequent name="INITIALISATION/inv12/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="12">
         <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiont"/>
         <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_DmB0EMHOEe609fto5wotHA"/>
-        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_CJbpkPRrEe60CqkwWvstGA"/>
         <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/>
         <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_DmB0EMHOEe609fto5wotHA"/>
         <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poSequent#INITIALISATION\/inv12\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
         <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD1"/>
     </org.eventb.core.poSequent>
-    <org.eventb.core.poSequent name="INITIALISATION/inv13/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="11">
+    <org.eventb.core.poSequent name="INITIALISATION/inv13/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="12">
         <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiont"/>
         <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_DmCbIMHOEe609fto5wotHA"/>
-        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_CJbpkPRrEe60CqkwWvstGA"/>
         <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/>
         <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_DmCbIMHOEe609fto5wotHA"/>
         <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poSequent#INITIALISATION\/inv13\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
         <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD2"/>
     </org.eventb.core.poSequent>
-    <org.eventb.core.poSequent name="INITIALISATION/inv14/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="11">
+    <org.eventb.core.poSequent name="INITIALISATION/inv14/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="12">
         <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiont"/>
         <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_DmDCMMHOEe609fto5wotHA"/>
-        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_CJbpkPRrEe60CqkwWvstGA"/>
         <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/>
         <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_DmDCMMHOEe609fto5wotHA"/>
         <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poSequent#INITIALISATION\/inv14\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
         <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD3"/>
     </org.eventb.core.poSequent>
-    <org.eventb.core.poSequent name="INITIALISATION/inv15/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="11">
+    <org.eventb.core.poSequent name="INITIALISATION/inv15/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="12">
         <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiont"/>
         <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_DmDpQMHOEe609fto5wotHA"/>
-        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_CJbpkPRrEe60CqkwWvstGA"/>
         <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/>
         <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_DmDpQMHOEe609fto5wotHA"/>
         <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poSequent#INITIALISATION\/inv15\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
         <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD4"/>
     </org.eventb.core.poSequent>
-    <org.eventb.core.poSequent name="INITIALISATION/inv16/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="11">
+    <org.eventb.core.poSequent name="INITIALISATION/inv16/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="12">
         <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiont"/>
         <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_DmEQUMHOEe609fto5wotHA"/>
-        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_CJbpkPRrEe60CqkwWvstGA"/>
         <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/>
         <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_DmEQUMHOEe609fto5wotHA"/>
         <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poSequent#INITIALISATION\/inv16\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
         <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD5"/>
     </org.eventb.core.poSequent>
-    <org.eventb.core.poSequent name="INITIALISATION/inv17/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="11">
+    <org.eventb.core.poSequent name="INITIALISATION/inv17/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="12">
         <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiont"/>
         <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_2MNd0MHOEe609fto5wotHA"/>
-        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_CJbpkPRrEe60CqkwWvstGA"/>
         <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/>
         <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_2MNd0MHOEe609fto5wotHA"/>
         <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poSequent#INITIALISATION\/inv17\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
diff --git a/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bps b/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bps
index 66139bea8b83c59f089fc44b2840f9b60d33dc04..3023c9498d20b0ab2b5915b17f92f27fad055802 100644
--- a/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bps
+++ b/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bps
@@ -1,12 +1,12 @@
 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
 <org.eventb.core.psFile>
-    <org.eventb.core.psStatus name="INITIALISATION/inv11/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="11" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIALISATION/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="11" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIALISATION/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="11" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIALISATION/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="11" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIALISATION/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="11" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIALISATION/inv16/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="11" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIALISATION/inv17/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="11" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIALISATION/inv11/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="12" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIALISATION/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="12" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIALISATION/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="12" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIALISATION/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="12" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIALISATION/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="12" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIALISATION/inv16/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="12" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIALISATION/inv17/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="12" org.eventb.core.psManual="false"/>
     <org.eventb.core.psStatus name="SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_ETHEREUM/inv11/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="11" org.eventb.core.psManual="false"/>
     <org.eventb.core.psStatus name="INITIATE_CC_TX_IN_ETHEREUM/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="11" org.eventb.core.psManual="false"/>
     <org.eventb.core.psStatus name="INITIATE_CC_TX_IN_ETHEREUM/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="11" org.eventb.core.psManual="false"/>
diff --git a/gateway-event-b/CCTx_Ethereum_Fabric_c2.buc b/gateway-event-b/CCTx_Ethereum_Fabric_c2.buc
index ff87242824725e3ee52d58bc462801359aa6dbc3..05090fd2ab4f6cd42d3c4cdbe1e28960107f2e9b 100644
--- a/gateway-event-b/CCTx_Ethereum_Fabric_c2.buc
+++ b/gateway-event-b/CCTx_Ethereum_Fabric_c2.buc
@@ -1,11 +1,11 @@
 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
-<org.eventb.core.contextFile org.eventb.core.configuration="org.eventb.core.fwd;de.prob.symbolic.ctxBase" org.eventb.core.generated="false" org.eventb.emf.persistence.emf_id="_c2YQRcQ6Ee609fto5wotHA" org.eventb.texttools.text_lastmodified="1707146581829" org.eventb.texttools.text_representation="context CCTx_Ethereum_Fabric_c2 extends CCTx_Abstract_DLT_c1&#10;&#10;sets PERMISSIONS USERS&#10;&#10;constants read write gateway_user&#10;&#10;axioms&#10;  @axm11 partition(PERMISSIONS, {read}, {write}) // Two only types of permissions exist: read and write&#10;  @axm12 gateway_user ∈ USERS // The gateway has an Hyperledger Fabric user&#10;end" version="3">
+<org.eventb.core.contextFile org.eventb.core.configuration="org.eventb.core.fwd;de.prob.symbolic.ctxBase" org.eventb.core.generated="false" org.eventb.emf.persistence.emf_id="_mAbXh_RqEe60CqkwWvstGA" org.eventb.texttools.text_lastmodified="1712444914938" org.eventb.texttools.text_representation="context CCTx_Ethereum_Fabric_c2 extends CCTx_Abstract_DLT_c1&#10;&#10;sets PERMISSIONS USERS&#10;&#10;constants read write gateway_user&#10;&#10;axioms&#10;  @axm11 partition(PERMISSIONS, {read}, {write}) // Only two types of permissions exist: read and write (REQ1)&#10;  @axm12 gateway_user ∈ USERS // The gateway has a Fabric user&#10;end" version="3">
     <org.eventb.core.extendsContext name="'" org.eventb.core.target="CCTx_Abstract_DLT_c1"/>
-    <org.eventb.core.axiom name="_c2chsMQ6Ee609fto5wotHA" org.eventb.core.comment="Two only types of permissions exist: read and write" org.eventb.core.generated="false" org.eventb.core.label="axm11" org.eventb.core.predicate="partition(PERMISSIONS, {read}, {write})" org.eventb.emf.persistence.emf_id="_c2YQQ8Q6Ee609fto5wotHA"/>
-    <org.eventb.core.axiom name="_c2dIwMQ6Ee609fto5wotHA" org.eventb.core.comment="The gateway has an Hyperledger Fabric user" org.eventb.core.generated="false" org.eventb.core.label="axm12" org.eventb.core.predicate="gateway_user ∈ USERS" org.eventb.emf.persistence.emf_id="_c2YQRMQ6Ee609fto5wotHA"/>
-    <org.eventb.core.constant name="_olcsor7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="read" org.eventb.emf.persistence.emf_id="_c2YQQMQ6Ee609fto5wotHA"/>
-    <org.eventb.core.constant name="_olcso77uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="write" org.eventb.emf.persistence.emf_id="_c2YQQcQ6Ee609fto5wotHA"/>
-    <org.eventb.core.constant name="_olcspL7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_user" org.eventb.emf.persistence.emf_id="_c2YQQsQ6Ee609fto5wotHA"/>
-    <org.eventb.core.carrierSet name="_olcspb7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="PERMISSIONS" org.eventb.emf.persistence.emf_id="_c2XpMMQ6Ee609fto5wotHA"/>
-    <org.eventb.core.carrierSet name="_olcspr7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="USERS" org.eventb.emf.persistence.emf_id="_c2XpMcQ6Ee609fto5wotHA"/>
+    <org.eventb.core.axiom name="_c2chsMQ6Ee609fto5wotHA" org.eventb.core.comment="Only two types of permissions exist: read and write (REQ1)" org.eventb.core.generated="false" org.eventb.core.label="axm11" org.eventb.core.predicate="partition(PERMISSIONS, {read}, {write})" org.eventb.emf.persistence.emf_id="_mAbXhfRqEe60CqkwWvstGA"/>
+    <org.eventb.core.axiom name="_c2dIwMQ6Ee609fto5wotHA" org.eventb.core.comment="The gateway has a Fabric user" org.eventb.core.generated="false" org.eventb.core.label="axm12" org.eventb.core.predicate="gateway_user ∈ USERS" org.eventb.emf.persistence.emf_id="_mAbXhvRqEe60CqkwWvstGA"/>
+    <org.eventb.core.constant name="_olcsor7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="read" org.eventb.emf.persistence.emf_id="_mAbXgvRqEe60CqkwWvstGA"/>
+    <org.eventb.core.constant name="_olcso77uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="write" org.eventb.emf.persistence.emf_id="_mAbXg_RqEe60CqkwWvstGA"/>
+    <org.eventb.core.constant name="_olcspL7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_user" org.eventb.emf.persistence.emf_id="_mAbXhPRqEe60CqkwWvstGA"/>
+    <org.eventb.core.carrierSet name="_olcspb7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="PERMISSIONS" org.eventb.emf.persistence.emf_id="_mAbXgPRqEe60CqkwWvstGA"/>
+    <org.eventb.core.carrierSet name="_olcspr7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="USERS" org.eventb.emf.persistence.emf_id="_mAbXgfRqEe60CqkwWvstGA"/>
 </org.eventb.core.contextFile>
diff --git a/gateway-event-b/CCTx_Ethereum_Fabric_m2.bcm b/gateway-event-b/CCTx_Ethereum_Fabric_m2.bcm
index 8e899c0cd874267ed1fb7294223bf7adcb9aa5c7..8bd5812a3152ed4c5da043dc9946297dd0fd7ab4 100644
--- a/gateway-event-b/CCTx_Ethereum_Fabric_m2.bcm
+++ b/gateway-event-b/CCTx_Ethereum_Fabric_m2.bcm
@@ -43,16 +43,16 @@
     <org.eventb.core.scVariable name="grants" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.variable#_2RlqIMErEe6yC4BToIaAqA" org.eventb.core.type="ℙ(USERS×PERMISSIONS)"/>
     <org.eventb.core.scVariable name="received_source_transactions" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.variable#_OjhzwPRgEe60CqkwWvstGA" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×SOURCE_TRANSACTIONS)"/>
     <org.eventb.core.scVariable name="authenticated_users" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.variable#_1toq4L7uEe6laZimEYihUg" org.eventb.core.type="ℙ(USERS)"/>
-    <org.eventb.core.scEvent name="received_target_transactiont" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="INITIALISATION" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh">
-        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Abstract_DLT_m1.bcm|org.eventb.core.scMachineFile#CCTx_Abstract_DLT_m1|org.eventb.core.scEvent#received_target_transactiont" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/>
+    <org.eventb.core.scEvent name="received_target_transactiont" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="INITIALISATION" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_CJbpkPRrEe60CqkwWvstGA">
+        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Abstract_DLT_m1.bcm|org.eventb.core.scMachineFile#CCTx_Abstract_DLT_m1|org.eventb.core.scEvent#received_target_transactiont" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_CJbpkPRrEe60CqkwWvstGA"/>
         <org.eventb.core.scAction name="'" org.eventb.core.assignment="received_source_transactions ≔ ∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×SOURCE_TRANSACTIONS)" org.eventb.core.label="act1" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_zpBMgMQ4Ee609fto5wotHA"/>
         <org.eventb.core.scAction name="(" org.eventb.core.assignment="emitted_events ≔ ∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×SMART_CONTRACT_EVENTS)" org.eventb.core.label="act2" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_zpBzkMQ4Ee609fto5wotHA"/>
         <org.eventb.core.scAction name=")" org.eventb.core.assignment="subscriptions ≔ ∅ ⦂ ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)" org.eventb.core.label="act3" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_zpBzkcQ4Ee609fto5wotHA"/>
         <org.eventb.core.scAction name="*" org.eventb.core.assignment="gateway_pending_events ≔ ∅ ⦂ ℙ(GATEWAYS×TARGET_TRANSACTIONS)" org.eventb.core.label="act4" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_zpBzksQ4Ee609fto5wotHA"/>
         <org.eventb.core.scAction name="+" org.eventb.core.assignment="received_target_transactions ≔ ∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS)" org.eventb.core.label="act6" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_zpCaoMQ4Ee609fto5wotHA"/>
-        <org.eventb.core.scAction name="," org.eventb.core.assignment="authenticated_users ≔ ∅ ⦂ ℙ(USERS)" org.eventb.core.label="act11" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_jV8FAMEWEe6yC4BToIaAqA"/>
-        <org.eventb.core.scAction name="-" org.eventb.core.assignment="authenticated_transactions ≔ ∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS×USERS)" org.eventb.core.label="act12" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_jV8FAcEWEe6yC4BToIaAqA"/>
-        <org.eventb.core.scAction name="." org.eventb.core.assignment="grants ≔ ∅ ⦂ ℙ(USERS×PERMISSIONS)" org.eventb.core.label="act14" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_0oC5cMErEe6yC4BToIaAqA"/>
+        <org.eventb.core.scAction name="," org.eventb.core.assignment="authenticated_users ≔ ∅ ⦂ ℙ(USERS)" org.eventb.core.label="act11" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_CJbpkPRrEe60CqkwWvstGA|org.eventb.core.action#_jV8FAMEWEe6yC4BToIaAqA"/>
+        <org.eventb.core.scAction name="-" org.eventb.core.assignment="authenticated_transactions ≔ ∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS×USERS)" org.eventb.core.label="act12" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_CJbpkPRrEe60CqkwWvstGA|org.eventb.core.action#_jV8FAcEWEe6yC4BToIaAqA"/>
+        <org.eventb.core.scAction name="." org.eventb.core.assignment="grants ≔ ∅ ⦂ ℙ(USERS×PERMISSIONS)" org.eventb.core.label="act14" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_CJbpkPRrEe60CqkwWvstGA|org.eventb.core.action#_0oC5cMErEe6yC4BToIaAqA"/>
     </org.eventb.core.scEvent>
     <org.eventb.core.scEvent name="received_target_transactionu" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_ETHEREUM" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_1tlnkr7uEe6laZimEYihUg">
         <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Abstract_DLT_m1.bcm|org.eventb.core.scMachineFile#CCTx_Abstract_DLT_m1|org.eventb.core.scEvent#received_target_transactionu" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_1tlnkr7uEe6laZimEYihUg|org.eventb.core.refinesEvent#_1tlnk77uEe6laZimEYihUg"/>
diff --git a/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo b/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo
index dae1e9f29857b35efc1a1677045dfd9f73ad15ba..93363eaecbd81e399009c8c5432f8577a0a59932 100644
--- a/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo
+++ b/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo
@@ -1,5 +1,5 @@
 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
-<org.eventb.core.poFile org.eventb.core.poStamp="39">
+<org.eventb.core.poFile org.eventb.core.poStamp="40">
     <org.eventb.core.poPredicateSet name="CTXHYP" org.eventb.core.poStamp="39">
         <org.eventb.core.poIdentifier name="TARGET_TRANSACTIONS" org.eventb.core.type="ℙ(TARGET_TRANSACTIONS)"/>
         <org.eventb.core.poIdentifier name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
@@ -35,38 +35,38 @@
         <org.eventb.core.poPredicate name="received_target_transactionw" org.eventb.core.predicate="gateway_pending_events∈GATEWAYS ↔ TARGET_TRANSACTIONS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.invariant#_zpK9gcQ4Ee609fto5wotHA"/>
         <org.eventb.core.poPredicate name="received_target_transactionx" org.eventb.core.predicate="received_target_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↔ TARGET_TRANSACTIONS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.invariant#_qTKs0MT7Ee609fto5wotHA"/>
     </org.eventb.core.poPredicateSet>
-    <org.eventb.core.poSequent name="INITIALISATION/inv12/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="39">
+    <org.eventb.core.poSequent name="INITIALISATION/inv12/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="40">
         <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiont"/>
         <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS×USERS))∈(∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS)) → (∅ ⦂ ℙ(USERS))" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_jV9TI8EWEe6yC4BToIaAqA"/>
         <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'"/>
-        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/>
+        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_CJbpkPRrEe60CqkwWvstGA"/>
         <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_jV9TI8EWEe6yC4BToIaAqA"/>
         <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poSequent#INITIALISATION\/inv12\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
         <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD1"/>
     </org.eventb.core.poSequent>
-    <org.eventb.core.poSequent name="INITIALISATION/inv13/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="39">
+    <org.eventb.core.poSequent name="INITIALISATION/inv13/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="40">
         <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiont"/>
         <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀tx⦂CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS·tx∈(∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS))⇒(∃u⦂USERS·u∈(∅ ⦂ ℙ(USERS))∧tx ↦ u∈(∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS×USERS)))" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_jV9TJMEWEe6yC4BToIaAqA"/>
         <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'"/>
-        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/>
+        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_CJbpkPRrEe60CqkwWvstGA"/>
         <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_jV9TJMEWEe6yC4BToIaAqA"/>
         <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poSequent#INITIALISATION\/inv13\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
         <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD2"/>
     </org.eventb.core.poSequent>
-    <org.eventb.core.poSequent name="INITIALISATION/inv14/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="39">
+    <org.eventb.core.poSequent name="INITIALISATION/inv14/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="40">
         <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiont"/>
         <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(∅ ⦂ ℙ(USERS×PERMISSIONS))∈(∅ ⦂ ℙ(USERS)) ↔ PERMISSIONS" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_OTstIMHNEe609fto5wotHA"/>
         <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'"/>
-        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/>
+        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_CJbpkPRrEe60CqkwWvstGA"/>
         <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_OTstIMHNEe609fto5wotHA"/>
         <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poSequent#INITIALISATION\/inv14\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
         <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD3"/>
     </org.eventb.core.poSequent>
-    <org.eventb.core.poSequent name="INITIALISATION/inv15/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="39">
+    <org.eventb.core.poSequent name="INITIALISATION/inv15/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="40">
         <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiont"/>
         <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀u⦂USERS·u∈(∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS×USERS))[∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS)]⇒u ↦ write∈(∅ ⦂ ℙ(USERS×PERMISSIONS))" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_jCLrMcHJEe6yC4BToIaAqA"/>
         <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'"/>
-        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/>
+        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_CJbpkPRrEe60CqkwWvstGA"/>
         <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_jCLrMcHJEe6yC4BToIaAqA"/>
         <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poSequent#INITIALISATION\/inv15\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
         <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD4"/>
diff --git a/gateway-event-b/CCTx_Ethereum_Fabric_m2.bps b/gateway-event-b/CCTx_Ethereum_Fabric_m2.bps
index 9298137fe70729edee9f50b2c3bb1d38bf4fe7c9..51419d451cde0556497748a2fc08974eaf1c3014 100644
--- a/gateway-event-b/CCTx_Ethereum_Fabric_m2.bps
+++ b/gateway-event-b/CCTx_Ethereum_Fabric_m2.bps
@@ -1,9 +1,9 @@
 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
 <org.eventb.core.psFile>
-    <org.eventb.core.psStatus name="INITIALISATION/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="39" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIALISATION/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="39" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIALISATION/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="39" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIALISATION/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="39" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIALISATION/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="40" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIALISATION/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="40" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIALISATION/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="40" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIALISATION/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="40" org.eventb.core.psManual="false"/>
     <org.eventb.core.psStatus name="SUBMIT_TX_TO_FABRIC/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="39" org.eventb.core.psManual="false"/>
     <org.eventb.core.psStatus name="SUBMIT_TX_TO_FABRIC/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="39" org.eventb.core.psManual="false"/>
     <org.eventb.core.psStatus name="SUBMIT_TX_TO_FABRIC/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="39" org.eventb.core.psManual="false"/>
diff --git a/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum b/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum
index 52471af3cc04c66b9498426e8ab87b1550c1604a..1c64266dc6ad32409afd6bf569caa98659c714c8 100644
--- a/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum
+++ b/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum
@@ -1,54 +1,54 @@
 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
-<org.eventb.core.machineFile org.eventb.core.configuration="org.eventb.core.fwd" org.eventb.core.generated="false" org.eventb.emf.persistence.emf_id="_mFWC-vRhEe60CqkwWvstGA" org.eventb.texttools.text_lastmodified="1712441049982" org.eventb.texttools.text_representation="machine CCTx_Ethereum_Fabric_m2 refines CCTx_Abstract_DLT_m1  sees CCTx_Ethereum_Fabric_c2&#10;&#10;variables received_source_transactions emitted_events subscriptions gateway_pending_events received_target_transactions authenticated_users authenticated_transactions grants&#10;&#10;invariants&#10;  @inv11 authenticated_users ⊆ USERS // Authenticated users are a subset of all the possible users&#10;  @inv12 authenticated_transactions ∈ received_target_transactions → authenticated_users // Authenticated transactions are received transactions submitted by an authenticated user&#10;  @inv13 ∀ tx · tx ∈ received_target_transactions ⇒ (∃ u · u ∈&#10;          authenticated_users ∧ tx ↦ u ∈ authenticated_transactions) //Every submitted transaction to Fabric must be authenticated (REQ4)&#10;  @inv14 grants ∈ authenticated_users ↔ PERMISSIONS // Users with read or write permissions&#10;  @inv15 ∀ u · u ∈ authenticated_transactions[received_target_transactions] ⇒ u ↦ write ∈ grants //Authenticated users that submitted a transaction must have write permissions (REQ5)&#10;&#10;events&#10;  event INITIALISATION extends INITIALISATION&#10;    then&#10;      @act11 authenticated_users ≔ ∅&#10;      @act12 authenticated_transactions ≔ ∅&#10;      @act14 grants ≔ ∅&#10;  end&#10;&#10;  event SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_ETHEREUM extends SUBSCRIBE_SMART_CONTRACT_EVENTS&#10;  end&#10;&#10;  event INITIATE_CC_TX_IN_ETHEREUM extends INITIATE_CC_TX&#10;  end&#10;&#10;  event EMIT_EVENT_IN_ETHEREUM extends EMIT_EVENT&#10;  end&#10;&#10;  event LISTEN_EVENT_IN_ETHEREUM extends LISTEN_EVENT&#10;  end&#10;&#10;  event SUBMIT_TX_TO_FABRIC extends SUBMIT_TX&#10;    any user&#10;    where&#10;      @grd11 user ∈ authenticated_users // Only allow authenticated users (REQ6)&#10;      @grd12 user ↦ write ∈ grants // Only allow authorized users (REQ7)&#10;    then&#10;      @act11 authenticated_transactions(target_smart_contract ↦ transaction) ≔ user // Audit user that submitted a transaction to a smart contract (REQ4)&#10;  end&#10;&#10;  event CREATE_GATEWAY_USER&#10;&#9;  when&#10;&#9;  &#9;@grd1 gateway_user ∉ authenticated_users&#10;&#9;  then&#10;&#9;  &#9;@act1 authenticated_users ≔ authenticated_users ∪ {gateway_user} // Create credentials for a user (e.g. gateway) to authenticate them (REQ2)&#10;  end&#10;&#10;  event GRANT_PERMISSION&#10;  &#9;any permission user&#10;  &#9;where&#10;  &#9;&#9;@grd1 permission ∈ PERMISSIONS&#10;  &#9;&#9;@grd2 user ∈ authenticated_users&#10;  &#9;&#9;@grd3 user ↦ permission ∉ grants&#10;  &#9;then&#10;  &#9;&#9;@act1 grants ≔ grants ∪ {user ↦ permission} // Grant permissions (e.g. write) to users (e.g. gateway) in Fabric (REQ3)&#10;  end&#10;end&#10;" version="5">
+<org.eventb.core.machineFile org.eventb.core.configuration="org.eventb.core.fwd" org.eventb.core.generated="false" org.eventb.emf.persistence.emf_id="_KQJcuvRsEe60CqkwWvstGA" org.eventb.texttools.text_lastmodified="1712445587675" org.eventb.texttools.text_representation="machine CCTx_Ethereum_Fabric_m2 refines CCTx_Abstract_DLT_m1  sees CCTx_Ethereum_Fabric_c2&#10;&#10;variables received_source_transactions emitted_events subscriptions gateway_pending_events received_target_transactions authenticated_users authenticated_transactions grants&#10;&#10;invariants&#10;  @inv11 authenticated_users ⊆ USERS // Authenticated users are a subset of all the possible users&#10;  @inv12 authenticated_transactions ∈ received_target_transactions → authenticated_users // Authenticated transactions are received transactions submitted by an authenticated user&#10;  @inv13 ∀ tx · tx ∈ received_target_transactions ⇒ (∃ u · u ∈&#10;          authenticated_users ∧ tx ↦ u ∈ authenticated_transactions) //Every submitted transaction to Fabric must be authenticated (REQ4)&#10;  @inv14 grants ∈ authenticated_users ↔ PERMISSIONS // Users with read or write permissions&#10;  @inv15 ∀ u · u ∈ authenticated_transactions[received_target_transactions] ⇒ u ↦ write ∈ grants //Authenticated users that submitted a transaction must have write permissions (REQ5)&#10;&#10;events&#10;  event INITIALISATION extends INITIALISATION&#10;    then&#10;      @act11 authenticated_users ≔ ∅&#10;      @act12 authenticated_transactions ≔ ∅&#10;      @act14 grants ≔ ∅&#10;  end&#10;&#10;  event SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_ETHEREUM extends SUBSCRIBE_SMART_CONTRACT_EVENTS&#10;  end&#10;&#10;  event INITIATE_CC_TX_IN_ETHEREUM extends INITIATE_CC_TX&#10;  end&#10;&#10;  event EMIT_EVENT_IN_ETHEREUM extends EMIT_EVENT&#10;  end&#10;&#10;  event LISTEN_EVENT_IN_ETHEREUM extends LISTEN_EVENT&#10;  end&#10;&#10;  event SUBMIT_TX_TO_FABRIC extends SUBMIT_TX&#10;    any user&#10;    where&#10;      @grd11 user ∈ authenticated_users // Only allow authenticated users (REQ6)&#10;      @grd12 user ↦ write ∈ grants // Only allow authorized users (REQ7)&#10;    then&#10;      @act11 authenticated_transactions(target_smart_contract ↦ transaction) ≔ user // Every submitted transaction to Fabric must be authenticated&#10;  end&#10;&#10;  event CREATE_GATEWAY_USER&#10;&#9;  when&#10;&#9;  &#9;@grd1 gateway_user ∉ authenticated_users&#10;&#9;  then&#10;&#9;  &#9;@act1 authenticated_users ≔ authenticated_users ∪ {gateway_user} // Create credentials for a user (e.g. gateway) to authenticate them (REQ2)&#10;  end&#10;&#10;  event GRANT_PERMISSION&#10;  &#9;any permission user&#10;  &#9;where&#10;  &#9;&#9;@grd1 permission ∈ PERMISSIONS&#10;  &#9;&#9;@grd2 user ∈ authenticated_users&#10;  &#9;&#9;@grd3 user ↦ permission ∉ grants&#10;  &#9;then&#10;  &#9;&#9;@act1 grants ≔ grants ∪ {user ↦ permission} // Grant permissions (e.g. write) to users (e.g. gateway) in Fabric (REQ3)&#10;  end&#10;end&#10;" version="5">
     <org.eventb.core.refinesMachine name="'" org.eventb.core.target="CCTx_Abstract_DLT_m1"/>
     <org.eventb.core.seesContext name="_1tlAgL7uEe6laZimEYihUg" org.eventb.core.target="CCTx_Ethereum_Fabric_c2"/>
-    <org.eventb.core.event name="_yREdbb7uEe6laZimEYihUh" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="INITIALISATION" org.eventb.emf.persistence.emf_id="_mFWC4PRhEe60CqkwWvstGA">
-        <org.eventb.core.action name="_jV8FAMEWEe6yC4BToIaAqA" org.eventb.core.assignment="authenticated_users ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act11" org.eventb.emf.persistence.emf_id="_mFWC3fRhEe60CqkwWvstGA"/>
-        <org.eventb.core.action name="_jV8FAcEWEe6yC4BToIaAqA" org.eventb.core.assignment="authenticated_transactions ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act12" org.eventb.emf.persistence.emf_id="_mFWC3vRhEe60CqkwWvstGA"/>
-        <org.eventb.core.action name="_0oC5cMErEe6yC4BToIaAqA" org.eventb.core.assignment="grants ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act14" org.eventb.emf.persistence.emf_id="_mFWC3_RhEe60CqkwWvstGA"/>
+    <org.eventb.core.event name="_CJbpkPRrEe60CqkwWvstGA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="INITIALISATION" org.eventb.emf.persistence.emf_id="_KQJcoPRsEe60CqkwWvstGA">
+        <org.eventb.core.action name="_jV8FAMEWEe6yC4BToIaAqA" org.eventb.core.assignment="authenticated_users ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act11" org.eventb.emf.persistence.emf_id="_KQJcnfRsEe60CqkwWvstGA"/>
+        <org.eventb.core.action name="_jV8FAcEWEe6yC4BToIaAqA" org.eventb.core.assignment="authenticated_transactions ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act12" org.eventb.emf.persistence.emf_id="_KQJcnvRsEe60CqkwWvstGA"/>
+        <org.eventb.core.action name="_0oC5cMErEe6yC4BToIaAqA" org.eventb.core.assignment="grants ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act14" org.eventb.emf.persistence.emf_id="_KQJcn_RsEe60CqkwWvstGA"/>
     </org.eventb.core.event>
-    <org.eventb.core.event name="_1tlnkr7uEe6laZimEYihUg" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_ETHEREUM" org.eventb.emf.persistence.emf_id="_mFWC4vRhEe60CqkwWvstGA">
+    <org.eventb.core.event name="_1tlnkr7uEe6laZimEYihUg" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_ETHEREUM" org.eventb.emf.persistence.emf_id="_KQJcovRsEe60CqkwWvstGA">
         <org.eventb.core.refinesEvent name="_1tlnk77uEe6laZimEYihUg" org.eventb.core.target="SUBSCRIBE_SMART_CONTRACT_EVENTS"/>
     </org.eventb.core.event>
-    <org.eventb.core.event name="_1g9W8MBFEe6yC4BToIaAqA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="INITIATE_CC_TX_IN_ETHEREUM" org.eventb.emf.persistence.emf_id="_mFWC5PRhEe60CqkwWvstGA">
+    <org.eventb.core.event name="_1g9W8MBFEe6yC4BToIaAqA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="INITIATE_CC_TX_IN_ETHEREUM" org.eventb.emf.persistence.emf_id="_KQJcpPRsEe60CqkwWvstGA">
         <org.eventb.core.refinesEvent name="_1g9-AMBFEe6yC4BToIaAqA" org.eventb.core.target="INITIATE_CC_TX"/>
     </org.eventb.core.event>
-    <org.eventb.core.event name="_eB-pUPRhEe60CqkwWvstGA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="EMIT_EVENT_IN_ETHEREUM" org.eventb.emf.persistence.emf_id="_mFWC5vRhEe60CqkwWvstGA">
+    <org.eventb.core.event name="_eB-pUPRhEe60CqkwWvstGA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="EMIT_EVENT_IN_ETHEREUM" org.eventb.emf.persistence.emf_id="_KQJcpvRsEe60CqkwWvstGA">
         <org.eventb.core.refinesEvent name="_eB-pUfRhEe60CqkwWvstGA" org.eventb.core.target="EMIT_EVENT"/>
     </org.eventb.core.event>
-    <org.eventb.core.event name="_eB-pUvRhEe60CqkwWvstGA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="LISTEN_EVENT_IN_ETHEREUM" org.eventb.emf.persistence.emf_id="_mFWC6PRhEe60CqkwWvstGA">
+    <org.eventb.core.event name="_eB-pUvRhEe60CqkwWvstGA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="LISTEN_EVENT_IN_ETHEREUM" org.eventb.emf.persistence.emf_id="_KQJcqPRsEe60CqkwWvstGA">
         <org.eventb.core.refinesEvent name="_eB-pU_RhEe60CqkwWvstGA" org.eventb.core.target="LISTEN_EVENT"/>
     </org.eventb.core.event>
-    <org.eventb.core.event name="_eB-pVPRhEe60CqkwWvstGA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="SUBMIT_TX_TO_FABRIC" org.eventb.emf.persistence.emf_id="_mFWC7vRhEe60CqkwWvstGA">
+    <org.eventb.core.event name="_eB-pVPRhEe60CqkwWvstGA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="SUBMIT_TX_TO_FABRIC" org.eventb.emf.persistence.emf_id="_KQJcrvRsEe60CqkwWvstGA">
         <org.eventb.core.refinesEvent name="_eB-pVfRhEe60CqkwWvstGA" org.eventb.core.target="SUBMIT_TX"/>
-        <org.eventb.core.action name="_jV8sEMEWEe6yC4BToIaAqA" org.eventb.core.assignment="authenticated_transactions(target_smart_contract ↦ transaction) ≔ user" org.eventb.core.comment="Audit user that submitted a transaction to a smart contract (REQ4)" org.eventb.core.generated="false" org.eventb.core.label="act11" org.eventb.emf.persistence.emf_id="_mFWC7fRhEe60CqkwWvstGA"/>
-        <org.eventb.core.guard name="_jV8sEcEWEe6yC4BToIaAqA" org.eventb.core.comment="Only allow authenticated users (REQ6)" org.eventb.core.generated="false" org.eventb.core.label="grd11" org.eventb.core.predicate="user ∈ authenticated_users" org.eventb.emf.persistence.emf_id="_mFWC6_RhEe60CqkwWvstGA"/>
-        <org.eventb.core.guard name="_jV8sEsEWEe6yC4BToIaAqA" org.eventb.core.comment="Only allow authorized users (REQ7)" org.eventb.core.generated="false" org.eventb.core.label="grd12" org.eventb.core.predicate="user ↦ write ∈ grants" org.eventb.emf.persistence.emf_id="_mFWC7PRhEe60CqkwWvstGA"/>
-        <org.eventb.core.parameter name="_1tncwL7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="user" org.eventb.emf.persistence.emf_id="_mFWC6vRhEe60CqkwWvstGA"/>
-    </org.eventb.core.event>
-    <org.eventb.core.event name="_K_21gMEXEe6yC4BToIaAqA" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="CREATE_GATEWAY_USER" org.eventb.emf.persistence.emf_id="_mFWC8vRhEe60CqkwWvstGA">
-        <org.eventb.core.action name="_jV9TIcEWEe6yC4BToIaAqA" org.eventb.core.assignment="authenticated_users ≔ authenticated_users ∪ {gateway_user}" org.eventb.core.comment="Create credentials for a user (e.g. gateway) to authenticate them (REQ2)" org.eventb.core.generated="false" org.eventb.core.label="act1" org.eventb.emf.persistence.emf_id="_mFWC8fRhEe60CqkwWvstGA"/>
-        <org.eventb.core.guard name="_y4y5cMEXEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.label="grd1" org.eventb.core.predicate="gateway_user ∉ authenticated_users" org.eventb.emf.persistence.emf_id="_mFWC8PRhEe60CqkwWvstGA"/>
-    </org.eventb.core.event>
-    <org.eventb.core.event name="_KHHS0MEbEe6yC4BToIaAqA" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="GRANT_PERMISSION" org.eventb.emf.persistence.emf_id="_mFWC-fRhEe60CqkwWvstGA">
-        <org.eventb.core.action name="_KHH54MEbEe6yC4BToIaAqA" org.eventb.core.assignment="grants ≔ grants ∪ {user ↦ permission}" org.eventb.core.comment="Grant permissions (e.g. write) to users (e.g. gateway) in Fabric (REQ3)" org.eventb.core.generated="false" org.eventb.core.label="act1" org.eventb.emf.persistence.emf_id="_mFWC-PRhEe60CqkwWvstGA"/>
-        <org.eventb.core.guard name="_KHH54cEbEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.label="grd1" org.eventb.core.predicate="permission ∈ PERMISSIONS" org.eventb.emf.persistence.emf_id="_mFWC9fRhEe60CqkwWvstGA"/>
-        <org.eventb.core.guard name="_KHH54sEbEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.label="grd2" org.eventb.core.predicate="user ∈ authenticated_users" org.eventb.emf.persistence.emf_id="_mFWC9vRhEe60CqkwWvstGA"/>
-        <org.eventb.core.guard name="_5yZW0MHNEe609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.label="grd3" org.eventb.core.predicate="user ↦ permission ∉ grants" org.eventb.emf.persistence.emf_id="_mFWC9_RhEe60CqkwWvstGA"/>
-        <org.eventb.core.parameter name="_KHIg8MEbEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="permission" org.eventb.emf.persistence.emf_id="_mFWC8_RhEe60CqkwWvstGA"/>
-        <org.eventb.core.parameter name="_KHIg8cEbEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="user" org.eventb.emf.persistence.emf_id="_mFWC9PRhEe60CqkwWvstGA"/>
-    </org.eventb.core.event>
-    <org.eventb.core.invariant name="_jV9TIsEWEe6yC4BToIaAqA" org.eventb.core.comment="Authenticated users are a subset of all the possible users" org.eventb.core.generated="false" org.eventb.core.label="inv11" org.eventb.core.predicate="authenticated_users ⊆ USERS" org.eventb.emf.persistence.emf_id="_mFWC2PRhEe60CqkwWvstGA"/>
-    <org.eventb.core.invariant name="_jV9TI8EWEe6yC4BToIaAqA" org.eventb.core.comment="Authenticated transactions are received transactions submitted by an authenticated user" org.eventb.core.generated="false" org.eventb.core.label="inv12" org.eventb.core.predicate="authenticated_transactions ∈ received_target_transactions → authenticated_users" org.eventb.emf.persistence.emf_id="_mFWC2fRhEe60CqkwWvstGA"/>
-    <org.eventb.core.invariant name="_jV9TJMEWEe6yC4BToIaAqA" org.eventb.core.comment="Every submitted transaction to Fabric must be authenticated (REQ4)" org.eventb.core.generated="false" org.eventb.core.label="inv13" org.eventb.core.predicate="∀ tx · tx ∈ received_target_transactions ⇒ (∃ u · u ∈&#10;          authenticated_users ∧ tx ↦ u ∈ authenticated_transactions)" org.eventb.emf.persistence.emf_id="_mFWC2vRhEe60CqkwWvstGA"/>
-    <org.eventb.core.invariant name="_OTstIMHNEe609fto5wotHA" org.eventb.core.comment="Users with read or write permissions" org.eventb.core.generated="false" org.eventb.core.label="inv14" org.eventb.core.predicate="grants ∈ authenticated_users ↔ PERMISSIONS" org.eventb.emf.persistence.emf_id="_mFWC2_RhEe60CqkwWvstGA"/>
-    <org.eventb.core.invariant name="_jCLrMcHJEe6yC4BToIaAqA" org.eventb.core.comment="Authenticated users that submitted a transaction must have write permissions (REQ5)" org.eventb.core.generated="false" org.eventb.core.label="inv15" org.eventb.core.predicate="∀ u · u ∈ authenticated_transactions[received_target_transactions] ⇒ u ↦ write ∈ grants" org.eventb.emf.persistence.emf_id="_mFWC3PRhEe60CqkwWvstGA"/>
-    <org.eventb.core.variable name="_OjhzwPRgEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="received_source_transactions" org.eventb.emf.persistence.emf_id="_mFWC0PRhEe60CqkwWvstGA"/>
-    <org.eventb.core.variable name="_Zk8OdfKVEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="emitted_events" org.eventb.emf.persistence.emf_id="_mFWC0fRhEe60CqkwWvstGA"/>
-    <org.eventb.core.variable name="_yREda77uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="subscriptions" org.eventb.emf.persistence.emf_id="_mFWC0vRhEe60CqkwWvstGA"/>
-    <org.eventb.core.variable name="_OjhzwfRgEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_pending_events" org.eventb.emf.persistence.emf_id="_mFWC0_RhEe60CqkwWvstGA"/>
-    <org.eventb.core.variable name="_Ojia0PRgEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="received_target_transactions" org.eventb.emf.persistence.emf_id="_mFWC1PRhEe60CqkwWvstGA"/>
-    <org.eventb.core.variable name="_1toq4L7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="authenticated_users" org.eventb.emf.persistence.emf_id="_mFWC1fRhEe60CqkwWvstGA"/>
-    <org.eventb.core.variable name="_1toq4b7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="authenticated_transactions" org.eventb.emf.persistence.emf_id="_mFWC1vRhEe60CqkwWvstGA"/>
-    <org.eventb.core.variable name="_2RlqIMErEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="grants" org.eventb.emf.persistence.emf_id="_mFWC1_RhEe60CqkwWvstGA"/>
+        <org.eventb.core.action name="_jV8sEMEWEe6yC4BToIaAqA" org.eventb.core.assignment="authenticated_transactions(target_smart_contract ↦ transaction) ≔ user" org.eventb.core.comment="Every submitted transaction to Fabric must be authenticated" org.eventb.core.generated="false" org.eventb.core.label="act11" org.eventb.emf.persistence.emf_id="_KQJcrfRsEe60CqkwWvstGA"/>
+        <org.eventb.core.guard name="_jV8sEcEWEe6yC4BToIaAqA" org.eventb.core.comment="Only allow authenticated users (REQ6)" org.eventb.core.generated="false" org.eventb.core.label="grd11" org.eventb.core.predicate="user ∈ authenticated_users" org.eventb.emf.persistence.emf_id="_KQJcq_RsEe60CqkwWvstGA"/>
+        <org.eventb.core.guard name="_jV8sEsEWEe6yC4BToIaAqA" org.eventb.core.comment="Only allow authorized users (REQ7)" org.eventb.core.generated="false" org.eventb.core.label="grd12" org.eventb.core.predicate="user ↦ write ∈ grants" org.eventb.emf.persistence.emf_id="_KQJcrPRsEe60CqkwWvstGA"/>
+        <org.eventb.core.parameter name="_1tncwL7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="user" org.eventb.emf.persistence.emf_id="_KQJcqvRsEe60CqkwWvstGA"/>
+    </org.eventb.core.event>
+    <org.eventb.core.event name="_K_21gMEXEe6yC4BToIaAqA" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="CREATE_GATEWAY_USER" org.eventb.emf.persistence.emf_id="_KQJcsvRsEe60CqkwWvstGA">
+        <org.eventb.core.action name="_jV9TIcEWEe6yC4BToIaAqA" org.eventb.core.assignment="authenticated_users ≔ authenticated_users ∪ {gateway_user}" org.eventb.core.comment="Create credentials for a user (e.g. gateway) to authenticate them (REQ2)" org.eventb.core.generated="false" org.eventb.core.label="act1" org.eventb.emf.persistence.emf_id="_KQJcsfRsEe60CqkwWvstGA"/>
+        <org.eventb.core.guard name="_y4y5cMEXEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.label="grd1" org.eventb.core.predicate="gateway_user ∉ authenticated_users" org.eventb.emf.persistence.emf_id="_KQJcsPRsEe60CqkwWvstGA"/>
+    </org.eventb.core.event>
+    <org.eventb.core.event name="_KHHS0MEbEe6yC4BToIaAqA" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="GRANT_PERMISSION" org.eventb.emf.persistence.emf_id="_KQJcufRsEe60CqkwWvstGA">
+        <org.eventb.core.action name="_KHH54MEbEe6yC4BToIaAqA" org.eventb.core.assignment="grants ≔ grants ∪ {user ↦ permission}" org.eventb.core.comment="Grant permissions (e.g. write) to users (e.g. gateway) in Fabric (REQ3)" org.eventb.core.generated="false" org.eventb.core.label="act1" org.eventb.emf.persistence.emf_id="_KQJcuPRsEe60CqkwWvstGA"/>
+        <org.eventb.core.guard name="_KHH54cEbEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.label="grd1" org.eventb.core.predicate="permission ∈ PERMISSIONS" org.eventb.emf.persistence.emf_id="_KQJctfRsEe60CqkwWvstGA"/>
+        <org.eventb.core.guard name="_KHH54sEbEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.label="grd2" org.eventb.core.predicate="user ∈ authenticated_users" org.eventb.emf.persistence.emf_id="_KQJctvRsEe60CqkwWvstGA"/>
+        <org.eventb.core.guard name="_5yZW0MHNEe609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.label="grd3" org.eventb.core.predicate="user ↦ permission ∉ grants" org.eventb.emf.persistence.emf_id="_KQJct_RsEe60CqkwWvstGA"/>
+        <org.eventb.core.parameter name="_KHIg8MEbEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="permission" org.eventb.emf.persistence.emf_id="_KQJcs_RsEe60CqkwWvstGA"/>
+        <org.eventb.core.parameter name="_KHIg8cEbEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="user" org.eventb.emf.persistence.emf_id="_KQJctPRsEe60CqkwWvstGA"/>
+    </org.eventb.core.event>
+    <org.eventb.core.invariant name="_jV9TIsEWEe6yC4BToIaAqA" org.eventb.core.comment="Authenticated users are a subset of all the possible users" org.eventb.core.generated="false" org.eventb.core.label="inv11" org.eventb.core.predicate="authenticated_users ⊆ USERS" org.eventb.emf.persistence.emf_id="_KQJcmPRsEe60CqkwWvstGA"/>
+    <org.eventb.core.invariant name="_jV9TI8EWEe6yC4BToIaAqA" org.eventb.core.comment="Authenticated transactions are received transactions submitted by an authenticated user" org.eventb.core.generated="false" org.eventb.core.label="inv12" org.eventb.core.predicate="authenticated_transactions ∈ received_target_transactions → authenticated_users" org.eventb.emf.persistence.emf_id="_KQJcmfRsEe60CqkwWvstGA"/>
+    <org.eventb.core.invariant name="_jV9TJMEWEe6yC4BToIaAqA" org.eventb.core.comment="Every submitted transaction to Fabric must be authenticated (REQ4)" org.eventb.core.generated="false" org.eventb.core.label="inv13" org.eventb.core.predicate="∀ tx · tx ∈ received_target_transactions ⇒ (∃ u · u ∈&#10;          authenticated_users ∧ tx ↦ u ∈ authenticated_transactions)" org.eventb.emf.persistence.emf_id="_KQJcmvRsEe60CqkwWvstGA"/>
+    <org.eventb.core.invariant name="_OTstIMHNEe609fto5wotHA" org.eventb.core.comment="Users with read or write permissions" org.eventb.core.generated="false" org.eventb.core.label="inv14" org.eventb.core.predicate="grants ∈ authenticated_users ↔ PERMISSIONS" org.eventb.emf.persistence.emf_id="_KQJcm_RsEe60CqkwWvstGA"/>
+    <org.eventb.core.invariant name="_jCLrMcHJEe6yC4BToIaAqA" org.eventb.core.comment="Authenticated users that submitted a transaction must have write permissions (REQ5)" org.eventb.core.generated="false" org.eventb.core.label="inv15" org.eventb.core.predicate="∀ u · u ∈ authenticated_transactions[received_target_transactions] ⇒ u ↦ write ∈ grants" org.eventb.emf.persistence.emf_id="_KQJcnPRsEe60CqkwWvstGA"/>
+    <org.eventb.core.variable name="_OjhzwPRgEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="received_source_transactions" org.eventb.emf.persistence.emf_id="_KQJckPRsEe60CqkwWvstGA"/>
+    <org.eventb.core.variable name="_Zk8OdfKVEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="emitted_events" org.eventb.emf.persistence.emf_id="_KQJckfRsEe60CqkwWvstGA"/>
+    <org.eventb.core.variable name="_yREda77uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="subscriptions" org.eventb.emf.persistence.emf_id="_KQJckvRsEe60CqkwWvstGA"/>
+    <org.eventb.core.variable name="_OjhzwfRgEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_pending_events" org.eventb.emf.persistence.emf_id="_KQJck_RsEe60CqkwWvstGA"/>
+    <org.eventb.core.variable name="_Ojia0PRgEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="received_target_transactions" org.eventb.emf.persistence.emf_id="_KQJclPRsEe60CqkwWvstGA"/>
+    <org.eventb.core.variable name="_1toq4L7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="authenticated_users" org.eventb.emf.persistence.emf_id="_KQJclfRsEe60CqkwWvstGA"/>
+    <org.eventb.core.variable name="_1toq4b7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="authenticated_transactions" org.eventb.emf.persistence.emf_id="_KQJclvRsEe60CqkwWvstGA"/>
+    <org.eventb.core.variable name="_2RlqIMErEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="grants" org.eventb.emf.persistence.emf_id="_KQJcl_RsEe60CqkwWvstGA"/>
 </org.eventb.core.machineFile>