scyther/spdl/bke-generalized-4.spdl
2005-05-24 14:31:55 +00:00

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);