andr3/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

- Remove some small modelling errors

Browse Source 
- New way to model Neumann Stub (it should be 2 distinct protocols)
This commit is contained in:
gijs 2005-06-27 11:50:24 +00:00
parent 6fb6aa33dd
commit c2b3f6492f
5 changed files with 79 additions and 43 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
spdl/SPORE/denning-sacco.spdl
View File

@ -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);

6
spdl/SPORE/kaochow-v2.spdl
View File

@ -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));
}
}

6
spdl/SPORE/kaochow-v3.spdl
View File

@ -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));
}
}

41
spdl/SPORE/ksl.spdl
View File

@ -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);

67
spdl/SPORE/neumannstub.spdl
View File

@ -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);