/*
Constraint Solver

Ascii Diagram version (from .mac site)
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+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 just principal names
%   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,!,
  solve(C,F,H).

reach(B,C,T,F,Lin,Lout,Auth) :-
  selectnode(B,send(M),B1),!, % send adds term 
  reach(B1,C,[M|T],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],...],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,H) :- 
  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,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(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,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).

%----------------------------------------------------------------------------
%     ASCII Protocol Diagram
%----------------------------------------------------------------------------

% The main function is showp(S), where
% S is a list of send([A,B,M]) and recv([A,B,M]) terms.
% A is the sender, B is the receiver, M is the message content.

% The display looks best on ground strands. groundp(S,T) can
% be used to turn variables into atoms.

% showp uses built-in SWI term_to_atom and atom_length
% groundp uses built-in SWI gensym, reset_gensym

leftcol('  |').

% shaft is the length of an arrow (less head).
% Increase it to accommodate longer messages.

shaft(36).

% make_arrow(direction,msg,side)

make_arrow(right,M,left) :-
  make_msg(M,' '),
  leftcol(L),write(L),
  shaft(S),
  dashes(S),write('>|'),
  blanks(S),writeln(' |').

make_arrow(left,M,left) :-
  make_msg(M,' '),
  leftcol(L),write(L),
  write('<'),
  shaft(S),dashes(S),
  write('|'),
  blanks(S),
  writeln(' |').

make_arrow(left,M,right) :-
  make_msg(' ',M),
  leftcol(L),write(L),
  shaft(S),
  blanks(S),write(' |'),
  write('<'),dashes(S),
  writeln('|').

make_arrow(right,M,right) :-
  make_msg(' ',M),
  leftcol(L),write(L),
  shaft(S),
  blanks(S),write(' |'),
  dashes(S),writeln('>|').

make_msg(M1,M2) :-  
  leftcol(L),write(L),
  shaft(S),
  place_msg(M1,S,E),
  write('|'),
  S2 is S - E,
  place_msg(M2,S2,_),
  writeln('|').

place_msg(M,S,Ep) :-	% assumes M is an atom, show_msg does this
  atom_length(M,N),
  BN is (S - N + 1)//2,
  line_of(BN,' '),
  write(M),
  AN is S + 1 - BN - N,
  line_of(AN,' '),
  E is N - S - 1,
  posbound(E,Ep).

dashes(N) :- line_of(N,'-').
blanks(N) :- line_of(N,' ').

line_of(1,C) :- !,write(C).
line_of(N,_) :- N < 1,!.
line_of(N,C) :-
  line_of(1,C),
  N1 is N-1,
  line_of(N1,C).

term_length(T,N) :-
  term_to_atom(T,A),
  atom_length(A,N).

posbound(N,0) :- N < 0,!.
posbound(N,N).

make_party(left,A) :-
  term_length(A,N),
  M is 3-(N + 1)//2,
  posbound(M,MP),
  line_of(MP,' '),
  write(A),
  shaft(S),
  M1 is S - N - MP + 4,
  line_of(M1,' '),
  write('|'),
  blanks(S),writeln(' |').

make_party(right,A) :-
  term_length(A,N),
  leftcol(L),write(L),
  shaft(S),
  blanks(S),write(' |'),
  M is S + 1 - N//2,
  line_of(M,' '),
  writeln(A).

% P is a list of send([A,B,M]) and recv([A,B,M]) terms

showp(P) :- 
  showp(P,null,null).

showp([],_LR,_RR).

showp([send([e,e,M])|P],LR,_) :- !,  % e -> e: M
  make_party(right,e),
  show_msg(right,M,right),
  showp(P,LR,e).

showp([recv([e,e,M])|P],LR,_) :- !, 
  make_party(right,e),
  show_msg(right,M,right),
  showp(P,LR,e).

showp([recv([e,B,M])|P],null,null) :- !, % initially
  make_party(left,B),
  show_msg(left,M,left),
  showp(P,B,null).

showp([recv([A,B,M])|P],A,B) :- !, % A -> B: M
  show_msg(right,M,right),
  showp(P,A,B).

showp([recv([A,B,M])|P],B,A) :- !, 
  show_msg(left,M,left),
  showp(P,B,A).

showp([recv([A,B,M])|P],_,B) :- !, % new A -> B: M
  make_party(left,A),
  show_msg(right,M,right),
  showp(P,A,B).

showp([recv([A,B,M])|P],B,_) :- !, 
  make_party(right,A),
  show_msg(left,M,left),
  showp(P,B,A).

showp([recv([A,B,M])|P],A,_) :- !, % A -> new B: M
  make_party(right,B),
  show_msg(right,M,right),
  showp(P,A,B).

showp([recv([A,B,M])|P],_,A) :- !, 
  make_party(left,B),
  show_msg(left,M,left),
  showp(P,B,A).

showp([recv([A,B,M])|P],_,_) :- !, % new A -> new B: M
  make_party(left,A),
  make_party(right,B),
  show_msg(right,M,right),
  showp(P,A,B).

showp([send([A,B,M])|P],A,B) :- !, % A -> B: M
  show_msg(right,M,left),
  showp(P,A,B).

showp([send([A,B,M])|P],A,_) :- !, % A -> new B: M
  make_party(right,B),
  show_msg(right,M,left),
  showp(P,A,B).

showp([send([A,B,M])|P],_,A) :- !, 
  make_party(left,B),
  show_msg(left,M,right),
  showp(P,B,A).

showp([send([A,B,M])|P],_,B) :- !, % new A -> B: M
  make_party(left,A),
  show_msg(right,M,left),
  showp(P,A,B).

showp([send([A,B,M])|P],B,_) :- !, 
  make_party(right,A),
  show_msg(left,M,right),
  showp(P,B,A).

showp([send([A,B,M])|P],_,_) :- !, % new A -> new B: M
  make_party(left,A),
  make_party(right,B),
  show_msg(right,M,left),
  showp(P,A,B).

showp([M|P],A,B) :-
  nl,write(M),writeln(' not in form send/recv([A,B,M])'),
  showp(P,A,B). 

show_msg(D,M,E) :-
  term_to_atom(M,Ma),
  make_arrow(D,Ma,E).

groundp(P,Q) :- reset_gensym,groundp1(P,Q).

groundp1(P,P) :- atomic(P),!.
groundp1(P,Q) :- var(P),!,
  gensym(v_,Q),
  P=Q.
groundp1([X|A],[Y|B]) :- !,
  groundp1(X,Y),groundp1(A,B).
groundp1(F,G) :- 
  F =.. A,
  groundp1(A,B),
  G =.. B.

% sample protocol traces

prot1([
  recv([a,b,[a,na]*kb]),
  recv([b,a,[na,nb]*ka]),
  recv([a,b,[nb]*kb])
]).

prot2(A,B,X,N,Nb,[
  send([A,X,[A,N]*pk(X)]),
  recv([A,B,[A,N]*pk(B)]),
  send([B,A,[N,Nb]*pk(A)]),
  recv([X,A,[N,Nb]*pk(A)]),
  send([A,X,[Nb]*pk(X)]),
  recv([A,B,[Nb]*pk(B)])
]).

prot3([
  recv([attester,guest,reallyveryextremelylongmessagebutoneatom]),
  recv([guest,attester,yetanotherreallyverylongmessagebutoneatom1]),
  recv([attester,appraiser,anothermessage]),
  recv([appraiser,enforcer,anothermessage1])
]).