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

% NSSK revised

%A->B:  A

%B->A:  {A, NbKbs

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

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

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

%B->A:  {Nb}Kab

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


protocol_step(alice,[],
	      [],
	      [agent(alice)]).

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

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

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