- Added BKE versions used in secrecy reduction article.
This commit is contained in:
parent
8dee89217e
commit
33441613e4
@ -1,61 +1,48 @@
|
||||
/*
|
||||
Bilateral Key Exchange with Public Key protocol (BKEPK)
|
||||
|
||||
CMV version with explicit secrecy claims.
|
||||
Broken version with man in the middle attack.
|
||||
*/
|
||||
|
||||
usertype Key;
|
||||
|
||||
const pk,hash: Function;
|
||||
secret sk,unhash: Function;
|
||||
const PK,h: Function;
|
||||
secret SK,hinv: Function;
|
||||
|
||||
inversekeys (pk,sk);
|
||||
inversekeys (hash,unhash);
|
||||
inversekeys (PK,SK);
|
||||
inversekeys (h,hinv);
|
||||
|
||||
protocol bkepk(Initiator,Responder)
|
||||
protocol bkepk(I,R)
|
||||
{
|
||||
role Initiator
|
||||
role I
|
||||
{
|
||||
const NI: Nonce;
|
||||
var NR: Nonce;
|
||||
var kab: Key;
|
||||
const ni: Nonce;
|
||||
var nr: Nonce;
|
||||
var kir: 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 );
|
||||
send_1 (I,R, { ni,I }PK(R) );
|
||||
read_2 (R,I, { h(ni),nr,kir }PK(I) );
|
||||
send_3 (I,R, { h(nr),kir }PK(R) );
|
||||
claim_4 (I, Secret, kir );
|
||||
}
|
||||
|
||||
role Responder
|
||||
role R
|
||||
{
|
||||
var NI: Nonce;
|
||||
const NR: Nonce;
|
||||
const kab: Key;
|
||||
var ni: Nonce;
|
||||
const nr: Nonce;
|
||||
const kir: 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 );
|
||||
read_1 (I,R, { ni,I }PK(R) );
|
||||
send_2 (R,I, { h(ni),nr,kir }PK(I) );
|
||||
read_3 (I,R, { h(nr),kir }PK(R) );
|
||||
claim_5 (R, Secret, kir );
|
||||
}
|
||||
}
|
||||
|
||||
const Alice,Bob,Eve: Agent;
|
||||
const a,b,e: Agent;
|
||||
|
||||
untrusted Eve;
|
||||
compromised sk(Eve);
|
||||
untrusted e;
|
||||
compromised SK(e);
|
||||
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);
|
||||
|
||||
|
||||
run bkepk.I(a,Agent);
|
||||
run bkepk.R(Agent,b);
|
||||
|
58
spdl/bke.spdl
Normal file
58
spdl/bke.spdl
Normal file
@ -0,0 +1,58 @@
|
||||
/*
|
||||
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 );
|
||||
}
|
||||
|
||||
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 );
|
||||
}
|
||||
}
|
||||
|
||||
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