%%% File:     generic-API.pl
%%% Author:   Graham Steel <Graham.Steel@ed.ac.uk>
%%% Created:  Mon Jan 26 2009
%%% Last Update: Tue Feb 10 15:43:09 2009



%% Demonstrates the generation of appropriate API rules from a protocol.


participant(alice).
participant(bob).
participant(server).

% protocol_step/4 specifies the protocol

%% this is consulted from another file

%% initial handles are also in the other file


%% the API commands stores as generate, decrypt, encrypt

%% for sicstus prolog
:- dynamic command/4.

%% for Gnu prolog 

%dynamic(command/4).

%% get a new name for a handle 

new_handle_name(Agent,Name,Name) :-
	\+ handle(h(Agent,Name,_,_)).

new_handle_name(Agent,Name,Name) :-
	new_handle_name(Agent,prime(Name),prime(Name)).
		 


%%% the algorithm


go(Protocol) :- consult(Protocol),
	        go,
		print_commands.


go :-
	findall(_,(
		   protocol_step(Played_by,LHS,MID,RHS),
		   treat_step(Played_by,LHS,MID,RHS)),_).


print_commands :-
	findall(_,(
		   command(Played_by,Commands1,Commands2,Commands3),
		   format("~n~n Command for ~w ~n~n Generate ~w ~n~n Decrypt ~w ~n~n Encrypt ~w ~n~n",[Played_by,Commands1,Commands2,Commands3])),_).


treat_step(Played_by,LHS,MID,RHS) :-

	generate_rules(Played_by,MID,Commands1),
	decrypt_rules(Played_by,LHS,Commands2), % tests included here
	encrypt_rules(Played_by,RHS,Commands3),
	assert(command(Played_by,Commands1,Commands2,Commands3)),!.


	      
generate_rules(_,[],[]).


generate_rules(Agent,[nonce(Agent,Name,Level,Set)|Rest],[gen(h(Agent,Name,Level,Set))|OtherCommands]) :-
	assert(handle(h(Agent,Name,Level,Set))),
	generate_rules(Agent,Rest,OtherCommands).

generate_rules(Agent,[key(Agent,Name,Level,Set)|Rest],[gen(h(Agent,Name,Level,Set))|OtherCommands]) :-
	assert(handle(h(Agent,Name,Level,Set))),
	generate_rules(Agent,Rest,OtherCommands).


decrypt_rules(_,[],[]).


decrypt_rules(Agent,[enc(List,Key)|Rest],[decrypt([enc(List,Key),h(Agent,Key,Level,Set),Test],RHS)|Commands]) :-

	handle(h(Agent,Key,Level,Set)),	
	treat_encrypted_terms(Agent,List,RHS),
	derive_tests(Agent,List,Test),

	decrypt_rules(Agent,Rest,Commands).


decrypt_rules(Agent,[_|Rest],Commands) :-
	
	decrypt_rules(Agent,Rest,Commands).


treat_encrypted_terms(_,[],[]) :- !.


treat_encrypted_terms(Agent,[agent(Name)|Rest],[agent(Name)|RHS]) :-

		     treat_encrypted_terms(Agent,Rest,RHS).

%forwarding of encrypted packets.

treat_encrypted_terms(Agent,[packet|Rest],[packet|RHS]) :-

		     treat_encrypted_terms(Agent,Rest,RHS).


%% nonce level 0 returned

treat_encrypted_terms(Agent,[nonce(Agent2,Name,0,S)|Rest],[nonce(Agent2,Name,0,S)|LHS]) :-

		     treat_encrypted_terms(Agent,Rest,LHS).


%%%%  nonce level 1 - get a new handle for it even if I generated it

treat_encrypted_terms(Agent,[nonce(_Agent2,Name,1,Set)|Rest],[h(Agent,Name2,1,Set)|LHS]) :-

	             new_handle_name(Agent,Name,Name2),

		     assert(handle(h(Agent,Name2,1,Set))),
		     
		     treat_encrypted_terms(Agent,Rest,LHS).


%%%%  key level 2 - get a new handle for it even if I generated it

treat_encrypted_terms(Agent,[key(_Agent2,Name,2,Set)|Rest],[h(Agent,Name2,2,Set)|LHS]) :-

	             new_handle_name(Agent,Name,Name2),

		     assert(handle(h(Agent,Name2,2,Set))),
		     
		     treat_encrypted_terms(Agent,Rest,LHS).

%%%%%%


encrypt_rules(_Agent,[],[]).


%% only an enc term is of interest



encrypt_rules(Agent,[enc(List,Key)|Rest],[encrypt([h(Agent,Key,L,Set),Terms],[enc(List,Key)])|Rules1]) :-

	handle(h(Agent,Key,L,Set)),
	
				% check for nested encryptions
	encrypt_rules(Agent,List,Rules2),

	treat_plaintexts(Agent,List,Terms),

	encrypt_rules(Agent,Rest,Rules3),
	append(Rules3,Rules2,Rules1).
	      
%% other stuff (this can also triggered if the encryption is with a key we don't have,
%% i.e. we forward a secret packet (assuming a sensible protocol..)

encrypt_rules(A,[_|Rest],RHS) :-
	encrypt_rules(A,Rest,RHS).


%%%%%%

treat_plaintexts(_Agent,[],[]).


%  agent name

treat_plaintexts(Agent,[agent(Name)|Rest],[agent(Name)|RHS]) :-

	treat_plaintexts(Agent,Rest,RHS).



%  a nested encryption (it will have its own rule)

treat_plaintexts(Agent,[enc(_,_)|Rest],[nested_encryption|RHS]) :-

	treat_plaintexts(Agent,Rest,RHS).


% one of my nonces, 0 or 1

treat_plaintexts(Agent,[nonce(Agent,Name,L,Set)|Rest],[h(Agent,Name,L,Set)|RHS]) :-
	handle(h(Agent,Name,L,Set)),
	treat_plaintexts(Agent,Rest,RHS).


%% someone elses nonce level 0 (i.e. public term)

treat_plaintexts(Agent,[nonce(Agent2,Name,0,Set)|Rest],[nonce(Agent2,Name,0,Set)|RHS]) :-
	Agent2 \== Agent,
	treat_plaintexts(Agent,Rest,RHS).


% key

treat_plaintexts(Agent,[key(Agent,Name,L,Set)|Rest],[h(Agent,Name,L,Set)|RHS]) :-

	handle(h(Agent,Name,L,Set)),
	       
	treat_plaintexts(Agent,Rest,RHS).


%% derive tests if necessary - return the empty list of tests if not necc

%% if we find something of level 2, we require

%% a test on something we generated of level 1, but that's it for the moment.

derive_tests(Agent,List,Tests) :-
	derive_tests(Agent,List,Tests,List).

derive_tests(_,[],[],_).

derive_tests(Agent,[key(_Agent2,_Name,2,_Set)|_Rest],[test(Handle)],List) :-
	find_test_nonce(Agent,Handle,List).

derive_tests(Agent,[_|Rest],Test,List) :-
	derive_tests(Agent,Rest,Test,List).

find_test_nonce(_,warning(missing_test),[]).

find_test_nonce(Agent,h(Agent,Name,L,Set),[nonce(Agent,Name,L,Set)|_]).

find_test_nonce(Agent,Handle,[_|List]) :-
	find_test_nonce(Agent,Handle,List).