%%% 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

% Carlsson secret key initiator

A->B:  A, Na

B->S:  A, Na, B, Nb

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

B->A: {Na, B, Kab}Kas, {Na}Kab, N'b

A->B:  {N'b}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,tb,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,tb,0,[alice,bob,server])],kbs),
	       nonce(bob,nb,0,[alice,bob,server])]).

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

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

%reception

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




	      

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