% sv.P by Corin and Etalle, U. Twente
%-------------------------------------
% Uses jkm solve, but new incremental reach
% changes by jkm for XSB marked with %%
%   changed strand form [name(args),[nodes]] back to [nodes]

% :- set_flag(occur_check, on). %% not in XSB
% :- table(solve/2).              %% XSB only

:- dynamic(cc/1).
:- assert(cc(0)).

%% resetcc resets the constraint set count to zero
%% (use it between trials)
%% ics increments it by one, used in reach

resetcc :- 
  retractall(cc(_)),
  assert(cc(0)).

ics(N1) :-
  retract(cc(N)),
  N1 is N+1,
  assert(cc(N1)).

%% search: typical reach call
search(B,A) :- 
  search(B,[a,b,e],A).

search(B,I,A) :-
  write('Starting mysv...'),nl,
  resetcc,
  reach(B,I,[],_T,A),
  write('Bundle:'),nl,write_ll(B),nl.
  
/*
reach/5: arguments: +B, +T, +F, ?Trace +Auth
B = semibundle
% S = final state desired %% use send(stop) instead
T = intruder knowledge w/possible instantiations
F = Varconstraints (initially empty list)
Trace = output trace
Auth = event pattern, [] if not used
*/

%% All strands complete
reach(B,_, _, Trace,_) :-
  allnull(B),!,
  reverse(Trace,Tr),nl,
  write('Trace:'),nl,write_ll(Tr),nl.

% Stop test %% modified 
reach(B, _, _, Trace,_) :-
  member([send(stop)|_],B),!,
  reverse(Trace,Tr),nl,
  write('Trace:'),nl,write_ll(Tr),nl.

%% Auth test
reach(B,T,L,Trace,A) :-
  A =.. H,
  authmatch(T,H),!,fail.

% always process 'send' messages first
reach(B,T,L,Trace,A) :-
  member([send(M)|_S],B),
  diff(B,send(M),B1),!,
  reach(B1, [M|T], L, [send(M)|Trace],A).

% recv or check
reach(B,T,L1,Trace,A) :- 
  create_const(B, T, CC),	% look for first nodes each strand of bundle
  member([Constr|TT], CC),	% create constraint
  ics(N),write(' Try '),write(N), 
  solve([[Constr|TT]], L),	% try to solve it
  append(L1,L,L2),
  simplify(L2,L3),		% simplify list of constraints
  (diff(B, recv(Constr), B1);	% if solved, remove it from strand (possibly repeated!!)
				% notice that B and T are unified against Constr
  diff(B, check(Constr), B1)),	
  
  reach(B1,  T, L3, [recv(Constr)|Trace],A).		

/*
simplify/2 arguments: +L1,?L2
L1 = list of constraints (input)
L2 = list of solved constraints (output)

fail if some constraint in L1 is not solvable
*/

simplify(L,L) :-
	all_variable(L).	% all simple constraints, finish

simplify(L,L1) :-
	mydelete([X|K],L,L2),	
	nonvar(X),
	solve([[X|K]],L3),	% nonsimple constraint, solve it
	append(L2,L3,L4),	
	simplify(L4,L1).	% maybe new non-simple constraint were added


/* all_variable/1 checks if all constraints are simple */
all_variable([]).	
all_variable([[X|_]|Rest]):-var(X), all_variable(Rest).

% diff(B,N,B1): bundle B minus node N is B1 %% back to mine

diff([[N|S]|B],N,[S|B]).
diff([S|B],N,[S|B1]) :- diff(B,N,B1).

% create constraints by choosing only the first nodes of the strands of the form recv(M)
%% revert strand form

create_const([],_,[]).
create_const([[]|B],T,C) :- create_const(B,T,C).
create_const([[recv(M)|_] |B],T,[[M|[T]]|C]) :- create_const(B, T, C).
create_const([[check(M)|_]|B],T,[[M|[T]]|C]) :- create_const(B, T, C).

%-------------------------------------

% solve([[expr, termlist],...],Varconstraints)
% apply reduct to each nonsimple constraint, in
% reverse (i.e., chronological) order.
% Build up (possibly empty) list of simple [var,termlist] constraints.
% Note that reduct may cause a var to be instantiated
% on the left side of a prior constraint, so
% tail recursion applies solve again from the beginning.

solve(C,C) :- allvarc(C), !.

solve([[A,T]|C],W1) :- 
   solve(C,V),
   remv(T,T1),
   reduct(A,T1,U),
   append(U,V,W),
   solve(W,W1). 

% reduct(M,T,C) performs one reduction step on
% an active constraint M:T and 
% records replacement constraints in C


reduct(M,T,[[M,T]]) :-
  var(M),!.		% pass over simple constraint

reduct(U=V,_,[]) :-		% (check)
  unify(U,V).


reduct(M,T,[]) :-  	% (un) with constant
  atomic(M),		% always safe
  member(M,T),!.


reduct([A,B],T,[[B,T],[A,T]]) :- !. 	% (pair), always safe

reduct([A|C],T,[[A,T]|D]) :- !, % (pair) extended, always safe %%
  reduct(C,T,D).

reduct(M/pk(e),T,[[M,T]]) :- !. 	% (sig), always safe

reduct(M,T,[]) :-		% (un)
  member(A,T),
  hunify(M,A).

reduct(sha(M),T,[[M,T]]).  	% (hash)

reduct(pk(A),T,[[A,T]]).	% public-key lookup

reduct(M*K,T,[[M,T],[K,T]]). 	% (penc)

reduct(M+K,T,[[M,T],[K,T]]).	% (senc)

reduct(M,T,[[M,T]]) :-
  do_ksub(T).

reduct(M,T,[[M,T2],[K,T1]]) :-
  do_ksyn(T,T2,K,T1).

% remv removes variables from a term list, if any.
% It also does (split) and (pdec), they're always safe.

remv([],[]) :- !.

remv([A|T],W) :-
  var(A),!,
  remv(T,W).

remv([[A,B]|T],W) :- !,	% (split)
  remv([A,B|T],W).

remv([[A|B]|T],W) :- !,	%% (split) extended
  remv([A,B|T],W).

remv([U*K|T],W) :-
  K==pk(e),!,		% (pdec)
  remv([U|T],W).

remv([A|T],[A|W]) :-
  remv(T,W).

% do_ksub looks for U*V in a term list
% and binds V to pk(e) if possible (and V not already pk(e))
% It fails if there is no instance to bind.

do_ksub([_U*V|_T]) :-
  \+V==pk(e),
  V=pk(e).

do_ksub([_A|T]) :- do_ksub(T).

% do_ksyn looks for U+K in a term list T
% and decrypts it to U.  We also insert the
% new constraint for K with U-K in T1.
% Fails iff there is no symmetric encryption.

do_ksyn([U+K|T],[U,K|T],K,[U-K|T]).

do_ksyn([A|T],[A|T2],K,[A|T1]) :- 
  do_ksyn(T,T2,K,T1).

% allnull tests for empty bundle

allnull([]).

allnull([[]|B]) :- allnull(B).

% allvarc tests for simple constraint set
%    in which all left sides are variables

allvarc([]).

allvarc([[X,_T]|C]) :-
  var(X),
  allvarc(C).

% hunify(M,A) turns A from - to + first if necessary.

hunify(M,U-V) :- unify(M,U+V),!.
hunify(M,A) :- unify(M,A).

%----------------------------------------------------------------------------
% "safe" unification with occurs check from C. Meadows
%----------------------------------------------------------------------------

unify(X,Y) :-
	var(X),var(Y),!,
	X=Y.
unify(X,Y) :-
	atomic(X),!,X=Y.	% atomic includes numbers
unify(X,Y) :-
	atomic(Y),!,X=Y.
unify(X,Y) :-
	var(X),!,
	notOccurs(X,Y),
	X=Y.
unify(X,Y) :-
	var(Y),!,
	notOccurs(Y,X),
	X=Y.
unify(X,Y) :-
	X =.. [A|B],
	Y =.. [A|C],
	list_unify(B,C),!.

list_unify([],[]).
list_unify([A|B],[C|D]) :-
	unify(A,C),
	list_unify(B,D).

notOccurs(X,Y) :- var(Y),!, \+ X == Y.
notOccurs(_X,Y) :- atomic(Y),!.
notOccurs(X,[Y|Z]) :- !,notOccurs(X,Y),notOccurs(X,Z).
notOccurs(X,Y) :- Y =.. [_F|N],notOccurs(X,N).


% pretty print of lists
write_ll([]).
write_ll([H|T]) :- writeq(H),nl,write_ll(T).

% mydelete ( delete not native in XSB) %%

mydelete(X,Y,L) :-	var(Y),!,fail.
mydelete(X,[X|L],L).
mydelete(X,[A|L],[A|L1]) :- mydelete(X,L,L1).

%----------------------------------------------------------------------------
% authmatch(T,H) finds a pattern match of H to some element of T
%   without binding any variable in T.
%   H is a =.. flattened function call, f(a,b) -> [f,a,b]
%----------------------------------------------------------------------------

authmatch(T,[[]]) :- !,fail. % no Auth pattern
authmatch([A|T],H) :-
  A=..AL,
  authmatch1(AL,H),!.
authmatch([A|T],H) :- authmatch(T,H).
authmatch1([],[]).
authmatch1([X|U],[Y|V]) :- 
  authmatch1a(X,Y),
  authmatch1(U,V).
authmatch1a(X,Y) :- var(Y),!,Y=X.
authmatch1a(X,Y) :- var(X),!,fail.
authmatch1a(X,Y) :- X==Y,!.
authmatch1a(X,Y) :- atomic(Y),!,fail.
authmatch1a(X,Y) :- atomic(X),!,fail.
authmatch1a(X,Y) :- X=..XL,Y=..YL,authmatch1(XL,YL).