- Add session compromise to all protocols that establish a session key

spdl/SPORE/andrew-ban-concrete.spdl

@@ -19,6 +19,7 @@
 usertype SessionKey;
 secret k: Function;
 const Fresh: Function;
+const Compromised: Function;
 
 protocol swapkey(X)
 {
@@ -31,6 +32,28 @@ protocol swapkey(X)
         send_X2(X,X,{T}k(R,I));
     }
 }
+
+protocol andrewConcreteSessionKeyCompromise(C)
+{
+    // Read the names of 3 agents and disclose a session between them including
+    // corresponding session key to simulate key compromise
+    role C {
+        const ni,nr: Nonce;
+        const kir: SessionKey;
+        var I,R: Agent;
+
+        read_C1(C,C,    I,R);
+        send_C2(C,C,    (I,ni),
+                        {ni,kir}k(I,R),
+                        {ni}kir,
+                        nr,
+                        kir
+               );
+        claim_C3(C,Empty, (Compromised,kir));
+    }
+}
+
+
 protocol andrewConcrete(I,R)
 {
     

spdl/SPORE/andrew-ban.spdl

@@ -14,6 +14,27 @@
 usertype SessionKey;
 secret k: Function;
 const Fresh: Function;
+const Compromised: Function;
+
+protocol andrewBanSessionKeyCompromise(C)
+{
+    // Read the names of 3 agents and disclose a session between them including
+    // corresponding session key to simulate key compromise
+    role C {
+        const ni,nr,nr2: Nonce;
+        const kir: SessionKey;
+        var I,R: Agent;
+
+        read_C1(C,C,    I,R);
+        send_C2(C,C,    (I,{ni}k(I,R)),
+                        {ni,nr}k(I,R),
+                        {nr}k(I,R),
+                        {kir,nr2,ni}k(I,R),
+                        kir
+               );
+        claim_C3(C,Empty, (Compromised,kir));
+    }
+}
 
 protocol andrewBan(I,R)
 {

spdl/SPORE/andrew-lowe-ban.spdl

@@ -21,6 +21,27 @@
 usertype SessionKey;
 secret k: Function;
 const Fresh: Function;
+const Compromised: Function;
+
+protocol andrewLoweBanSessionKeyCompromise(C)
+{
+    // Read the names of 2 agents and disclose a session between them including
+    // corresponding session key to simulate key compromise
+    role C {
+        const ni,nr: Nonce;
+        const kir: SessionKey;
+        var I,R: Agent;
+
+        read_C1(C,C,    I,R);
+        send_C2(C,C,    (I,ni),
+                        {ni,kir,R}k(I,R),
+                        {ni}kir,
+                        nr,
+                        kir
+               );
+        claim_C3(C,Empty, (Compromised,kir));
+    }
+}
 
 protocol andrewLoweBan(I,R)
 {

spdl/SPORE/andrew.spdl

@@ -13,6 +13,27 @@ usertype SessionKey;
 secret k: Function;
 const succ: Function;
 const Fresh: Function;
+const Compromised: Function;
+
+protocol andrewSessionKeyCompromise(C)
+{
+    // Read the names of 2 agents and disclose a session between them including
+    // corresponding session key to simulate key compromise
+    role C {
+        const ni,nr,nr2: Nonce;
+        const kir: SessionKey;
+        var I,R: Agent;
+
+        read_C1(C,C,    I,R);
+        send_C2(C,C,    (I,{ni}k(I,R)),
+                        {succ(ni),nr}k(I,R),
+                        {succ(nr)}k(I,R),
+                        {kir,nr2}k(I,R),
+                        kir
+               );
+        claim_C3(C,Empty, (Compromised,kir));
+    }
+}
 
 protocol andrew(I,R)
 {

spdl/SPORE/denning-sacco-lowe.spdl

@@ -18,6 +18,29 @@ secret k: Function;
 usertype PseudoFunction;
 const dec: PseudoFunction;
 const Fresh: Function;
+const Compromised: Function;
+
+protocol denningSaccoLoweSessionKeyCompromise(C)
+{
+    // Read the names of 3 agents and disclose a session between them including
+    // corresponding session key to simulate key compromise
+    role C {
+        const Ni,Nr: Nonce;
+        const Kir: SessionKey;
+        const T: TimeStamp;
+        var I,R,S: Agent;
+
+        read_C1(C,C,    I,R,S);
+        send_C2(C,C,    (I,R),
+                        {R,Kir,T,{Kir,I,T}k(R,S)}k(I,S),
+                        {Kir,I,T}k(R,S),
+                        {Nr}Kir,
+                        {{Nr}dec}Kir,
+                        Kir
+               );
+        claim_C3(C,Empty, (Compromised,Kir));
+    }
+}
 
 protocol denningSaccoLowe(I,R,S)
 {

spdl/SPORE/denning-sacco.spdl

@@ -13,6 +13,27 @@ usertype SessionKey;
 usertype TimeStamp;
 secret k: Function;
 const Fresh: Function;
+const Compromised: Function;
+
+protocol denningSaccoSessionKeyCompromise(C)
+{
+    // Read the names of 3 agents and disclose a session between them including
+    // corresponding session key to simulate key compromise
+    role C {
+        const Ni,Nr: Nonce;
+        const Kir: SessionKey;
+        const T: Ticket;
+        var I,R,S: Agent;
+
+        read_C1(C,C,    I,R,S);
+        send_C2(C,C,    (I,R),
+                        {R,Kir,T,{Kir,I,T}k(R,S)}k(I,S),
+                        {Kir,I,T}k(R,S),
+                        Kir
+               );
+        claim_C3(C,Empty, (Compromised,Kir));
+    }
+}
 
 protocol denningSacco(I,R,S)
 {

spdl/SPORE/kaochow-v2.spdl

@@ -8,9 +8,33 @@
 # the protocol using the ARACHNE engine (-a)
 #
 
-usertype Sessionkey;
+usertype SessionKey;
 secret k: Function;
 const Fresh: Function;
+const Compromised: Function;
+
+protocol kaochow2SessionKeyCompromise(C)
+{
+    // Read the names of 3 agents and disclose a session between them including
+    // corresponding session key to simulate key compromise
+    role C {
+        const Ni,Nr: Nonce;
+        const Kir,Kt: SessionKey;
+        var I,R,S: Agent;
+
+        read_C1(C,C,    I,R,S);
+        send_C2(C,C,    (I,R,Ni),
+                        {I,R,Ni,Kir,Kt}k(I,S),
+                        {I,R,Ni,Kir,Kt}k(R,S),
+                        R, Nr,
+                        {Nr,Kir}Kt,
+                        Kir,
+                        Kt
+               );
+        claim_C3(C,Empty, (Compromised,Kir));
+        claim_C4(C,Empty, (Compromised,Kt));
+    }
+}
 
 protocol kaochow2(I,R,S)
 {
@@ -18,7 +42,7 @@ protocol kaochow2(I,R,S)
     {
         const ni: Nonce;
         var nr: Nonce;
-        var kir,kt: Sessionkey;
+        var kir,kt: SessionKey;
 
         send_1 (I,S, I,R,ni);
         read_3 (R,I, R, {I,R,ni,kir,kt}k(I,S), {ni, kir}kt, nr );
@@ -34,7 +58,7 @@ protocol kaochow2(I,R,S)
     {
         var ni: Nonce;
         const nr: Nonce;
-        var kir,kt: Sessionkey;
+        var kir,kt: SessionKey;
         var T: Ticket;
 
         read_2 (S,R, T, { I,R,ni,kir,kt }k(R,S)  ); 
@@ -50,7 +74,7 @@ protocol kaochow2(I,R,S)
     role S
     {
         var ni: Nonce;
-        const kir, kt: Sessionkey;
+        const kir, kt: SessionKey;
 
         read_1 (I,S, I,R,ni);
         send_2 (S,R, {I,R,ni,kir,kt}k(I,S), { I,R,ni,kir,kt }k(R,S)  ); 
@@ -62,7 +86,7 @@ const Alice,Bob,Simon,Eve: Agent;
 untrusted Eve;
 const ne: Nonce;
 const te: Ticket;
-const ke: Sessionkey;
+const ke: SessionKey;
 compromised k(Eve,Eve);
 compromised k(Eve,Alice);
 compromised k(Eve,Bob);

spdl/SPORE/kaochow-v3.spdl

@@ -8,10 +8,37 @@
 # the protocol using the ARACHNE engine (-a)
 #
 
-usertype Sessionkey;
+usertype SessionKey;
 usertype Timestamp;
 secret k: Function;
 const Fresh: Function;
+const Compromised: Function;
+
+protocol kaochow3SessionKeyCompromise(C)
+{
+    // Read the names of 3 agents and disclose a session between them including
+    // corresponding session key to simulate key compromise
+    role C {
+        const Ni,Nr: Nonce;
+        const Kir,Kt: SessionKey;
+        const T2: Timestamp;
+        var I,R,S: Agent;
+
+        read_C1(C,C,    I,R,S);
+        send_C2(C,C,    (I,R,Ni),
+                        {I,R,Ni,Kir,Kt}k(I,S),
+                        {I,R,Ni,Kir,Kt}k(R,S),
+                        {Ni,Kir}Kt,
+                        Nr,
+                        {I,R,T2,Kir}k(R,S),
+                        {Nr,Kir}Kt,
+                        Kir,
+                        Kt
+               );
+        claim_C3(C,Empty, (Compromised,Kir));
+        claim_C4(C,Empty, (Compromised,Kt));
+    }
+}
 
 protocol kaochow3(I,R,S)
 {
@@ -19,11 +46,11 @@ protocol kaochow3(I,R,S)
     {
         const ni: Nonce;
         var nr: Nonce;
-        var kir,kt: Sessionkey;
+        var kir,kt: SessionKey;
         var T2: Ticket;
 
         send_1 (I,S, I,R,ni);
-        read_3 (R,I, R, {I,R,ni,kir,kt}k(I,S), {ni, kir}kt, nr, T2 );
+        read_3 (R,I, {I,R,ni,kir,kt}k(I,S), {ni, kir}kt, nr, T2 );
         send_4 (I,R, {nr,kir}kt, T2 );
 
         claim_I1 (I, Nisynch);
@@ -36,12 +63,12 @@ protocol kaochow3(I,R,S)
     {
         var ni: Nonce;
         const nr: Nonce;
-        var kir,kt: Sessionkey;
+        var kir,kt: SessionKey;
         var T: Ticket;
         const tr: Timestamp;
 
         read_2 (S,R, T, { I,R,ni,kir,kt }k(R,S)  ); 
-        send_3 (R,I, R, T, {ni, kir}kt, nr, {I,R,tr,kir}k(R,S) );
+        send_3 (R,I, T, {ni, kir}kt, nr, {I,R,tr,kir}k(R,S) );
         read_4 (I,R, {nr,kir}kt, {I,R,tr,kir}k(R,S) );
 
         claim_R1 (R, Nisynch);
@@ -53,7 +80,7 @@ protocol kaochow3(I,R,S)
     role S
     {
         var ni: Nonce;
-        const kir, kt: Sessionkey;
+        const kir, kt: SessionKey;
 
         read_1 (I,S, I,R,ni);
         send_2 (S,R, {I,R,ni,kir,kt}k(I,S), { I,R,ni,kir,kt }k(R,S)  ); 
@@ -65,7 +92,7 @@ const Alice,Bob,Simon,Eve: Agent;
 untrusted Eve;
 const ne: Nonce;
 const te: Ticket;
-const ke: Sessionkey;
+const ke: SessionKey;
 compromised k(Eve,Eve);
 compromised k(Eve,Alice);
 compromised k(Eve,Bob);

spdl/SPORE/kaochow.spdl

@@ -8,9 +8,31 @@
 # the protocol using the ARACHNE engine (-a) 
 #
 
-usertype Sessionkey;
+usertype SessionKey;
 secret k: Function;
 const Fresh: Function;
+const Compromised: Function;
+
+protocol kaochowSessionKeyCompromise(C)
+{
+    // Read the names of 3 agents and disclose a session between them including
+    // corresponding session key to simulate key compromise
+    role C {
+        const Ni,Nr: Nonce;
+        const Kir: SessionKey;
+        var I,R,S: Agent;
+
+        read_C1(C,C,    I,R,S);
+        send_C2(C,C,    (I,R,Ni),
+                        {I,R,Ni,Kir}k(I,S),
+                        {I,R,Ni,Kir}k(R,S),
+                        {Ni}Kir, Nr,
+                        {Nr}Kir,
+                        Kir
+               );
+        claim_C3(C,Empty, (Compromised,Kir));
+    }
+}
 
 protocol kaochow(I,R,S)
 {
@@ -18,7 +40,7 @@ protocol kaochow(I,R,S)
     {
         const ni: Nonce;
         var nr: Nonce;
-        var kir: Sessionkey;
+        var kir: SessionKey;
 
         send_1 (I,S, I,R,ni);
         read_3 (R,I, {I,R,ni,kir}k(I,S), {ni}kir, nr );
@@ -34,7 +56,7 @@ protocol kaochow(I,R,S)
     {
         var ni: Nonce;
         const nr: Nonce;
-        var kir: Sessionkey;
+        var kir: SessionKey;
         var T;
 
         read_2 (S,R, T, { I,R,ni,kir }k(R,S) ); 
@@ -50,7 +72,7 @@ protocol kaochow(I,R,S)
     role S
     {
         var ni: Nonce;
-        const kir: Sessionkey;
+        const kir: SessionKey;
 
         read_1 (I,S, I,R,ni);
         send_2 (S,R, {I,R,ni,kir}k(I,S), { I,R,ni,kir }k(R,S)  ); 
@@ -62,7 +84,7 @@ const Alice,Bob,Simon,Eve: Agent;
 untrusted Eve;
 const ne: Nonce;
 const te: Ticket;
-const ke: Sessionkey;
+const ke: SessionKey;
 compromised k(Eve,Eve);
 compromised k(Eve,Alice);
 compromised k(Eve,Bob);

spdl/SPORE/ksl-lowe.spdl

@@ -17,6 +17,7 @@ secret k: Function;
 const a, b, e: Agent;
 const s: Server;
 const Fresh: Function;
+const Compromised: Function;
 
 
 const ne: Nonce;
@@ -24,6 +25,34 @@ const kee: SessionKey;
 untrusted e;
 compromised k(e,s);
 
+protocol kslLoweSessionKeyCompromise(C)
+{
+    // Read the names of 3 agents and disclose a session between them including
+    // corresponding session key to simulate key compromise
+    role C {
+        const Ni,Nr,Nc,Ma,Mb: Nonce;
+        const Kir: SessionKey;
+        const Kbb: TicketKey;
+        const Tr: GeneralizedTimestamp;
+        var I,R,S: Agent;
+
+        read_C1(C,C,    I,R,S);
+        send_C2(C,C,    (Ni,I),
+                        (Ni,I,Nr,R),
+                        {I,Nr,Kir}k(R,S),{Ni,R,Kir}k(I,S),
+                        {Tr,I,Kir}Kbb,Nc,{R,Ni}k(I,R),
+                        {Nc}Kir,
+                        Ma,
+                        Mb,{Ma,R}Kir,
+                        {I,Mb}Kir,
+                        Kir,
+                        Kbb
+               );
+        claim_C3(C,Empty, (Compromised,Kir));
+        claim_C4(C,Empty, (Compromised,Kbb));
+    }
+}
+
 protocol kslLowe(A,B,S)
 {
     role A

spdl/SPORE/ksl.spdl

@@ -15,12 +15,42 @@ secret k: Function;
 const a, b, e: Agent;
 const s: Server;
 const Fresh: Function;
+const Compromised: Function;
 
 const ne: Nonce;
 const kee: SessionKey;
 untrusted e;
 compromised k(e,s);
 
+protocol kslSessionKeyCompromise(C)
+{
+    // Read the names of 3 agents and disclose a session between them including
+    // corresponding session key to simulate key compromise
+    role C {
+        const Ni,Nr,Nc,Ma,Mb: Nonce;
+        const Kir: SessionKey;
+        const Kbb: TicketKey;
+        const Tr: GeneralizedTimestamp;
+        var I,R,S: Agent;
+
+        read_C1(C,C,    I,R,S);
+        send_C2(C,C,    (Ni,I),
+                        (Ni,I,Nr,R),
+                        {Nr,I,Kir}k(R,S),{Ni,R,Kir}k(I,S),
+                        {Tr,I,Kir}Kbb,Nc,{Ni}k(I,R),
+                        {Nc}Kir,
+                        Ma,
+                        Mb,{Ma}Kir,
+                        {Mb}Kir,
+                        Kir,
+                        Kbb
+               );
+        claim_C3(C,Empty, (Compromised,Kir));
+        claim_C4(C,Empty, (Compromised,Kbb));
+    }
+}
+
+
 protocol ksl(A,B,S)
 {
     role A

spdl/SPORE/needham-schroeder-sk-amend.spdl

@@ -20,6 +20,30 @@ const dec,inc: Function;
 inversekeys(dec,inc);
 usertype SessionKey;
 const Fresh: Function;
+const Compromised: Function;
+
+protocol needhamschroederskamendSessionKeyCompromise(C)
+{
+    // Read the names of 3 agents and disclose a session between them including
+    // corresponding session key to simulate key compromise
+    role C {
+        const Ni,Nr: Nonce;
+        const Kir: SessionKey;
+        var I,R,S: Agent;
+
+        read_C1(C,C,    I,R,S);
+        send_C2(C,C,    I,
+                        {I,Nr}k(R,S),
+                        I,R,Ni,{I,Nr}k(R,S),
+                        {Ni,R,Kir,{Kir,Nr,I}k(R,S)}k(I,S),
+                        {Kir,Nr,I}k(R,S),
+                        {Nr}Kir,
+                        {{Nr}dec}Kir,
+                        Kir
+               );
+        claim_C3(C,Empty, (Compromised,Kir));
+    }
+}
 
 protocol needhamschroederskamend(I,R,S)
 {

spdl/SPORE/needham-schroeder-sk.spdl

@@ -16,6 +16,28 @@ const dec,inc: Function;
 inversekeys(dec,inc);
 usertype SessionKey;
 const Fresh: Function;
+const Compromised: Function;
+
+protocol needhamschroederSessionKeyCompromise(C)
+{
+    // Read the names of 3 agents and disclose a session between them including
+    // corresponding session key to simulate key compromise
+    role C {
+        const Ni,Nr: Nonce;
+        const Kir: SessionKey;
+        var I,R,S: Agent;
+
+        read_C1(C,C,    I,R,S);
+        send_C2(C,C,    (I,R,Ni),
+                        {Ni,R,Kir,{Kir,I}k(R,S)}k(I,S),
+                        {Kir,I}k(R,S),
+                        {Nr}Kir,
+                        {{Nr}dec}Kir,
+                        Kir
+               );
+        claim_C3(C,Empty, (Compromised,Kir));
+    }
+}
 
 protocol needhamschroedersk(I,R,S)
 {

spdl/SPORE/neumannstub-hwang.spdl

@@ -18,12 +18,38 @@ secret k: Function;
 const a, b, e: Agent;
 const s: Server;
 const Fresh: Function;
+const Compromised: Function;
 
 const ne: Nonce;
 const kee: SessionKey;
 untrusted e;
 compromised k(e,s);
 
+protocol neustubHwangSessionKeyCompromise(C)
+{
+    // Read the names of 3 agents and disclose a session between them including
+    // corresponding session key to simulate key compromise
+    role C {
+        const Ni,Nr,Mi,Mr: Nonce;
+        const Kir: SessionKey;
+        const Tr: TimeStamp;
+        var I,R,S: Agent;
+
+        read_C1(C,C,    I,R,S);
+        send_C2(C,C,    I,Ni,
+                        R,{I,Ni,Tr,Nr}k(R,S),
+                        {R,Ni,Kir,Tr}k(I,S),
+                        {I,Kir,Tr}k(R,S), Nr,
+                        {Nr}Kir,
+                        Mi,{I,Kir,Tr}k(R,S),
+                        Mr,{Mr}Kir,
+                        {Mr}Kir,
+                        Kir
+               );
+        claim_C3(C,Empty, (Compromised,Kir));
+    }
+}
+
 protocol neustubHwang(I,R,S)
 {
     role I

spdl/SPORE/neumannstub.spdl

@@ -15,12 +15,38 @@ secret k: Function;
 const a, b, e: Agent;
 const s: Server;
 const Fresh: Function;
+const Compromised: Function;
 
 const ne: Nonce;
 const kee: SessionKey;
 untrusted e;
 compromised k(e,s);
 
+protocol neustubSessionKeyCompromise(C)
+{
+    // Read the names of 3 agents and disclose a session between them including
+    // corresponding session key to simulate key compromise
+    role C {
+        const Ni,Nr,Mi,Mr: Nonce;
+        const Kir: SessionKey;
+        const Tr: TimeStamp;
+        var I,R,S: Agent;
+
+        read_C1(C,C,    I,R,S);
+        send_C2(C,C,    I,Ni,
+                        R,{I,Ni,Tr}k(R,S),Nr,
+                        {R,Ni,Kir,Tr}k(I,S),
+                        {I,Kir,Tr}k(R,S), Nr,
+                        {Nr}Kir,
+                        Mi,{I,Kir,Tr}k(R,S),
+                        Mr,{Mi}Kir,
+                        {Mr}Kir,
+                        Kir
+               );
+        claim_C3(C,Empty, (Compromised,Kir));
+    }
+}
+
 protocol neustub(I,R,S)
 {
     role I

spdl/SPORE/otwayrees.spdl

@@ -12,9 +12,30 @@
 
 secret const k : Function;
 const Fresh: Function;
+const Compromised: Function;
 
 usertype String,SessionKey;
 
+protocol otwayReesSessionKeyCompromise(C)
+{
+    // Read the names of 3 agents and disclose a session between them including
+    // corresponding session key to simulate key compromise
+    role C {
+        const Ni,Nr: Nonce;
+        const M: String;
+        const Kir: SessionKey;
+        var I,R,S: Agent;
+
+        read_C1(C,C,    I,R,S);
+        send_C2(C,C,    M,I,R,{Ni,M,I,R}k(I,S),
+                        {Nr,M,I,R}k(R,S),
+                        {Ni,Kir}k(I,S), {Nr,Kir}k(R,S),
+                        Kir
+               );
+        claim_C3(C,Empty, (Compromised,Kir));
+    }
+}
+
 protocol otwayrees(I,R,S)
 {
     role I

spdl/SPORE/tmn.spdl

@@ -13,6 +13,26 @@ const pk: Function;
 secret sk: Function;
 inversekeys(pk,sk);
 const Fresh: Function;
+const Compromised: Function;
+
+protocol tmnSessionKeyCompromise(C)
+{
+    // Read the names of 3 agents and disclose a session between them including
+    // corresponding session key to simulate key compromise
+    role C {
+        const Ni,Nr: Nonce;
+        const Kr,Ki: Key;
+        var I,R,S: Agent;
+
+        read_C1(C,C,    I,R,S);
+        send_C2(C,C,    R,{Ki}pk(S),
+                        I, {Kr}pk(S),
+                        {Kr}Ki,
+                        Kr
+               );
+        claim_C3(C,Empty, (Compromised,Kr));
+    }
+}
 
 protocol tmn(I,R,S)
 {

spdl/SPORE/wmf-lowe.spdl

@@ -14,9 +14,31 @@ usertype TimeStamp;
 const succ,pred: Function;
 inversekeys (succ,pred);
 const Fresh: Function;
+const Compromised: Function;
 
 secret k: Function;
 
+protocol wmfLoweSessionKeyCompromise(C)
+{
+    // Read the names of 3 agents and disclose a session between them including
+    // corresponding session key to simulate key compromise
+    role C {
+        const Ni,Nr: Nonce;
+        const Kir: Key;
+        const Ti,Ts: TimeStamp;
+        var I,R,S: Agent;
+
+        read_C1(C,C,    I,R,S);
+        send_C2(C,C,    I, {Ti,R,Kir}k(I,S),
+                        {Ts,I,Kir}k(R,S),
+                        {Nr}k(I,S),
+                        {{Nr}succ}k(I,S),
+                        Kir
+               );
+        claim_C3(C,Empty, (Compromised,Kir));
+    }
+}
+
 protocol wmfLowe(I,R,S)
 {
     role I

spdl/SPORE/wmf.spdl

@@ -9,6 +9,26 @@ usertype TimeStamp;
 
 secret k: Function;
 const Fresh: Function;
+const Compromised: Function;
+
+protocol wmfSessionKeyCompromise(C)
+{
+    // Read the names of 3 agents and disclose a session between them including
+    // corresponding session key to simulate key compromise
+    role C {
+        const Ni,Nr: Nonce;
+        const Kir: Key;
+        const Ti,Ts: TimeStamp;
+        var I,R,S: Agent;
+
+        read_C1(C,C,    I,R,S);
+        send_C2(C,C,    I, {Ti,R,Kir}k(I,S),
+                        {Ts,I,Kir}k(R,S),
+                        Kir
+               );
+        claim_C3(C,Empty, (Compromised,Kir));
+    }
+}
 
 protocol wmf(I,R,S)
 {

spdl/SPORE/woo-lam.spdl

@@ -13,6 +13,31 @@ usertype Key;
 
 secret k: Function;
 const Fresh: Function;
+const Compromised: Function;
+
+protocol woolamSessionKeyCompromise(C)
+{
+    // Read the names of 3 agents and disclose a session between them including
+    // corresponding session key to simulate key compromise
+    role C {
+        const N1,N2: Nonce;
+        const Kir: Key;
+        var I,R,S: Agent;
+
+        read_C1(C,C,    I,R,S);
+        send_C2(C,C,    I,N1,
+                        R,N2,
+                        {I,R,N1,N2}k(I,S),
+                        {I,R,N1,N2}k(R,S),
+                        {R,N1,N2,Kir}k(I,S),
+                        {I,N1,N2,Kir}k(R,S),
+                        {N1,N2}Kir,
+                        {N2}Kir,
+                        Kir
+               );
+        claim_C3(C,Empty, (Compromised,Kir));
+    }
+}
 
 protocol woolam(I,R,S)
 {

spdl/SPORE/yahalom-ban.spdl

@@ -12,6 +12,29 @@ secret k : Function;
 
 usertype Key;
 const Fresh: Function;
+const Compromised: Function;
+
+protocol yahalomBANSessionKeyCompromise(C)
+{
+    // Read the names of 3 agents and disclose a session between them including
+    // corresponding session key to simulate key compromise
+    role C {
+        const Ni,Nr: Nonce;
+        const Kir: Key;
+        var I,R,S: Agent;
+
+        read_C1(C,C,    I,R,S);
+        send_C2(C,C,    I,Ni,
+                        R,Nr,{I,Ni}k(R,S),
+                        Nr,{R,Kir,Ni}k(I,S),
+                        {I,Kir,Nr}k(R,S),
+                        {Nr}Kir,
+                        Kir
+               );
+        claim_C3(C,Empty, (Compromised,Kir));
+    }
+}
+
 
 
 protocol yahalomBAN(I,R,S)

spdl/SPORE/yahalom-paulson.spdl

@@ -10,9 +10,31 @@
 
 secret k : Function;
 const Fresh: Function;
+const Compromised: Function;
 
 usertype Key;
 
+protocol yahalomPaulsonSessionKeyCompromise(C)
+{
+    // Read the names of 3 agents and disclose a session between them including
+    // corresponding session key to simulate key compromise
+    role C {
+        const Ni,Nr: Nonce;
+        const Kir: Key;
+        var I,R,S: Agent;
+
+        read_C1(C,C,    I,R,S);
+        send_C2(C,C,    I,Ni,
+                        R,Nr,{I,Ni}k(R,S),
+                        Nr,{R,Kir,Ni}k(I,S),
+                        {I,R,Kir,Nr}k(R,S),
+                        {Nr}Kir,
+                        Kir
+               );
+        claim_C3(C,Empty, (Compromised,Kir));
+    }
+}
+
 
 protocol yahalomPaulson(I,R,S)
 {

spdl/SPORE/yahalom.spdl

@@ -12,6 +12,28 @@ secret k : Function;
 
 usertype Key;
 const Fresh: Function;
+const Compromised: Function;
+
+protocol yahalomSessionKeyCompromise(C)
+{
+    // Read the names of 3 agents and disclose a session between them including
+    // corresponding session key to simulate key compromise
+    role C {
+        const Ni,Nr: Nonce;
+        const Kir: Key;
+        var I,R,S: Agent;
+
+        read_C1(C,C,    I,R,S);
+        send_C2(C,C,    I,Ni,
+                        R,{I,Ni,Nr}k(R,S),
+                        {R,Kir,Ni,Nr}k(I,S),
+                        {I,Kir}k(R,S),
+                        {Nr}Kir,
+                        Kir
+               );
+        claim_C3(C,Empty, (Compromised,Kir));
+    }
+}
 
 
 protocol yahalom(I,R,S)