105 lines
2.0 KiB
Plaintext
105 lines
2.0 KiB
Plaintext
/*
|
|
* Generalized Bilateral Key Exchange protocol.
|
|
* Four-party version.
|
|
*
|
|
* Specific order of interleaving in message 1-4 is required to (a)
|
|
* avoid type flaws whilst (b) retaining BKE structure for the simple
|
|
* case.
|
|
*
|
|
* Cas Cremers
|
|
* Mon May 23 15:15:37 CEST 2005
|
|
*/
|
|
|
|
const zero;
|
|
const pk: Function;
|
|
secret sk: Function;
|
|
inversekeys (pk,sk);
|
|
|
|
protocol bkegen4(R1,R2,R3,R4)
|
|
{
|
|
role R1
|
|
{
|
|
const n1: Nonce;
|
|
var n2,n3,n4: Nonce;
|
|
|
|
send_1(R1,R2, {n1,R1,R3,R4}pk(R2) );
|
|
read_4(R4,R1, {n1,n2,n3,n4,R2,R3,R4}pk(R1) );
|
|
send_5(R1,R2, {n2,n3}n4 );
|
|
|
|
claim_r1a(R1,Secret,n1);
|
|
claim_r1b(R1,Secret,n2);
|
|
claim_r1c(R1,Secret,n3);
|
|
claim_r1d(R1,Secret,n4);
|
|
|
|
claim_r1A(R1,Niagree);
|
|
claim_r1S(R1,Nisynch);
|
|
}
|
|
|
|
role R2
|
|
{
|
|
const n2: Nonce;
|
|
var n1,n3,n4: Nonce;
|
|
|
|
read_1(R1,R2, {n1,R1,R3,R4}pk(R2) );
|
|
send_2(R2,R3, {n1,R1,n2,R2,R4}pk(R3) );
|
|
read_5(R1,R2, {n2,n3}n4 );
|
|
send_6(R2,R3, {n3}n4 );
|
|
|
|
claim_r2a(R2,Secret,n1);
|
|
claim_r2b(R2,Secret,n2);
|
|
claim_r2c(R2,Secret,n3);
|
|
claim_r2d(R2,Secret,n4);
|
|
|
|
claim_r2A(R2,Niagree);
|
|
claim_r2S(R2,Nisynch);
|
|
}
|
|
|
|
role R3
|
|
{
|
|
const n3: Nonce;
|
|
var n1,n2,n4: Nonce;
|
|
|
|
read_2(R2,R3, {n1,R1,n2,R2,R4}pk(R3) );
|
|
send_3(R3,R4, {n1,R1,n2,R2,n3,R3}pk(R4) );
|
|
read_6(R2,R3, {n3}n4 );
|
|
send_7(R3,R4, {zero}n4 );
|
|
|
|
claim_r3a(R3,Secret,n1);
|
|
claim_r3b(R3,Secret,n2);
|
|
claim_r3c(R3,Secret,n3);
|
|
claim_r3d(R3,Secret,n4);
|
|
|
|
claim_r3A(R3,Niagree);
|
|
claim_r3S(R3,Nisynch);
|
|
}
|
|
|
|
role R4
|
|
{
|
|
const n4: Nonce;
|
|
var n1,n2,n3: Nonce;
|
|
|
|
read_3(R3,R4, {n1,R1,n2,R2,n3,R3}pk(R4) );
|
|
send_4(R4,R1, {n1,n2,n3,n4,R2,R3,R4}pk(R1) );
|
|
read_7(R3,R4, {zero}n4 );
|
|
|
|
claim_r4a(R4,Secret,n1);
|
|
claim_r4b(R4,Secret,n2);
|
|
claim_r4c(R4,Secret,n3);
|
|
claim_r4d(R4,Secret,n4);
|
|
|
|
claim_r4A(R4,Niagree);
|
|
claim_r4S(R4,Nisynch);
|
|
}
|
|
}
|
|
|
|
const Alice,Bob,Eve: Agent;
|
|
|
|
untrusted Eve;
|
|
const ne: Nonce;
|
|
compromised sk(Eve);
|
|
|
|
run bkegen4.R1(Agent,Agent,Agent,Agent);
|
|
run bkegen4.R2(Agent,Agent,Agent,Agent);
|
|
run bkegen4.R3(Agent,Agent,Agent,Agent);
|
|
run bkegen4.R4(Agent,Agent,Agent,Agent);
|