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

- Added two (SPORE) splice-AS variants.

Browse Source
This commit is contained in:
ccremers 2004-10-14 14:50:49 +00:00
parent 15ed7a99fa
commit 29445bbd5f
2 changed files with 132 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

66
spdl/splice-as-hc-cj.spdl Normal file
View File

@ -0,0 +1,66 @@
usertype TimeStamp, LifeTime;
const pk: Function;
secret sk: Function;
inversekeys (pk,sk);
protocol spliceAShcCJ(C,AS,S)
{
role C
{
const N1,N2: Nonce;
const T: TimeStamp;
const L: LifeTime;
send_1(C,AS, C, S, N1 );
read_2(AS,C, AS, {AS, C, N1, S, pk(S)}sk(AS) );
send_3(C,S, C, S, {T, L, {C, N2}pk(S)}sk(C) );
read_6(S,C, S, C, {N2}pk(C) );
claim_7(C, Secret, N2);
claim_9(C, Niagree);
claim_10(C, Nisynch);
}
role AS
{
var N1,N3: Nonce;
read_1(C,AS, C, S, N1 );
send_2(AS,C, AS, {AS, C, N1, S, pk(S)}sk(AS) );
read_4(S,AS, S, C, N3 );
send_5(AS,S, AS, {AS, S, N3, C, pk(C)}sk(AS) );
}
role S
{
const N3: Nonce;
var N2: Nonce;
var T: TimeStamp;
var L: LifeTime;
var ni: Nonce;
const nr: Nonce;
read_3(C,S, C, S, {T, L, {C, N2}pk(S)}sk(C) );
send_4(S,AS, S, C, N3 );
read_5(AS,S, AS, {AS, S, N3, C, pk(C)}sk(AS) );
send_6(S,C, S, C, {N2}pk(C) );
claim_8(S, Secret, N2);
claim_11(S, Niagree);
claim_12(S, Nisynch);
}
}
const Al,Bo,Eve: Agent;
untrusted Eve;
const ne: Nonce;
compromised sk(Eve);
run spliceAShcCJ.C(Agent,Agent,Agent);
run spliceAShcCJ.AS(Agent,Agent,Agent);
run spliceAShcCJ.S(Agent,Agent,Agent);

66
spdl/splice-as-hc.spdl Normal file
View File

@ -0,0 +1,66 @@
usertype TimeStamp, LifeTime;
const pk: Function;
secret sk: Function;
inversekeys (pk,sk);
protocol spliceAShc(C,AS,S)
{
role C
{
const N1,N2: Nonce;
const T: TimeStamp;
const L: LifeTime;
send_1(C,AS, C, S, N1 );
read_2(AS,C, AS, {AS, C, N1, S, pk(S)}sk(AS) );
send_3(C,S, C, S, {C, T, L, {N2}pk(S)}sk(C) );
read_6(S,C, S, C, {S, N2}pk(C) );
claim_7(C, Secret, N2);
claim_9(C, Niagree);
claim_10(C, Nisynch);
}
role AS
{
var N1,N3: Nonce;
read_1(C,AS, C, S, N1 );
send_2(AS,C, AS, {AS, C, N1, S, pk(S)}sk(AS) );
read_4(S,AS, S, C, N3 );
send_5(AS,S, AS, {AS, S, N3, C, pk(C)}sk(AS) );
}
role S
{
const N3: Nonce;
var N2: Nonce;
var T: TimeStamp;
var L: LifeTime;
var ni: Nonce;
const nr: Nonce;
read_3(C,S, C, S, {C, T, L, {N2}pk(S)}sk(C) );
send_4(S,AS, S, C, N3 );
read_5(AS,S, AS, {AS, S, N3, C, pk(C)}sk(AS) );
send_6(S,C, S, C, {S, N2}pk(C) );
claim_8(S, Secret, N2);
claim_11(S, Niagree);
claim_12(S, Nisynch);
}
}
const Al,Bo,Eve: Agent;
untrusted Eve;
const ne: Nonce;
compromised sk(Eve);
run spliceAShc.C(Agent,Agent,Agent);
run spliceAShc.AS(Agent,Agent,Agent);
run spliceAShc.S(Agent,Agent,Agent);