Moved key-compromise models into their own directory and removed key-compromise models from base protocols.

gui/Protocols/README.txt

@@ -0,0 +1,6 @@
+The protocols here are modeled according to their description in the
+SPORE library.
+
+In the 'key-compromise' directory one can find the same protocols, but
+modified to model the compromise of earlier sessions and the leakage of
+the corresponding local values.

gui/Protocols/andrew-ban-concrete.spdl

@@ -33,27 +33,6 @@ protocol @swapkey(X)
     }
 }
 
-protocol andrew-Concrete^KeyCompromise(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 andrew-Concrete(I,R)
 {
     

gui/Protocols/andrew-ban.spdl

@@ -16,26 +16,6 @@ secret k: Function;
 const Fresh: Function;
 const Compromised: Function;
 
-protocol andrew-Ban^KeyCompromise(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 andrew-Ban(I,R)
 {
     role I

gui/Protocols/andrew-lowe-ban.spdl

@@ -23,26 +23,6 @@ secret k: Function;
 const Fresh: Function;
 const Compromised: Function;
 
-protocol andrew-LoweBan^KeyCompromise(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 andrew-LoweBan(I,R)
 {
     role I

gui/Protocols/andrew.spdl

@@ -15,26 +15,6 @@ const succ: Function;
 const Fresh: Function;
 const Compromised: Function;
 
-protocol andrew^KeyCompromise(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)
 {
     role I

gui/Protocols/denning-sacco-lowe.spdl

@@ -17,28 +17,6 @@ const dec: PseudoFunction;
 const Fresh: Function;
 const Compromised: Function;
 
-protocol denningSacco-Lowe^KeyCompromise(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: ExpiredTimeStamp;
-        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 denningSacco-Lowe(I,R,S)
 {
     role I

gui/Protocols/denning-sacco.spdl

@@ -12,26 +12,6 @@ secret k: Function;
 const Fresh: Function;
 const Compromised: Function;
 
-protocol denningSacco^KeyCompromise(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: ExpiredTimeStamp;
-        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)
 {
     role I

gui/Protocols/kaochow-v2.spdl

@@ -9,29 +9,6 @@ secret k: Function;
 const Fresh: Function;
 const Compromised: Function;
 
-protocol kaochow-2^KeyCompromise(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 kaochow-2(I,R,S)
 {
     role I

gui/Protocols/kaochow-v3.spdl

@@ -11,32 +11,6 @@ secret k: Function;
 const Fresh: Function;
 const Compromised: Function;
 
-protocol kaochow-3^KeyCompromise(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: ExpiredTimeStamp;
-        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 kaochow-3(I,R,S)
 {
     role I

gui/Protocols/kaochow.spdl

@@ -9,27 +9,6 @@ secret k: Function;
 const Fresh: Function;
 const Compromised: Function;
 
-protocol kaochow^KeyCompromise(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)
 {
     role I

gui/Protocols/ksl-lowe.spdl

@@ -22,34 +22,6 @@ const kee: SessionKey;
 untrusted e;
 compromised k(e,s);
 
-protocol ksl-Lowe^KeyCompromise(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: ExpiredTimeStamp;
-        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 ksl-Lowe(I,R,S)
 {
     role I

gui/Protocols/needham-schroeder-sk-amend.spdl

@@ -18,29 +18,6 @@ usertype SessionKey;
 const Fresh: Function;
 const Compromised: Function;
 
-protocol needhamschroedersk-amend^KeyCompromise(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 needhamschroedersk-amend(I,R,S)
 {
     role I

gui/Protocols/needham-schroeder-sk.spdl

@@ -14,27 +14,6 @@ usertype SessionKey;
 const Fresh: Function;
 const Compromised: Function;
 
-protocol needhamschroedersk^KeyCompromise(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)
 {
     role I

gui/Protocols/neumannstub-hwang.spdl

@@ -22,31 +22,6 @@ const kee: SessionKey;
 untrusted e;
 compromised k(e,s);
 
-protocol neustub-Hwang^KeyCompromise(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: ExpiredTimeStamp;
-        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,{Mi}Kir,
-                        {Mr}Kir,
-                        Kir
-               );
-        claim_C3(C,Empty, (Compromised,Kir));
-    }
-}
-
 protocol neustub-Hwang(I,R,S)
 {
     role I

gui/Protocols/neumannstub-keycompromise.spdl

@@ -21,31 +21,6 @@ const kee: SessionKey;
 untrusted Eve;
 compromised k(Eve,Simon);
 
-protocol neustub^KeyCompromise(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: ExpiredTimeStamp;
-        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^Repeat(I,R,S)
 {
     const Kir: SessionKey;

gui/Protocols/otwayrees.spdl

@@ -11,26 +11,6 @@ const Compromised: Function;
 
 usertype String,SessionKey;
 
-protocol otwayRees^KeyCompromise(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

gui/Protocols/tmn.spdl

@@ -14,25 +14,6 @@ inversekeys(pk,sk);
 const Fresh: Function;
 const Compromised: Function;
 
-protocol tmn^KeyCompromise(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: SessionKey;
-        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)
 {
     role I

gui/Protocols/wmf-lowe.spdl

@@ -19,27 +19,6 @@ const Compromised: Function;
 
 secret k: Function;
 
-protocol wmf-Lowe^KeyCompromise(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 Ti,Ts: ExpiredTimeStamp;
-        var I,R,S: Agent;
-
-        read_!C1(C,C,    I,R,S);
-        send_!C2(C,C,    I, {I,Ti,R,Kir}k(I,S),
-                        {S,Ts,I,Kir}k(R,S),
-                        {R,Nr}Kir,
-                        {I,{Nr}succ}Kir,
-                        Kir
-               );
-        claim_C3(C,Empty, (Compromised,Kir));
-    }
-}
-
 protocol wmf-Lowe(I,R,S)
 {
     role I

gui/Protocols/wmf.spdl

@@ -16,25 +16,6 @@ secret k: Function;
 const Fresh: Function;
 const Compromised: Function;
 
-protocol wmf^KeyCompromise(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 Ti,Ts: ExpiredTimeStamp;
-        var I,R,S: Agent;
-
-        read_!C1(C,C,    I,R,S);
-        send_!C2(C,C,    I, {I,Ti,R,Kir}k(I,S),
-                        {S,Ts,I,Kir}k(R,S),
-                        Kir
-               );
-        claim_C3(C,Empty, (Compromised,Kir));
-    }
-}
-
 protocol wmf(I,R,S)
 {
     role I

gui/Protocols/woo-lam.spdl

@@ -11,30 +11,6 @@ secret k: Function;
 const Fresh: Function;
 const Compromised: Function;
 
-protocol woolam^KeyCompromise(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: SessionKey;
-        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)
 {
     role I

gui/Protocols/yahalom-ban.spdl

@@ -10,29 +10,6 @@ usertype SessionKey;
 const Fresh: Function;
 const Compromised: Function;
 
-protocol yahalom-BAN^KeyCompromise(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,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 yahalom-BAN(I,R,S)
 {
     role I

gui/Protocols/yahalom-paulson.spdl

@@ -11,28 +11,6 @@ const Compromised: Function;
 
 usertype SessionKey;
 
-//protocol yahalom-Paulson^KeyCompromise(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,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 yahalom-Paulson(I,R,S)
 {
     role I