scyther/spdl/bke-broken.spdl
2004-03-21 16:26:31 +00:00

62 lines
1.3 KiB
Plaintext

/*
Bilateral Key Exchange with Public Key protocol (BKEPK)
CMV version with explicit secrecy claims.
*/
usertype Key;
const pk,hash: Function;
secret sk,unhash: Function;
inversekeys (pk,sk);
inversekeys (hash,unhash);
protocol bkepk(Initiator,Responder)
{
role Initiator
{
const NI: Nonce;
var NR: Nonce;
var kab: Key;
send_1 (Initiator,Responder, { NI,Responder }pk(Responder) );
read_2 (Responder,Initiator, { hash(NI),NR,Responder,kab }pk(Initiator) );
send_3 (Initiator,Responder, { hash(NR) }kab );
claim_4 (Initiator, Secret, kab );
}
role Responder
{
var NI: Nonce;
const NR: Nonce;
const kab: Key;
read_1 (Initiator,Responder, { NI,Responder }pk(Responder) );
send_2 (Responder,Initiator, { hash(NI),NR,Responder,kab }pk(Initiator) );
read_3 (Initiator,Responder, { hash(NR) }kab );
claim_5 (Responder, Secret, kab );
}
}
const Alice,Bob,Eve: Agent;
untrusted Eve;
compromised sk(Eve);
const ne: Nonce;
run bkepk.Initiator(Alice,Agent);
run bkepk.Responder(Agent,Bob);
run bkepk.Initiator(Alice,Agent);
run bkepk.Responder(Agent,Bob);
run bkepk.Initiator(Alice,Agent);
run bkepk.Responder(Agent,Bob);
run bkepk.Initiator(Alice,Agent);
run bkepk.Responder(Agent,Bob);
run bkepk.Initiator(Alice,Agent);
run bkepk.Responder(Agent,Bob);