%%% File:     yahalom.pl
%%% Author:   Graham Steel <Graham.Steel@ed.ac.uk>
%%% Created:  Tue Jan 27 2009
%%% Last Update: Tue Jan 27 09:36:22 2009

% Yahalom

%A->B: A, Na

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

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

%A->B:  {A, Kab}Kbs, {Nb}Kab



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

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


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

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


protocol_step(alice,

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

%% final reception step

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

% 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])).