/*
Constraint Solver

This version uses showp.pl for ascii trace diagrams
showp.pl defines showp(<bundle>) and groundp(<term>,<ground_term>).

This version adds the invertible signature operator //
A//B works like [A,A/pk(B)].

Uses these nonstandard built-in SWI-Prolog predicates:
  term_to_atom, atom_length, gensym, reset_gensym

Protocol analysis based on "Constraint Solving
for Bounded Cryptographic Protocol Analysis"
ACM CCS-8, 2001

Copyright Jonathan Millen, 2008.

N-ary concatenation, but not associative
   Elements of a cat may be cats

Use search for convenience

'stop' and 'Auth' tests for secrecy and authentication
   'stop' interrupt added to selectnode 9/16/2010

Operators:

[U,V, ...] is concatenation, n-ary

U*K is U pk-encrypted with K, usually pk(A)

U/pk(A) is signature of U by A (not invertible)

U//A is U signed by A (invertible) like [U,U/pk(A)]     % added 4/2021

U+K is U encrypted with K as symmetric key

U-K is hidden symmetric encryption (see paper)

sha(U) is a hash function

e is the attacker

msk(A,B) deprecated, seems to cause search divergence
*/

% :- table(solve/2). can't be used in this (SWI) version

:- 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(B) :- search(B,[]).

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

search(B,I,Auth) :-
  write('Starting csolve...'),nl,
  resetcc,
  reach(B,[],I,F,[],Lout,Auth),nl,
  write('Simple constraints:'),nl,prlist(F),nl,
  reverse(Lout,Tr),
  write('Trace:'),nl,prlist(Tr),nl,
  groundp(Tr,Tg),
  showp(Tg), 
  write('Bundle:'),nl,prlist(B),nl.

% reach(Bundle,Constraintlist,Terms,FinalConstraintList,interLeavings in/out, Auth)
%   Constraintlist initially empty
%     Constraint is [term, termlist]
%   Terms is a list of terms known to attacker
%     Terms initially includes principal names, other constants
%   Bundle is a list of strands. (Actually a "semibundle")
%     Strand is list of send(M) and recv(M) nodes
%   Interleavings: Lin initially empty, Lout variable
%   Auth is a pattern used for authentication tests
%     Auth=event_name(A1,A2,...)  any event_name OK
%     Auth message sent causes immediate solve failure
%     Auth=[] for no auth. test
% reach creates the initial list of constraints
%   from a possible merge and passes it to solve

reach(B,C,_T,F,Lin,Lin,Auth) :-
  allnull(B),
  ics(N),
  write(' Try '),write(N),
%  prlist(Lin),
  Auth =.. H,!,		% H is the list form of the Auth term
  solve(C,F,H).

reach(B,C,T,F,Lin,Lout,Auth) :-
  selectnode(B,send(M),B1),!, % send adds term 
  isig(M,M1),	% macro expansion for invertible sig A//B, principal B
  append(M1,T,T1), % write('isig '),writeln(M),write(' to '),writeln(M1),
  reach(B1,C,T1,F,[send(M)|Lin],Lout,Auth).
  
reach(B,C,T,F,Lin,Lout,Auth) :-
  selectnode(B,recv(M),B1),   % recv adds constraint
  reach(B1,[[M,T]|C],T,F,[recv(M)|Lin],Lout,Auth).

% selectnode(B,N,B1) separates B into the first node
% N of some strand and the remaining strand set B1.
% selectnode fails if B is all null.
% Note: to optimize, we select all send nodes first, any order.
% (but usually only one send is available anyway)
% If all nodes are recv, order does matter, so all orders
% are attempted.

selectnode(B,send([e,e,stop]),[]) :-  % interrupt at stop
  member([send([_,_,stop])|_S],B),!.

selectnode(B,send([e,e,stop]),[]) :-  % interrupt at stop
  member([send(stop)|_S],B),!.

selectnode(B,send(M),B1) :-
  member([send(M)|_S],B),!,     % this cut for send optimization
  diff(B,send(M),B1).

selectnode([[recv(M)|S]|B],recv(M),[S|B]). % remove recv from first strand,

selectnode([S|B],recv(M),[S|B1]) :-  % or from some other strand
  selectnode(B,recv(M),B1).

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

diff([[N|S]|B],N,[S|B]).

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

% solve([[expr, termlist],...],Simple_constraints,H)
% simple constraints have the form [var,termlist].
% Apply reduct to each nonsimple constraint, in
% reverse (i.e., chronological) order.
% Build up (possibly empty) list of simple 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,H) :- % W1 is an output, H is the auth msg
  solve(C,V,H),
  remv(T,T1),
  solve1(A,T1,C,V,W1,H). % test for stopping conditions

solve1(_A,T,_C,_V,_W,_H) :-
  member(stop,T),!.

solve1(_A,T,_C,_V,_W,H) :-
  authmatch(T,H),!,
  fail.

solve1(A,T1,_C,V,W1,H) :-
  reduct(A,T1,U),
  append(U,V,W),
  solve(W,W1,H).

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

% "safe" steps preserve all possible solutions

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

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

reduct([A],T,[[A,T]]) :- !.	% synth singleton cat -jkm 3/8/21
 
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//e,T,[[M,T]]) :- !. 	% (isig), 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(msk(e,_A),_T,[]).		% e knows own msk's
reduct(msk(_A,e),_T,[]).		

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]|T],W) :- !, 	% (split) for singleton -jkm 4/21
  remv([A|T],W).

remv([[A,B]|T],W) :- !, % (split) for pair
  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.
%  (can show that "-" can occur only at top level)

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),!.

unify(msk(A,B),msk(B1,A1)) :-	% msk is commutative
	unify(A,A1),
	unify(B,B1).

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

%----------------------------------------------------------------------------
%     Printing
%----------------------------------------------------------------------------

% Print list elements

prlist([]).
prlist([X|L]) :-
  write(X),nl,
  prlist(L).


%----------------------------------------------------------------------------
% authmatch(T,H) finds a pattern match of H to some element of T
%   without binding any variable in T.
%----------------------------------------------------------------------------

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

%----------------------------------------------------------------------------
% macro expansion of invertible signature A//P to [A,A//P]
%----------------------------------------------------------------------------

isig(M,M) :- atomic(M),!.

isig(A,A) :- var(A),!.

isig(A//P,[B,B//P]) :-
	atomic(P),!,
	isig(A,B).

isig(A//P,[B,B//P]) :-
	var(P),!,
	isig(A,B).

isig([M|L],M1) :- !,isigl([M|L],M1).

isig(M,M1) :-
	M =.. [F|L],
	isigl(L,L1),
	M1 =.. [F|L1].

isigl([M],[M1]) :- !,isig(M,M1).

isigl([M|L],[M1|L1]) :-
	isig(M,M1),
	isigl(L,L1).