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

% NSSK original version

%A -> S:  A, B, Na

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

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

%B -> A:  {Nb}Kab

%A -> B:  {Nb,Nb}Kab note modelling of -1


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

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


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

	      [packet]).


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

protocol_step(alice,[enc([nonce(bob,nb,0,[alice,bob,server])],kab)],
	      [],
	      [enc([nonce(bob,nb,0,[alice,bob,server]),nonce(bob,nb,0,[alice,bob,server])],kab)]).

protocol_step(bob,[enc([nonce(bob,nb,0,[alice,bob,server]),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])).