diff --git a/spdl/SPORE/denning-sacco.spdl b/spdl/SPORE/denning-sacco.spdl index de96c8a..5aca4cd 100644 --- a/spdl/SPORE/denning-sacco.spdl +++ b/spdl/SPORE/denning-sacco.spdl @@ -22,7 +22,7 @@ protocol denningSaccoSessionKeyCompromise(C) role C { const Ni,Nr: Nonce; const Kir: SessionKey; - const T: Ticket; + const T: TimeStamp; var I,R,S: Agent; read_C1(C,C, I,R,S); diff --git a/spdl/SPORE/kaochow-v2.spdl b/spdl/SPORE/kaochow-v2.spdl index d81823d..1dd4268 100644 --- a/spdl/SPORE/kaochow-v2.spdl +++ b/spdl/SPORE/kaochow-v2.spdl @@ -28,11 +28,11 @@ protocol kaochow2SessionKeyCompromise(C) {I,R,Ni,Kir,Kt}k(R,S), R, Nr, {Nr,Kir}Kt, - Kir, - Kt + Kir + // Kt ); claim_C3(C,Empty, (Compromised,Kir)); - claim_C4(C,Empty, (Compromised,Kt)); + // claim_C4(C,Empty, (Compromised,Kt)); } } diff --git a/spdl/SPORE/kaochow-v3.spdl b/spdl/SPORE/kaochow-v3.spdl index 7fd50b9..640e214 100644 --- a/spdl/SPORE/kaochow-v3.spdl +++ b/spdl/SPORE/kaochow-v3.spdl @@ -32,11 +32,11 @@ protocol kaochow3SessionKeyCompromise(C) Nr, {I,R,T2,Kir}k(R,S), {Nr,Kir}Kt, - Kir, - Kt + Kir + // Kt ); claim_C3(C,Empty, (Compromised,Kir)); - claim_C4(C,Empty, (Compromised,Kt)); + // claim_C4(C,Empty, (Compromised,Kt)); } } diff --git a/spdl/SPORE/ksl.spdl b/spdl/SPORE/ksl.spdl index e15be0b..77b162f 100644 --- a/spdl/SPORE/ksl.spdl +++ b/spdl/SPORE/ksl.spdl @@ -12,15 +12,14 @@ usertype Server, SessionKey, GeneralizedTimestamp, TicketKey; secret k: Function; -const a, b, e: Agent; -const s: Server; +const Alice, Bob, Simon, Eve: Agent; const Fresh: Function; const Compromised: Function; const ne: Nonce; const kee: SessionKey; -untrusted e; -compromised k(e,s); +untrusted Eve; +compromised k(Eve,Simon); protocol kslSessionKeyCompromise(C) { @@ -37,7 +36,7 @@ protocol kslSessionKeyCompromise(C) 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), + {Tr,I,Kir}Kbb,Nc,{Ni}Kir, {Nc}Kir, Ma, Mb,{Ma}Kir, @@ -51,22 +50,22 @@ protocol kslSessionKeyCompromise(C) } -protocol ksl(A,B,S) +protocol ksl(I,R,S) { - role A + role I { - const Na, Ma: Nonce; - var Nc, Mb: Nonce; + const Ni, Mi: Nonce; + var Nr2, Mr: Nonce; var T: Ticket; - var Kab: SessionKey; + var Kir: SessionKey; - send_1(A,B, Na, A); - read_4(B,A, { Na,B,Kab }k(A,S), T, Nc, {Na}Kab ); - send_5(A,B, { Nc }Kab ); + send_1(I,R, Ni, I); + read_4(R,I, {Ni,R,Kir}k(I,S), T, Nr2, {Ni}Kir); + send_5(I,R, {Nr2}Kir ); - send_6(A,B, Ma,T ); - read_7(B,A, Mb,{Ma}Kab ); - send_8(A,B, {Mb}Kab ); + send_6(I,R, Mi,T ); + read_7(R,I, Mr,{Mi}Kir ); + send_8(I,R, {Mr}Kir ); claim_A1(A,Secret, Kab); claim_A2(A,Niagree); @@ -77,8 +76,8 @@ protocol ksl(A,B,S) role B { var Na,Ma: Nonce; - const Nb,Nc,Mb: Nonce; - var Kab: SessionKey; + const Nr,Nr2,Mr: Nonce; + var Kir: SessionKey; const Kbb: TicketKey; const Tb: GeneralizedTimestamp; var T: Ticket; @@ -109,7 +108,7 @@ protocol ksl(A,B,S) } } -run ksl.A(a,b,s); -run ksl.B(a,b,s); -run ksl.S(a,b,s); +run ksl.A(Alice,Bob,Simon); +run ksl.B(Alice,Bob,Simon); +run ksl.S(Alice,Bob,Simon); diff --git a/spdl/SPORE/neumannstub.spdl b/spdl/SPORE/neumannstub.spdl index 997f740..86b92eb 100644 --- a/spdl/SPORE/neumannstub.spdl +++ b/spdl/SPORE/neumannstub.spdl @@ -7,20 +7,23 @@ # This protocol uses a ticket so scyther will only be able to verify # the protocol using the ARACHNE engine (-a) # +# Note: +# In SPORE this protocol is not described correctly, there are in fact 2 +# different protocols (the key establishment protocol and the repeated +# authentication protocol) usertype Server, SessionKey, TimeStamp, TicketKey; secret k: Function; -const a, b, e: Agent; -const s: Server; +const Alice, Bob, Simon, Eve: Agent; const Fresh: Function; const Compromised: Function; const ne: Nonce; const kee: SessionKey; -untrusted e; -compromised k(e,s); +untrusted Eve; +compromised k(Eve,Simon); protocol neustubSessionKeyCompromise(C) { @@ -47,12 +50,52 @@ protocol neustubSessionKeyCompromise(C) } } +protocol neustubRepeat(I,R,S) +{ + const Kir: SessionKey; + + role I + { + const Mi: Nonce; + var Mr: Nonce; + const Kir: SessionKey; + const Tr: TimeStamp; + + send_5(I,R,Mi,{I,Kir,Tr}k(R,S)); + read_6(R,I,Mr,{Mi}Kir); + send_7(I,R,{Mr}Kir); + claim_I1(I,Secret, Kir); + claim_I2(I,Niagree); + claim_I3(I,Nisynch); + claim_I4(I,Empty,(Fresh,Kir)); + } + + role R + { + const Mr: Nonce; + var Tr: TimeStamp; + var Kir: SessionKey; + var Mi: Nonce; + + read_5(I,R,Mi,{I,Kir,Tr}k(R,S)); + send_6(R,I,Mr,{Mi}Kir); + read_7(I,R,{Mr}Kir); + claim_R1(R,Secret, Kir); + claim_R2(R,Niagree); + claim_R3(R,Nisynch); + claim_R4(R,Empty,(Fresh,Kir)); + } + + role S + { + } +} protocol neustub(I,R,S) { role I { - const Ni,Mi: Nonce; - var Nr,Mr: Nonce; + const Ni: Nonce; + var Nr: Nonce; var T: Ticket; var Tb: TimeStamp; var Kir: SessionKey; @@ -60,9 +103,6 @@ protocol neustub(I,R,S) send_1(I,R, I, Ni); read_3(S,I, { R,Ni,Kir,Tb}k(I,S), T, Nr); send_4(I,R,T,{Nr}Kir); - send_5(I,R,Mi,T); - read_6(R,I,Mr,{Mi}Kir); - send_7(I,R,{Mr}Kir); claim_I1(I,Secret, Kir); claim_I2(I,Niagree); @@ -81,9 +121,6 @@ protocol neustub(I,R,S) read_1(I,R, I, Ni); send_2(R,S, R, {I, Ni, Tb}k(R,S),Nr); read_4(I,R,{I,Kir,Tb}k(R,S),{Nr}Kir); - read_5(I,R,Mi,T); - send_6(R,I,Mr,{Mi}Kir); - read_7(I,R,{Mr}Kir); claim_R1(R,Secret, Kir); claim_R2(R,Niagree); @@ -102,7 +139,7 @@ protocol neustub(I,R,S) } } -run neustub.A(a,b,s); -run neustub.B(a,b,s); -run neustub.S(a,b,s); +run neustub.I(Alice,Bob,Simon); +run neustub.R(Alice,Bob,Simon); +run neustub.S(Alice,Bob,Simon);