scyther/testing/kerberos-rddm.spdl

155 lines
2.6 KiB
Plaintext

/*
* Scyther description of Kerberos as in RDDM'07
*
*/
usertype Sessionkey;
usertype Text;
secret ktk: Function;
secret kck: Function;
secret kst: Function;
protocol @swapkey-ktk(I,R)
{
# Protocol added to work around the symmetry problems where k(I,R) != k(R,I)
role I
{
var T:Ticket;
recv_!X1(R,I,{T}ktk(I,R));
send_!X2(I,R,{T}ktk(R,I));
}
role R
{
}
}
protocol @swapkey-kck(I,R)
{
# Protocol added to work around the symmetry problems where k(I,R) != k(R,I)
role I
{
var T:Ticket;
recv_!X1(R,I,{T}kck(I,R));
send_!X2(I,R,{T}kck(R,I));
}
role R
{
}
}
protocol @swapkey-kst(I,R)
{
# Protocol added to work around the symmetry problems where k(I,R) != k(R,I)
role I
{
var T:Ticket;
recv_!X1(R,I,{T}kst(I,R));
send_!X2(I,R,{T}kst(R,I));
}
role R
{
}
}
protocol kerberos(C,K,T,S) {
role C {
fresh n1: Nonce;
fresh n2: Nonce;
var tgt: Ticket;
var st: Ticket;
var AKey: Sessionkey;
var SKey: Sessionkey;
fresh t: Text;
send_1(C,K, C,T,n1);
recv_2(K,C, tgt, { AKey,n1,T }kck(C,K) );
// Stage boundary
send_3(C,T, tgt, { C }AKey,C,S,n2 );
recv_4(T,C, C, st, { SKey, n2, S }AKey );
// Stage boundary
send_5(C,S, st, { C,t }SKey );
recv_6(S,C, { t }SKey );
// Theorem 5 (a)
// If C,K are honest
claim(C,Reachable);
// Theorem 6 (a)
// If C,K,T are all honest
claim(C,Secret,AKey);
// Theorem 7 (a)
// If C,K,S are all honest
claim(C, Reachable);
// Theorem 8
// If C,K,S are all honest
claim(C, Secret, SKey);
}
role K {
var n1: Nonce;
fresh AKey: Sessionkey;
recv_1(C,K, C,T,n1);
send_2(K,C, { AKey, C }ktk(T,K), { AKey,n1,T }kck(C,K) );
// Theorem 6 (a)
// If C,K,T are all honest
claim_K1(K,Secret,AKey);
}
role T {
var AKey: Sessionkey;
var n2: Nonce;
fresh SKey: Sessionkey;
recv_3(C,T, { AKey, C }ktk(T,K), { C }AKey,C,S,n2 );
send_4(T,C, C,{ SKey, C }kst(S,T), { SKey, n2, S }AKey );
// Theorem 5 (a)
// If C,K are honest
claim(T,Reachable);
// Theorem 6 (a)
// If C,K,T are all honest
claim(T,Secret,AKey);
// My own
claim(T,Secret,SKey);
}
role S {
var t: Text;
var SKey: Sessionkey;
recv_5(C,S, { SKey, C }kst(S,T), { C,t }SKey );
send_6(S,C, { t }SKey );
// Theorem 7 (b)
// If C,K,S,T are honest
claim(S, Reachable);
// My own
claim(S, Secret, t);
claim(S, Secret, SKey);
}
}
const Alice,Bob,Charlie,Eve: Agent;
// C untrusted
// K untrusted
// T untrusted
// S untrusted