% A Challenge-Response protocol
%
% MSR encoding of the TDL specification: processes communicate 
% via reconfigurable channels
%
% Initial States
% Note: The constant "zero" is treated as a global memory zero(Z)
%
%

rule([init],[initM(Z),fresh(X),zero(Z)],  {X>Z},initialize_system).
              
%
% the Main thread (initM) is always active and non deterministically 
% creates instances of Alice and Bob
% The local variable x is encoded as the sole argument of initM

%
% TDL Rule: initM -- id --> creatM [x:=new] 
%

rule([initM(_),fresh(X)],[create(Y),fresh(X1)], {X1>Y,Y>X},call_create).

%
% TDL Rule: create -- newA --> initM [run Alice with idA:=x,nA:=Zero,nB:=Zero] 
%

rule([create(Y),zero(Z)],[initM(Y),zero(Z),initA(Y,Z,Z)], {},create_alice).

%
% TDL Rule: create -- newB --> initM [run Bob with idA:=x,nA:=Zero,nB:=Zero] 
%

rule([create(Y),zero(Z)],[initM(Y),zero(Z),initB(Y,Z,Z)], {},create_bob).

%
% Alice starts the protocol and generates a fresh name 
%

%
% TDL Rule: initA -- fresh --> genA [nA:= new] 
%

rule([initA(I,_,M),fresh(U)],[genA(I,Na,M),fresh(U1)],{U1>Na,Na>U},alice_generates_a_fresh_name).

%
% Rendez-vous over a fixed port 
% The name N is passed from Alice to Bob
% Note: equality constraints are implicitly defined by the use of
% occurrences of the same variable (as for Na)
% 

%
% TDL Rules: genA  -- c!<nA> --> waitA [true] 
%            initB -- c?<x> --> waitA [nB:=x] 
%
% Note: c is a constant, it disappears in the MSR translation
%

rule([genA(I,Na,M), initB(Y,_,Q)],[waitA(I,Na,M),genB(Y,Na,Q)],{},alice_sends_nonce_Na_to_bob).

%
% Bob generates a fresh name Nb

%
% TDL Rule: initB -- fresh --> genB [mB:= new] 
%

rule([genB(I,Na,_), fresh(U)],[readyB(I,Na,Nb),fresh(U1)],{U1>Nb,Nb>U},bob_generates_a_fresh_name).

%
% Rendez-vous over a the channel name N (a variable local to Alice and Bob) 
% M is passed from Bob to Alice
%

%
% TDL Rules: genB  -- nB!<mB> --> waitA [true] 
%            initB -- nA?<y>  --> waitA [mA:=y] 
%
% Note: nB and nA are used here as communication ports
% In the following rule this is expressed via an implicit guard 
% waitA(I,Na,_)|readyB(Y,Na',Nb) .... Na=Na'
%

rule([waitA(I,Na,_),readyB(Y,Na,Nb)],[stopA(I,Na,Nb),stopB(Y,Na,Nb)],{},rendez_vous_over_Nb_for_alice_and_bob).

%
% Alice and Bob restart 
%

rule([stopA(I,_,_),zero(Z)],[initA(I,Z,Z),zero(Z)],           {},alice_restarts).

rule([stopB(I,_,_),zero(Z)],[initB(I,Z,Z),zero(Z)],           {},bob_restarts).

% 
% Seed of backward exploration: 
% The states in the "unsafe([unsafe(M1,C1),....,unsafe(Mk,Ck)])" list represents the "disjunction"
% M1:C1 or ... or Mk:Ck (their denotation is the union of the upward closure of the instances
% of every constrained configuration Mi:Ci
% This formula represents "violations" to a given Safety Property, e.g., Secrecy.
%
% Here we want to prove that it not possible that A and B 
% excahnge only the first nonce while concluding the protocol
%
% Thus, the possible violations are:
%
unsafe([         
	 unsafe([stopA(_,X,Y),stopB(_,X,Z)],{Y>Z}),
	 unsafe([stopA(_,X,Y),stopB(_,X,Z)],{Y<Z})
]).

%     
%
% Pruning with complement of invariant properties
% 
% All states subsumed by some constrained configuration M:C stored as inv(M,C)
% are removed during the symbolic backward exploration
% 
% Thus inv(M,C) denotes a "violation" of an invariant that must hold in any 
% protocol execution. However, if not used in 
% adequate way, they might render the analysis "incomplete". 
% 
% Here are invariants we can infer automatically from the initial state and the rules
% (adding them propagates information coming from the initial states into 
% the backward search)
%

invariants([inv([initM(_),initM(_)],{}),
            inv([create(_),create(_)],{})
            inv([init,init],{}),
            inv([fresh(_),fresh(_)],{}),
	    inv([zero(_),zero(_)],{})
	   ]).


% Test for the initial state

check(K,L):-
 f(K,[init],_,L,_,_).
 
trace(K,L):-
 check(K,L),
 tracer(K,L).