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

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

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

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

protocol_step(bob,
	      [enc([nonce(bob,nbb,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])).