diff --git a/Chapter04_REWIRE_OTOKEN/README.md b/Chapter04_REWIRE_OTOKEN/README.md
new file mode 100644
index 0000000000000000000000000000000000000000..b2027a28c4cfb15595e6f775b0697f65851113ed
--- /dev/null
+++ b/Chapter04_REWIRE_OTOKEN/README.md
@@ -0,0 +1,25 @@
+TAMARIN Models from Chapter 4
+=============================
+
+This is the README for the Tamarin files associated with my thesis
+Chapter 4. Additionally, we have stored the proved models in the `analysed`
+folder.
+
+
+Running Tamarin on the models
+-----------------------------
+
+To run the verification on the models from within this folder you may:
+
+* Load the models in the GUI mode and run the proofs yourself.
+```bash
+$ tamarin-prover interactive .
+```
+and then point your browser to [http://localhost:3001/](http://localhost:3001/).
+
+* Run the autoprover from the terminal without loading the GUI. Note, this will need to be done for each model.
+```bash
+$ tamarin-prover --prove ./REWIRE_plain.spthy
+```
+
+* To load and run the proved models see the README in the `analysed` folder. 
diff --git a/Chapter04_REWIRE_OTOKEN/REWIRE_otoken.spthy b/Chapter04_REWIRE_OTOKEN/REWIRE_otoken.spthy
new file mode 100644
index 0000000000000000000000000000000000000000..97b50de5535c4471d083dd77ef8293f4921e2202
--- /dev/null
+++ b/Chapter04_REWIRE_OTOKEN/REWIRE_otoken.spthy
@@ -0,0 +1,419 @@
+/*
+ * Authors: Jorden Whitefield, Liqun Chen, Frank Kargl, Andrew Paverd,
+ * Steve Schneider, Helen Treharne, and Stephan Wesemeyer
+ * References
+ *     REWIRE Revocation Without Resolution A Privacy-Friendly
+ *     Revocation Mechanism for Vehicular Ad-Hoc Networks by David
+ *     Forster, Hans Lohr, Jan Zibuschka, and Frank Kargl
+ *
+ * Purpose: Formal Model of R-Token revocation REWIRE variant Results:
+ * Failure to meet authentication properties. Meets lemmas G1, G5 and
+ * G6
+ *
+ * Model Name: otoken.spthy
+ * Status: STABLE
+ */
+
+theory REWIRE_OTOKEN
+begin
+
+builtins:   symmetric-encryption, signing
+
+
+/* Restrictions */
+
+
+// Under perfect cryptography assumption all checks must succeed
+restriction equality_checks_succeed:
+"All x y #i. Eq( x, y ) @ i ==> x = y"
+
+
+/* Key initialisation restrictions */
+
+// Restricts the RA key setup event to occur only once
+restriction single_RA:
+"All #i #j. SetupRevAuthKeys( ) @ i & SetupRevAuthKeys(  ) @ j ==> #i = #j"
+
+
+// Restricts a Vj long-term key setup event to occur only once
+restriction single_Ltk_setup:
+"All id #i #j. SetupVehicleLtk( id ) @ i & SetupVehicleLtk( id ) @ j ==> #i = #j"
+
+
+// Restricts a Vj pseudonym key setup event to occur only once
+restriction single_psi_init:
+"All id key #i #j. InitPSiKey( id, key ) @ i & InitPSiKey( id, key ) @ j ==> #i = #j"
+
+
+// Restricts a Vj otoken key setup event to occur only once
+restriction single_okey_init:
+"All id key #i #j. InitOKey( id, key ) @ i & InitOKey( id, key ) @ j ==> #i = #j"
+
+
+// Restricts a Vj pseudonym certificate setup event to occur only once
+restriction single_init_event:
+"All id #i #j . InitVjPseudonym( id ) @ #i & InitVjPseudonym( id ) @ #j ==> #i = #j"
+
+
+/* Restrictions representing non key leak */
+
+
+// ASSUMPTION: The RA is a trusted third party and the key cannot be leaked.
+restriction no_ra_leak:
+"not ( Ex id key #i #j . SetupRAKeys( id, key ) @ #i & K( key ) @ #j )"
+
+
+// PROTOCOL START ----------------------------------------------------
+
+
+/* Key Setup */
+
+
+// Establish the long term key pair of the Revocation Authority (RA)
+rule RA_SETUP:
+let
+    PK_RA = pk( ~SK_RA )
+in
+    [ Fr( ~SK_RA )  ]
+  --[
+        SetupRevAuthKeys(  )
+      , SetupRAKeys( $RA, ~SK_RA )
+    ]->
+    [
+        !RevAuthSK( $RA, ~SK_RA )
+      , !RevAuthPK( $RA, PK_RA )
+      , Out( PK_RA )
+    ]
+
+
+// Setup the long-term symmetric key of vehicle $Vj
+rule SETUP_VEHICLE_LTK:
+    [ Fr( ~Ltk ) ]
+  --[
+        SetupVehicleLtk( $Vj )
+      , VehicleSetup( $Vj, ~Ltk )
+    ]->
+    [ !Ltk( $Vj, ~Ltk ) ]
+
+
+// Reveal the long-term key pair of $Vj
+rule REVEAL_VEHICLE_LTK:
+    [ !Ltk( $Vj, Ltk ) ]
+  --[
+        VehicleCompromised( $Vj, Ltk )
+      , RevealLtk( $Vj )
+    ]->
+    [ Out( Ltk ) ]
+
+
+// Asymmetric pseudonym key pair for Vj
+rule SETUP_PSI_KEY:
+    [ Fr( ~SK_PSi ) ]
+  --[ InitPSiKey( $Vj, ~SK_PSi ) ]->
+    [ !VehiclePSi( $Vj, ~SK_PSi ) ]
+
+
+// Reveal asymmetric pseudonym key pair for Vj
+rule REVEAL_PSI_KEY:
+    [ !VehiclePSi( $Vj, SK_PSi )  ]
+  --[ VjSKPSiReveal( $Vj, SK_PSi ) ]->
+    [ Out( SK_PSi ) ]
+
+
+// Asymmetric otoken key-pair for Vj
+rule SETUP_OKEY:
+    [ Fr( ~SK_O ) ]
+  --[ InitOKey( $Vj, ~SK_O ) ]->
+    [ !VehicleOKey( $Vj, ~SK_O ) ]
+
+
+// Reveal asymmetric otoken key pair for Vj
+rule REVEAL_VEHICLE_O_KEY:
+    [ !VehicleOKey( $Vj, SK_O ) ]
+  --[
+        VjOReveal( $Vj, SK_O )
+      , RevealO( $Vj )
+    ]->
+    [ Out( SK_O ) ]
+
+
+// Initialises the first pseudonym of Vj
+rule SETUP_VEHICLE_PSEUDONYM_INIT:
+let
+    PK_PSi      = pk( SK_PSi )
+    PK_O        = pk( SK_O )
+    O_Token     = senc( SK_O, Ltk )
+    pseudonym   = < $Vj, PK_PSi, PK_O, O_Token >
+in
+    [
+        !Ltk( $Vj, Ltk )
+      , !VehiclePSi( $Vj, SK_PSi )
+      , !VehicleOKey( $Vj, SK_O )
+    ]
+  --[ InitVjPseudonym( $Vj ) ]->
+    [
+        !VehiclePseudonym( $Vj, pseudonym )
+      , CanChange( $Vj, pseudonym )
+      , Out( pseudonym )
+    ]
+
+
+// Changes the current pseudonym of Vj
+rule CHANGE_PSEUDONYM:
+let
+    PK_PSi    = pk( ~SK_PSi )
+    PK_O      = pk( ~SK_O )
+    O_Token   = senc( ~SK_O, Ltk )
+    pseudonym = < $Vj, PK_PSi, PK_O, O_Token >
+in
+    [
+        !Ltk( $Vj, Ltk )
+      , Fr( ~SK_PSi )
+      , Fr( ~SK_O )
+      , CanChange( $Vj, old )
+    ]
+  --[ ChangePseudonymForVehicle( $Vj, old, pseudonym ) ]->
+    [
+        !VehiclePseudonym( $Vj, pseudonym )
+      , CanChange( $Vj, pseudonym )
+      , Out( pseudonym )
+    ]
+
+
+// Creates report to RA, beginning the revocation process
+rule REPORT:
+    [ !VehiclePseudonym( $Vj, pseudonym ) ]
+  --[
+        Reported( $Vj, pseudonym )
+      , HasReport( $Vj )
+    ]->
+    [ Report( pseudonym ) ]
+
+
+/* Revocation Protocol
+ * RA -> Vj : osr-req := {| 'revoke', pseudonym |}PK_RA
+ * Vj       : Verify osr-req, extract O_Token, Attempt decrypt to recover SK_O
+             If T
+                    delete all pseudonyms
+             ELSE
+                    nothing
+ * Vj -> RA : osr-conf := {| 'confirm', O_Token |}SK_O
+ */
+
+
+rule OSR_REQ_SEND:
+let
+    // O_Token     = aenc( SK_O, Ltk )
+    pseudonym   = < $Vj, PK_PSi, PK_O, O_Token >
+    osrReq      = < 'revoke', pseudonym, 'reason' >
+    osrReqSig   = sign( osrReq, SK_RA )
+    osrReqMsg   = < $RA, $Vj, osrReq, osrReqSig >
+in
+    [
+        Report( pseudonym )
+      , !RevAuthSK( $RA, SK_RA )
+    ]
+  --[
+        OsrReqMsgSentTo( $RA, $Vj, O_Token )
+      , Send( $RA, osrReqMsg )
+      , Running( $Vj, $RA, osrReqMsg )
+    ]->
+    [
+        AwaitRevokeConfirmation( $RA, $Vj, PK_O, SK_RA )
+      , Out( osrReqMsg )
+    ]
+
+
+rule OSR_REQ_RECV:
+let
+    O_Token     = senc( SK_O, Ltk )
+    pseudonym   = < $Vj, PK_PSi, PK_O, O_Token >
+    osrReq      = < 'revoke', pseudonym, 'reason' >
+    osrReqSig   = sign( osrReq, SK_RA )
+    osrReqMsg   = < $RA, $Vj, osrReq, osrReqSig >
+    osrConf     = < $Vj, 'confirm', O_Token >
+    osrConfSig  = sign( osrConf, SK_O )
+    osrConfMsg  = < $Vj, $RA, osrConf, osrConfSig >
+in
+    [
+        In( osrReqMsg )
+      , !RevAuthPK( $RA, PK_RA )
+      , !Ltk( $Vj, Ltk )
+      , CanChange( $Vj, pseudonym )
+    ]
+  --[
+        Commit( $RA, $Vj, osrReqMsg )
+      , OsrReqMsgRecvBy( $Vj, $RA, O_Token )
+      , Recv( $Vj, osrReqMsg )
+      , Eq( verify( osrReqSig, osrReq, PK_RA ), true )
+      , OsrReqVerified( $Vj, O_Token )
+      , Eq( sdec( O_Token, Ltk ), SK_O )
+      , DeleteAllPseudonyms( $Vj, SK_O, O_Token )
+      , Running( $RA, $Vj, osrConfMsg )
+      , OsrConfSentBy( $Vj, $RA, O_Token )
+    ]->
+    [ Out( osrConfMsg ) ]
+
+
+rule REV_AUTH_OSR_CONF_RECV:
+  let
+      // O_Token     = aenc( SK_O, Ltk )
+      osrConf     = < $Vj, 'confirm', O_Token >
+      osrConfSig  = sign( osrConf, SK_O )
+      osrConfMsg  = < $Vj, $RA, osrConf, osrConfSig >
+  in
+    [
+        In( osrConfMsg )
+      , AwaitRevokeConfirmation( $RA, $Vj, PK_O, SK_RA )
+    ]
+  --[
+        Commit( $Vj, $RA, osrConfMsg )
+      , Eq( verify( osrConfSig, osrConf, PK_O ), true )
+      , OsrConfAcceptedBy( $RA, $Vj, O_Token )
+    ]->
+    [  ]
+
+
+// PROTOCOL END ------------------------------------------------------
+
+
+/* Functional Correctness Lemmas */
+
+
+/*
+ * Proof Goal G1
+ *    Sanity check of the protocol to ensure correct execution
+ */
+lemma executable: exists-trace
+" /* It should be possible that when an osr-req is sent it's received */
+    Ex id_ra id_vj m t #i #j #k . Send( id_ra, m ) @ i & Recv( id_vj, m ) @ j
+    /* and the osr-conf is accepted by the RA */
+    & OsrConfAcceptedBy( id_ra, id_vj, t ) @ k
+    /* such that the osr-req is sent, received and then accepted */
+    & i < j
+    & j < k
+"
+
+
+/*
+ * Proof Goal G2
+ *    This lemma states that if a vehicle Vj changes its pseudonym and a previous
+ *    pseudonym is revoked, it should be possible for the vehicle to create an
+ *    OSR-Conf message
+ */
+lemma revoke_after_change_exists: exists-trace
+"   /* It should be possible that when a report for Vj is made with pseudonym 1 (ps1) */
+Ex id_vj id_ra t ps1 ps2 #i #j #k .
+    Reported( id_vj, ps1 ) @ #i
+    /* and there has been a change of pseudonym from ps1 to ps2 */
+    & ChangePseudonymForVehicle( id_vj, ps1, ps2 ) @ #j
+    /* and an OSR-Conf should be sent after the change occurred */
+    & OsrConfSentBy( id_vj, id_ra, t ) @ #k
+    /* and the report occurred before the change to ps2 */
+    & #i < #j
+    & #j < #k
+    /* and the adversary did not perform a long-term / otoken key reveal on Vj  */
+    & not( Ex k #n. VehicleCompromised( id_vj, k ) @ #n )
+    & not( Ex k #n . VjOReveal( id_vj, k ) @ #n )
+"
+
+
+/*
+ * Proof Goal G3
+ *    G3 demonstrates a vehicle's ability to receive and create a confirmation.
+ *    Since G3 is defined over all traces this includes the case where the
+ *    pseudonym has changed.
+ */
+lemma osr_req_received_with_change_all:
+" /* If there was an OSR-Conf message sent by a vehicle Vj with O-Token t */
+  ( All id_vj id_ra t #i .
+      OsrConfSentBy( id_vj, id_ra, t ) @ #i
+      /* and the adversary did not perform a long-term / otoken key reveal on Vj */
+      & not( Ex key #k. VehicleCompromised( id_vj, key ) @ #k )
+      & not( Ex key #q . VjOReveal( id_vj, key ) @ #q )
+              /* Then there was an OSR-Req sent to Vj with the O-Token t */
+        ==> ( Ex #a . OsrReqMsgSentTo( id_ra, id_vj, t ) @ #a
+              /* such that a OSR-Req is sent before Vj sends OSR-Conf */
+              & a < i ) )
+"
+
+
+/*
+ * Proof Goal G4
+ *    If a confirmation of a pseudonym revocation is accepted by the RA from a
+ *    vehicle then that vehicle will have accepted and processed a revocation
+ *    request from the RA.
+ */
+lemma revoke_with_change_all:
+" /* If there was an OSR-Conf accepted by the RA with O-Token t */
+  ( All id_ra id_vj t #i .
+    OsrConfAcceptedBy( id_ra, id_vj, t ) @ i
+    /* and the adversary did not perform a long-term / otoken key reveal on Vj */
+    & not( Ex key #k. VehicleCompromised( id_vj, key ) @ k )
+    & not( Ex  okey #q . VjOReveal( id_vj, okey ) @ q )
+      /* Then there was an OSR-Req message received by Vj with t */
+      ==> ( Ex #l . OsrReqMsgRecvBy( id_vj, id_ra, t ) @ l
+      /* such that the OSR-Req is received by Vj before OSR-Conf is received by the RA */
+      & l < i ) )
+"
+
+
+/* Authentication Lemmas */
+
+
+/*
+ * Proof Goal G5
+ *    Weak agreement is a form of authentication which guarantees that when the
+ *    RA completes a run of the protocol it guarantees that it was
+ *    interacting with the Vj who had also been running the protocol.
+ */
+lemma weak_agreement:
+   " /* If there was an RA that accept an OSR-Conf message from a vehicle with otoken t */
+    All id_vj id_ra t #i.
+        OsrConfAcceptedBy( id_ra, id_vj, t ) @ i
+     /* Then there exists a vehicle with the otoken t who received the OSR-Req */
+     ==>  ( Ex t2 #j. OsrReqMsgRecvBy( id_vj, id_ra, t2 ) @ j )
+                /* or the adversary perform a long-term key / O key reveal on the vehicle */
+          | ( Ex #r. RevealLtk( id_vj ) @ r )
+          | ( Ex #r. RevealO( id_vj )   @ r )
+   "
+
+
+/*
+ * Proof Goal G6
+ *    Non-injective agreement guarantees that the RA and vehicle Vj each agree upon
+ *    the completion of a run with each other and that in those runs the contents
+ *    of the received messages correspond to the sent messages.
+ */
+lemma noninjective_agreement:
+  " /* Whenever a vehicle or RA commits to running a session, then */
+    All a b msg #i.
+        Commit( a, b, msg ) @ i
+    /* there is RA / vehicle running a session with the same parameters */
+    ==> ( Ex #j. Running( b, a, msg ) @ j )
+            /* or the adversary perform a long-term key / O key reveal on the vehicle */
+          | ( Ex C #r. RevealLtk( C ) @ r )
+          | ( Ex C #r. RevealO( C ) @ r )
+  "
+
+
+/*
+ * Proof Goal G7
+ *    Non-injective synchronisation is very similar to non-injective agreement
+ *    but additionally requires that the corresponding send and receive messages
+ *    have to be executed in their expected order.
+ */
+lemma noninjective_synchronisation:
+" /* If there was an RA that accept an OSR-Conf message from a vehicle with O-Token t */
+  ( All id_ra id_vj t #i . OsrConfAcceptedBy( id_ra, id_vj, t ) @ #i
+  /* and the adversary perform a long-term / otoken key reveal on the vehicle */
+  & not( Ex #q . RevealLtk( id_vj ) @ #q )
+  & not( Ex #q . RevealO( id_vj ) @ #q )
+    /* Then there exists a vehicle with the O-Token t who received the OSR-Req */
+    ==> ( Ex #l . OsrReqMsgRecvBy( id_vj, id_ra, t ) @ #l
+          /* such that OSR-Req was received before a OSR-Conf is accepted by the RA */
+          & #l < #i ) )
+"
+
+
+end
diff --git a/Chapter04_REWIRE_OTOKEN/REWIRE_plain.spthy b/Chapter04_REWIRE_OTOKEN/REWIRE_plain.spthy
new file mode 100644
index 0000000000000000000000000000000000000000..e5c63856ea6886d67fa991c0e507439449132559
--- /dev/null
+++ b/Chapter04_REWIRE_OTOKEN/REWIRE_plain.spthy
@@ -0,0 +1,335 @@
+/*
+ * Authors: Jorden Whitefield, Liqun Chen, Frank Kargl, Andrew Paverd,
+ * Steve Schneider, Helen Treharne, and Stephan Wesemeyer
+ *
+ * References:
+ * REWIRE Revocation Without Resolution A Privacy-Friendly
+ * Revocation Mechanism for Vehicular Ad-Hoc Networks by David
+ * Forster, Hans Lohr, Jan Zibuschka, and Frank Kargl
+ *
+ * Purpose: Formal Model of R-Token revocation REWIRE variant
+ *
+ * Results:
+ * Failure to meet authentication properties. Meets lemmas G1, G5 and
+ * G6
+ *
+ * Model Name: REWIRE_plain.spthy
+ * Status: STABLE
+ */
+
+theory REWIRE_PLAIN
+begin
+
+builtins:   asymmetric-encryption, signing
+
+
+/* Restrictions */
+
+
+// Under perfect cryptography assumption all checks must succeed
+restriction equality_checks_succeed:
+"All x y #i. Eq( x, y ) @ i ==> x = y"
+
+
+/* Key initialisation restrictions */
+
+// Restricts the RA key setup event to occur only once
+restriction single_RA:
+"All #i #j. SetupRevAuthKeys( ) @ i & SetupRevAuthKeys(  ) @ j ==> #i = #j"
+
+
+// Restricts a Vj long-term key setup event to occur only once
+restriction single_Ltk_setup:
+"All id #i #j. SetupVehicleLtk( id ) @ i & SetupVehicleLtk( id ) @ j ==> #i = #j"
+
+
+// Restricts a Vj pseudonym key setup event to occur only once
+restriction single_psi_init:
+"All id #i #j. InitPSiKey( id ) @ i & InitPSiKey( id ) @ j ==> #i = #j"
+
+
+/* Restrictions representing non key leak */
+
+
+// The RA is a trusted third party and the key cannot be leaked.
+restriction no_ra_leak:
+"not ( Ex id key #i #j . SetupRAKeys( id, key ) @ #i & K( key ) @ #j )"
+
+
+// PROTOCOL START ----------------------------------------------------
+
+
+/* Key Setup */
+
+
+// Establish the long term key pair of the Revocation Authority (RA)
+rule RA_SETUP:
+let
+  PK_RA = pk( ~SK_RA )
+in
+    [ Fr( ~SK_RA )  ]
+  --[ SetupRevAuthKeys(  ), SetupRAKeys( $RA, ~SK_RA ) ]->
+    [
+        !RevAuthSK( $RA, ~SK_RA )
+      , !RevAuthPK( $RA, PK_RA )
+      , Out( PK_RA )
+    ]
+
+
+// Setup the long-term symmetric key of vehicle $Vj
+rule SETUP_VEHICLE_LTK:
+    [ Fr( ~Ltk ) ]
+  --[
+        SetupVehicleLtk( $Vj )
+      , VehicleSetup( $Vj, ~Ltk )
+    ]->
+    [ !Ltk( $Vj, ~Ltk ) ]
+
+
+// Reveal the long-term key pair of $Vj
+rule REVEAL_VEHICLE_LTK:
+    [ !Ltk( $Vj, Ltk ) ]
+  --[
+        VehicleCompromised( $Vj, Ltk )
+      , RevealLtk( $Vj )
+    ]->
+    [ Out( Ltk ) ]
+
+
+// Asymmetric pseudonym key pair for Vj
+rule SETUP_PSI_KEY:
+  let
+    PK_PSi = pk( ~SK_PSi )
+  in
+    [ Fr( ~SK_PSi ) ]
+  --[ InitPSiKey( $Vj ) ]->
+    [
+        !VehiclePSi( $Vj, ~SK_PSi )
+      , !VehiclePKPSi( $Vj, PK_PSi )
+      , CanChange( $Vj, ~SK_PSi )
+    ]
+
+
+// Reveal asymmetric pseudonym key pair for Vj
+rule REVEAL_PSI_KEY:
+    [ !VehiclePSi( $Vj, SK_PSi )  ]
+  --[
+        VjSKPSiReveal( $Vj, SK_PSi )
+      , RevealSKPSi( $Vj )
+    ]->
+    [ Out( SK_PSi ) ]
+
+
+// Changes the current pseudonym of Vj
+rule CHANGE_PSEUDONYM:
+  let
+    old_PK_PSi = pk( old_SK_PSi )
+    PK_PSi = pk( ~SK_PSi )
+  in
+    [
+        Fr( ~SK_PSi ),
+        CanChange( $Vj, old_SK_PSi )
+    ]
+  --[ ChangePseudonymForVehicle( $Vj, old_PK_PSi, PK_PSi ) ]->
+    [
+        !VehiclePSi( $Vj, ~SK_PSi )
+      , CanChange( $Vj, ~SK_PSi )
+      , Out( PK_PSi )
+    ]
+
+
+// Creates report to RA, beginning the revocation process
+rule REPORT:
+  let
+    PK_PSi = pk( SK_PSi )
+  in
+    [ !VehiclePKPSi( $Vj, PK_PSi ) ]
+  --[ Reported( $Vj, PK_PSi ), HasReport( $Vj ) ]->
+    [ Report( $Vj, PK_PSi ) ]
+
+
+/* Revocation Protocol
+ * RA -> Vj : osr-req := {| 'revoke', PK_PSi, 'reason' |}PK_RA
+ * Vj       : Verify osr-req
+ * Vj -> RA : osr-conf := {| 'confirm', PK_PSi |}SK_PSi
+ */
+
+
+rule OSR_REQ_SEND:
+  let
+    PK_PSi      = pk( SK_PSi )
+    osrReq      = < 'revoke', PK_PSi, 'reason' >
+    osrReqSig   = sign( osrReq, SK_RA )
+    osrReqMsg   = < $RA, $Vj, osrReq, osrReqSig >
+  in
+    [
+        Report( $Vj, PK_PSi )
+      , !RevAuthSK( $RA, SK_RA )
+    ]
+  --[
+        OsrReqMsgSentTo( $RA, $Vj, PK_PSi )
+      , Send($RA, osrReqMsg)
+      , Running( $Vj, $RA, osrReqMsg )
+    ]->
+    [
+        AwaitRevokeConfirmation( $RA, $Vj, PK_PSi, SK_RA )
+      , Out( osrReqMsg )
+    ]
+
+
+rule OSR_REQ_RECV:
+  let
+    PK_PSi      = pk( SK_PSi )
+    osrReq      = < 'revoke', PK_PSi, 'reason' >
+    osrReqSig   = sign( osrReq, SK_RA )
+    osrReqMsg   = < $RA, $Vj, osrReq, osrReqSig >
+    osrConf     = < $Vj, 'confirm', PK_PSi >
+    osrConfSig  = sign( osrConf, SK_PSi )
+    osrConfMsg  = < $Vj, $RA, osrConf, osrConfSig >
+  in
+    [
+        In( osrReqMsg )
+      , !RevAuthPK( $RA, PK_RA )
+      , !VehiclePSi( $Vj, SK_PSi )
+      , CanChange( $Vj, SK_PSi )
+    ]
+  --[   Commit( $RA, $Vj, osrReqMsg )
+      , OsrReqMsgRecvBy( $Vj, $RA, PK_PSi )
+      , Recv($Vj, osrReqMsg)
+      , Eq( verify( osrReqSig, osrReq, PK_RA ), true )
+      , OsrReqVerified( $Vj, PK_PSi )
+      , Running( $RA, $Vj, osrConfMsg )
+      , OsrConfSentBy( $Vj, $RA, PK_PSi )
+    ]->
+    [ Out( osrConfMsg ) ]
+
+
+rule REV_AUTH_OSR_CONF_RECV:
+ let
+    PK_PSi      = pk( SK_PSi )
+    osrConf     = < $Vj, 'confirm', PK_PSi >
+    osrConfSig  = sign( osrConf, SK_PSi )
+    osrConfMsg  = < $Vj, $RA, osrConf, osrConfSig >
+  in
+    [
+        In( osrConfMsg )
+      , AwaitRevokeConfirmation( $RA, $Vj, PK_PSi, SK_RA )
+    ]
+  --[
+        Commit( $Vj, $RA, osrConfMsg )
+      , Eq( verify( osrConfSig, osrConf, PK_PSi ), true )
+      , OsrConfAcceptedBy( $RA, $Vj, PK_PSi )
+    ]->
+    [  ]
+
+
+// PROTOCOL END ------------------------------------------------------
+
+
+/* Functional Correctness Lemmas */
+
+
+/*
+ * Proof Goal G1
+ *    Sanity check of the protocol to ensure correct execution
+ */
+lemma executable:
+  exists-trace
+    "/* It should be possible that when an osr-req is sent it's received */
+      Ex id_ra id_vj m t #i #j #k .
+        Send(id_ra, m) @ #i
+      & Recv(id_vj, m) @ #j
+      /* and the OSR-Conf is accepted by the RA */
+      & OsrConfAcceptedBy( id_ra, id_vj, t ) @ #k
+      /* such that the OSR-Req is sent, received and then accepted */
+      & #i < #j
+      & #j < #k
+    "
+
+
+/*
+ * Proof Goal G2
+ *    This lemma states that if a vehicle Vj changes its pseudonym and a previous
+ *    pseudonym is revoked, it should be possible for the vehicle to create an
+ *    OSR-Conf message
+ */
+lemma revoke_after_change_exists:
+  exists-trace
+  "/* It should be possible that when a report for Vj is made with pseudonym 1 (t1) */
+    ( Ex id_vj ps1 ps2 id_ra #i #j #k .
+        Reported( id_vj, ps1 ) @ #i
+        /* and there has been a change of pseudonym from t1 to t2 */
+        & ChangePseudonymForVehicle( id_vj, ps1, ps2 ) @ #j
+        /* and an OSR-Conf should be sent after the change occurred */
+        & OsrConfSentBy( id_vj, id_ra, ps1 ) @ #k
+        /* and the report occurred before the change to t2 */
+        & #i < #j
+        /* and the change occurs prior to the confirmation*/
+        & #j < #k
+        /* and the adversary did not perform a long-term / pseudonym key reveal on Vj  */
+         & not( Ex k #n. VehicleCompromised( id_vj, k ) @ #n )
+         & not( Ex k #n . VjSKPSiReveal( id_vj, k ) @ #n )
+  )
+  "
+
+/* Authentication Lemmas */
+
+
+/*
+ * Proof Goal G5
+ *    Weak agreement is a form of authentication which guarantees that when the
+ *    RA completes a run of the protocol it guarantees that it was
+ *    interacting with the Vj who had also been running the protocol.
+ */
+lemma weak_agreement:
+   " /* If there was an RA that accept an OSR-Conf message from a vehicle with pseudonym t */
+    All id_vj id_ra t #i.
+        OsrConfAcceptedBy( id_ra, id_vj, t ) @ i
+     /* Then there exists a vehicle with the pseudonym t who received the OSR-Req */
+     ==>  ( Ex t2 #j. OsrReqMsgRecvBy( id_vj, id_ra, t2 ) @ j )
+          /* or the adversary perform a long-term key / pseudonym key reveal on the vehicle */
+          | ( Ex #r. RevealLtk( id_vj )   @ r )
+          | ( Ex #r. RevealSKPSi( id_vj ) @ r )
+   "
+
+
+/*
+ * Proof Goal G6
+ *    Non-injective agreement guarantees that the RA and vehicle Vj each agree upon
+ *    the completion of a run with each other and that in those runs the contents
+ *    of the received messages correspond to the sent messages.
+ */
+lemma noninjective_agreement:
+  all-traces
+  " /* Whenever a vehicle or RA commits to running a session, then */
+    All a b msg #i.
+      Commit( a, b, msg ) @ i
+    /* there is RA / vehicle running a session with the same parameters */
+    ==> ( Ex #j. Running( b, a, msg ) @ j )
+        /* or the adversary perform a long-term key / pseudonym key reveal on the vehicle */
+        | ( Ex C #r. RevealLtk( C ) @ r )
+        | ( Ex C #r. RevealSKPSi( C ) @ r )
+  "
+
+
+/*
+ * Proof Goal G7
+ *    Non-injective synchronisation is very similar to non-injective agreement
+ *    but additionally requires that the corresponding send and receive messages
+ *    have to be executed in their expected order.
+ */
+lemma noninjective_synchronisation:
+  all-traces
+    "/* If there was an RA that accept an OSR-Conf message from a vehicle with pseudonym t */
+    ( All id_ra id_vj ps #i .
+        OsrConfAcceptedBy( id_ra, id_vj, ps ) @ #i
+        /* and the adversary perform a pseudonym key reveal on the vehicle */
+         & not( Ex k1 #q . VjSKPSiReveal( id_vj, k1 ) @ #q )
+        /* Then there exists a vehicle with the pseudonym t who received the OSR-Req */
+  ==> ( Ex #l . OsrReqMsgRecvBy( id_vj, id_ra, ps ) @ #l
+        /* such that OSR-Req was received before a OSR-Conf is accepted by the RA */
+        & #l < #i ) )
+    "
+
+
+end
diff --git a/Chapter04_REWIRE_OTOKEN/REWIRE_rtoken.spthy b/Chapter04_REWIRE_OTOKEN/REWIRE_rtoken.spthy
new file mode 100644
index 0000000000000000000000000000000000000000..04921a6693ab4b95381deb8e3cbeec6f6e8f3c2f
--- /dev/null
+++ b/Chapter04_REWIRE_OTOKEN/REWIRE_rtoken.spthy
@@ -0,0 +1,401 @@
+/*
+ *  Authors:    Jorden Whitefield, Liqun Chen, Frank Kargl, Andrew Paverd,
+ *              Steve Schneider, Helen Treharne, and Stephan Wesemeyer
+ *  References
+ *              REWIRE Revocation Without Resolution A Privacy-Friendly
+ *              Revocation Mechanism for Vehicular Ad-Hoc Networks
+ *              by David Forster, Hans Lohr, Jan Zibuschka, and Frank Kargl
+ *
+ *  Purpose: Formal Model of R-Token revocation REWIRE variant
+ *  Results: Failure to meet authentication properties. Meets lemmas G1, G5 and G6
+ *
+ *  Model Name: REWIRE_rtoken.spthy
+ *  Status: STABLE
+ */
+
+theory REWIRE_RTOKEN
+begin
+
+builtins:   asymmetric-encryption, signing
+
+
+/* Restrictions */
+
+
+// Under perfect cryptography assumption all checks must succeed
+restriction equality_checks_succeed:
+"All x y #i. Eq( x, y ) @ i ==> x = y"
+
+
+/* Key initialisation restrictions */
+
+
+// Restricts the RA key setup event to occur only once
+restriction single_RA:
+"All #i #j. SetupRevAuthKeys( ) @ i & SetupRevAuthKeys(  ) @ j ==> #i = #j"
+
+
+// Restricts a Vj asymmetric key setup event to occur only once
+restriction single_vj_sk_setup:
+"All id #i #j. SetupVehicleSK( id ) @ i & SetupVehicleSK( id ) @ j ==> #i = #j"
+
+
+// Restricts a Vj pseudonym key setup event to occur only once
+restriction single_psi_init:
+"All id key #i #j. InitPSiKey( id, key ) @ i & InitPSiKey( id, key ) @ j ==> #i = #j"
+
+
+// Restricts a Vj pseudonym certificate setup event to occur only once
+restriction single_init_event:
+"All id #i #j . InitVjPseudonym( id ) @ #i & InitVjPseudonym( id ) @ #j ==> #i = #j"
+
+
+/* Restrictions representing non key leak */
+
+
+// The RA is a trusted third party and the key cannot be leaked
+restriction no_ra_leak:
+"not ( Ex id key #i #j . SetupRAKeys( id, key ) @ #i & K( key ) @ #j )"
+
+
+// PROTOCOL START ----------------------------------------------------
+
+
+/* Key Setup */
+
+
+// Establish the long term key pair of the Revocation Authority (RA)
+rule RA_SETUP:
+  let
+    PK_RA = pk( ~SK_RA )
+  in
+    [ Fr( ~SK_RA )  ]
+  --[
+        SetupRevAuthKeys(  )
+      , SetupRAKeys( $RA, ~SK_RA )
+    ]->
+    [
+        !RevAuthSK( $RA, ~SK_RA )
+      , !RevAuthPK( $RA, PK_RA )
+      , Out( PK_RA )
+    ]
+
+
+// Setup the asymmetric key pair of $Vj
+rule SETUP_VEHICLE_KEY_PAIR:
+  let
+    PK_Vj = pk( ~SK_Vj )
+  in
+    [ Fr( ~SK_Vj ) ]
+  --[
+        SetupVehicleSK( $Vj )
+      , VehicleSetup( $Vj, ~SK_Vj )
+    ]->
+    [
+        !VjSK( $Vj, ~SK_Vj )
+      , !VjPK( $Vj, PK_Vj )
+    ]
+
+
+// Reveal the asymmetric key pair of $Vj
+rule REVEAL_VEHICLE_SK:
+    [ !VjSK( $Vj, SK_Vj ) ]
+  --[
+        VehicleCompromised( $Vj, SK_Vj )
+      , RevealSK( $Vj )
+    ]->
+    [ Out( SK_Vj ) ]
+
+
+// Asymmetric pseudonym key pair for Vj
+rule SETUP_PSI_KEY:
+    [ Fr( ~SK_PSi ) ]
+  --[ InitPSiKey( $Vj, ~SK_PSi ) ]->
+    [ !VehiclePSi( $Vj, ~SK_PSi ) ]
+
+
+// Reveal asymmetric pseudonym key pair for Vj
+rule REVEAL_PSI_KEY:
+    [ !VehiclePSi( $Vj, SK_PSi )  ]
+  --[ VjSKPSiReveal( $Vj, SK_PSi ) ]->
+    [ Out( SK_PSi ) ]
+
+
+// Initialises the first pseudonym of Vj
+rule SETUP_VEHICLE_PSEUDONYM:
+  let
+    PK_PSi      = pk( SK_PSi )
+    R           = < $Vj, PK_Vj, ~r >
+    R_Token     = aenc( R, PK_Vj )
+    pseudonym   = < PK_PSi, R_Token >
+  in
+    [
+        !VjSK( $Vj, SK_Vj )
+      , !VjPK( $Vj, PK_Vj )
+      , !VehiclePSi( $Vj, SK_PSi )
+      , Fr( ~r )
+    ]
+  --[ InitVjPseudonym( $Vj ) ]->
+    [
+        !VehiclePseudonym( $Vj, pseudonym )
+      , CanChange( $Vj, pseudonym )
+      , Out( pseudonym )
+    ]
+
+
+// Changes the current pseudonym of Vj
+rule CHANGE_PSEUDONYM:
+  let
+    PK_PSi      = pk( ~SK_PSi )
+    R           = < $Vj, PK_Vj, ~r >
+    R_Token     = aenc( R, PK_Vj )
+    pseudonym   = < PK_PSi, R_Token >
+  in
+    [
+        !VjSK( $Vj, SK_Vj )
+      , !VjPK( $Vj, PK_Vj )
+      , Fr( ~SK_PSi )
+      , Fr( ~r )
+      , CanChange( $Vj, old )
+    ]
+    --[ ChangePseudonymForVehicle( $Vj, old, pseudonym ) ]->
+    [
+        !VehiclePseudonym( $Vj, pseudonym )
+      , CanChange( $Vj, pseudonym )
+      , Out( pseudonym )
+    ]
+
+
+// Creates report to RA, beginning the revocation process
+rule REPORT:
+    [ !VehiclePseudonym( $Vj, pseudonym ) ]
+  --[ Reported( $Vj, pseudonym ) ]->
+    [ Report( pseudonym ) ]
+
+
+/* Revocation Protocol
+ * RA -> Vj : osr-req := {| 'revoke', pseudonym |}PK_RA
+ * Vj       : Verify osr-req, extract R_Token, Attempt decypt R_Token
+                                               If T
+                                                  delete all pseudonyms
+                                               ELSE
+                                                  nothing
+ * Vj -> RA : osr-conf := {| 'confirm', R_Token |}LTK_Vj
+ */
+
+
+rule OSR_REQ_SEND:
+  let
+    R           = < $Vj, PK_Vj, r >
+    R_Token     = aenc( R, PK_Vj )
+    pseudonym   = < PK_PSi, R_Token >
+    osrReq      = < 'revoke', pseudonym, 'reason' >
+    osrReqSig   = sign( osrReq, SK_RA )
+    osrReqMsg   = < $RA, $Vj, osrReq, osrReqSig >
+  in
+    [
+        Report( pseudonym )
+      , !RevAuthSK( $RA, SK_RA )
+    ]
+  --[
+        OsrReqMsgSentTo( $RA, $Vj, R_Token )
+      , Send($RA, osrReqMsg)
+      , Running( $Vj, $RA, osrReqMsg )
+    ]->
+    [
+        AwaitRevokeConfirmation( $RA, $Vj, R_Token, SK_RA )
+      , Out( osrReqMsg )
+    ]
+
+
+rule OSR_REQ_RECV:
+  let
+    R           = < $Vj, PK_Vj, ~r >
+    R_Token     = aenc( R, PK_Vj )
+    pseudonym   = < PK_PSi, R_Token >
+    osrReq      = < 'revoke', pseudonym, 'reason' >
+    osrReqSig   = sign( osrReq, SK_RA )
+    osrReqMsg   = < $RA, $Vj, osrReq, osrReqSig >
+    osrConf     = < $Vj, 'confirm', R_Token >
+    osrConfSig  = sign( osrConf, SK_Vj )
+    osrConfMsg  = < $Vj, $RA, osrConf, osrConfSig >
+  in
+    [
+        In( osrReqMsg )
+      , !RevAuthPK( $RA, PK_RA )
+      , !VjSK( $Vj, SK_Vj )
+      , !VjPK( $Vj, PK_Vj )
+      , CanChange( $Vj, pseudonym )
+    ]
+  --[   Commit( $RA, $Vj, osrReqMsg )
+      , OsrReqMsgRecvBy( $Vj, $RA, R_Token )
+      , Recv( $Vj, osrReqMsg )
+      , Eq( verify( osrReqSig, osrReq, PK_RA ), true )
+      , OsrReqVerified( $Vj, R_Token )
+      , Eq( adec( R_Token, SK_Vj ), R )
+      , DeleteAllPseudonyms( $Vj, SK_Vj, R_Token )
+      , Running( $RA, $Vj, osrConfMsg )
+      , OsrConfSentBy( $Vj, $RA, R_Token )
+    ]->
+    [ Out( osrConfMsg ) ]
+
+
+rule REV_AUTH_OSR_CONF_RECV:
+ let
+    osrConf     = < $Vj, 'confirm', R_Token >
+    osrConfSig  = sign( osrConf, SK_Vj )
+    osrConfMsg  = < $Vj, $RA, osrConf, osrConfSig >
+  in
+    [
+        In( osrConfMsg )
+      , AwaitRevokeConfirmation( $RA, $Vj, R_Token, SK_RA )
+    ]
+--[     Commit( $Vj, $RA, osrConfMsg )
+      , OsrConfAcceptedBy( $RA, $Vj, R_Token )
+    ]->
+    [  ]
+
+
+// PROTOCOL END ------------------------------------------------------
+
+
+/* Functional Correctness Lemmas */
+
+
+/*
+ * Proof Goal G1
+ *    Sanity check of the protocol to ensure correct execution
+ */
+lemma executable:
+exists-trace
+  " /* It should be possible that when an osr-req is sent it's received */
+    Ex id_ra id_vj m t #i #j #k . Send( id_ra, m ) @ i & Recv( id_vj, m ) @ j
+    /* and the OSR-Conf is accepted by the RA */
+    & OsrConfAcceptedBy( id_ra, id_vj, t ) @ k
+    /* such that the OSR-Req is sent, received and then accepted */
+    & i < j
+    & j < k
+  "
+
+
+/*
+ * Proof Goal G2
+ *    This lemma states that if a vehicle Vj changes its pseudonym and a previous
+ *    pseudonym is revoked, it should be possible for the vehicle to create an
+ *    OSR-Conf message
+ */
+lemma revoke_after_change_exists:
+  exists-trace
+  "/* It should be possible that when a report for Vj is made with pseudonym 1 (ps1) */
+  ( Ex id_vj id_ra t ps1 ps2 #i #j #k .
+      Reported( id_vj, ps1 ) @ #i
+      /* and there has been a change of pseudonym from ps1 to ps2 */
+      & ChangePseudonymForVehicle( id_vj, ps1, ps2 ) @ #j
+      /* and an OSR-Conf should be sent after the change occurred */
+      & OsrConfSentBy( id_vj, id_ra, t ) @ #k
+      /* and the report occurred before the change to ps2 */
+      & #i < #j
+      & #j < k
+      /* and the adversary did not perform a asymmetric key reveal on Vj  */
+      & not( Ex k #n. VehicleCompromised( id_vj, k ) @ #n )
+  )
+  "
+
+
+/*
+ * Proof Goal G3
+ *    G3 demonstrates a vehicle's ability to receive and create a confirmation.
+ *    Since G3 is defined over all traces this includes the case where the
+ *    pseudonym has changed.
+ */
+lemma osr_req_received_with_change_all:
+  "/* If there was an OSR-Conf message sent by a vehicle Vj with R-Token t */
+  ( All id_vj id_ra t #i .
+      OsrConfSentBy( id_vj, id_ra, t ) @ #i
+      /* and the adversary did not perform a asymmetric key reveal on Vj */
+      & not( Ex key #k. VehicleCompromised( id_vj, key ) @ #k )
+        /* Then there was an OSR-Req sent to Vj with the R-Token t */
+  ==> ( Ex #a . OsrReqMsgSentTo( id_ra, id_vj, t ) @ #a
+        /* such that a OSR-Req is sent before Vj sends OSR-Conf */
+        & a < i )
+  )
+  "
+
+
+/*
+ * Proof Goal G4
+ *    If a confirmation of a pseudonym revocation is accepted by the RA from a
+ *    vehicle then that vehicle will have accepted and processed a revocation
+ *    request from the RA.
+ */
+lemma revoke_with_change_all:
+  "/* If there was an OSR-Conf accepted by the RA with R-Token t */
+  ( All id_ra id_vj t #i .
+      OsrConfAcceptedBy( id_ra, id_vj, t ) @ i
+      /* and the adversary did not perform a asymmetric key reveal on Vj */
+      & not( Ex key #k. VehicleCompromised( id_vj, key ) @ k )
+        /* Then there was an OSR-Req message received by Vj with t */
+  ==> ( Ex #l . OsrReqMsgRecvBy( id_vj, id_ra, t ) @ l
+        /* such that the OSR-Req is received by Vj before OSR-Conf is received by the RA */
+        & l < i )
+  )
+  "
+
+
+/* Authentication Lemmas */
+
+
+/*
+ * Proof Goal G5
+ *    Weak agreement is a form of authentication which guarantees that when the
+ *    RA completes a run of the protocol it guarantees that it was
+ *    interacting with the Vj who had also been running the protocol.
+ */
+lemma weak_agreement:
+   " /* If there was an RA that accept an OSR-Conf message from a vehicle with R-Token t */
+    All id_vj id_ra t #i.
+        OsrConfAcceptedBy( id_ra, id_vj, t ) @ i
+     /* Then there exists a vehicle with the R-Token t who received the OSR-Req */
+     ==>  ( Ex t2 #j. OsrReqMsgRecvBy( id_vj, id_ra, t2 ) @ j )
+          /* or the adversary perform a asymmetric key reveal on the vehicle */
+          | ( Ex #r. RevealSK( id_vj ) @ r )
+   "
+
+
+/*
+ * Proof Goal G6
+ *    Non-injective agreement guarantees that the RA and vehicle Vj each agree upon
+ *    the completion of a run with each other and that in those runs the contents
+ *    of the received messages correspond to the sent messages.
+ */
+lemma noninjective_agreement:
+  " /* Whenever a vehicle or RA commits to running a session, then */
+    All a b msg #i.
+      Commit( a, b, msg ) @ i
+    /* there is RA / vehicle running a session with the same parameters */
+    ==> ( Ex #j. Running( b, a, msg ) @ j )
+        /* or the adversary perform a asymmetric key reveal on the vehicle */
+        | ( Ex C #r. RevealSK( C ) @ r )
+  "
+
+
+/*
+ * Proof Goal G7
+ *    Non-injective synchronisation is very similar to non-injective agreement
+ *    but additionally requires that the corresponding send and receive messages
+ *    have to be executed in their expected order.
+ */
+lemma noninjective_synchronisation:
+  "/* If there was an RA that accept an OSR-Conf message from a vehicle with R-Token t */
+  ( All id_ra id_vj t #i .
+      OsrConfAcceptedBy( id_ra, id_vj, t ) @ #i
+      /* and the adversary perform a asymmetric key reveal on the vehicle */
+      & not( Ex #q . RevealSK( id_vj ) @ #q )
+      /* Then there exists a vehicle with the R-Token t who received the OSR-Req */
+  ==> ( Ex #l . OsrReqMsgRecvBy( id_vj, id_ra, t ) @ #l
+      /* such that OSR-Req was received before a OSR-Conf is accepted by the RA */
+        & #l < #i ) )
+  "
+
+
+end
diff --git a/Chapter04_REWIRE_OTOKEN/analysed/README.md b/Chapter04_REWIRE_OTOKEN/analysed/README.md
new file mode 100644
index 0000000000000000000000000000000000000000..bda17987bd0d1338ce3b388e0d582268fb7b4173
--- /dev/null
+++ b/Chapter04_REWIRE_OTOKEN/analysed/README.md
@@ -0,0 +1,15 @@
+TAMARIN Models from Chapter 4
+=============================
+
+This is the README for the Tamarin files associated with my thesis
+Chapter 4. Additionally, we have stored the proved models in the `analysed`
+folder.
+
+Running Tamarin on the models
+-----------------------------
+
+To load the proved models from within this folder load the models in the GUI mode:
+```bash
+$ tamarin-prover interactive .
+```
+and then point your browser to [http://localhost:3001/](http://localhost:3001/).
diff --git a/Chapter04_REWIRE_OTOKEN/analysed/REWIRE_OTOKEN.analysed.spthy b/Chapter04_REWIRE_OTOKEN/analysed/REWIRE_OTOKEN.analysed.spthy
new file mode 100644
index 0000000000000000000000000000000000000000..c013910f6934781b9a8762b04c6d2a3dc14befd6
--- /dev/null
+++ b/Chapter04_REWIRE_OTOKEN/analysed/REWIRE_OTOKEN.analysed.spthy
@@ -0,0 +1,808 @@
+theory REWIRE_OTOKEN begin
+
+// Function signature and definition of the equational theory E
+
+functions: fst/1, pair/2, pk/1, sdec/2, senc/2, sign/2, snd/1,
+           true/0, verify/3
+equations:
+    fst(<x.1, x.2>) = x.1,
+    sdec(senc(x.1, x.2), x.2) = x.1,
+    snd(<x.1, x.2>) = x.2,
+    verify(sign(x.1, x.2), x.1, pk(x.2)) = true
+
+restriction equality_checks_succeed:
+  "∀ x y #i. (Eq( x, y ) @ #i) ⇒ (x = y)"
+  // safety formula
+
+restriction single_RA:
+  "∀ #i #j.
+    ((SetupRevAuthKeys( ) @ #i) ∧ (SetupRevAuthKeys( ) @ #j)) ⇒
+    (#i = #j)"
+  // safety formula
+
+restriction single_Ltk_setup:
+  "∀ id #i #j.
+    ((SetupVehicleLtk( id ) @ #i) ∧ (SetupVehicleLtk( id ) @ #j)) ⇒
+    (#i = #j)"
+  // safety formula
+
+restriction single_psi_init:
+  "∀ id key #i #j.
+    ((InitPSiKey( id, key ) @ #i) ∧ (InitPSiKey( id, key ) @ #j)) ⇒
+    (#i = #j)"
+  // safety formula
+
+restriction single_okey_init:
+  "∀ id key #i #j.
+    ((InitOKey( id, key ) @ #i) ∧ (InitOKey( id, key ) @ #j)) ⇒
+    (#i = #j)"
+  // safety formula
+
+restriction single_init_event:
+  "∀ id #i #j.
+    ((InitVjPseudonym( id ) @ #i) ∧ (InitVjPseudonym( id ) @ #j)) ⇒
+    (#i = #j)"
+  // safety formula
+
+restriction no_ra_leak:
+  "¬(∃ id key #i #j.
+      (SetupRAKeys( id, key ) @ #i) ∧ (K( key ) @ #j))"
+  // safety formula
+
+rule (modulo E) RA_SETUP:
+   [ Fr( ~SK_RA ) ]
+  --[ SetupRevAuthKeys( ), SetupRAKeys( $RA, ~SK_RA ) ]->
+   [
+   !RevAuthSK( $RA, ~SK_RA ), !RevAuthPK( $RA, pk(~SK_RA) ),
+   Out( pk(~SK_RA) )
+   ]
+
+  /* has exactly the trivial AC variant */
+
+rule (modulo E) SETUP_VEHICLE_LTK:
+   [ Fr( ~Ltk ) ]
+  --[ SetupVehicleLtk( $Vj ), VehicleSetup( $Vj, ~Ltk ) ]->
+   [ !Ltk( $Vj, ~Ltk ) ]
+
+  /* has exactly the trivial AC variant */
+
+rule (modulo E) REVEAL_VEHICLE_LTK:
+   [ !Ltk( $Vj, Ltk ) ]
+  --[ VehicleCompromised( $Vj, Ltk ), RevealLtk( $Vj ) ]->
+   [ Out( Ltk ) ]
+
+  /* has exactly the trivial AC variant */
+
+rule (modulo E) SETUP_PSI_KEY:
+   [ Fr( ~SK_PSi ) ]
+  --[ InitPSiKey( $Vj, ~SK_PSi ) ]->
+   [ !VehiclePSi( $Vj, ~SK_PSi ) ]
+
+  /* has exactly the trivial AC variant */
+
+rule (modulo E) REVEAL_PSI_KEY:
+   [ !VehiclePSi( $Vj, SK_PSi ) ]
+  --[ VjSKPSiReveal( $Vj, SK_PSi ) ]->
+   [ Out( SK_PSi ) ]
+
+  /* has exactly the trivial AC variant */
+
+rule (modulo E) SETUP_OKEY:
+   [ Fr( ~SK_O ) ]
+  --[ InitOKey( $Vj, ~SK_O ) ]->
+   [ !VehicleOKey( $Vj, ~SK_O ) ]
+
+  /* has exactly the trivial AC variant */
+
+rule (modulo E) REVEAL_VEHICLE_O_KEY:
+   [ !VehicleOKey( $Vj, SK_O ) ]
+  --[ VjOReveal( $Vj, SK_O ), RevealO( $Vj ) ]->
+   [ Out( SK_O ) ]
+
+  /* has exactly the trivial AC variant */
+
+rule (modulo E) SETUP_VEHICLE_PSEUDONYM_INIT:
+   [
+   !Ltk( $Vj, Ltk ), !VehiclePSi( $Vj, SK_PSi ),
+   !VehicleOKey( $Vj, SK_O )
+   ]
+  --[ InitVjPseudonym( $Vj ) ]->
+   [
+   !VehiclePseudonym( $Vj,
+                      <$Vj, pk(SK_PSi), pk(SK_O), senc(SK_O, Ltk)>
+   ),
+   CanChange( $Vj, <$Vj, pk(SK_PSi), pk(SK_O), senc(SK_O, Ltk)> ),
+   Out( <$Vj, pk(SK_PSi), pk(SK_O), senc(SK_O, Ltk)> )
+   ]
+
+  /* has exactly the trivial AC variant */
+
+rule (modulo E) CHANGE_PSEUDONYM:
+   [
+   !Ltk( $Vj, Ltk ), Fr( ~SK_PSi ), Fr( ~SK_O ), CanChange( $Vj, old )
+   ]
+  --[
+  ChangePseudonymForVehicle( $Vj, old,
+                             <$Vj, pk(~SK_PSi), pk(~SK_O), senc(~SK_O, Ltk)>
+  )
+  ]->
+   [
+   !VehiclePseudonym( $Vj,
+                      <$Vj, pk(~SK_PSi), pk(~SK_O), senc(~SK_O, Ltk)>
+   ),
+   CanChange( $Vj, <$Vj, pk(~SK_PSi), pk(~SK_O), senc(~SK_O, Ltk)> ),
+   Out( <$Vj, pk(~SK_PSi), pk(~SK_O), senc(~SK_O, Ltk)> )
+   ]
+
+  // loop breaker: [3]
+  /* has exactly the trivial AC variant */
+
+rule (modulo E) REPORT:
+   [ !VehiclePseudonym( $Vj, pseudonym ) ]
+  --[ Reported( $Vj, pseudonym ), HasReport( $Vj ) ]->
+   [ Report( pseudonym ) ]
+
+  /* has exactly the trivial AC variant */
+
+rule (modulo E) OSR_REQ_SEND:
+   [ Report( <$Vj, PK_PSi, PK_O, O_Token> ), !RevAuthSK( $RA, SK_RA )
+   ]
+  --[
+  OsrReqMsgSentTo( $RA, $Vj, O_Token ),
+  Send( $RA,
+        <$RA, $Vj, <'revoke', <$Vj, PK_PSi, PK_O, O_Token>, 'reason'>, 
+         sign(<'revoke', <$Vj, PK_PSi, PK_O, O_Token>, 'reason'>, SK_RA)>
+  ),
+  Running( $Vj, $RA,
+           <$RA, $Vj, <'revoke', <$Vj, PK_PSi, PK_O, O_Token>, 'reason'>, 
+            sign(<'revoke', <$Vj, PK_PSi, PK_O, O_Token>, 'reason'>, SK_RA)>
+  )
+  ]->
+   [
+   AwaitRevokeConfirmation( $RA, $Vj, PK_O, SK_RA ),
+   Out( <$RA, $Vj, 
+         <'revoke', <$Vj, PK_PSi, PK_O, O_Token>, 'reason'>, 
+         sign(<'revoke', <$Vj, PK_PSi, PK_O, O_Token>, 'reason'>, SK_RA)>
+   )
+   ]
+
+  /* has exactly the trivial AC variant */
+
+rule (modulo E) OSR_REQ_RECV:
+   [
+   In( <$RA, $Vj, 
+        <'revoke', <$Vj, PK_PSi, PK_O, senc(SK_O, Ltk)>, 'reason'>, 
+        sign(<'revoke', <$Vj, PK_PSi, PK_O, senc(SK_O, Ltk)>, 'reason'>,
+             SK_RA)
+       >
+   ),
+   !RevAuthPK( $RA, PK_RA ), !Ltk( $Vj, Ltk ),
+   CanChange( $Vj, <$Vj, PK_PSi, PK_O, senc(SK_O, Ltk)> )
+   ]
+  --[
+  Commit( $RA, $Vj,
+          <$RA, $Vj, 
+           <'revoke', <$Vj, PK_PSi, PK_O, senc(SK_O, Ltk)>, 'reason'>, 
+           sign(<'revoke', <$Vj, PK_PSi, PK_O, senc(SK_O, Ltk)>, 'reason'>,
+                SK_RA)
+          >
+  ),
+  OsrReqMsgRecvBy( $Vj, $RA, senc(SK_O, Ltk) ),
+  Recv( $Vj,
+        <$RA, $Vj, 
+         <'revoke', <$Vj, PK_PSi, PK_O, senc(SK_O, Ltk)>, 'reason'>, 
+         sign(<'revoke', <$Vj, PK_PSi, PK_O, senc(SK_O, Ltk)>, 'reason'>,
+              SK_RA)
+        >
+  ),
+  Eq( verify(sign(<'revoke', <$Vj, PK_PSi, PK_O, senc(SK_O, Ltk)>, 
+                   'reason'>,
+                  SK_RA),
+             <'revoke', <$Vj, PK_PSi, PK_O, senc(SK_O, Ltk)>, 'reason'>, PK_RA),
+      true
+  ),
+  OsrReqVerified( $Vj, senc(SK_O, Ltk) ),
+  Eq( sdec(senc(SK_O, Ltk), Ltk), SK_O ),
+  DeleteAllPseudonyms( $Vj, SK_O, senc(SK_O, Ltk) ),
+  Running( $RA, $Vj,
+           <$Vj, $RA, <$Vj, 'confirm', senc(SK_O, Ltk)>, 
+            sign(<$Vj, 'confirm', senc(SK_O, Ltk)>, SK_O)>
+  ),
+  OsrConfSentBy( $Vj, $RA, senc(SK_O, Ltk) )
+  ]->
+   [
+   Out( <$Vj, $RA, <$Vj, 'confirm', senc(SK_O, Ltk)>, 
+         sign(<$Vj, 'confirm', senc(SK_O, Ltk)>, SK_O)>
+   )
+   ]
+
+  /*
+  rule (modulo AC) OSR_REQ_RECV:
+     [
+     In( <$RA, $Vj, 
+          <'revoke', <$Vj, PK_PSi, PK_O, senc(SK_O, Ltk)>, 'reason'>, 
+          sign(<'revoke', <$Vj, PK_PSi, PK_O, senc(SK_O, Ltk)>, 'reason'>,
+               SK_RA)
+         >
+     ),
+     !RevAuthPK( $RA, PK_RA ), !Ltk( $Vj, Ltk ),
+     CanChange( $Vj, <$Vj, PK_PSi, PK_O, senc(SK_O, Ltk)> )
+     ]
+    --[
+    Commit( $RA, $Vj,
+            <$RA, $Vj, 
+             <'revoke', <$Vj, PK_PSi, PK_O, senc(SK_O, Ltk)>, 'reason'>, 
+             sign(<'revoke', <$Vj, PK_PSi, PK_O, senc(SK_O, Ltk)>, 'reason'>,
+                  SK_RA)
+            >
+    ),
+    OsrReqMsgRecvBy( $Vj, $RA, senc(SK_O, Ltk) ),
+    Recv( $Vj,
+          <$RA, $Vj, 
+           <'revoke', <$Vj, PK_PSi, PK_O, senc(SK_O, Ltk)>, 'reason'>, 
+           sign(<'revoke', <$Vj, PK_PSi, PK_O, senc(SK_O, Ltk)>, 'reason'>,
+                SK_RA)
+          >
+    ),
+    Eq( z, true ), OsrReqVerified( $Vj, senc(SK_O, Ltk) ),
+    Eq( SK_O, SK_O ),
+    DeleteAllPseudonyms( $Vj, SK_O, senc(SK_O, Ltk) ),
+    Running( $RA, $Vj,
+             <$Vj, $RA, <$Vj, 'confirm', senc(SK_O, Ltk)>, 
+              sign(<$Vj, 'confirm', senc(SK_O, Ltk)>, SK_O)>
+    ),
+    OsrConfSentBy( $Vj, $RA, senc(SK_O, Ltk) )
+    ]->
+     [
+     Out( <$Vj, $RA, <$Vj, 'confirm', senc(SK_O, Ltk)>, 
+           sign(<$Vj, 'confirm', senc(SK_O, Ltk)>, SK_O)>
+     )
+     ]
+    variants (modulo AC)
+    1. $Vj   = $Vj.20
+       Ltk   = Ltk.21
+       PK_O  = PK_O.22
+       PK_PSi
+             = PK_PSi.23
+       PK_RA = PK_RA.24
+       SK_O  = SK_O.25
+       SK_RA = SK_RA.26
+       z     = verify(sign(<'revoke', 
+                            <$Vj.20, PK_PSi.23, PK_O.22, senc(SK_O.25, Ltk.21)>, 'reason'>,
+                           SK_RA.26),
+                      <'revoke', <$Vj.20, PK_PSi.23, PK_O.22, senc(SK_O.25, Ltk.21)>, 
+                       'reason'>,
+                      PK_RA.24)
+    
+    2. PK_RA = pk(SK_RA.14)
+       SK_RA = SK_RA.14
+       z     = true
+  */
+
+rule (modulo E) REV_AUTH_OSR_CONF_RECV:
+   [
+   In( <$Vj, $RA, <$Vj, 'confirm', O_Token>, 
+        sign(<$Vj, 'confirm', O_Token>, SK_O)>
+   ),
+   AwaitRevokeConfirmation( $RA, $Vj, PK_O, SK_RA )
+   ]
+  --[
+  Commit( $Vj, $RA,
+          <$Vj, $RA, <$Vj, 'confirm', O_Token>, 
+           sign(<$Vj, 'confirm', O_Token>, SK_O)>
+  ),
+  Eq( verify(sign(<$Vj, 'confirm', O_Token>, SK_O),
+             <$Vj, 'confirm', O_Token>, PK_O),
+      true
+  ),
+  OsrConfAcceptedBy( $RA, $Vj, O_Token )
+  ]->
+   [ ]
+
+  /*
+  rule (modulo AC) REV_AUTH_OSR_CONF_RECV:
+     [
+     In( <$Vj, $RA, <$Vj, 'confirm', O_Token>, 
+          sign(<$Vj, 'confirm', O_Token>, SK_O)>
+     ),
+     AwaitRevokeConfirmation( $RA, $Vj, PK_O, SK_RA )
+     ]
+    --[
+    Commit( $Vj, $RA,
+            <$Vj, $RA, <$Vj, 'confirm', O_Token>, 
+             sign(<$Vj, 'confirm', O_Token>, SK_O)>
+    ),
+    Eq( z, true ), OsrConfAcceptedBy( $RA, $Vj, O_Token )
+    ]->
+     [ ]
+    variants (modulo AC)
+    1. $Vj   = $Vj.10
+       O_Token
+             = O_Token.11
+       PK_O  = PK_O.12
+       SK_O  = SK_O.13
+       z     = verify(sign(<$Vj.10, 'confirm', O_Token.11>, SK_O.13),
+                      <$Vj.10, 'confirm', O_Token.11>, PK_O.12)
+    
+    2. PK_O  = pk(SK_O.10)
+       SK_O  = SK_O.10
+       z     = true
+  */
+
+lemma executable:
+  exists-trace
+  "∃ id_ra id_vj m t #i #j #k.
+    ((((Send( id_ra, m ) @ #i) ∧ (Recv( id_vj, m ) @ #j)) ∧
+      (OsrConfAcceptedBy( id_ra, id_vj, t ) @ #k)) ∧
+     (#i < #j)) ∧
+    (#j < #k)"
+/*
+guarded formula characterizing all satisfying traces:
+"∃ id_ra id_vj m t #i #j #k.
+  (Send( id_ra, m ) @ #i) ∧
+  (Recv( id_vj, m ) @ #j) ∧
+  (OsrConfAcceptedBy( id_ra, id_vj, t ) @ #k)
+ ∧
+  (#i < #j) ∧ (#j < #k)"
+*/
+simplify
+solve( Report( <$Vj, PK_PSi, PK_O, senc(SK_O, Ltk)> ) â–¶â‚€ #i )
+  case REPORT_case_1
+  solve( !RevAuthSK( $RA, SK_RA ) ▶₁ #i )
+    case RA_SETUP
+    solve( !RevAuthPK( $RA, pk(~SK_RA) ) ▶₁ #j )
+      case RA_SETUP
+      solve( !Ltk( $Vj, ~Ltk ) â–¶â‚‚ #j )
+        case SETUP_VEHICLE_LTK
+        solve( CanChange( $Vj,
+                          <$Vj, pk(~SK_PSi), pk(~SK_O), senc(~SK_O, ~Ltk)>
+               ) ▶₃ #j )
+          case SETUP_VEHICLE_PSEUDONYM_INIT
+          solve( AwaitRevokeConfirmation( $RA, $Vj, pk(SK_O.1), SK_RA.1
+                 ) ▶₁ #k )
+            case OSR_REQ_SEND_case_1
+            solve( !KU( sign(<$Vj, 'confirm', t>, ~SK_O) ) @ #vk.23 )
+              case OSR_REQ_RECV
+              solve( !KU( sign(<'revoke', 
+                                <$Vj, pk(~SK_PSi), pk(~SK_O), senc(~SK_O, ~Ltk)>, 'reason'>,
+                               ~SK_RA)
+                     ) @ #vk.21 )
+                case OSR_REQ_SEND
+                solve( !KU( senc(~SK_O, ~Ltk) ) @ #vk.19 )
+                  case OSR_REQ_SEND
+                  solve( !KU( pk(~SK_PSi) ) @ #vk.17 )
+                    case OSR_REQ_SEND
+                    solve( !KU( pk(~SK_O) ) @ #vk.20 )
+                      case OSR_REQ_SEND
+                      SOLVED // trace found
+                    qed
+                  qed
+                qed
+              qed
+            qed
+          qed
+        qed
+      qed
+    qed
+  qed
+qed
+
+lemma revoke_after_change_exists:
+  exists-trace
+  "∃ id_vj id_ra t ps1 ps2 #i #j #k.
+    ((((((Reported( id_vj, ps1 ) @ #i) ∧
+         (ChangePseudonymForVehicle( id_vj, ps1, ps2 ) @ #j)) ∧
+        (OsrConfSentBy( id_vj, id_ra, t ) @ #k)) ∧
+       (#i < #j)) ∧
+      (#j < #k)) ∧
+     (¬(∃ k.1 #n. VehicleCompromised( id_vj, k.1 ) @ #n))) ∧
+    (¬(∃ k.1 #n. VjOReveal( id_vj, k.1 ) @ #n))"
+/*
+guarded formula characterizing all satisfying traces:
+"∃ id_vj id_ra t ps1 ps2 #i #j #k.
+  (Reported( id_vj, ps1 ) @ #i) ∧
+  (ChangePseudonymForVehicle( id_vj, ps1, ps2 ) @ #j) ∧
+  (OsrConfSentBy( id_vj, id_ra, t ) @ #k)
+ ∧
+  (#i < #j) ∧
+  (#j < #k) ∧
+  (∀ k.1 #n. (VehicleCompromised( id_vj, k.1 ) @ #n) ⇒ ⊥) ∧
+  (∀ k.1 #n. (VjOReveal( id_vj, k.1 ) @ #n) ⇒ ⊥)"
+*/
+simplify
+solve( !VehiclePseudonym( $Vj, ps1 ) â–¶â‚€ #i )
+  case CHANGE_PSEUDONYM
+  solve( !Ltk( $Vj, Ltk.1 ) â–¶â‚€ #j )
+    case SETUP_VEHICLE_LTK
+    solve( !RevAuthPK( $RA, pk(SK_RA) ) ▶₁ #k )
+      case RA_SETUP
+      solve( !Ltk( $Vj, Ltk.1 ) â–¶â‚‚ #k )
+        case SETUP_VEHICLE_LTK
+        solve( CanChange( $Vj, <$Vj, PK_PSi, PK_O, senc(SK_O.2, ~Ltk)>
+               ) ▶₃ #k )
+          case CHANGE_PSEUDONYM
+          solve( !KU( sign(<'revoke', 
+                            <$Vj, pk(~SK_PSi.2), pk(~SK_O.2), senc(~SK_O.2, ~Ltk)>, 'reason'>,
+                           ~SK_RA)
+                 ) @ #vk.15 )
+            case OSR_REQ_SEND
+            solve( CanChange( $Vj,
+                              <$Vj, pk(~SK_PSi), pk(~SK_O), senc(~SK_O, ~Ltk)>
+                   ) ▶₃ #j )
+              case CHANGE_PSEUDONYM
+              solve( CanChange( $Vj, old ) ▶₃ #vr )
+                case SETUP_VEHICLE_PSEUDONYM_INIT
+                solve( CanChange( $Vj, old ) ▶₃ #vr.3 )
+                  case CHANGE_PSEUDONYM
+                  solve( CanChange( $Vj, old ) ▶₃ #vr.12 )
+                    case CHANGE_PSEUDONYM
+                    solve( CanChange( $Vj, old ) ▶₃ #vr.13 )
+                      case SETUP_VEHICLE_PSEUDONYM_INIT
+                      solve( !KU( senc(~SK_O.2, ~Ltk) ) @ #vk.14 )
+                        case CHANGE_PSEUDONYM
+                        solve( !KU( pk(~SK_PSi.2) ) @ #vk.12 )
+                          case CHANGE_PSEUDONYM
+                          solve( !KU( pk(~SK_O.2) ) @ #vk.14 )
+                            case CHANGE_PSEUDONYM
+                            SOLVED // trace found
+                          qed
+                        qed
+                      qed
+                    qed
+                  qed
+                qed
+              qed
+            qed
+          qed
+        qed
+      qed
+    qed
+  qed
+qed
+
+lemma osr_req_received_with_change_all:
+  all-traces
+  "∀ id_vj id_ra t #i.
+    (((OsrConfSentBy( id_vj, id_ra, t ) @ #i) ∧
+      (¬(∃ key #k. VehicleCompromised( id_vj, key ) @ #k))) ∧
+     (¬(∃ key #q. VjOReveal( id_vj, key ) @ #q))) ⇒
+    (∃ #a. (OsrReqMsgSentTo( id_ra, id_vj, t ) @ #a) ∧ (#a < #i))"
+/*
+guarded formula characterizing all counter-examples:
+"∃ id_vj id_ra t #i.
+  (OsrConfSentBy( id_vj, id_ra, t ) @ #i)
+ ∧
+  (∀ key #k. (VehicleCompromised( id_vj, key ) @ #k) ⇒ ⊥) ∧
+  (∀ key #q. (VjOReveal( id_vj, key ) @ #q) ⇒ ⊥) ∧
+  (∀ #a. (OsrReqMsgSentTo( id_ra, id_vj, t ) @ #a) ⇒ ¬(#a < #i))"
+*/
+simplify
+solve( !RevAuthPK( $RA, pk(SK_RA) ) ▶₁ #i )
+  case RA_SETUP
+  solve( !Ltk( $Vj, Ltk ) â–¶â‚‚ #i )
+    case SETUP_VEHICLE_LTK
+    solve( CanChange( $Vj, <$Vj, PK_PSi, PK_O, senc(SK_O, ~Ltk)>
+           ) ▶₃ #i )
+      case CHANGE_PSEUDONYM
+      solve( !KU( sign(<'revoke', 
+                        <$Vj, pk(~SK_PSi), pk(~SK_O), senc(~SK_O, ~Ltk)>, 'reason'>,
+                       ~SK_RA)
+             ) @ #vk.15 )
+        case OSR_REQ_SEND
+        by contradiction /* from formulas */
+      next
+        case c_sign
+        by solve( !KU( ~SK_RA ) @ #vk.16 )
+      qed
+    next
+      case SETUP_VEHICLE_PSEUDONYM_INIT
+      solve( !KU( sign(<'revoke', 
+                        <$Vj, pk(~SK_PSi), pk(~SK_O), senc(~SK_O, ~Ltk)>, 'reason'>,
+                       ~SK_RA)
+             ) @ #vk.15 )
+        case OSR_REQ_SEND
+        by contradiction /* from formulas */
+      next
+        case c_sign
+        by solve( !KU( ~SK_RA ) @ #vk.16 )
+      qed
+    qed
+  qed
+qed
+
+lemma revoke_with_change_all:
+  all-traces
+  "∀ id_ra id_vj t #i.
+    (((OsrConfAcceptedBy( id_ra, id_vj, t ) @ #i) ∧
+      (¬(∃ key #k. VehicleCompromised( id_vj, key ) @ #k))) ∧
+     (¬(∃ okey #q. VjOReveal( id_vj, okey ) @ #q))) ⇒
+    (∃ #l. (OsrReqMsgRecvBy( id_vj, id_ra, t ) @ #l) ∧ (#l < #i))"
+/*
+guarded formula characterizing all counter-examples:
+"∃ id_ra id_vj t #i.
+  (OsrConfAcceptedBy( id_ra, id_vj, t ) @ #i)
+ ∧
+  (∀ key #k. (VehicleCompromised( id_vj, key ) @ #k) ⇒ ⊥) ∧
+  (∀ okey #q. (VjOReveal( id_vj, okey ) @ #q) ⇒ ⊥) ∧
+  (∀ #l. (OsrReqMsgRecvBy( id_vj, id_ra, t ) @ #l) ⇒ ¬(#l < #i))"
+*/
+simplify
+solve( AwaitRevokeConfirmation( $RA, $Vj, pk(SK_O), SK_RA ) ▶₁ #i )
+  case OSR_REQ_SEND_case_1
+  solve( !KU( sign(<$Vj, 'confirm', t>, ~SK_O) ) @ #vk.9 )
+    case OSR_REQ_RECV
+    by contradiction /* from formulas */
+  next
+    case c_sign
+    solve( !KU( ~SK_O ) @ #vk.10 )
+      case OSR_REQ_SEND
+      solve( !KU( ~Ltk ) @ #vk.11 )
+        case REVEAL_VEHICLE_LTK
+        by contradiction /* from formulas */
+      qed
+    next
+      case REVEAL_VEHICLE_O_KEY
+      by contradiction /* from formulas */
+    next
+      case SETUP_VEHICLE_PSEUDONYM_INIT
+      solve( !KU( ~Ltk ) @ #vk.11 )
+        case REVEAL_VEHICLE_LTK
+        by contradiction /* from formulas */
+      qed
+    qed
+  qed
+next
+  case OSR_REQ_SEND_case_2
+  solve( !KU( sign(<$Vj, 'confirm', t>, ~SK_O) ) @ #vk.9 )
+    case OSR_REQ_RECV
+    by contradiction /* from formulas */
+  next
+    case c_sign
+    solve( !KU( ~SK_O ) @ #vk.10 )
+      case CHANGE_PSEUDONYM
+      solve( !KU( ~Ltk ) @ #vk.11 )
+        case REVEAL_VEHICLE_LTK
+        by contradiction /* from formulas */
+      qed
+    next
+      case OSR_REQ_SEND
+      solve( !KU( ~Ltk ) @ #vk.11 )
+        case REVEAL_VEHICLE_LTK
+        by contradiction /* from formulas */
+      qed
+    qed
+  qed
+qed
+
+lemma weak_agreement:
+  all-traces
+  "∀ id_vj id_ra t #i.
+    (OsrConfAcceptedBy( id_ra, id_vj, t ) @ #i) ⇒
+    (((∃ t2 #j. OsrReqMsgRecvBy( id_vj, id_ra, t2 ) @ #j) ∨
+      (∃ #r. RevealLtk( id_vj ) @ #r)) ∨
+     (∃ #r. RevealO( id_vj ) @ #r))"
+/*
+guarded formula characterizing all counter-examples:
+"∃ id_vj id_ra t #i.
+  (OsrConfAcceptedBy( id_ra, id_vj, t ) @ #i)
+ ∧
+  (∀ t2 #j. (OsrReqMsgRecvBy( id_vj, id_ra, t2 ) @ #j) ⇒ ⊥) ∧
+  (∀ #r. (RevealLtk( id_vj ) @ #r) ⇒ ⊥) ∧
+  (∀ #r. (RevealO( id_vj ) @ #r) ⇒ ⊥)"
+*/
+simplify
+solve( AwaitRevokeConfirmation( $RA, $Vj, pk(SK_O), SK_RA ) ▶₁ #i )
+  case OSR_REQ_SEND_case_1
+  solve( !KU( sign(<$Vj, 'confirm', t>, ~SK_O) ) @ #vk.9 )
+    case OSR_REQ_RECV
+    by contradiction /* from formulas */
+  next
+    case c_sign
+    solve( !KU( ~SK_O ) @ #vk.10 )
+      case OSR_REQ_SEND
+      solve( !KU( ~Ltk ) @ #vk.11 )
+        case REVEAL_VEHICLE_LTK
+        by contradiction /* from formulas */
+      qed
+    next
+      case REVEAL_VEHICLE_O_KEY
+      by contradiction /* from formulas */
+    next
+      case SETUP_VEHICLE_PSEUDONYM_INIT
+      solve( !KU( ~Ltk ) @ #vk.11 )
+        case REVEAL_VEHICLE_LTK
+        by contradiction /* from formulas */
+      qed
+    qed
+  qed
+next
+  case OSR_REQ_SEND_case_2
+  solve( !KU( sign(<$Vj, 'confirm', t>, ~SK_O) ) @ #vk.9 )
+    case OSR_REQ_RECV
+    by contradiction /* from formulas */
+  next
+    case c_sign
+    solve( !KU( ~SK_O ) @ #vk.10 )
+      case CHANGE_PSEUDONYM
+      solve( !KU( ~Ltk ) @ #vk.11 )
+        case REVEAL_VEHICLE_LTK
+        by contradiction /* from formulas */
+      qed
+    next
+      case OSR_REQ_SEND
+      solve( !KU( ~Ltk ) @ #vk.11 )
+        case REVEAL_VEHICLE_LTK
+        by contradiction /* from formulas */
+      qed
+    qed
+  qed
+qed
+
+lemma noninjective_agreement:
+  all-traces
+  "∀ a b msg #i.
+    (Commit( a, b, msg ) @ #i) ⇒
+    (((∃ #j. Running( b, a, msg ) @ #j) ∨
+      (∃ C #r. RevealLtk( C ) @ #r)) ∨
+     (∃ C #r. RevealO( C ) @ #r))"
+/*
+guarded formula characterizing all counter-examples:
+"∃ a b msg #i.
+  (Commit( a, b, msg ) @ #i)
+ ∧
+  (∀ #j. (Running( b, a, msg ) @ #j) ⇒ ⊥) ∧
+  (∀ C #r. (RevealLtk( C ) @ #r) ⇒ ⊥) ∧
+  (∀ C #r. (RevealO( C ) @ #r) ⇒ ⊥)"
+*/
+simplify
+solve( Commit( a, b, msg ) @ #i )
+  case OSR_REQ_RECV
+  solve( !RevAuthPK( $RA, pk(SK_RA) ) ▶₁ #i )
+    case RA_SETUP
+    solve( !Ltk( $Vj, Ltk ) â–¶â‚‚ #i )
+      case SETUP_VEHICLE_LTK
+      solve( CanChange( $Vj, <$Vj, PK_PSi, PK_O, senc(SK_O, ~Ltk)>
+             ) ▶₃ #i )
+        case CHANGE_PSEUDONYM
+        solve( !KU( sign(<'revoke', 
+                          <$Vj, pk(~SK_PSi), pk(~SK_O), senc(~SK_O, ~Ltk)>, 'reason'>,
+                         ~SK_RA)
+               ) @ #vk.15 )
+          case OSR_REQ_SEND
+          by contradiction /* from formulas */
+        next
+          case c_sign
+          by solve( !KU( ~SK_RA ) @ #vk.16 )
+        qed
+      next
+        case SETUP_VEHICLE_PSEUDONYM_INIT
+        solve( !KU( sign(<'revoke', 
+                          <$Vj, pk(~SK_PSi), pk(~SK_O), senc(~SK_O, ~Ltk)>, 'reason'>,
+                         ~SK_RA)
+               ) @ #vk.15 )
+          case OSR_REQ_SEND
+          by contradiction /* from formulas */
+        next
+          case c_sign
+          by solve( !KU( ~SK_RA ) @ #vk.16 )
+        qed
+      qed
+    qed
+  qed
+next
+  case REV_AUTH_OSR_CONF_RECV
+  solve( AwaitRevokeConfirmation( $RA, $Vj, pk(SK_O), SK_RA ) ▶₁ #i )
+    case OSR_REQ_SEND_case_1
+    solve( !KU( sign(<$Vj, 'confirm', O_Token>, ~SK_O) ) @ #vk.9 )
+      case OSR_REQ_RECV
+      by contradiction /* from formulas */
+    next
+      case c_sign
+      solve( !KU( ~SK_O ) @ #vk.10 )
+        case OSR_REQ_SEND
+        solve( !KU( ~Ltk ) @ #vk.11 )
+          case REVEAL_VEHICLE_LTK
+          by contradiction /* from formulas */
+        qed
+      next
+        case REVEAL_VEHICLE_O_KEY
+        by contradiction /* from formulas */
+      next
+        case SETUP_VEHICLE_PSEUDONYM_INIT
+        solve( !KU( ~Ltk ) @ #vk.11 )
+          case REVEAL_VEHICLE_LTK
+          by contradiction /* from formulas */
+        qed
+      qed
+    qed
+  next
+    case OSR_REQ_SEND_case_2
+    solve( !KU( sign(<$Vj, 'confirm', O_Token>, ~SK_O) ) @ #vk.9 )
+      case OSR_REQ_RECV
+      by contradiction /* from formulas */
+    next
+      case c_sign
+      solve( !KU( ~SK_O ) @ #vk.10 )
+        case CHANGE_PSEUDONYM
+        solve( !KU( ~Ltk ) @ #vk.11 )
+          case REVEAL_VEHICLE_LTK
+          by contradiction /* from formulas */
+        qed
+      next
+        case OSR_REQ_SEND
+        solve( !KU( ~Ltk ) @ #vk.11 )
+          case REVEAL_VEHICLE_LTK
+          by contradiction /* from formulas */
+        qed
+      qed
+    qed
+  qed
+qed
+
+lemma noninjective_synchronisation:
+  all-traces
+  "∀ id_ra id_vj t #i.
+    (((OsrConfAcceptedBy( id_ra, id_vj, t ) @ #i) ∧
+      (¬(∃ #q. RevealLtk( id_vj ) @ #q))) ∧
+     (¬(∃ #q. RevealO( id_vj ) @ #q))) ⇒
+    (∃ #l. (OsrReqMsgRecvBy( id_vj, id_ra, t ) @ #l) ∧ (#l < #i))"
+/*
+guarded formula characterizing all counter-examples:
+"∃ id_ra id_vj t #i.
+  (OsrConfAcceptedBy( id_ra, id_vj, t ) @ #i)
+ ∧
+  (∀ #q. (RevealLtk( id_vj ) @ #q) ⇒ ⊥) ∧
+  (∀ #q. (RevealO( id_vj ) @ #q) ⇒ ⊥) ∧
+  (∀ #l. (OsrReqMsgRecvBy( id_vj, id_ra, t ) @ #l) ⇒ ¬(#l < #i))"
+*/
+simplify
+solve( AwaitRevokeConfirmation( $RA, $Vj, pk(SK_O), SK_RA ) ▶₁ #i )
+  case OSR_REQ_SEND_case_1
+  solve( !KU( sign(<$Vj, 'confirm', t>, ~SK_O) ) @ #vk.9 )
+    case OSR_REQ_RECV
+    by contradiction /* from formulas */
+  next
+    case c_sign
+    solve( !KU( ~SK_O ) @ #vk.10 )
+      case OSR_REQ_SEND
+      solve( !KU( ~Ltk ) @ #vk.11 )
+        case REVEAL_VEHICLE_LTK
+        by contradiction /* from formulas */
+      qed
+    next
+      case REVEAL_VEHICLE_O_KEY
+      by contradiction /* from formulas */
+    next
+      case SETUP_VEHICLE_PSEUDONYM_INIT
+      solve( !KU( ~Ltk ) @ #vk.11 )
+        case REVEAL_VEHICLE_LTK
+        by contradiction /* from formulas */
+      qed
+    qed
+  qed
+next
+  case OSR_REQ_SEND_case_2
+  solve( !KU( sign(<$Vj, 'confirm', t>, ~SK_O) ) @ #vk.9 )
+    case OSR_REQ_RECV
+    by contradiction /* from formulas */
+  next
+    case c_sign
+    solve( !KU( ~SK_O ) @ #vk.10 )
+      case CHANGE_PSEUDONYM
+      solve( !KU( ~Ltk ) @ #vk.11 )
+        case REVEAL_VEHICLE_LTK
+        by contradiction /* from formulas */
+      qed
+    next
+      case OSR_REQ_SEND
+      solve( !KU( ~Ltk ) @ #vk.11 )
+        case REVEAL_VEHICLE_LTK
+        by contradiction /* from formulas */
+      qed
+    qed
+  qed
+qed
+
+/* All well-formedness checks were successful. */
+
+end
\ No newline at end of file
diff --git a/Chapter04_REWIRE_OTOKEN/analysed/REWIRE_PLAIN.analysed.spthy b/Chapter04_REWIRE_OTOKEN/analysed/REWIRE_PLAIN.analysed.spthy
new file mode 100644
index 0000000000000000000000000000000000000000..592668d0f4d5737cf9e79679d8e41d7637c66ba2
--- /dev/null
+++ b/Chapter04_REWIRE_OTOKEN/analysed/REWIRE_PLAIN.analysed.spthy
@@ -0,0 +1,462 @@
+theory REWIRE_PLAIN begin
+
+// Function signature and definition of the equational theory E
+
+functions: adec/2, aenc/2, fst/1, pair/2, pk/1, sign/2, snd/1,
+           true/0, verify/3
+equations:
+    adec(aenc(x.1, pk(x.2)), x.2) = x.1,
+    fst(<x.1, x.2>) = x.1,
+    snd(<x.1, x.2>) = x.2,
+    verify(sign(x.1, x.2), x.1, pk(x.2)) = true
+
+restriction equality_checks_succeed:
+  "∀ x y #i. (Eq( x, y ) @ #i) ⇒ (x = y)"
+  // safety formula
+
+restriction single_RA:
+  "∀ #i #j.
+    ((SetupRevAuthKeys( ) @ #i) ∧ (SetupRevAuthKeys( ) @ #j)) ⇒
+    (#i = #j)"
+  // safety formula
+
+restriction single_Ltk_setup:
+  "∀ id #i #j.
+    ((SetupVehicleLtk( id ) @ #i) ∧ (SetupVehicleLtk( id ) @ #j)) ⇒
+    (#i = #j)"
+  // safety formula
+
+restriction single_psi_init:
+  "∀ id #i #j.
+    ((InitPSiKey( id ) @ #i) ∧ (InitPSiKey( id ) @ #j)) ⇒ (#i = #j)"
+  // safety formula
+
+restriction no_ra_leak:
+  "¬(∃ id key #i #j.
+      (SetupRAKeys( id, key ) @ #i) ∧ (K( key ) @ #j))"
+  // safety formula
+
+rule (modulo E) RA_SETUP:
+   [ Fr( ~SK_RA ) ]
+  --[ SetupRevAuthKeys( ), SetupRAKeys( $RA, ~SK_RA ) ]->
+   [
+   !RevAuthSK( $RA, ~SK_RA ), !RevAuthPK( $RA, pk(~SK_RA) ),
+   Out( pk(~SK_RA) )
+   ]
+
+  /* has exactly the trivial AC variant */
+
+rule (modulo E) SETUP_VEHICLE_LTK:
+   [ Fr( ~Ltk ) ]
+  --[ SetupVehicleLtk( $Vj ), VehicleSetup( $Vj, ~Ltk ) ]->
+   [ !Ltk( $Vj, ~Ltk ) ]
+
+  /* has exactly the trivial AC variant */
+
+rule (modulo E) REVEAL_VEHICLE_LTK:
+   [ !Ltk( $Vj, Ltk ) ]
+  --[ VehicleCompromised( $Vj, Ltk ), RevealLtk( $Vj ) ]->
+   [ Out( Ltk ) ]
+
+  /* has exactly the trivial AC variant */
+
+rule (modulo E) SETUP_PSI_KEY:
+   [ Fr( ~SK_PSi ) ]
+  --[ InitPSiKey( $Vj ) ]->
+   [
+   !VehiclePSi( $Vj, ~SK_PSi ), !VehiclePKPSi( $Vj, pk(~SK_PSi) ),
+   CanChange( $Vj, ~SK_PSi )
+   ]
+
+  /* has exactly the trivial AC variant */
+
+rule (modulo E) REVEAL_PSI_KEY:
+   [ !VehiclePSi( $Vj, SK_PSi ) ]
+  --[ VjSKPSiReveal( $Vj, SK_PSi ), RevealSKPSi( $Vj ) ]->
+   [ Out( SK_PSi ) ]
+
+  /* has exactly the trivial AC variant */
+
+rule (modulo E) CHANGE_PSEUDONYM:
+   [ Fr( ~SK_PSi ), CanChange( $Vj, old_SK_PSi ) ]
+  --[ ChangePseudonymForVehicle( $Vj, pk(old_SK_PSi), pk(~SK_PSi) )
+  ]->
+   [
+   !VehiclePSi( $Vj, ~SK_PSi ), CanChange( $Vj, ~SK_PSi ),
+   Out( pk(~SK_PSi) )
+   ]
+
+  // loop breaker: [1]
+  /* has exactly the trivial AC variant */
+
+rule (modulo E) REPORT:
+   [ !VehiclePKPSi( $Vj, pk(SK_PSi) ) ]
+  --[ Reported( $Vj, pk(SK_PSi) ), HasReport( $Vj ) ]->
+   [ Report( $Vj, pk(SK_PSi) ) ]
+
+  /* has exactly the trivial AC variant */
+
+rule (modulo E) OSR_REQ_SEND:
+   [ Report( $Vj, pk(SK_PSi) ), !RevAuthSK( $RA, SK_RA ) ]
+  --[
+  OsrReqMsgSentTo( $RA, $Vj, pk(SK_PSi) ),
+  Send( $RA,
+        <$RA, $Vj, <'revoke', pk(SK_PSi), 'reason'>, 
+         sign(<'revoke', pk(SK_PSi), 'reason'>, SK_RA)>
+  ),
+  Running( $Vj, $RA,
+           <$RA, $Vj, <'revoke', pk(SK_PSi), 'reason'>, 
+            sign(<'revoke', pk(SK_PSi), 'reason'>, SK_RA)>
+  )
+  ]->
+   [
+   AwaitRevokeConfirmation( $RA, $Vj, pk(SK_PSi), SK_RA ),
+   Out( <$RA, $Vj, <'revoke', pk(SK_PSi), 'reason'>, 
+         sign(<'revoke', pk(SK_PSi), 'reason'>, SK_RA)>
+   )
+   ]
+
+  /* has exactly the trivial AC variant */
+
+rule (modulo E) OSR_REQ_RECV:
+   [
+   In( <$RA, $Vj, <'revoke', pk(SK_PSi), 'reason'>, 
+        sign(<'revoke', pk(SK_PSi), 'reason'>, SK_RA)>
+   ),
+   !RevAuthPK( $RA, PK_RA ), !VehiclePSi( $Vj, SK_PSi ),
+   CanChange( $Vj, SK_PSi )
+   ]
+  --[
+  Commit( $RA, $Vj,
+          <$RA, $Vj, <'revoke', pk(SK_PSi), 'reason'>, 
+           sign(<'revoke', pk(SK_PSi), 'reason'>, SK_RA)>
+  ),
+  OsrReqMsgRecvBy( $Vj, $RA, pk(SK_PSi) ),
+  Recv( $Vj,
+        <$RA, $Vj, <'revoke', pk(SK_PSi), 'reason'>, 
+         sign(<'revoke', pk(SK_PSi), 'reason'>, SK_RA)>
+  ),
+  Eq( verify(sign(<'revoke', pk(SK_PSi), 'reason'>, SK_RA),
+             <'revoke', pk(SK_PSi), 'reason'>, PK_RA),
+      true
+  ),
+  OsrReqVerified( $Vj, pk(SK_PSi) ),
+  Running( $RA, $Vj,
+           <$Vj, $RA, <$Vj, 'confirm', pk(SK_PSi)>, 
+            sign(<$Vj, 'confirm', pk(SK_PSi)>, SK_PSi)>
+  ),
+  OsrConfSentBy( $Vj, $RA, pk(SK_PSi) )
+  ]->
+   [
+   Out( <$Vj, $RA, <$Vj, 'confirm', pk(SK_PSi)>, 
+         sign(<$Vj, 'confirm', pk(SK_PSi)>, SK_PSi)>
+   )
+   ]
+
+  /*
+  rule (modulo AC) OSR_REQ_RECV:
+     [
+     In( <$RA, $Vj, <'revoke', pk(SK_PSi), 'reason'>, 
+          sign(<'revoke', pk(SK_PSi), 'reason'>, SK_RA)>
+     ),
+     !RevAuthPK( $RA, PK_RA ), !VehiclePSi( $Vj, SK_PSi ),
+     CanChange( $Vj, SK_PSi )
+     ]
+    --[
+    Commit( $RA, $Vj,
+            <$RA, $Vj, <'revoke', pk(SK_PSi), 'reason'>, 
+             sign(<'revoke', pk(SK_PSi), 'reason'>, SK_RA)>
+    ),
+    OsrReqMsgRecvBy( $Vj, $RA, pk(SK_PSi) ),
+    Recv( $Vj,
+          <$RA, $Vj, <'revoke', pk(SK_PSi), 'reason'>, 
+           sign(<'revoke', pk(SK_PSi), 'reason'>, SK_RA)>
+    ),
+    Eq( z, true ), OsrReqVerified( $Vj, pk(SK_PSi) ),
+    Running( $RA, $Vj,
+             <$Vj, $RA, <$Vj, 'confirm', pk(SK_PSi)>, 
+              sign(<$Vj, 'confirm', pk(SK_PSi)>, SK_PSi)>
+    ),
+    OsrConfSentBy( $Vj, $RA, pk(SK_PSi) )
+    ]->
+     [
+     Out( <$Vj, $RA, <$Vj, 'confirm', pk(SK_PSi)>, 
+           sign(<$Vj, 'confirm', pk(SK_PSi)>, SK_PSi)>
+     )
+     ]
+    variants (modulo AC)
+    1. PK_RA = PK_RA.13
+       SK_PSi
+             = SK_PSi.14
+       SK_RA = SK_RA.15
+       z     = verify(sign(<'revoke', pk(SK_PSi.14), 'reason'>, SK_RA.15),
+                      <'revoke', pk(SK_PSi.14), 'reason'>, PK_RA.13)
+    
+    2. PK_RA = pk(SK_RA.11)
+       SK_RA = SK_RA.11
+       z     = true
+  */
+
+rule (modulo E) REV_AUTH_OSR_CONF_RECV:
+   [
+   In( <$Vj, $RA, <$Vj, 'confirm', pk(SK_PSi)>, 
+        sign(<$Vj, 'confirm', pk(SK_PSi)>, SK_PSi)>
+   ),
+   AwaitRevokeConfirmation( $RA, $Vj, pk(SK_PSi), SK_RA )
+   ]
+  --[
+  Commit( $Vj, $RA,
+          <$Vj, $RA, <$Vj, 'confirm', pk(SK_PSi)>, 
+           sign(<$Vj, 'confirm', pk(SK_PSi)>, SK_PSi)>
+  ),
+  Eq( verify(sign(<$Vj, 'confirm', pk(SK_PSi)>, SK_PSi),
+             <$Vj, 'confirm', pk(SK_PSi)>, pk(SK_PSi)),
+      true
+  ),
+  OsrConfAcceptedBy( $RA, $Vj, pk(SK_PSi) )
+  ]->
+   [ ]
+
+  /*
+  rule (modulo AC) REV_AUTH_OSR_CONF_RECV:
+     [
+     In( <$Vj, $RA, <$Vj, 'confirm', pk(SK_PSi)>, 
+          sign(<$Vj, 'confirm', pk(SK_PSi)>, SK_PSi)>
+     ),
+     AwaitRevokeConfirmation( $RA, $Vj, pk(SK_PSi), SK_RA )
+     ]
+    --[
+    Commit( $Vj, $RA,
+            <$Vj, $RA, <$Vj, 'confirm', pk(SK_PSi)>, 
+             sign(<$Vj, 'confirm', pk(SK_PSi)>, SK_PSi)>
+    ),
+    Eq( true, true ), OsrConfAcceptedBy( $RA, $Vj, pk(SK_PSi) )
+    ]->
+     [ ]
+  */
+
+lemma executable:
+  exists-trace
+  "∃ id_ra id_vj m t #i #j #k.
+    ((((Send( id_ra, m ) @ #i) ∧ (Recv( id_vj, m ) @ #j)) ∧
+      (OsrConfAcceptedBy( id_ra, id_vj, t ) @ #k)) ∧
+     (#i < #j)) ∧
+    (#j < #k)"
+/*
+guarded formula characterizing all satisfying traces:
+"∃ id_ra id_vj m t #i #j #k.
+  (Send( id_ra, m ) @ #i) ∧
+  (Recv( id_vj, m ) @ #j) ∧
+  (OsrConfAcceptedBy( id_ra, id_vj, t ) @ #k)
+ ∧
+  (#i < #j) ∧ (#j < #k)"
+*/
+simplify
+solve( Report( $Vj, pk(SK_PSi) ) â–¶â‚€ #i )
+  case REPORT
+  solve( !RevAuthSK( $RA, SK_RA ) ▶₁ #i )
+    case RA_SETUP
+    solve( !RevAuthPK( $RA, pk(~SK_RA) ) ▶₁ #j )
+      case RA_SETUP
+      solve( !VehiclePSi( $Vj, ~SK_PSi ) â–¶â‚‚ #j )
+        case SETUP_PSI_KEY
+        solve( CanChange( $Vj, ~SK_PSi ) ▶₃ #j )
+          case SETUP_PSI_KEY
+          solve( AwaitRevokeConfirmation( $RA, $Vj, pk(SK_PSi.1), SK_RA.1
+                 ) ▶₁ #k )
+            case OSR_REQ_SEND
+            solve( !KU( sign(<'revoke', pk(~SK_PSi), 'reason'>, ~SK_RA)
+                   ) @ #vk.15 )
+              case OSR_REQ_SEND
+              solve( !KU( sign(<$Vj, 'confirm', pk(~SK_PSi)>, ~SK_PSi)
+                     ) @ #vk.17 )
+                case OSR_REQ_RECV
+                solve( !KU( pk(~SK_PSi) ) @ #vk.14 )
+                  case OSR_REQ_SEND
+                  SOLVED // trace found
+                qed
+              qed
+            qed
+          qed
+        qed
+      qed
+    qed
+  qed
+qed
+
+lemma revoke_after_change_exists:
+  exists-trace
+  "∃ id_vj ps1 ps2 id_ra #i #j #k.
+    ((((((Reported( id_vj, ps1 ) @ #i) ∧
+         (ChangePseudonymForVehicle( id_vj, ps1, ps2 ) @ #j)) ∧
+        (OsrConfSentBy( id_vj, id_ra, ps1 ) @ #k)) ∧
+       (#i < #j)) ∧
+      (#j < #k)) ∧
+     (¬(∃ k.1 #n. VehicleCompromised( id_vj, k.1 ) @ #n))) ∧
+    (¬(∃ k.1 #n. VjSKPSiReveal( id_vj, k.1 ) @ #n))"
+/*
+guarded formula characterizing all satisfying traces:
+"∃ id_vj ps1 ps2 id_ra #i #j #k.
+  (Reported( id_vj, ps1 ) @ #i) ∧
+  (ChangePseudonymForVehicle( id_vj, ps1, ps2 ) @ #j) ∧
+  (OsrConfSentBy( id_vj, id_ra, ps1 ) @ #k)
+ ∧
+  (#i < #j) ∧
+  (#j < #k) ∧
+  (∀ k.1 #n. (VehicleCompromised( id_vj, k.1 ) @ #n) ⇒ ⊥) ∧
+  (∀ k.1 #n. (VjSKPSiReveal( id_vj, k.1 ) @ #n) ⇒ ⊥)"
+*/
+simplify
+solve( !VehiclePKPSi( $Vj, pk(SK_PSi) ) â–¶â‚€ #i )
+  case SETUP_PSI_KEY
+  solve( !RevAuthPK( $RA, pk(SK_RA) ) ▶₁ #k )
+    case RA_SETUP
+    solve( !VehiclePSi( $Vj, ~SK_PSi ) â–¶â‚‚ #k )
+      case SETUP_PSI_KEY
+      solve( CanChange( $Vj, ~SK_PSi ) ▶₃ #k )
+        case SETUP_PSI_KEY
+        solve( !KU( sign(<'revoke', pk(~SK_PSi), 'reason'>, ~SK_RA)
+               ) @ #vk.10 )
+          case OSR_REQ_SEND
+          by solve( CanChange( $Vj, ~SK_PSi ) ▶₁ #j )
+        next
+          case c_sign
+          by solve( !KU( ~SK_RA ) @ #vk.11 )
+        qed
+      qed
+    qed
+  qed
+qed
+
+lemma weak_agreement:
+  all-traces
+  "∀ id_vj id_ra t #i.
+    (OsrConfAcceptedBy( id_ra, id_vj, t ) @ #i) ⇒
+    (((∃ t2 #j. OsrReqMsgRecvBy( id_vj, id_ra, t2 ) @ #j) ∨
+      (∃ #r. RevealLtk( id_vj ) @ #r)) ∨
+     (∃ #r. RevealSKPSi( id_vj ) @ #r))"
+/*
+guarded formula characterizing all counter-examples:
+"∃ id_vj id_ra t #i.
+  (OsrConfAcceptedBy( id_ra, id_vj, t ) @ #i)
+ ∧
+  (∀ t2 #j. (OsrReqMsgRecvBy( id_vj, id_ra, t2 ) @ #j) ⇒ ⊥) ∧
+  (∀ #r. (RevealLtk( id_vj ) @ #r) ⇒ ⊥) ∧
+  (∀ #r. (RevealSKPSi( id_vj ) @ #r) ⇒ ⊥)"
+*/
+simplify
+solve( AwaitRevokeConfirmation( $RA, $Vj, pk(SK_PSi), SK_RA
+       ) ▶₁ #i )
+  case OSR_REQ_SEND
+  solve( !KU( sign(<$Vj, 'confirm', pk(~SK_PSi)>, ~SK_PSi)
+         ) @ #vk.9 )
+    case OSR_REQ_RECV
+    by contradiction /* from formulas */
+  next
+    case c_sign
+    solve( !KU( ~SK_PSi ) @ #vk.10 )
+      case REVEAL_PSI_KEY
+      by contradiction /* from formulas */
+    qed
+  qed
+qed
+
+lemma noninjective_agreement:
+  all-traces
+  "∀ a b msg #i.
+    (Commit( a, b, msg ) @ #i) ⇒
+    (((∃ #j. Running( b, a, msg ) @ #j) ∨
+      (∃ C #r. RevealLtk( C ) @ #r)) ∨
+     (∃ C #r. RevealSKPSi( C ) @ #r))"
+/*
+guarded formula characterizing all counter-examples:
+"∃ a b msg #i.
+  (Commit( a, b, msg ) @ #i)
+ ∧
+  (∀ #j. (Running( b, a, msg ) @ #j) ⇒ ⊥) ∧
+  (∀ C #r. (RevealLtk( C ) @ #r) ⇒ ⊥) ∧
+  (∀ C #r. (RevealSKPSi( C ) @ #r) ⇒ ⊥)"
+*/
+simplify
+solve( Commit( a, b, msg ) @ #i )
+  case OSR_REQ_RECV
+  solve( !RevAuthPK( $RA, pk(SK_RA) ) ▶₁ #i )
+    case RA_SETUP
+    solve( !VehiclePSi( $Vj, SK_PSi ) â–¶â‚‚ #i )
+      case CHANGE_PSEUDONYM
+      solve( CanChange( $Vj, ~SK_PSi ) ▶₃ #i )
+        case CHANGE_PSEUDONYM
+        solve( !KU( sign(<'revoke', pk(~SK_PSi), 'reason'>, ~SK_RA)
+               ) @ #vk.10 )
+          case c_sign
+          by solve( !KU( ~SK_RA ) @ #vk.11 )
+        qed
+      qed
+    next
+      case SETUP_PSI_KEY
+      solve( CanChange( $Vj, ~SK_PSi ) ▶₃ #i )
+        case SETUP_PSI_KEY
+        solve( !KU( sign(<'revoke', pk(~SK_PSi), 'reason'>, ~SK_RA)
+               ) @ #vk.10 )
+          case OSR_REQ_SEND
+          by contradiction /* from formulas */
+        next
+          case c_sign
+          by solve( !KU( ~SK_RA ) @ #vk.11 )
+        qed
+      qed
+    qed
+  qed
+next
+  case REV_AUTH_OSR_CONF_RECV
+  solve( AwaitRevokeConfirmation( $RA, $Vj, pk(SK_PSi), SK_RA
+         ) ▶₁ #i )
+    case OSR_REQ_SEND
+    solve( !KU( sign(<$Vj, 'confirm', pk(~SK_PSi)>, ~SK_PSi)
+           ) @ #vk.9 )
+      case OSR_REQ_RECV
+      by contradiction /* from formulas */
+    next
+      case c_sign
+      solve( !KU( ~SK_PSi ) @ #vk.10 )
+        case REVEAL_PSI_KEY
+        by contradiction /* from formulas */
+      qed
+    qed
+  qed
+qed
+
+lemma noninjective_synchronisation:
+  all-traces
+  "∀ id_ra id_vj ps #i.
+    ((OsrConfAcceptedBy( id_ra, id_vj, ps ) @ #i) ∧
+     (¬(∃ k1 #q. VjSKPSiReveal( id_vj, k1 ) @ #q))) ⇒
+    (∃ #l. (OsrReqMsgRecvBy( id_vj, id_ra, ps ) @ #l) ∧ (#l < #i))"
+/*
+guarded formula characterizing all counter-examples:
+"∃ id_ra id_vj ps #i.
+  (OsrConfAcceptedBy( id_ra, id_vj, ps ) @ #i)
+ ∧
+  (∀ k1 #q. (VjSKPSiReveal( id_vj, k1 ) @ #q) ⇒ ⊥) ∧
+  (∀ #l. (OsrReqMsgRecvBy( id_vj, id_ra, ps ) @ #l) ⇒ ¬(#l < #i))"
+*/
+simplify
+solve( AwaitRevokeConfirmation( $RA, $Vj, pk(SK_PSi), SK_RA
+       ) ▶₁ #i )
+  case OSR_REQ_SEND
+  solve( !KU( sign(<$Vj, 'confirm', pk(~SK_PSi)>, ~SK_PSi)
+         ) @ #vk.9 )
+    case OSR_REQ_RECV
+    by contradiction /* from formulas */
+  next
+    case c_sign
+    solve( !KU( ~SK_PSi ) @ #vk.10 )
+      case REVEAL_PSI_KEY
+      by contradiction /* from formulas */
+    qed
+  qed
+qed
+
+/* All well-formedness checks were successful. */
+
+end
\ No newline at end of file
diff --git a/Chapter04_REWIRE_OTOKEN/analysed/REWIRE_RTOKEN.analysed.spthy b/Chapter04_REWIRE_OTOKEN/analysed/REWIRE_RTOKEN.analysed.spthy
new file mode 100644
index 0000000000000000000000000000000000000000..e2c19ce68b6d507a0364297eb7f1e0f89143ec36
--- /dev/null
+++ b/Chapter04_REWIRE_OTOKEN/analysed/REWIRE_RTOKEN.analysed.spthy
@@ -0,0 +1,633 @@
+theory REWIRE_RTOKEN begin
+
+// Function signature and definition of the equational theory E
+
+functions: adec/2, aenc/2, fst/1, pair/2, pk/1, sign/2, snd/1,
+           true/0, verify/3
+equations:
+    adec(aenc(x.1, pk(x.2)), x.2) = x.1,
+    fst(<x.1, x.2>) = x.1,
+    snd(<x.1, x.2>) = x.2,
+    verify(sign(x.1, x.2), x.1, pk(x.2)) = true
+
+restriction equality_checks_succeed:
+  "∀ x y #i. (Eq( x, y ) @ #i) ⇒ (x = y)"
+  // safety formula
+
+restriction single_RA:
+  "∀ #i #j.
+    ((SetupRevAuthKeys( ) @ #i) ∧ (SetupRevAuthKeys( ) @ #j)) ⇒
+    (#i = #j)"
+  // safety formula
+
+restriction single_vj_sk_setup:
+  "∀ id #i #j.
+    ((SetupVehicleSK( id ) @ #i) ∧ (SetupVehicleSK( id ) @ #j)) ⇒
+    (#i = #j)"
+  // safety formula
+
+restriction single_psi_init:
+  "∀ id key #i #j.
+    ((InitPSiKey( id, key ) @ #i) ∧ (InitPSiKey( id, key ) @ #j)) ⇒
+    (#i = #j)"
+  // safety formula
+
+restriction single_init_event:
+  "∀ id #i #j.
+    ((InitVjPseudonym( id ) @ #i) ∧ (InitVjPseudonym( id ) @ #j)) ⇒
+    (#i = #j)"
+  // safety formula
+
+restriction no_ra_leak:
+  "¬(∃ id key #i #j.
+      (SetupRAKeys( id, key ) @ #i) ∧ (K( key ) @ #j))"
+  // safety formula
+
+rule (modulo E) RA_SETUP:
+   [ Fr( ~SK_RA ) ]
+  --[ SetupRevAuthKeys( ), SetupRAKeys( $RA, ~SK_RA ) ]->
+   [
+   !RevAuthSK( $RA, ~SK_RA ), !RevAuthPK( $RA, pk(~SK_RA) ),
+   Out( pk(~SK_RA) )
+   ]
+
+  /* has exactly the trivial AC variant */
+
+rule (modulo E) SETUP_VEHICLE_KEY_PAIR:
+   [ Fr( ~SK_Vj ) ]
+  --[ SetupVehicleSK( $Vj ), VehicleSetup( $Vj, ~SK_Vj ) ]->
+   [ !VjSK( $Vj, ~SK_Vj ), !VjPK( $Vj, pk(~SK_Vj) ) ]
+
+  /* has exactly the trivial AC variant */
+
+rule (modulo E) REVEAL_VEHICLE_SK:
+   [ !VjSK( $Vj, SK_Vj ) ]
+  --[ VehicleCompromised( $Vj, SK_Vj ), RevealSK( $Vj ) ]->
+   [ Out( SK_Vj ) ]
+
+  /* has exactly the trivial AC variant */
+
+rule (modulo E) SETUP_PSI_KEY:
+   [ Fr( ~SK_PSi ) ]
+  --[ InitPSiKey( $Vj, ~SK_PSi ) ]->
+   [ !VehiclePSi( $Vj, ~SK_PSi ) ]
+
+  /* has exactly the trivial AC variant */
+
+rule (modulo E) REVEAL_PSI_KEY:
+   [ !VehiclePSi( $Vj, SK_PSi ) ]
+  --[ VjSKPSiReveal( $Vj, SK_PSi ) ]->
+   [ Out( SK_PSi ) ]
+
+  /* has exactly the trivial AC variant */
+
+rule (modulo E) SETUP_VEHICLE_PSEUDONYM:
+   [
+   !VjSK( $Vj, SK_Vj ), !VjPK( $Vj, PK_Vj ),
+   !VehiclePSi( $Vj, SK_PSi ), Fr( ~r )
+   ]
+  --[ InitVjPseudonym( $Vj ) ]->
+   [
+   !VehiclePseudonym( $Vj, <pk(SK_PSi), aenc(<$Vj, PK_Vj, ~r>, PK_Vj)>
+   ),
+   CanChange( $Vj, <pk(SK_PSi), aenc(<$Vj, PK_Vj, ~r>, PK_Vj)> ),
+   Out( <pk(SK_PSi), aenc(<$Vj, PK_Vj, ~r>, PK_Vj)> )
+   ]
+
+  /* has exactly the trivial AC variant */
+
+rule (modulo E) CHANGE_PSEUDONYM:
+   [
+   !VjSK( $Vj, SK_Vj ), !VjPK( $Vj, PK_Vj ), Fr( ~SK_PSi ), Fr( ~r ),
+   CanChange( $Vj, old )
+   ]
+  --[
+  ChangePseudonymForVehicle( $Vj, old,
+                             <pk(~SK_PSi), aenc(<$Vj, PK_Vj, ~r>, PK_Vj)>
+  )
+  ]->
+   [
+   !VehiclePseudonym( $Vj,
+                      <pk(~SK_PSi), aenc(<$Vj, PK_Vj, ~r>, PK_Vj)>
+   ),
+   CanChange( $Vj, <pk(~SK_PSi), aenc(<$Vj, PK_Vj, ~r>, PK_Vj)> ),
+   Out( <pk(~SK_PSi), aenc(<$Vj, PK_Vj, ~r>, PK_Vj)> )
+   ]
+
+  // loop breaker: [4]
+  /* has exactly the trivial AC variant */
+
+rule (modulo E) REPORT:
+   [ !VehiclePseudonym( $Vj, pseudonym ) ]
+  --[ Reported( $Vj, pseudonym ) ]->
+   [ Report( pseudonym ) ]
+
+  /* has exactly the trivial AC variant */
+
+rule (modulo E) OSR_REQ_SEND:
+   [
+   Report( <PK_PSi, aenc(<$Vj, PK_Vj, r>, PK_Vj)> ),
+   !RevAuthSK( $RA, SK_RA )
+   ]
+  --[
+  OsrReqMsgSentTo( $RA, $Vj, aenc(<$Vj, PK_Vj, r>, PK_Vj) ),
+  Send( $RA,
+        <$RA, $Vj, 
+         <'revoke', <PK_PSi, aenc(<$Vj, PK_Vj, r>, PK_Vj)>, 'reason'>, 
+         sign(<'revoke', <PK_PSi, aenc(<$Vj, PK_Vj, r>, PK_Vj)>, 'reason'>,
+              SK_RA)
+        >
+  ),
+  Running( $Vj, $RA,
+           <$RA, $Vj, 
+            <'revoke', <PK_PSi, aenc(<$Vj, PK_Vj, r>, PK_Vj)>, 'reason'>, 
+            sign(<'revoke', <PK_PSi, aenc(<$Vj, PK_Vj, r>, PK_Vj)>, 'reason'>,
+                 SK_RA)
+           >
+  )
+  ]->
+   [
+   AwaitRevokeConfirmation( $RA, $Vj, aenc(<$Vj, PK_Vj, r>, PK_Vj),
+                            SK_RA
+   ),
+   Out( <$RA, $Vj, 
+         <'revoke', <PK_PSi, aenc(<$Vj, PK_Vj, r>, PK_Vj)>, 'reason'>, 
+         sign(<'revoke', <PK_PSi, aenc(<$Vj, PK_Vj, r>, PK_Vj)>, 'reason'>,
+              SK_RA)
+        >
+   )
+   ]
+
+  /* has exactly the trivial AC variant */
+
+rule (modulo E) OSR_REQ_RECV:
+   [
+   In( <$RA, $Vj, 
+        <'revoke', <PK_PSi, aenc(<$Vj, PK_Vj, ~r>, PK_Vj)>, 'reason'>, 
+        sign(<'revoke', <PK_PSi, aenc(<$Vj, PK_Vj, ~r>, PK_Vj)>, 'reason'>,
+             SK_RA)
+       >
+   ),
+   !RevAuthPK( $RA, PK_RA ), !VjSK( $Vj, SK_Vj ), !VjPK( $Vj, PK_Vj ),
+   CanChange( $Vj, <PK_PSi, aenc(<$Vj, PK_Vj, ~r>, PK_Vj)> )
+   ]
+  --[
+  Commit( $RA, $Vj,
+          <$RA, $Vj, 
+           <'revoke', <PK_PSi, aenc(<$Vj, PK_Vj, ~r>, PK_Vj)>, 'reason'>, 
+           sign(<'revoke', <PK_PSi, aenc(<$Vj, PK_Vj, ~r>, PK_Vj)>, 'reason'>,
+                SK_RA)
+          >
+  ),
+  OsrReqMsgRecvBy( $Vj, $RA, aenc(<$Vj, PK_Vj, ~r>, PK_Vj) ),
+  Recv( $Vj,
+        <$RA, $Vj, 
+         <'revoke', <PK_PSi, aenc(<$Vj, PK_Vj, ~r>, PK_Vj)>, 'reason'>, 
+         sign(<'revoke', <PK_PSi, aenc(<$Vj, PK_Vj, ~r>, PK_Vj)>, 'reason'>,
+              SK_RA)
+        >
+  ),
+  Eq( verify(sign(<'revoke', 
+                   <PK_PSi, aenc(<$Vj, PK_Vj, ~r>, PK_Vj)>, 'reason'>,
+                  SK_RA),
+             <'revoke', <PK_PSi, aenc(<$Vj, PK_Vj, ~r>, PK_Vj)>, 'reason'>,
+             PK_RA),
+      true
+  ),
+  OsrReqVerified( $Vj, aenc(<$Vj, PK_Vj, ~r>, PK_Vj) ),
+  Eq( adec(aenc(<$Vj, PK_Vj, ~r>, PK_Vj), SK_Vj), <$Vj, PK_Vj, ~r> ),
+  DeleteAllPseudonyms( $Vj, SK_Vj, aenc(<$Vj, PK_Vj, ~r>, PK_Vj) ),
+  Running( $RA, $Vj,
+           <$Vj, $RA, <$Vj, 'confirm', aenc(<$Vj, PK_Vj, ~r>, PK_Vj)>, 
+            sign(<$Vj, 'confirm', aenc(<$Vj, PK_Vj, ~r>, PK_Vj)>, SK_Vj)>
+  ),
+  OsrConfSentBy( $Vj, $RA, aenc(<$Vj, PK_Vj, ~r>, PK_Vj) )
+  ]->
+   [
+   Out( <$Vj, $RA, <$Vj, 'confirm', aenc(<$Vj, PK_Vj, ~r>, PK_Vj)>, 
+         sign(<$Vj, 'confirm', aenc(<$Vj, PK_Vj, ~r>, PK_Vj)>, SK_Vj)>
+   )
+   ]
+
+  /*
+  rule (modulo AC) OSR_REQ_RECV:
+     [
+     In( <$RA, $Vj, 
+          <'revoke', <PK_PSi, aenc(<$Vj, PK_Vj, ~r>, PK_Vj)>, 'reason'>, 
+          sign(<'revoke', <PK_PSi, aenc(<$Vj, PK_Vj, ~r>, PK_Vj)>, 'reason'>,
+               SK_RA)
+         >
+     ),
+     !RevAuthPK( $RA, PK_RA ), !VjSK( $Vj, SK_Vj ), !VjPK( $Vj, PK_Vj ),
+     CanChange( $Vj, <PK_PSi, aenc(<$Vj, PK_Vj, ~r>, PK_Vj)> )
+     ]
+    --[
+    Commit( $RA, $Vj,
+            <$RA, $Vj, 
+             <'revoke', <PK_PSi, aenc(<$Vj, PK_Vj, ~r>, PK_Vj)>, 'reason'>, 
+             sign(<'revoke', <PK_PSi, aenc(<$Vj, PK_Vj, ~r>, PK_Vj)>, 'reason'>,
+                  SK_RA)
+            >
+    ),
+    OsrReqMsgRecvBy( $Vj, $RA, aenc(<$Vj, PK_Vj, ~r>, PK_Vj) ),
+    Recv( $Vj,
+          <$RA, $Vj, 
+           <'revoke', <PK_PSi, aenc(<$Vj, PK_Vj, ~r>, PK_Vj)>, 'reason'>, 
+           sign(<'revoke', <PK_PSi, aenc(<$Vj, PK_Vj, ~r>, PK_Vj)>, 'reason'>,
+                SK_RA)
+          >
+    ),
+    Eq( z, true ),
+    OsrReqVerified( $Vj, aenc(<$Vj, PK_Vj, ~r>, PK_Vj) ),
+    Eq( z.1, <$Vj, PK_Vj, ~r> ),
+    DeleteAllPseudonyms( $Vj, SK_Vj, aenc(<$Vj, PK_Vj, ~r>, PK_Vj) ),
+    Running( $RA, $Vj,
+             <$Vj, $RA, <$Vj, 'confirm', aenc(<$Vj, PK_Vj, ~r>, PK_Vj)>, 
+              sign(<$Vj, 'confirm', aenc(<$Vj, PK_Vj, ~r>, PK_Vj)>, SK_Vj)>
+    ),
+    OsrConfSentBy( $Vj, $RA, aenc(<$Vj, PK_Vj, ~r>, PK_Vj) )
+    ]->
+     [
+     Out( <$Vj, $RA, <$Vj, 'confirm', aenc(<$Vj, PK_Vj, ~r>, PK_Vj)>, 
+           sign(<$Vj, 'confirm', aenc(<$Vj, PK_Vj, ~r>, PK_Vj)>, SK_Vj)>
+     )
+     ]
+    variants (modulo AC)
+    1. $Vj   = $Vj.21
+       ~r    = ~r.22
+       PK_PSi
+             = PK_PSi.23
+       PK_RA = PK_RA.24
+       PK_Vj = PK_Vj.25
+       SK_RA = SK_RA.26
+       SK_Vj = SK_Vj.27
+       z     = verify(sign(<'revoke', 
+                            <PK_PSi.23, aenc(<$Vj.21, PK_Vj.25, ~r.22>, PK_Vj.25)>, 'reason'>,
+                           SK_RA.26),
+                      <'revoke', <PK_PSi.23, aenc(<$Vj.21, PK_Vj.25, ~r.22>, PK_Vj.25)>, 
+                       'reason'>,
+                      PK_RA.24)
+       z.1   = adec(aenc(<$Vj.21, PK_Vj.25, ~r.22>, PK_Vj.25), SK_Vj.27)
+    
+    2. $Vj   = $Vj.21
+       ~r    = ~r.22
+       PK_PSi
+             = PK_PSi.23
+       PK_RA = PK_RA.24
+       PK_Vj = pk(SK_Vj.27)
+       SK_RA = SK_RA.26
+       SK_Vj = SK_Vj.27
+       z     = verify(sign(<'revoke', 
+                            <PK_PSi.23, aenc(<$Vj.21, pk(SK_Vj.27), ~r.22>, pk(SK_Vj.27))>, 
+                            'reason'>,
+                           SK_RA.26),
+                      <'revoke', 
+                       <PK_PSi.23, aenc(<$Vj.21, pk(SK_Vj.27), ~r.22>, pk(SK_Vj.27))>, 
+                       'reason'>,
+                      PK_RA.24)
+       z.1   = <$Vj.21, pk(SK_Vj.27), ~r.22>
+    
+    3. $Vj   = $Vj.21
+       ~r    = ~r.22
+       PK_RA = pk(SK_RA.26)
+       PK_Vj = PK_Vj.25
+       SK_RA = SK_RA.26
+       SK_Vj = SK_Vj.27
+       z     = true
+       z.1   = adec(aenc(<$Vj.21, PK_Vj.25, ~r.22>, PK_Vj.25), SK_Vj.27)
+    
+    4. $Vj   = $Vj.21
+       ~r    = ~r.22
+       PK_RA = pk(SK_RA.26)
+       PK_Vj = pk(SK_Vj.27)
+       SK_RA = SK_RA.26
+       SK_Vj = SK_Vj.27
+       z     = true
+       z.1   = <$Vj.21, pk(SK_Vj.27), ~r.22>
+  */
+
+rule (modulo E) REV_AUTH_OSR_CONF_RECV:
+   [
+   In( <$Vj, $RA, <$Vj, 'confirm', R_Token>, 
+        sign(<$Vj, 'confirm', R_Token>, SK_Vj)>
+   ),
+   AwaitRevokeConfirmation( $RA, $Vj, R_Token, SK_RA )
+   ]
+  --[
+  Commit( $Vj, $RA,
+          <$Vj, $RA, <$Vj, 'confirm', R_Token>, 
+           sign(<$Vj, 'confirm', R_Token>, SK_Vj)>
+  ),
+  OsrConfAcceptedBy( $RA, $Vj, R_Token )
+  ]->
+   [ ]
+
+  /* has exactly the trivial AC variant */
+
+lemma executable:
+  exists-trace
+  "∃ id_ra id_vj m t #i #j #k.
+    ((((Send( id_ra, m ) @ #i) ∧ (Recv( id_vj, m ) @ #j)) ∧
+      (OsrConfAcceptedBy( id_ra, id_vj, t ) @ #k)) ∧
+     (#i < #j)) ∧
+    (#j < #k)"
+/*
+guarded formula characterizing all satisfying traces:
+"∃ id_ra id_vj m t #i #j #k.
+  (Send( id_ra, m ) @ #i) ∧
+  (Recv( id_vj, m ) @ #j) ∧
+  (OsrConfAcceptedBy( id_ra, id_vj, t ) @ #k)
+ ∧
+  (#i < #j) ∧ (#j < #k)"
+*/
+simplify
+solve( Report( <PK_PSi, aenc(<$Vj, pk(SK_Vj), ~r>, pk(SK_Vj))>
+       ) â–¶â‚€ #i )
+  case REPORT_case_1
+  solve( !RevAuthSK( $RA, SK_RA ) ▶₁ #i )
+    case RA_SETUP
+    solve( !RevAuthPK( $RA, pk(~SK_RA) ) ▶₁ #j )
+      case RA_SETUP
+      solve( !VjSK( $Vj, ~SK_Vj ) â–¶â‚‚ #j )
+        case SETUP_VEHICLE_KEY_PAIR
+        solve( !VjPK( $Vj, pk(~SK_Vj) ) ▶₃ #j )
+          case SETUP_VEHICLE_KEY_PAIR
+          solve( CanChange( $Vj,
+                            <pk(~SK_PSi), aenc(<$Vj, pk(~SK_Vj), ~r>, pk(~SK_Vj))>
+                 ) â–¶â‚„ #j )
+            case SETUP_VEHICLE_PSEUDONYM
+            solve( AwaitRevokeConfirmation( $RA, $Vj, t, SK_RA.1 ) ▶₁ #k )
+              case OSR_REQ_SEND_case_1
+              solve( !KU( sign(<$Vj, 'confirm', 
+                                aenc(<$Vj, pk(~SK_Vj), ~r>, pk(~SK_Vj))>,
+                               SK_Vj.1)
+                     ) @ #vk.19 )
+                case OSR_REQ_RECV
+                solve( !KU( sign(<'revoke', 
+                                  <pk(~SK_PSi), aenc(<$Vj, pk(~SK_Vj), ~r>, pk(~SK_Vj))>, 'reason'>,
+                                 ~SK_RA)
+                       ) @ #vk.18 )
+                  case OSR_REQ_SEND
+                  solve( !KU( aenc(<$Vj, pk(~SK_Vj), ~r>, pk(~SK_Vj)) ) @ #vk.16 )
+                    case OSR_REQ_SEND
+                    solve( !KU( pk(~SK_PSi) ) @ #vk.16 )
+                      case OSR_REQ_SEND
+                      SOLVED // trace found
+                    qed
+                  qed
+                qed
+              qed
+            qed
+          qed
+        qed
+      qed
+    qed
+  qed
+qed
+
+lemma revoke_after_change_exists:
+  exists-trace
+  "∃ id_vj id_ra t ps1 ps2 #i #j #k.
+    (((((Reported( id_vj, ps1 ) @ #i) ∧
+        (ChangePseudonymForVehicle( id_vj, ps1, ps2 ) @ #j)) ∧
+       (OsrConfSentBy( id_vj, id_ra, t ) @ #k)) ∧
+      (#i < #j)) ∧
+     (#j < #k)) ∧
+    (¬(∃ k.1 #n. VehicleCompromised( id_vj, k.1 ) @ #n))"
+/*
+guarded formula characterizing all satisfying traces:
+"∃ id_vj id_ra t ps1 ps2 #i #j #k.
+  (Reported( id_vj, ps1 ) @ #i) ∧
+  (ChangePseudonymForVehicle( id_vj, ps1, ps2 ) @ #j) ∧
+  (OsrConfSentBy( id_vj, id_ra, t ) @ #k)
+ ∧
+  (#i < #j) ∧
+  (#j < #k) ∧
+  (∀ k.1 #n. (VehicleCompromised( id_vj, k.1 ) @ #n) ⇒ ⊥)"
+*/
+simplify
+solve( !VehiclePseudonym( $Vj, ps1 ) â–¶â‚€ #i )
+  case CHANGE_PSEUDONYM
+  solve( !VjSK( $Vj, SK_Vj.1 ) â–¶â‚€ #j )
+    case SETUP_VEHICLE_KEY_PAIR
+    solve( !VjPK( $Vj, PK_Vj ) ▶₁ #j )
+      case SETUP_VEHICLE_KEY_PAIR
+      solve( !RevAuthPK( $RA, pk(SK_RA) ) ▶₁ #k )
+        case RA_SETUP
+        solve( !VjSK( $Vj, SK_Vj.1 ) â–¶â‚‚ #k )
+          case SETUP_VEHICLE_KEY_PAIR
+          solve( !VjPK( $Vj, pk(~SK_Vj) ) ▶₃ #k )
+            case SETUP_VEHICLE_KEY_PAIR
+            solve( CanChange( $Vj,
+                              <PK_PSi, aenc(<$Vj, pk(~SK_Vj), ~r.2>, pk(~SK_Vj))>
+                   ) â–¶â‚„ #k )
+              case CHANGE_PSEUDONYM
+              solve( !KU( sign(<'revoke', 
+                                <pk(~SK_PSi.2), aenc(<$Vj, pk(~SK_Vj), ~r.2>, pk(~SK_Vj))>, 
+                                'reason'>,
+                               ~SK_RA)
+                     ) @ #vk.12 )
+                case OSR_REQ_SEND
+                solve( CanChange( $Vj,
+                                  <pk(~SK_PSi), aenc(<$Vj, pk(~SK_Vj), ~r>, pk(~SK_Vj))>
+                       ) â–¶â‚„ #j )
+                  case CHANGE_PSEUDONYM
+                  solve( CanChange( $Vj, old ) â–¶â‚„ #vr )
+                    case SETUP_VEHICLE_PSEUDONYM
+                    solve( CanChange( $Vj, old ) â–¶â‚„ #vr.3 )
+                      case CHANGE_PSEUDONYM
+                      solve( CanChange( $Vj, old ) â–¶â‚„ #vr.11 )
+                        case SETUP_VEHICLE_PSEUDONYM
+                        solve( !KU( aenc(<$Vj, pk(~SK_Vj), ~r.1>, pk(~SK_Vj)) ) @ #vk.11 )
+                          case CHANGE_PSEUDONYM
+                          solve( !KU( pk(~SK_PSi.1) ) @ #vk.11 )
+                            case CHANGE_PSEUDONYM
+                            SOLVED // trace found
+                          qed
+                        qed
+                      qed
+                    qed
+                  qed
+                qed
+              qed
+            qed
+          qed
+        qed
+      qed
+    qed
+  qed
+qed
+
+lemma osr_req_received_with_change_all:
+  all-traces
+  "∀ id_vj id_ra t #i.
+    ((OsrConfSentBy( id_vj, id_ra, t ) @ #i) ∧
+     (¬(∃ key #k. VehicleCompromised( id_vj, key ) @ #k))) ⇒
+    (∃ #a. (OsrReqMsgSentTo( id_ra, id_vj, t ) @ #a) ∧ (#a < #i))"
+/*
+guarded formula characterizing all counter-examples:
+"∃ id_vj id_ra t #i.
+  (OsrConfSentBy( id_vj, id_ra, t ) @ #i)
+ ∧
+  (∀ key #k. (VehicleCompromised( id_vj, key ) @ #k) ⇒ ⊥) ∧
+  (∀ #a. (OsrReqMsgSentTo( id_ra, id_vj, t ) @ #a) ⇒ ¬(#a < #i))"
+*/
+simplify
+solve( !RevAuthPK( $RA, pk(SK_RA) ) ▶₁ #i )
+  case RA_SETUP
+  solve( !VjSK( $Vj, SK_Vj ) â–¶â‚‚ #i )
+    case SETUP_VEHICLE_KEY_PAIR
+    solve( !VjPK( $Vj, pk(~SK_Vj) ) ▶₃ #i )
+      case SETUP_VEHICLE_KEY_PAIR
+      solve( CanChange( $Vj,
+                        <PK_PSi, aenc(<$Vj, pk(~SK_Vj), ~r>, pk(~SK_Vj))>
+             ) â–¶â‚„ #i )
+        case CHANGE_PSEUDONYM
+        solve( !KU( sign(<'revoke', 
+                          <pk(~SK_PSi), aenc(<$Vj, pk(~SK_Vj), ~r>, pk(~SK_Vj))>, 'reason'>,
+                         ~SK_RA)
+               ) @ #vk.12 )
+          case OSR_REQ_SEND
+          by contradiction /* from formulas */
+        next
+          case c_sign
+          by solve( !KU( ~SK_RA ) @ #vk.13 )
+        qed
+      next
+        case SETUP_VEHICLE_PSEUDONYM
+        solve( !KU( sign(<'revoke', 
+                          <pk(~SK_PSi), aenc(<$Vj, pk(~SK_Vj), ~r>, pk(~SK_Vj))>, 'reason'>,
+                         ~SK_RA)
+               ) @ #vk.12 )
+          case OSR_REQ_SEND
+          by contradiction /* from formulas */
+        next
+          case c_sign
+          by solve( !KU( ~SK_RA ) @ #vk.13 )
+        qed
+      qed
+    qed
+  qed
+qed
+
+lemma revoke_with_change_all:
+  all-traces
+  "∀ id_ra id_vj t #i.
+    ((OsrConfAcceptedBy( id_ra, id_vj, t ) @ #i) ∧
+     (¬(∃ key #k. VehicleCompromised( id_vj, key ) @ #k))) ⇒
+    (∃ #l. (OsrReqMsgRecvBy( id_vj, id_ra, t ) @ #l) ∧ (#l < #i))"
+/*
+guarded formula characterizing all counter-examples:
+"∃ id_ra id_vj t #i.
+  (OsrConfAcceptedBy( id_ra, id_vj, t ) @ #i)
+ ∧
+  (∀ key #k. (VehicleCompromised( id_vj, key ) @ #k) ⇒ ⊥) ∧
+  (∀ #l. (OsrReqMsgRecvBy( id_vj, id_ra, t ) @ #l) ⇒ ¬(#l < #i))"
+*/
+simplify
+solve( AwaitRevokeConfirmation( $RA, $Vj, t, SK_RA ) ▶₁ #i )
+  case OSR_REQ_SEND_case_1
+  solve( !KU( sign(<$Vj, 'confirm', 
+                    aenc(<$Vj, pk(~SK_Vj), ~r>, pk(~SK_Vj))>,
+                   SK_Vj.1)
+         ) @ #vk.9 )
+    case c_sign
+    solve( !KU( aenc(<$Vj, pk(~SK_Vj), ~r>, pk(~SK_Vj)) ) @ #vk.9 )
+      case OSR_REQ_SEND
+      SOLVED // trace found
+    qed
+  qed
+qed
+
+lemma weak_agreement:
+  all-traces
+  "∀ id_vj id_ra t #i.
+    (OsrConfAcceptedBy( id_ra, id_vj, t ) @ #i) ⇒
+    ((∃ t2 #j. OsrReqMsgRecvBy( id_vj, id_ra, t2 ) @ #j) ∨
+     (∃ #r. RevealSK( id_vj ) @ #r))"
+/*
+guarded formula characterizing all counter-examples:
+"∃ id_vj id_ra t #i.
+  (OsrConfAcceptedBy( id_ra, id_vj, t ) @ #i)
+ ∧
+  (∀ t2 #j. (OsrReqMsgRecvBy( id_vj, id_ra, t2 ) @ #j) ⇒ ⊥) ∧
+  (∀ #r. (RevealSK( id_vj ) @ #r) ⇒ ⊥)"
+*/
+simplify
+solve( AwaitRevokeConfirmation( $RA, $Vj, t, SK_RA ) ▶₁ #i )
+  case OSR_REQ_SEND_case_1
+  solve( !KU( sign(<$Vj, 'confirm', 
+                    aenc(<$Vj, pk(~SK_Vj), ~r>, pk(~SK_Vj))>,
+                   SK_Vj.1)
+         ) @ #vk.9 )
+    case c_sign
+    solve( !KU( aenc(<$Vj, pk(~SK_Vj), ~r>, pk(~SK_Vj)) ) @ #vk.9 )
+      case OSR_REQ_SEND
+      SOLVED // trace found
+    qed
+  qed
+qed
+
+lemma noninjective_agreement:
+  all-traces
+  "∀ a b msg #i.
+    (Commit( a, b, msg ) @ #i) ⇒
+    ((∃ #j. Running( b, a, msg ) @ #j) ∨ (∃ C #r. RevealSK( C ) @ #r))"
+/*
+guarded formula characterizing all counter-examples:
+"∃ a b msg #i.
+  (Commit( a, b, msg ) @ #i)
+ ∧
+  (∀ #j. (Running( b, a, msg ) @ #j) ⇒ ⊥) ∧
+  (∀ C #r. (RevealSK( C ) @ #r) ⇒ ⊥)"
+*/
+simplify
+solve( Commit( a, b, msg ) @ #i )
+  case REV_AUTH_OSR_CONF_RECV
+  solve( AwaitRevokeConfirmation( $RA, $Vj, R_Token, SK_RA ) ▶₁ #i )
+    case OSR_REQ_SEND_case_1
+    solve( !KU( sign(<$Vj, 'confirm', 
+                      aenc(<$Vj, pk(~SK_Vj), ~r>, pk(~SK_Vj))>,
+                     SK_Vj.1)
+           ) @ #vk.9 )
+      case c_sign
+      solve( !KU( aenc(<$Vj, pk(~SK_Vj), ~r>, pk(~SK_Vj)) ) @ #vk.9 )
+        case OSR_REQ_SEND
+        SOLVED // trace found
+      qed
+    qed
+  qed
+qed
+
+lemma noninjective_synchronisation:
+  all-traces
+  "∀ id_ra id_vj t #i.
+    ((OsrConfAcceptedBy( id_ra, id_vj, t ) @ #i) ∧
+     (¬(∃ #q. RevealSK( id_vj ) @ #q))) ⇒
+    (∃ #l. (OsrReqMsgRecvBy( id_vj, id_ra, t ) @ #l) ∧ (#l < #i))"
+/*
+guarded formula characterizing all counter-examples:
+"∃ id_ra id_vj t #i.
+  (OsrConfAcceptedBy( id_ra, id_vj, t ) @ #i)
+ ∧
+  (∀ #q. (RevealSK( id_vj ) @ #q) ⇒ ⊥) ∧
+  (∀ #l. (OsrReqMsgRecvBy( id_vj, id_ra, t ) @ #l) ⇒ ¬(#l < #i))"
+*/
+simplify
+solve( AwaitRevokeConfirmation( $RA, $Vj, t, SK_RA ) ▶₁ #i )
+  case OSR_REQ_SEND_case_1
+  solve( !KU( sign(<$Vj, 'confirm', 
+                    aenc(<$Vj, pk(~SK_Vj), ~r>, pk(~SK_Vj))>,
+                   SK_Vj.1)
+         ) @ #vk.9 )
+    case c_sign
+    solve( !KU( aenc(<$Vj, pk(~SK_Vj), ~r>, pk(~SK_Vj)) ) @ #vk.9 )
+      case OSR_REQ_SEND
+      SOLVED // trace found
+    qed
+  qed
+qed
+
+/* All well-formedness checks were successful. */
+
+end
\ No newline at end of file