%%% File:     woo-lam.pl
%%% Author:   Graham Steel <Graham.Steel@ed.ac.uk>
%%% Created:  Wed Jan 28 2009
%%% Last Update: Thu Feb  5 13:37:43 2009




%%% Woo lam  mutual auth and key estab
%% p and q mapped to A and B

%A->B:  A, Na

%B->A:  B, Nb

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

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

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

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

%A->B:  {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),nonce(bob,nb,0,[alice,bob,server])]).

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

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

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

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

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

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


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

%A->B:  {Nb}Kab

% handle store - should always be declared in protocol file

%:- dynamic handle/1.

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