(** Contents :

   0: General House Keeping

   1: Syntax definitions 

   2: Equality, membership and extraction functions for the syntax
      2A: Equality functions
      2B: Membership functions
      2C: Extraction of submembers functions


   3: Substitution

   4: Ground terms and rules instances

   5: Tamarin Reduction

   6: Example

   7: Definitions from Chapter 5 of the thesis


   8: Tests and Definitions for Well formedness 
       8A: Functions to test no or One Input / Output in facts
       8B: Definitions on Variables and Terms  for Equivalence proof 
       8C: Well formedness definitions 
       
    9: Some useful lemmas on well formedness

   10: Definitions from Chapter 6 of the thesis
      10A: Types of Facts allowed in the system  

   11: Props and Theorems from Chapter 6 

**)


Load Sec5_TamarinReduction.



(** ===================== 
  *** 6: Example  
 ===================== **)
(* This section shows how we can generate a trace for an example 
   Tamarin protocol, taken from https://github.com/tamarin-prover/manual/blob/master/code/NSLPK3.spthy *)

(* First we define that rules that model an attacker: *)
Definition varX : term := Bterm (Var "x") .
Definition varY : term := Bterm (Var "Y") .
Definition AttackerReceive (ts:terms) : rule := RuleProto [ OUT ts ] emptyLabel [ K ts ].
Definition AttackerReceive1 : rule := RuleProto [ OUT [varX] ] emptyLabel [ K [varX] ].
Definition AttackerReceive2 : rule := RuleProto [ OUT [varX;varY] ] emptyLabel [ K [varX]; K [varY] ].
Definition AttackerSend (ts:terms) : rule := RuleProto [ K ts ] emptyLabel [ IN ts ].
Definition AttackerSend1 : rule := RuleProto [ K [varX] ] emptyLabel [ K [varX] ].
Definition AttackerSend2 : rule := RuleProto [ K [varX]; K [varY] ] emptyLabel [ IN [varX; varY] ].
Definition LtkFact : name := Pub "LtkFact".
Definition ltkA_var : baseTerm := (Var  "ltkA").
Definition ltkB_var : baseTerm := (Var  "ltkB").
(* 
Definition ltkA_var : freshNameSetup := "ltkA".
Definition ltkB_var : freshNameSetup := "ltkB".
 *)
Definition PkFact : name := Pub "PkFact".
Definition PkName : string := "Pkname".
Definition Pk : string := "Pkname".
Definition A : term := Bterm (Name (Pub "A")).
Definition B : term := Bterm (Name (Pub "B")).
Definition C : term := Bterm (Name (Pub "C")).

(* The first protocol setup rule is:
rule Register_pk:
  [ Fr(~ltkA) ]
  -->
  [ !Ltk($A, ~ltkA), !Pk($A, pk(~ltkA)), Out(pk(~ltkA)) ]
*)

(* $A means any constant, we model this here by making multiple copies of the rule.
   As our key theorem will be of the form, forall rule list ..., this is valid *)


Definition registerPKruleA : rule := RuleSetup [ FR_P ltkA_var ] emptyLabel 
                                [STATE LtkFact [A;   (Bterm ltkA_var)]; STATE PkFact [A; Func PkName [ltkA_var]];
                                       OUT [Func PkName [ltkA_var]] ].


Definition registerPKruleB : rule := RuleSetup [ FR_P ltkB_var ] emptyLabel 
                                [STATE LtkFact [B;  (Bterm ltkB_var)]; STATE PkFact [B; Func PkName [ltkB_var]]; 
                                          OUT [Func PkName [ltkB_var]] ].
 

(* The rule for the first step of the protocol models the sending of the first message:
rule I_1:
  let m1 = aenc{'1', ~ni, $I}pkR
  in
    [ Fr(~ni), !Pk($R, pkR) ]
  --[ OUT_I_1(m1)]->
    [ Out( m1 ), St_I_1($I, $R, ~ni)]

*)
Definition St_I_1 : name := Pub "St_I_1".

Definition ni : baseTerm := (Var  "ni"). 

(* Definition ni : freshNameProto := "ni". *)

Definition m1 : term :=  Func "aenc" [ ni; (Name (Pub "A"))].

Definition I_1_A_to_B : rule := RuleProto  [(FR_P  ni); STATE PkFact [B; Func PkName [ltkB_var]]]  
                                      (BasicLabel [ ActLabel (Pub "Out") [m1] ])
                                      [OUT [m1]; STATE St_I_1 [A; B; (Bterm ni)]; STATE PkFact [B; Func PkName [ltkB_var]]].

(* This rule only let's "A" send the first message. We would need more rules to model others starting the protocol *)

(* The whole protoocl is modelled by all of the rules:*)
Definition SetupAndProtocolRules : ruleList := [registerPKruleA; registerPKruleB; I_1_A_to_B].


(* The first step of the protocol is to generate a fresh name for A *)
Lemma protocolRun1Step : run SetupAndProtocolRules [] [] [FR_P (Name (Fresh_P "ltkA")) ].
Proof.
  apply Run_FreshStepP with (fn:="ltkA") (f2:= [FR_P (Name (Fresh_P "ltkA")) ]).
  + apply (SetupFreshNameStep "ltkA").
  + apply Run_Stop.
Qed.

(* The second step of the protocol is to generate a fresh name for B *)
Lemma protocolRun2Step : run SetupAndProtocolRules [] [] 
              [FR_P (Name (Fresh_P "ltkB")); FR_P (Name (Fresh_P "ltkA"))].
Proof.
  apply Run_FreshStepP  with (fn:="ltkA") (f2:= [FR_P (Name (Fresh_P "ltkA")) ]).
  + apply (SetupFreshNameStep "ltkA").
  +   apply Run_FreshStepP  with (fn:="ltkB") (f2:= [FR_P (Name (Fresh_P "ltkB")); FR_P (Name (Fresh_P "ltkA"))]).
    - apply (SetupFreshNameStep "ltkB") with (fs:=[FR_P (Name (Fresh_P "ltkA")) ]).
    - apply Run_Stop.
Qed.

(* The third step of the protocol, sets up A's keys using the registerPKruleA rule*)
(* For this we need a substitution that maps the variable "ltkA" to a name:*)

Definition mapLtkAvarToName := "ltkA" !-> Fresh_P "ltkA"; subs_empty.

(* This is the ground version of the rule we will use: *) 
Definition registerPKruleAground : rule := RuleSetup [ FR_P (Name (Fresh_P "ltkA")) ] 
                                emptyLabel 
                                [STATE LtkFact [A; Bterm (Name (Fresh_P "ltkA"))]; 
                                 STATE PkFact [A; Func PkName [(Name (Fresh_P "ltkA"))]]; 
                                 OUT [Func PkName [(Name (Fresh_P "ltkA"))]] ].

Lemma protocolRun2to3Step : run SetupAndProtocolRules
              [FR_P (Name (Fresh_P "ltkB")); FR_P (Name (Fresh_P "ltkA"))]
              []
              [STATE LtkFact [A; (Bterm (Name (Fresh_P "ltkA")))]; 
               STATE PkFact [A; Func PkName [(Name (Fresh_P "ltkA"))]]; 
               OUT [Func PkName [(Name (Fresh_P "ltkA"))]];
               FR_P (Name (Fresh_P "ltkB"))].
Proof.
  eapply Run_Step_Silent.
   + unfold SetupAndProtocolRules. unfold reduceWithRules. exists registerPKruleAground. split. 
     - apply GinstHead. apply Ginst. split. 
       * exists mapLtkAvarToName. reflexivity.
       * unfold groundRule. unfold registerPKruleAground. split. 
        unfold groundFacts. split. reflexivity. reflexivity. split. unfold groundFacts. split. 
        unfold groundFact. unfold groundTerms. split. reflexivity. split. reflexivity. 
        reflexivity. split. unfold groundFact. unfold groundTerms. split. reflexivity. split.
        unfold groundTerm. unfold groundBaseTerms. split. reflexivity. reflexivity. reflexivity.
        unfold groundFact. unfold groundTerms. split. split.  unfold groundTerm. 
        unfold groundBaseTerms. split. reflexivity. reflexivity. reflexivity. reflexivity. reflexivity.
     - apply R_match. simpl. auto. 
   + apply Run_Stop. 
Qed.


Lemma protocolRunToStop3: run SetupAndProtocolRules [] []
              [STATE LtkFact [A; (Bterm (Name (Fresh_P "ltkA")))]; 
               STATE PkFact [A; Func PkName [(Name (Fresh_P "ltkA"))]]; 
               OUT [Func PkName [(Name (Fresh_P "ltkA"))]];
               FR_P (Name (Fresh_P "ltkB"))].
Proof.
  eapply runTransitive with (l1:=[]) (l2:=[]). split. apply protocolRun2Step.
  apply protocolRun2to3Step.
Qed.