139 lines
2.5 KiB
Plaintext
139 lines
2.5 KiB
Plaintext
|
# Buttyan Nagy Vajda protocol 2 (4-party)
|
||
|
|
#
|
||
|
|
# Modelled after the description in the paper
|
||
|
|
# "Efficient multi-party challenge-response protocols for entity
|
||
|
|
# authentication"
|
||
|
|
#
|
||
|
|
# Note:
|
||
|
|
# Does not seem to reach the claim. I don't know why yet. TODO
|
||
|
|
# investigate.
|
||
|
|
#
|
||
|
|
|
||
|
|
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 bunava24(A,B,C,D)
|
||
|
|
{
|
||
|
|
role A
|
||
|
|
{
|
||
|
|
const ra: Nonce;
|
||
|
|
var rb,rc,rd: Nonce;
|
||
|
|
var Tacd, Tabd: Ticket;
|
||
|
|
|
||
|
|
send_1(A,B, ra);
|
||
|
|
read_4(D,A, rd,
|
||
|
|
Tacd,
|
||
|
|
Tabd,
|
||
|
|
{ D, { C, { B,ra }k(A,B) }k(A,C) }k(A,D)
|
||
|
|
);
|
||
|
|
# send_5(A,B,
|
||
|
|
# { A, rd }k(A,D),
|
||
|
|
# { A, Tacd }k(A,C),
|
||
|
|
# { A, Tabd }k(A,B)
|
||
|
|
# );
|
||
|
|
|
||
|
|
claim_A1(A, Niagree);
|
||
|
|
claim_A2(A, Nisynch);
|
||
|
|
}
|
||
|
|
|
||
|
|
role B
|
||
|
|
{
|
||
|
|
const rb: Nonce;
|
||
|
|
var ra,rc,rd: Nonce;
|
||
|
|
var Tbad, Tbac: Ticket;
|
||
|
|
|
||
|
|
read_1(A,B, ra);
|
||
|
|
send_2(B,C, rb,
|
||
|
|
{ B,ra }k(A,B)
|
||
|
|
);
|
||
|
|
# read_5(A,B,
|
||
|
|
# Tbad,
|
||
|
|
# Tbac,
|
||
|
|
# { A, { D, { C,rb }k(B,C) }k(B,D) }k(A,B)
|
||
|
|
# );
|
||
|
|
# send_6(B,C,
|
||
|
|
# { B, Tbad }k(B,D),
|
||
|
|
# { B, Tbac }k(B,C)
|
||
|
|
# );
|
||
|
|
#
|
||
|
|
# claim_B1(B, Niagree);
|
||
|
|
# claim_B2(B, Nisynch);
|
||
|
|
}
|
||
|
|
|
||
|
|
role C
|
||
|
|
{
|
||
|
|
const rc: Nonce;
|
||
|
|
var ra,rb,rd: Nonce;
|
||
|
|
var Tcab,Tcbd: Ticket;
|
||
|
|
|
||
|
|
read_2(B,C, rb, Tcab );
|
||
|
|
send_3(C,D, rc,
|
||
|
|
{ C, rb }k(B,C),
|
||
|
|
{ C, Tcab }k(A,C)
|
||
|
|
);
|
||
|
|
# read_6(B,C,
|
||
|
|
# Tcbd,
|
||
|
|
# { B, { A,{ D,rc }k(C,D) }k(A,C) }k(B,C)
|
||
|
|
# );
|
||
|
|
# send_7(C,D,
|
||
|
|
# { C, Tcbd }k(C,D)
|
||
|
|
# );
|
||
|
|
#
|
||
|
|
# claim_C1(C, Niagree);
|
||
|
|
# claim_C2(C, Nisynch);
|
||
|
|
}
|
||
|
|
|
||
|
|
role D
|
||
|
|
{
|
||
|
|
const rd: Nonce;
|
||
|
|
var ra,rb,rc: Nonce;
|
||
|
|
var Tdbc,Tdac: Ticket;
|
||
|
|
|
||
|
|
read_3(C,D, rc, Tdbc, Tdac );
|
||
|
|
send_4(D,A, rd,
|
||
|
|
{ D, rc }k(C,D),
|
||
|
|
{ D, Tdbc }k(B,D),
|
||
|
|
{ D, Tdac }k(A,D)
|
||
|
|
);
|
||
|
|
# read_7(C,D,
|
||
|
|
# { C, { B,{ A,rd }k(A,D) }k(B,D) }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
|
||
|
|
|
||
|
|
run bunava24.A(Agent,Agent,Agent,Agent);
|
||
|
|
run bunava24.B(Agent,Agent,Agent,Agent);
|
||
|
|
run bunava24.C(Agent,Agent,Agent,Agent);
|
||
|
|
run bunava24.D(Agent,Agent,Agent,Agent);
|
||
|
|
run bunava24.A(Agent,Agent,Agent,Agent);
|
||
|
|
run bunava24.B(Agent,Agent,Agent,Agent);
|
||
|
|
run bunava24.C(Agent,Agent,Agent,Agent);
|
||
|
|
run bunava24.D(Agent,Agent,Agent,Agent);
|