% psltl.P -
% Ari Saptawijaya, last modified: Sept 21, 2005
% Ref.: "PS-LTL for Constraint-based Security Protocol Analysis", 2005
% Translation to DNF is inspired from S. Hoelldobler's ICL script
% ------------------------------

/* operator definitions */
:-op(130,fy,yest).
:-op(130,fy,hist).
:-op(130,fy,once).
:-op(140,fy,neg).
:-op(145,xfx,since).
:-op(150,xfy,and).
:-op(160,xfy,or).
:-op(170,xfx,imp).


/* *********************************************************************** */
/* Translation to DNF */
/* *********************************************************************** */

/*
step_EF/4 (F,Tr,I,G) rewrites PS-LTL formulas to EF formulas
 Arguments:
 F: PS-LTL formula
 Tr: Trace
 I: initial intruder knowledge
 G: EF formula
*/

step_EF(some(X,F),Tr,I,some(X,G)) :- step_EF(F,Tr,I,G),!.
step_EF(all(X,F),Tr,I,all(X,G)) :- step_EF(F,Tr,I,G),!.
step_EF(neg X,Tr,I,neg Y) :- step_EF(X,Tr,I,Y),!.
step_EF(X and Y,Tr,I,U and V) :- step_EF(X,Tr,I,U),step_EF(Y,Tr,I,V),!.
step_EF(X or Y,Tr,I,U or V) :- step_EF(X,Tr,I,U), step_EF(Y,Tr,I,V),!.
step_EF(X imp Y,Tr,I,U imp V) :- step_EF(X,Tr,I,U), step_EF(Y,Tr,I,V),!.
step_EF(yest _,[],_,false) :- !.
step_EF(yest X,[_|SubTr],I,U) :- step_EF(X,SubTr,I,U),!.
step_EF(_ since Y,[],I,U) :- step_EF(Y,[],I,U),!.
step_EF(X since Y,[Hd|SubTr],I,U or V and W) :- 
  step_EF(Y,[Hd|SubTr],I,U),step_EF(X,[Hd|SubTr],I,V),
  step_EF(X since Y,SubTr,I,W),!.
step_EF(once X,[],I,Y) :- step_EF(X,[],I,Y),!.
step_EF(once X,[Hd|SubTr],I,U or V) :- 
  step_EF(X,[Hd|SubTr],I,U),step_EF(once X,SubTr,I,V),!.
step_EF(hist X,[],I,Y) :- step_EF(X,[],I,Y),!.
step_EF(hist X,[Hd|SubTr],I,U and V) :- 
  step_EF(X,[Hd|SubTr],I,U),step_EF(hist X,SubTr,I,V),!.
step_EF(learn(M),Tr,I,[M,T]) :- know(Tr,T1),append(T1,I,T),!.
step_EF([_,_],[],_,false) :- !.
step_EF([_,X],[[_,Hd]|_],_,false) :- 
  X =.. [H1|Lx],Hd =.. [H2|Lh],len(Lx,Len1),len(Lh,Len2),
  (H1\==H2,!;Len1=\=Len2),!.
step_EF([_,X],[[_,Hd]|_],_,Y) :- X =.. [_|Lx],Hd =.. [_|Lh],
  con_event(Lx,Lh,Y),!.
step_EF(X,_,_,X).

% know/2 computes the intruder knowledge from all send messages 
% of a given trace
know([],[]).
know([[_,send(M)]|SubTr],[M|K]) :- know(SubTr,K),!.
know([_|SubTr],K) :- know(SubTr,K).

% len/2 computes the length of a list
len([],0).
len([_|Y],L) :- len(Y,L1), L is 1+L1.

% con_event/2 produces EF atomic formula t1=t2 from the parameters 
%of two status events
con_event([H1],[H2],(H1=H2)).
con_event([H1|L1],[H2|L2],(H1=H2) and C) :- con_event(L1,L2,C).

% step_imp/2 rewrites implications
step_imp(some(X,F),some(X,G)) :- step_imp(F,G),!.
step_imp(all(X,F),all(X,G)) :- step_imp(F,G),!.
step_imp(neg X,neg Y) :- step_imp(X,Y),!.
step_imp(X and Y,U and V) :- step_imp(X,U), step_imp(Y,V),!.
step_imp(X or Y,U or V) :- step_imp(X,U), step_imp(Y,V),!.
step_imp(X imp Y,neg U or V) :- step_imp(X,U), step_imp(Y,V),!.
step_imp(X,X).

% step_morg/2 applies De Morgan, push negation inside, and removing 
% double negation 
step_morg(some(X,F),some(X,G)) :- step_morg(F,G),!.
step_morg(all(X,F),all(X,G)) :- step_morg(F,G),!.
step_morg(X and Y,U and V) :- step_morg(X,U), step_morg(Y,V),!.
step_morg(X or Y,U or V) :- step_morg(X,U), step_morg(Y,V),!.
step_morg(neg(some(X,F)),all(X,G)) :- step_morg(neg F,G),!.
step_morg(neg(all(X,F)),some(X,G)) :- step_morg(neg F,G),!.
step_morg(neg(X and Y),U or V) :- step_morg(neg X,U), step_morg(neg Y,V),!.
step_morg(neg(X or Y),U and V) :- step_morg(neg X,U), step_morg(neg Y,V),!.
step_morg(neg neg X,Y) :- step_morg(X,Y),!.
step_morg(X,X).


% step_push/2 pushes universal quantifiers as far as possible and 
% then simplifies the result whenever possible
step_push(X and Y,U and V) :- step_push(X,U),step_push(Y,V),!.
step_push(X or Y,U or V) :- step_push(X,U),step_push(Y,V),!.
step_push(some(X,F),some(X,G)) :- step_push(F,G),!.
step_push(all(X,F),U) :- 
   F =.. [all|_],step_push(F,F1),F\==F1,step_push(all(X,F1),U),!.
step_push(all(X,F),U and V) :- 
   F =.. [and,F1,F2],step_push(all(X,F1),U),step_push(all(X,F2),V),!.
step_push(all(X,F),U or V) :- 
   F =.. [or,F1,F2],(\+free(X,F1),!;\+free(X,F2)),step_push(all(X,F1),U),
   step_push(all(X,F2),V),!.
step_push(all(X,F),U) :- \+free(X,F),step_push(F,U),!.
step_push(all(X,Y=_),false) :- X==Y,!.
step_push(all(X,neg (Y=_)),false) :- X==Y,!.
step_push(all(X,[Y,_]),false) :- X==Y,!.
step_push(all(X,neg [Y,_]),false) :- X==Y,!.
step_push(X,X).

/* 
free/2 checks whether a variable is free in an EF formula, given that
no same variables are bound twice (alpha conversion is always available)
*/

free(X,Y=_) :- X == Y.
free(X,neg (Y=_)) :- X == Y.
free(X,[Y,_]) :- X == Y.
free(X,neg [Y,_]) :- X == Y.
free(X,F and G) :- free(X,F);free(X,G).
free(X,F or G) :- free(X,F);free(X,G).
free(X,all(_,F)) :- free(X,F).
free(X,some(_,F)) :- free(X,F).

/* negation normal form */
negation(X,Tr,I,Y) :- 
   step_EF(X,Tr,I,X3), step_imp(X3,X4), step_morg(X4,X5), step_push(X5,Y),!.

% computes the disjuntive normal form (in dual clause form), 
% or reject formula if the translation is not existential
% dual clause form: [[a,b],[c,d]] means (a and b) or (c and d)
dual_clause_form(X,Tr,I,Y1) :- 
   negation(X,Tr,I,Z1),
   (ex_form(Z1,Z2) -> (simp_ex(Z2,Z),expand([[Z]],Y1),!)
                      ;(write('FORMULA UNACCEPTED'),nl,fail)).

ex_form(some(_,F),U) :- ex_form(F,U),!.
ex_form(F and G,U and V) :- ex_form(F,U),ex_form(G,V),!.
ex_form(F or G,U or V) :- ex_form(F,U),ex_form(G,V),!.
ex_form(X,X) :- X =.. [H|_],\+quantifier(H),\+connectives(H).

quantifier(some).
quantifier(all).

connectives(and).
connectives(or).

% simp_ex/2 and simp_lit/2 simplify an existential formula as much as
% possible by manipulating "true" and "false" in the formula
simp_ex(X,Y) :- simp_lit(X,Z),X\==Z,simp_ex(Z,Y),!.
simp_ex(X,X).

simp_lit(F and G,U) :- member(F,[true,neg false]),simp_lit(G,U),!.
simp_lit(F and G,U) :- member(G,[true,neg false]),simp_lit(F,U),!.
simp_lit(F and _,false) :- member(F,[false,neg true]),!.
simp_lit(_ and G,false) :- member(G,[false,neg true]),!.
simp_lit(F and G,U and V) :- simp_lit(F,U),simp_lit(G,V),!.
simp_lit(F or G,U) :- member(F,[false,neg true]),simp_lit(G,U),!.
simp_lit(F or G,U) :- member(G,[false,neg true]),simp_lit(F,U),!.
simp_lit(F or _,true) :- member(F,[true,neg false]),!.
simp_lit(_ or G,true) :- member(G,[true,neg false]),!.
simp_lit(F or G,U or V) :- simp_lit(F,U),simp_lit(G,V),!.
simp_lit(X,X).

/* expand/2 and step_dist/2 for distributing conjunction over disjunction */

expand(X,Y) :- step_dist(X,Z), expand(Z,Y),!.
expand(X,X).

step_dist([K|R],Y) :-
   member(Disj,K),
   Disj = X1 or X2,
   my_remove(Disj,K,Temp),
   Newdis1 = [X1|Temp],
   Newdis2 = [X2|Temp],
   Y = [Newdis1,Newdis2|R].

step_dist([K|R],Y) :-
   member(Conj,K),
   Conj = X1 and X2,
   my_remove(Conj,K,Temp),
   Newdis = [X1,X2|Temp],
   Y = [Newdis|R].

step_dist([K|R],[K|NR]) :- step_dist(R,NR).

my_remove(_,[],[]).
my_remove(X,[H|T],T1) :- X==H,!,my_remove(X,T,T1).
my_remove(X,[H|T],[H|T1]) :- my_remove(X,T,T1).

/* *********************************************************************** */
/* Decision Procedure */
/* *********************************************************************** */

/* decision/4: decides whether a PS-LTL formula is true or false
- F: PS-LTL formula
- Tr: Trace
- I: initial intruder knowledge
- Cs: constraint store
*/

decision(F,Tr,I,Cs) :- dual_clause_form(F,Tr,I,X),decide(X,Cs).

/*
 decide/2 (F,Cs)
 Arguments:
- F: existential EF formula
- Cs: constraint store
 It is the main decision procedure, to implement procedure P(\pi,CS) from the paper
 it splits a conjunction part into 5 partitions, check whether "false" exists in 
 partition E by using dec_E/1, try to find an MGU for every equality in partition A
 that solves the constraint set Cs and the constraints in partition C, then check 
 whether the negation part of constraints in D are solvable (by using dec_D/1) and 
 finally check whether the negation part of equalities (partition B) is true using 
 dec_B/1
*/

decide([H|_],Cs) :- 
   split_lit(H,A,B,C,D,E),dec_E(E),execute(A),append(Cs,C,Cs1),solve(Cs1,Cs2),const_var(Cs2,0),
   dec_D(D),\+dec_B(B),!.
decide([_|T],Cs) :- decide(T,Cs).



% const_var/2 assigns each variable that occurs in a solved constraint set a fresh and distinct constant.
const_var([],_).
const_var([[X,_]|T],N) :- create_const(c,N,X), N1 is N+1, const_var(T,N1).

create_const(X,N,Y) :- name(X,L1), name(N,L2), append(L1,L2,L), name(New,L), Y=New.

/* split_lit/6 (L,La,Lb,Lc,Ld,Le) splits a clause into five partitions:
- L: a clause
- La: partition for equalities
- Lb: partition for negation of equalities
- Lc: positive constraint
- Ld: negative constraint
- Le: truth values only
*/
split_lit([],[],[],[],[],[]).
split_lit([H|T],La,Lb,Lc,Ld,[H|Te]) :- 
   member(H,[true,false]),!,split_lit(T,La,Lb,Lc,Ld,Te).
split_lit([H|T],La,Lb,Lc,[A|Td],Le) :- 
   H=neg A,!,is_constraint(A),A = [A1,_],
   (gr(A1) -> split_lit(T,La,Lb,Lc,Td,Le)
             ;(write('FORMULA UNACCEPTED: "neg learn" WITH NON-GROUND ARGUMENT'),nl,fail)).
split_lit([H|T],La,[A|Tb],Lc,Ld,Le) :- 
   H=neg A,!,\+is_constraint(A),split_lit(T,La,Tb,Lc,Ld,Le).
split_lit([H|T],La,Lb,[H|Tc],Ld,Le) :- 
   is_constraint(H),!,split_lit(T,La,Lb,Tc,Ld,Le).
split_lit([H|T],[H|Ta],Lb,Lc,Ld,Le) :- 
   split_lit(T,Ta,Lb,Lc,Ld,Le).


% gr/1 check whether or not a term T is ground
gr(T) :- \+var(T), T =.. L, gr1(L).

gr1([]).
gr1([Hd|Tl]) :- atom(Hd), !, gr1(Tl).
gr1([Hd|Tl]) :- compound(Hd), Hd =.. L, gr1(L), gr1(Tl).

% check if an entity is in the form of constraint, i.e. a list
is_constraint([_,_]).

% dec_E/1, check whether "false" is contained in a clause
dec_E([]).
dec_E([H|T]) :- H\==false,dec_E(T).

% execute every element of a list, applies to partition A and gives an MGU
execute([]).
execute([H|T]) :- H,execute(T).

% dec_D/1 to check whether the negation part of constraints (partition D) 
% is unsolvable
dec_D([]).
dec_D([H|T]) :- \+solve([H],_),dec_D(T).

% dec_B/1, check whether an equality holds or not by checking whether 
% L and R are syntactically different.

dec_B([L=R|_]) :- L==R.
dec_B([_|T]) :- dec_B(T).

