%%% File:     yahalom.pl
%%% Author:   Graham Steel <Graham.Steel@ed.ac.uk>
%%% Created:  Tue Jan 27 2009
%%% Last Update: Tue Jan 27 17:59:43 2009

% Otway-Rees (original version)

%% known attack is type flaw

%A->B:  M, A, B, {Na, M, A, B}Kas

%B->S:  M, A, B, {Na, M, A, B}Kas, {Nb, M, A, B}Kbs

%S->B:  M, {Na, Kab}Kas, {Nb, Kab}Kbs

%B->A:  M, {Na, Kab}Kas





protocol_step(alice,
	      [],
	      [nonce(alice,m,0,[alice,bob,server]),
	       nonce(alice,na,0,[alice,bob,server])],
	      [nonce(alice,m,0,[alice,bob,server]),agent(alice),agent(bob),enc([nonce(alice,na,0,[alice,bob,server]),nonce(alice,m,0,[alice,bob,server]),agent(alice),agent(bob)],kas)]).

protocol_step(bob,
	      [nonce(alice,m,0,[alice,bob,server]),agent(alice),agent(bob),packet],
	      [nonce(bob,nb,0,[alice,bob,server])],
	      [nonce(alice,m,0,[alice,bob,server]),agent(alice),agent(bob),packet,enc([nonce(bob,nb,0,[alice,bob,server]),nonce(alice,m,0,[alice,bob,server]),agent(alice),agent(bob)],kbs)]).

protocol_step(server,
	      [nonce(alice,m,0,[alice,bob,server]),agent(alice),agent(bob),
	       enc([nonce(alice,na,0,[alice,bob,server]),nonce(alice,m,0,[alice,bob,server]),agent(alice),agent(bob)],kas),
	       enc([nonce(bob,nb,0,[alice,bob,server]),nonce(alice,m,0,[alice,bob,server]),agent(alice),agent(bob)],kbs)],
	      [key(server,kab,2,[alice,bob,server])],
	      [nonce(alice,m,0,[alice,bob,server]),
	       enc([nonce(alice,na,0,[alice,bob,server]),key(server,kab,2,[alice,bob,server])],kas),
	       enc([nonce(bob,nb,0,[alice,bob,server]),key(server,kab,2,[alice,bob,server])],kbs)]).

protocol_step(bob,
	      [nonce(alice,m,0,[alice,bob,server]),
	       packet,
	       enc([nonce(bob,nb,0,[alice,bob,server]),key(server,kab,2,[alice,bob,server])],kbs)],
	      [],
	      [nonce(alice,m,0,[alice,bob,server]),
	       packet]).

protocol_step(alice,
	      [nonce(alice,m,0,[alice,bob,server]),
	       enc([nonce(alice,na,0,[alice,bob,server]),key(server,kab,2,[alice,bob,server])],kas)],
	      [],
	      []).


	      

% handle store - should always be declared in protocol file

:- dynamic handle/1.





%% initial handles

handle(h(alice,kas,3,[alice,server])).
handle(h(bob,kbs,3,[bob,server])).
handle(h(server,kas,3,[alice,server])).
handle(h(server,kbs,3,[bob,server])).