andr3/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

- Testing to see what the gains are of using one regular agent. Turns

Browse Source 
out to be half of the states, thus twice as fast.
This commit is contained in:
ccremers 2004-09-07 10:20:20 +00:00
parent be366afa0e
commit f771d3ef4c
1 changed files with 58 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

58
spdl/bke-one.spdl Normal file
View 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,e: Agent;
untrusted e;
compromised sk(e);
const ne: Nonce;
run bkepk.I(a,Agent);
run bkepk.R(Agent,a);
run bkepk.I(a,Agent);
run bkepk.R(Agent,a);
run bkepk.I(a,Agent);
run bkepk.R(Agent,a);
run bkepk.I(a,Agent);
run bkepk.R(Agent,a);
run bkepk.I(a,Agent);
run bkepk.R(Agent,a);