scyther/gui/Protocols/MultiProtocolAttacks/yahalom-ban-paulson-modified.spdl

50 lines
915 B
Plaintext

// BAN modified version of the yahalom protocol
//
// Modeled as version in Paulson's paper:
// "Relations Between Secrets: Two Formal Analyses of the Yahalom
// Protocol"
//
// Modified (improved) version from page 16.
usertype Server;
usertype SessionKey;
protocol yahalom-BAN-Paulson-modified(A,B,S)
{
role A
{
fresh na: Nonce;
var nb: Nonce;
var ticket: Ticket;
var kab: SessionKey;
send_1(A,B, A,na);
read_3(S,A, nb, {B,kab,na}k(A,S), ticket );
send_4(A,B, ticket, {nb}kab );
claim_5(A, Secret,kab);
}
role B
{
fresh nb: Nonce;
var na: Nonce;
var ticket: Ticket;
var kab: SessionKey;
read_1(A,B, A,na);
send_2(B,S, B, nb, {A,na}k(B,S) );
read_4(A,B, {A,B,kab,nb}k(B,S) , {nb}kab );
claim_6(B, Secret,kab);
}
role S
{
fresh kab: SessionKey;
var na,nb: Nonce;
read_2(B,S, B, nb, {A,na}k(B,S) );
send_3(S,A, nb, {B,kab,na}k(A,S), {A,B,kab,nb}k(B,S) );
}
}