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

- Better text.

Browse Source 
- Added four-party version.
This commit is contained in:
ccremers 2005-07-01 09:32:53 +00:00
parent 0cf19b98a3
commit 342d968895
2 changed files with 113 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
spdl/bunava-1-3.spdl
View File

@ -25,7 +25,7 @@ protocol intruderhelp(Swap)
} }
} }
protocol bunava1(A,B,C) protocol bunava13(A,B,C)
{ {
role A role A
{ {
@ -81,9 +81,9 @@ compromised k(Eve,Charlie);
# General scenario, 2 parallel runs of the protocol # General scenario, 2 parallel runs of the protocol
run bunava1.A(Agent,Agent,Agent); run bunava13.A(Agent,Agent,Agent);
run bunava1.B(Agent,Agent,Agent); run bunava13.B(Agent,Agent,Agent);
run bunava1.C(Agent,Agent,Agent); run bunava13.C(Agent,Agent,Agent);
run bunava1.A(Agent,Agent,Agent); run bunava13.A(Agent,Agent,Agent);
run bunava1.B(Agent,Agent,Agent); run bunava13.B(Agent,Agent,Agent);
run bunava1.C(Agent,Agent,Agent); run bunava13.C(Agent,Agent,Agent);

106
spdl/bunava-1-4.spdl Normal file
View File

@ -0,0 +1,106 @@
# Buttyan Nagy Vajda protocol 1 (4-party)
#
# Modelled after the description in the paper
# "Efficient multi-party challenge-response protocols for entity
# authentication"
#
# Attacks:
# Does not satisfy ni-agree, because when Alice in the A role terminates
# it cannot be sure that the agent in role B is aware of having sent a
# reply for Alice.
# A type flaw attack exists in which there are only three agents active.
# Especially -m2 attack 17 is nice, I think.
#
secret k: Function;
protocol intruderhelp(Swap)
{
role Swap
{
var T: Ticket;
var A,B: Agent;
read_1(Swap,Swap, { T }k(A,B) );
send_2(Swap,Swap, { T }k(B,A) );
}
}
protocol bunava14(A,B,C,D)
{
role A
{
const ra: Nonce;
var rb,rc,rd: Nonce;
send_1(A,B, ra);
read_4(D,A, rd,{D,rc,C,rb,B,ra}k(A,D) );
send_5(A,B, {A,rd,D,rc,C,rb}k(A,B) );
claim_A1(A, Niagree);
claim_A2(A, Nisynch);
}
role B
{
const rb: Nonce;
var ra,rc,rd: Nonce;
read_1(A,B, ra);
send_2(B,C, rb,{B,ra}k(B,C) );
read_5(A,B, {A,rd,D,rc,C,rb}k(A,B) );
send_6(B,C, {B,A,rd,D,rc}k(B,C) );
claim_B1(B, Niagree);
claim_B2(B, Nisynch);
}
role C
{
const rc: Nonce;
var ra,rb,rd: Nonce;
read_2(B,C, rb,{B,ra}k(B,C) );
send_3(C,D, rc,{C,rb,B,ra}k(C,D) );
read_6(B,C, {B,A,rd,D,rc}k(B,C) );
send_7(C,D, {C,B,A,rd}k(C,D) );
claim_C1(C, Niagree);
claim_C2(C, Nisynch);
}
role D
{
const rd: Nonce;
var ra,rb,rc: Nonce;
read_3(C,D, rc,{C,rb,B,ra}k(C,D) );
send_4(D,A, rd,{D,rc,C,rb,B,ra}k(A,D) );
read_7(C,D, {C,B,A,rd}k(C,D) );
claim_D1(D, Niagree);
claim_D2(D, Nisynch);
}
}
const Alice,Bob,Charlie,Eve: Agent;
untrusted Eve;
const ne: Nonce;
compromised k(Alice,Eve);
compromised k(Bob,Eve);
compromised k(Charlie,Eve);
compromised k(Eve,Alice);
compromised k(Eve,Bob);
compromised k(Eve,Charlie);
# General scenario, 2 parallel runs of the protocol
run bunava14.A(Agent,Agent,Agent,Agent);
run bunava14.B(Agent,Agent,Agent,Agent);
run bunava14.C(Agent,Agent,Agent,Agent);
run bunava14.D(Agent,Agent,Agent,Agent);
run bunava14.A(Agent,Agent,Agent,Agent);
run bunava14.B(Agent,Agent,Agent,Agent);
run bunava14.C(Agent,Agent,Agent,Agent);
run bunava14.D(Agent,Agent,Agent,Agent);