- Cleanup.
This commit is contained in:
parent
5edfc1ba46
commit
96ade10f29
@ -1,62 +0,0 @@
|
||||
/*
|
||||
Bilateral Key Exchange with Public Key protocol (BKEPK)
|
||||
*/
|
||||
|
||||
usertype Key;
|
||||
|
||||
const pk,hash: Function;
|
||||
secret sk,unhash: Function;
|
||||
|
||||
inversekeys (pk,sk);
|
||||
inversekeys (hash,unhash);
|
||||
|
||||
protocol bkepk(I,R)
|
||||
{
|
||||
role I
|
||||
{
|
||||
const ni: Nonce;
|
||||
var nr: Nonce;
|
||||
var kir: Key;
|
||||
|
||||
send_1 (I,R, { ni,I }pk(R) );
|
||||
read_2 (R,I, { hash(ni),nr,R,kir }pk(I) );
|
||||
send_3 (I,R, { hash(nr) }kir );
|
||||
claim_4 (I, Secret, kir );
|
||||
claim_6 (I, Nisynch );
|
||||
claim_8 (I, Niagree );
|
||||
}
|
||||
|
||||
role R
|
||||
{
|
||||
var ni: Nonce;
|
||||
const nr: Nonce;
|
||||
const kir: Key;
|
||||
|
||||
read_1 (I,R, { ni,I }pk(R) );
|
||||
send_2 (R,I, { hash(ni),nr,R,kir }pk(I) );
|
||||
read_3 (I,R, { hash(nr) }kir );
|
||||
claim_5 (R, Secret, kir );
|
||||
claim_7 (R, Nisynch );
|
||||
claim_9 (R, Niagree );
|
||||
}
|
||||
}
|
||||
|
||||
const a,b,e: Agent;
|
||||
|
||||
untrusted e;
|
||||
compromised sk(e);
|
||||
const ne: Nonce;
|
||||
|
||||
run bkepk.I(a,Agent);
|
||||
run bkepk.R(Agent,b);
|
||||
run bkepk.I(a,Agent);
|
||||
run bkepk.R(Agent,b);
|
||||
|
||||
run bkepk.I(a,Agent);
|
||||
run bkepk.R(Agent,b);
|
||||
run bkepk.I(a,Agent);
|
||||
run bkepk.R(Agent,b);
|
||||
|
||||
run bkepk.I(a,Agent);
|
||||
run bkepk.R(Agent,b);
|
||||
|
Loading…
Reference in New Issue
Block a user