90 lines
1.7 KiB
Plaintext
90 lines
1.7 KiB
Plaintext
# 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;
|
|
|
|
recv_!1(Swap,Swap, { T }k(A,B) );
|
|
send_!2(Swap,Swap, { T }k(B,A) );
|
|
}
|
|
}
|
|
|
|
protocol bunava14(A,B,C,D)
|
|
{
|
|
role A
|
|
{
|
|
fresh ra: Nonce;
|
|
var rb,rc,rd: Nonce;
|
|
|
|
send_1(A,B, ra);
|
|
recv_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
|
|
{
|
|
fresh rb: Nonce;
|
|
var ra,rc,rd: Nonce;
|
|
|
|
recv_1(A,B, ra);
|
|
send_2(B,C, rb,{B,ra}k(B,C) );
|
|
recv_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
|
|
{
|
|
fresh rc: Nonce;
|
|
var ra,rb,rd: Nonce;
|
|
|
|
recv_2(B,C, rb,{B,ra}k(B,C) );
|
|
send_3(C,D, rc,{C,rb,B,ra}k(C,D) );
|
|
recv_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
|
|
{
|
|
fresh rd: Nonce;
|
|
var ra,rb,rc: Nonce;
|
|
|
|
recv_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) );
|
|
recv_7(C,D, {C,B,A,rd}k(C,D) );
|
|
|
|
claim_D1(D, Niagree);
|
|
claim_D2(D, Nisynch);
|
|
}
|
|
}
|
|
|
|
|
|
|
|
# General scenario, 2 parallel runs of the protocol
|
|
|