%%% -*- Mode: prolog -*-

%% SCSP Solver security.pl
%% version 21. Dec 2001, 18:00
%% Stefano Bistarelli, Thom Fruehwirth, Michael Marte, Munich, December 2001

%% Works fine with Sicstus Prolog 3.8.6 but not with 3.9.0beta1.

:-
	module(security,
	       [use_semiring/1,
		ca/1, cal/0]).

:-
	use_module(library(terms)),
	use_module(library(chr)),
	use_module(library(lists),
		   [member/2, select/3, is_list/1, append/3, remove_duplicates/2]),
	use_module(library(ordsets)).


handler security.


option(debug_compile,off).
option(already_in_heads, on).
option(check_guard_bindings, off).


operator(700,xfx,'in').

constraints in/2.


:- retractall(semiring(_)), assert(semiring(security)).

use_semiring(S) :-
        retractall(semiring(_)),
        assert(semiring(S)).


security @ [X] in A, [X] in B <=> semiring(security) |
        sec_comb(A, B, C), [X] in C.

sec_comb(A, B, C) :-
        union(A,B,C1),
        keysort(C1,C2),
        alltimes(C2,C,security).

alltimes([], [], _).
alltimes([A-W], [A-W], _) :-
	!.
alltimes([A-W1, A-W2|Def0], Def, S) :-
	!,
        times(S, W1, W2, W3),
        alltimes([A-W3|Def0], Def, S).
alltimes([A-W1|Def0], [A-W1|Def], S) :-
        alltimes(Def0, Def, S).


encryption @ [X] in A ==> semiring(security) |
        findall(enk(M1,M2)-V3,
	     (member(M1-V1,A),member(M2-V2,A),
	     atomic(M1), atomic(M2),
             plus(security,V1,V2,V3)),
	     B),
        [X] in B.



/*
decryption @ [X] in A ==> semiring(security) |
        findall(M1-V1,
             (member(inv(M2)-V2,A),member(enk(M2,M1)-V3,A),
             times(security,V2,V3,V1)),
	     B),
        [X] in B.
*/


decryption @ [X] in A <=> semiring(security) |
        findall(M1-V1,
		(   member(M0-V0, A),
		    (	M0 = enk(M2, M1),
		    	member(inv(M2)-V2,A),
			member(M2-_,A)
		    ->	times(security,V2,V0,V1)
		    ;	M1-V1 = M0-V0)),
		B),
        [X] in B.

concatenation @ [X] in A ==> semiring(security) |
        findall(pair(M1,M2)-V3,
             (member(M1-V1,A),member(M2-V2,A),
	     atomic(M1), atomic(M2),
             plus(security,V1,V2,V3)),
	     B),
        [X] in B.


/*
splitting @ [X] in A ==> semiring(security) |
        findall(M-V3,
             (member(pair(M1,M2)-V3,A),
	     (M=M1;M=M2)),
	     B),
        [X] in B.
*/

splitting @ [X] in A <=> semiring(security) |
        findall(M3-V0,
		(   member(M0-V0, A),
		    (	M0 = pair(M1, M2)
		    ->	(M3=M1; M3=M2)
		    ;	M3 = M0)),
		B),
        [X] in B.


% tracing

%[X] in A ==> write([X] in A),nl.


%% ---------------------------------------
%% Security semiring
%% The user has to assert use_semiring(security).

times(security,_,public,public).
times(security,public,_,public).
times(security,A,A,A).
times(security,unknown,private,private).
times(security,unknown,traded,traded).
times(security,private,unknown,private).
times(security,private,traded,traded).
times(security,traded,unknown,traded).	
times(security,traded,private,traded).	

plus(security,unknown,_,unknown).
plus(security,_,unknown,unknown).
plus(security,A,A,A).
plus(security,private,traded,private).
plus(security,private,public,private).
plus(security,traded,private,private).
plus(security,traded,public,traded).
plus(security,public,private,private).
plus(security,public,traded,traded).

idempotent(security).

zero(security, public).
one(security, unknown).

%%---------------------------------------------------------------
%% partial ordering over the semiring

leqs(A, B) :- plus(A, B, B).

%% Sometimes there seem to be several semiring facts,
%% so we need a cut here to avoid a choicepoint.
plus(W1,W2,W3) :- semiring(S), !, plus(S,W1,W2,W3).
times(W1,W2,W3) :- semiring(S), !, times(S,W1,W2,W3).
one(One) :- semiring(S), !, one(S, One).
zero(Zero) :- semiring(S), !, zero(S, Zero).


cal :-
	ca(Attack),
	fail.

ca(Attack) :-
	confidentiality_attack(Attack),
	writeln(Attack).


confidentiality_attack(Attack) :-
	use_semiring(security),
	initial([(A0, a), (B0, b), (C0, c)]),
	policy((A0, a), (B0, b)),
	policy((A0, a), (C0, c)),
	initial([(A1, a), (B1, b), (C1, c)]),
	imputable(A1, B1, C1),
	find_constraint(A0, [A0] in DefA0, _),
	find_constraint(B0, [B0] in DefB0, _),
	find_constraint(C0, [C0] in DefC0, _),
	find_constraint(A1, [A1] in DefA1, _),
	find_constraint(B1, [B1] in DefB1, _),
	find_constraint(C1, [C1] in DefC1, _),
	member((Agent, Def1, Def0), [(a, DefA1, DefA0), (b, DefB1, DefB0), (c, DefC1, DefC0)]),
	writeln(checking(agent(Agent))),
	attack(Def1, Def0, Attack).
	

attack([M-W1|_], Def0, attack(M, policy_level(W0), attack_level(W1))) :-
	(   member(M-W0, Def0)
	->  \+ leqs(W0, W1)
	;   W0 = unknown).
attack([_|Def1], Def0, Attack) :-
	attack(Def1, Def0, Attack).


%% Needham-Schroeder policy

initial(L) :-
	findall(T-W, (member((_, NA), L), member(T-W, [NA-public, k(NA)-public])), PK),
	initial1(L, PK).

initial1([], _).
initial1([(A, NA)|R], PK) :-
	[A] in [inv(k(NA))-private|PK],
	initial1(R, PK).

policy((A, NA), (C, NC)):-
[A] in [n(NA, NC)-traded],
[C] in [enk(k(NC),pair(n(NA, NC),NA))-traded],
[C] in [n(NC, NA)-traded],
[A] in [enk(k(NA),pair(n(NA, NC),n(NC, NA)))-traded],
[C] in [enk(k(NC),n(NC, NA))-traded].


%% Lowe's attack

imputable(A,B,C):-
[A] in [n(a, c)-traded],
[B] in [enk(k(b),pair(n(a, c),a))-traded],
[B] in [n(b, a)-traded],
[C] in [enk(k(a),pair(n(a, c),n(b, a)))-traded],
[A] in [enk(k(a),pair(n(a, c),n(b, a)))-traded],
[C] in [enk(k(c),n(b, a))-traded],
[B] in [enk(k(b),n(b, a))-traded].


union(A, B, D) :- append(A, B, C), remove_duplicates(C, D).


writeln(T) :- write(T), nl.

