# 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);