(** 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 Sec10_Chap6Defs.


(**=======================================================
**** 11: Props and Theorems from Chapter 6 
==========================================================**)


(* Proposition 1 Given a valid rule list  RL=[R1,..,R_j]  and 
a normal run of the protocol with rules  using  sigma_1, .., sigma_j  as substitutions
for the reductions in each step of the run. If the variable  v  is directly linked 
as per Def6_5_variableDirectlyLinked in the rule  R_j  w.r.t.  [R_1,..,R_{j-1}]  
then either  v  does not appear in    [R_1,..,R_{j-1}]  
or "there exists some  sigma_i  such that   sigma_i(v)=sigma_j(v)  and  not (i=j)"
i.e., sigma_j is the last element and sigma_i is present in the list of sigmas anywhere but at the end.
*)


Axiom Prop1_DirectlyLinkedVariablesHaveSameValues : forall fs1 fs2 sigma_j tr v r rlProto rlSetup SigmaList,
        ((Def6_9_validRuleList (appendAny rlProto [r]) 
              /\ runInOrderSigma (appendAny rlProto [r]) rlSetup (appendAny SigmaList [sigma_j]) fs1 tr fs2))                               

          -> ((Def6_5_variableDirectlyLinked v r rlProto)
                ->     (variableIsNew v rlProto)  
                        \/                   
                         (exists sigma_i, (eq_name (sigma_i v) (sigma_j v))  
                                   /\ ((member sigma_i SigmaList)))
                          ).
(* 
Proof.
  intros.
  inversion H0.
  - destruct rlProto. 
    + inversion H1.
    + destruct reverseHeadList with (h:=r0) (ts:=rlProto). inversion H2.
      rewrite H3. unfold variableInInputAndOutput in H1.
      inversion H1. inversion H4. inversion H5. inversion H7.
      right. exists ( lastElement subs_empty  SigmaList). split.
      * apply termsEqDiffSigma with (trms1:=x2) (trms2:=x3). split. 
        eapply outputMatchesNextInputEnd with (rulesList := x0). inversion H. rewrite H3 in H11. 
        rewrite appendAnyAppendAny in H11. apply H11.
       unfold appendAny in H11.  apply H11.   
  
 *)

(* Proposition 2 Given a valid rule list  RL=[R_1,..,R_j]  and 
a normal run of the protocol with rules using  sigma_1, .., sigma_j  as substitutions
for the reductions in each step of the run. If the variable  v  is directly linked 
as per Def6_6_variableIndirectlyLinked in the rule  R_j  w.r.t.  [R_1,..,R_{j-1}]  
then either  v  does not appear in    [R_1,..,R_{j-1}]  
or there exists some  sigma_i such that  sigma_i(v)=sigma_j(v) and not (i=j). 
*)


Axiom Prop2_IndirectlyLinkedVariablesHaveSameValues : forall fs1 fs2 sigma_j tr v r rlProto rlSetup SigmaList,
        ((Def6_9_validRuleList (appendAny rlProto [r]) 
              /\ runInOrderSigma (appendAny rlProto [r]) rlSetup (appendAny SigmaList [sigma_j]) fs1 tr fs2))                               
          -> ((Def6_6_variableIndirectlyLinked v r rlProto)
                ->     (variableIsNew v rlProto)  
                        \/                   
                         (exists sigma_i, (eq_name (sigma_i v) (sigma_j v))  
                                   /\ ((member sigma_i SigmaList)))
                          ).


(* Proposition 3 Given a valid rule list RL and a normal run of the protocol let
sigma_1,..sigma_n be the substitutions used for the reductions in each step of the run, then
there exists a substitution sigma such for all sigma_i and v in domain(sigma_i); 
sigma(v) = sigma_i(v).*)

Axiom Prop3_AllSigmasCanBeReplacedbyASingleSigma : forall fs1 fs2 tr r rlProto rlSetup SigmaList,
        (Def6_9_validRuleList (appendAny rlProto [r]) 
               /\  runInOrderSigma (appendAny rlProto [r]) rlSetup SigmaList fs1 tr fs2)
                   -> (exists sigma, forall v sigma_i, (Def6_7_validVariable r rlProto v) 
                          /\ (member sigma_i SigmaList)
                        ->   (eq_name (sigma_i v) (sigma v))
                        ).


Axiom Prop4_ExistsTraceAndSigmaForTemplate : forall  allowSeq rlSetup rlp tr_temp, 
        (Def6_9_validRuleList rlp /\ Def5_3_Valid_AllowSequences allowSeq rlp)
          -> exists tr_log sigma SigmaList, Def5_7_Standard_Trace allowSeq rlSetup SigmaList tr_log
                ->    (Def6_10_StdTemplate allowSeq [tr_temp])
                                  /\ (eq (applySubTrace sigma [tr_temp]) tr_log)
                                      /\ (member sigma SigmaList).


(* Theorem 1 Given a valid rule list RL, for every standard trace with logs
tr_log, there exists a template tr_template of RL and a substitution sigma such as
sigma(tr_template) = tr_log. *)
Theorem Thm_6_1_ExistsTemplateAndSigmaForTrace : forall  allowSeq rlSetup rlp tr_log, 
        (Def6_9_validRuleList rlp /\ Def5_3_Valid_AllowSequences allowSeq rlp)
          ->  exists SigmaList, Def5_7_Standard_Trace allowSeq rlSetup SigmaList tr_log
                ->    exists tr_template sigma, (Def6_10_StdTemplate allowSeq tr_template)
                                  /\ (eq (applySubTrace sigma tr_template) tr_log)
                                      /\ (member sigma SigmaList).


(** Def 6.13 Equivalent (n1,n2) **)

Inductive Def6_13_Equivalent : ruleList -> term  -> term -> Prop :=
     | Def613_IO          : forall newRule pastRules ts1 ts2 t1 t2,  
                           (member (IN ts1) (premiseFacts newRule))
                              /\ lastOutputNoInput ts2 pastRules
                                /\ TermsInSamePosition ts1 ts2 t1 t2  ->
                                      Def6_13_Equivalent (newRule::pastRules) t1 t2
     | Def613_SamePosUSF  : forall RL usf t1 t2,  
                            (PresentInSamePositionUSF RL usf t1 t2) -> 
                                      Def6_13_Equivalent RL t1 t2
     | Def613_SamePosUAF  : forall RL t1 t2 uaf,  
                            ((PresentInSamePositionUAF RL uaf t1 t2)
                             /\
                             (exists t3 t4, (PresentInSamePositionUAF RL uaf t3 t4)
                              /\
                                   (not ((eq_term t1 t3) \/ (eq_term t1 t4) 
                                        \/ (eq_term t2 t3)\/ (eq_term t2 t4)))
                                /\ (not (PresentInSamePositionUAF RL uaf t1 t3))
                                /\ (not (PresentInSamePositionUAF RL uaf t2 t4))
                                /\ Def6_13_Equivalent RL t3 t4))
                                   ->
                                    Def6_13_Equivalent RL t1 t2
     | Def613_EmptyFunc   : forall RL fn ,  
                          (Def6_13_Equivalent RL (Func fn []) (Func fn []))

     | Def613_FuncList      : forall RL fn t1 t2 t3 t4,  
                          (Def6_13_Equivalent RL (Func fn (t1::t3)) (Func fn (t2::t4))) ->
                            Def6_13_Equivalent RL (Bterm t1) (Bterm t2) ->
                              Def6_13_Equivalent RL (Func fn t3) (Func fn t4)
     | Def613_Reflexive  : forall RL n1 ,  
                          (Def6_13_Equivalent RL n1 n1)

     | Def613_Symmetric  : forall RL n1 n2 ,  
                          (Def6_13_Equivalent RL n1 n2) ->
                                          (Def6_13_Equivalent RL n2 n1)
     | Def613_Transitive : forall RL n1 n2 n3 ,  
                            (Def6_13_Equivalent RL n1 n2) 
                                    /\ (Def6_13_Equivalent RL n2 n3) ->
                                                (Def6_13_Equivalent RL n1 n3). 


                          
Fixpoint isEquivalent (rl:ruleList) (t1:term) (t2:term) : bool :=
  match (Def6_13_Equivalent rl t1 t2) with
      | True    =>  true
  end.

(* A helper definition for Def 9 to return one equivalent term for t1 *)
Fixpoint DefequivalentTerm (rl:ruleList) (t1:term) (t2:term) : term :=
  match (isEquivalent rl t1 t2) with
    | true    => t2 
    | false   => t1
  end.

(*How to collect all values returned by earlier def?*)
Inductive Def6_15_EquivalenceClass: ruleList -> term -> terms -> Prop :=  
  | Eqv_base  : forall rl t1, Def6_15_EquivalenceClass rl t1 [t1]
  | Eqv_step  : forall rl t1 t2 ts, Def6_13_Equivalent rl t1 t2 -> Def6_15_EquivalenceClass rl t1 ts 
                                -> not (member t2 ts) -> Def6_15_EquivalenceClass rl t1 (t2::ts).

Fixpoint isEquivalenceClass (rl:ruleList) (t1:term) (ts:terms) : bool :=
  match (Def6_15_EquivalenceClass rl t1 ts) with
      | True    =>  true
  end.


Axiom equivalentClassProperty : forall rl t ts t1 t2 f1 f2 l1 l2,
    Def6_9_validRuleList rl -> 
        Def6_15_EquivalenceClass rl t ts ->
          (member t1 ts) /\ (member t2 ts) -> 
            ((eq_term t1 (Bterm (Name (Pub n))) -> ((eq_term t1 t2) \/ (eq_term t2 (Bterm (Var x)))))
            \/ ((eq_term t1 (Func f1 l1 )) -> ((eq_term t2 (Func f2 l2 )) \/ (eq_term t2 (Bterm (Var x)))))).

Axiom Prop5_sigmaOfTermsSameForEquivalenceClass : forall rl rlSetup fs1 tr fs2 sigmaList sigma t t1 t2 ts,
    Def6_9_validRuleList rl -> 
          runInOrderSigma rl rlSetup sigmaList fs1 tr fs2 ->
              Def6_15_EquivalenceClass rl t ts ->
                (member t1 ts) /\ (member t2 ts) /\ (member sigma sigmaList) ->
                          (eq_term (applySubTerm sigma t1) (applySubTerm sigma t2)).



Fixpoint termAppearsInFacts (fs: facts) (tm:term) : Prop := 
  match fs with
    | f1::fss => (match f1 with 
                        | IN   ts => member tm ts 
                        | OUT  ts => member tm ts
                        | K    ts => member tm ts
                        | STATE n ts => member tm ts
                        | FR_P bt => eq_term (Bterm bt) tm 
                  end ) \/ termAppearsInFacts fss tm
    | []      => False 
  end.


Fixpoint termAppearsInRuleList (rl: ruleList) (tm:term) : Prop := 
  termAppearsInFacts (appendAny (allPremiseFacts rl) (allConclFacts rl)) tm.

Fixpoint termsFromFacts (fs: facts): list term  := 
  match fs with
    | f1::fss => appendAny (match f1 with 
                        | IN   ts => ts 
                        | OUT  ts => ts
                        | K    ts => ts
                        | STATE n ts => ts
                        | FR_P bt => [Bterm bt]
                  end ) (termsFromFacts fss) 
    | []      => []
  end.


Fixpoint AllTermsFromRuleList (rl: ruleList) : list term := 
  uniqueTerms (termsFromFacts (appendAny (allPremiseFacts rl) (allConclFacts rl))).


Fixpoint Def_ListArgs (uaf:fact) (r:rule) : terms :=
match (Def6_8_validRule r []) /\ (uniqueArgumentsFact uaf r []) with
    | True    =>   match uaf with 
                   | STATE n ts =>  ts
                   | _          => []
                   end
end.

Definition Def6_16_LinkedEqClasses (rl:ruleList) (e1:terms) (e2:terms) : Prop :=
    forall t1 t2,
        Def6_9_validRuleList rl /\ 
           Def6_15_EquivalenceClass rl t1 e1 /\
              Def6_15_EquivalenceClass rl t2 e2 
                ->
                  exists uaf a1 a2 r, 
                            (member a1 e1) /\ 
                            (member a2 e2) /\
                            (uniqueArgumentsFact uaf r rl) /\
                            (member a1 (Def_ListArgs uaf r)) /\
                            (member a2 (Def_ListArgs uaf r)) /\
                            (member r rl).

Definition termEqTogether (rl:ruleList) (t:term) (t1:term) : terms :=
    if (isEquivalent rl t t1) then uniqueTerms (appendAny [t] [t1]) else  [t1].
  

Fixpoint termsEqTogether (rl:ruleList) (t:term) (ts:terms) : terms :=
 match ts with
    | ts1::tss   => uniqueTerms (appendAny (termEqTogether rl t ts1) ( termsEqTogether rl t tss))
    | []        =>  []
  end.

(*Eq class for one term*)
Fixpoint singleEqClass (rl:ruleList) (t:term)  : terms := 
      termsEqTogether rl  t (AllTermsFromRuleList rl) .

(*Eq classes for all terms*)
Fixpoint EqClassesTogether (rl:ruleList) (ts:terms) : list terms :=
 match ts with
    | ts1::tss   =>  (singleEqClass rl ts1)::( EqClassesTogether rl tss)
    | []        =>  []
  end.

(*Set of Eq classes for all terms*)
Fixpoint SetofEqClasses (rl:ruleList)  : list terms :=
    EqClassesTogether rl (AllTermsFromRuleList rl).

(**Def 6.17??**)

Definition Def_MinEqSet (rl:ruleList) (EqOfEq:list terms) : Prop :=
    forall EqSet eq1 eq2,
        Def6_9_validRuleList rl /\ 
           eq  EqSet (SetofEqClasses rl) 
                ->
                 member eq1 (SetofEqClasses rl) /\
                    member eq2 EqOfEq /\
                      Def6_16_LinkedEqClasses rl eq1 eq2.


Fixpoint SetupUAFsFromRL (RL:ruleList): list fact := 
  match RL with
    | (RuleSetup f1 l1 f2)::rs  =>  appendAny (collectUniqueArgFacts f1 (RuleSetup f1 l1 f2) rs) 
                                                 (SetupUAFsFromRL rs)
    | (RuleProto _ _ _)::rs     => SetupUAFsFromRL rs
    | []                        =>  []
  end.



Fixpoint ProtocolUAFsFromRL (RL:ruleList): list fact := 
  match RL with
    | (RuleProto f1 l1 f2)::rs  =>  appendAny (collectUniqueArgFacts f1 (RuleSetup f1 l1 f2) rs) 
                                                 (ProtocolUAFsFromRL rs)
    | (RuleSetup _ _ _)::rs     => ProtocolUAFsFromRL rs
    | []                        =>  []
  end.


Fixpoint TermsFromUAFs (ft:facts): list term :=
  match ft with
    | (STATE nm tm)::fs =>  appendAny tm (TermsFromUAFs fs)
    | _::fs             => TermsFromUAFs fs
    | []                =>  []
  end.
  



Fixpoint AllBaseTerms (btm:list baseTerm) : list term :=
  match btm with
    | bt1::bts    => (Bterm bt1) :: (AllBaseTerms bts)
    | []          => []
  end.

Fixpoint subTermsFromTerms (tm:list term) : list term :=
    match tm with
      | t1::ts    => match  t1 with
                          | Bterm _   => t1::(subTermsFromTerms ts)
                          | Func nm bts  => appendAny (AllBaseTerms bts) (subTermsFromTerms ts)
                    end
      | []      =>  []
    end.

Fixpoint termsFromActionLabel (al:actionLabel) : list term :=
    match al with
      | ActLabel nm ll           => subTermsFromTerms ll
    end.

Definition termsFromActionLabels : (list actionLabel) -> list term := mapListFunction termsFromActionLabel.

Fixpoint termsFromLabel (lb:label) : list term :=
    match lb with
      | BasicLabel ll           => termsFromActionLabels ll
      | LoggedLabel lg ll       => appendAny (termsFromActionLabel lg) (termsFromActionLabels ll)
      | LoggedSIDLabel t lg ll  => appendAny (termsFromActionLabel lg) (termsFromActionLabels ll)
    end.


Fixpoint termsFromTemplate (tmp:trace) : list term :=
    match tmp with
      | l1::ls    => appendAny (termsFromLabel l1) (termsFromTemplate ls)
      | []        =>  []  
    end.


Fixpoint rewriteBaseTerm (bt:baseTerm) (t1:term) (t2:term) : baseTerm :=
   match t1, t2 with
      | Bterm told, Bterm tnew  =>  if (beq_baseTerm bt told) then tnew else bt 
      | _, _                    =>  bt
  end.


Fixpoint rewriteBaseTerms (lbt:baseTerms) (t1:term) (t2:term) : baseTerms :=
   match lbt with
      | bt1::bts    =>  (rewriteBaseTerm bt1 t1 t2)::(rewriteBaseTerms bts t1 t2)
      | []          =>  []
  end.

(*This version will allow replacing of baseterms inside the functions.
  N.B.:We do not support functions as aurguments of function *)

Fixpoint rewriteTerms (tm:terms) (t1:term) (t2:term) : terms :=
   match tm with
      | tm1::tms    =>  match tm1 with
                        | Func fn lbt => if (beq_term tm1 t1) then ((Func fn (rewriteBaseTerms lbt t1 t2))::(rewriteTerms tms t1 t2))
                                  else  (tm1::(rewriteTerms tms t1 t2))

                        | Bterm bt    => if (beq_term tm1 t1) then (t2::(rewriteTerms tms t1 t2))
                                  else  (tm1::(rewriteTerms tms t1 t2))
                      end
      | []        => []
   end. 



Fixpoint rewriteTermsInActionLabel (al:actionLabel) (t1:term) (t2:term) := 
  match al with
      | ActLabel nm ll          => ActLabel nm  (rewriteTerms ll t1 t2)
    end.


Fixpoint rewriteTermsInActionLabels (als:list actionLabel) (t1:term) (t2:term) := 
  match als with
      | al1::alss => (rewriteTermsInActionLabel al1 t1 t2)::( rewriteTermsInActionLabels alss t1 t2)
      | []        => []
    end.

Fixpoint rewriteTermsInLabel (lbl:label) (t1:term) (t2:term)  := 
  match lbl with
      | BasicLabel ll           => BasicLabel (rewriteTermsInActionLabels ll t1 t2)
      | LoggedLabel lg ll       => LoggedLabel (rewriteTermsInActionLabel lg t1 t2)  (rewriteTermsInActionLabels ll t1 t2) 
      | LoggedSIDLabel t lg ll  => LoggedSIDLabel t (rewriteTermsInActionLabel lg t1 t2) (rewriteTermsInActionLabels ll t1 t2)
    end.

(* "funPresent ft trms" returns "ft" if no function term present in terms else returns a function term *)

Fixpoint funPresent (ft:term) (eqtrms:terms) : term :=
  match eqtrms with
    | eq1::eqs    =>  match eq1 with
                        | Func _ _  => eq1
                        | _         => funPresent ft eqs
                      end
    | []          => ft
  end.



Fixpoint termIsFunc (ft:term) : Prop :=
  match ft with
    | Func _ _  => True
    | _         => False
  end.


Fixpoint b_termIsFunc (ft:term) : bool :=
  match ft with
    | Func _ _  => true
    | _         => false
  end.

Fixpoint b_pubTerm (ts:baseTerm) : bool :=
  match ts with
    | Name n => true
    | _ => false
  end.

Definition b_pubTerms : baseTerms -> bool := btrueForOne b_pubTerm.

(* "pubPresent ft trms" returns "pb" if no public name  present in terms else returns a public name *)

Fixpoint pubPresent (pb:term) (eqtrms:terms) : term :=
  match eqtrms with
    | eq1::eqs    =>  match eq1 with
                        | Bterm (Name nm1)   => eq1
                        | _                  => pubPresent pb eqs
                      end
    | []          => pb
  end.


Fixpoint termIsPub (t:term) : Prop :=
  match t with
    | Bterm (Name (Pub _))   =>  True
    | _           =>  False
  end.



Fixpoint b_termIsPub (t:term) : bool :=
  match t with
    | Bterm (Name (Pub _))    =>  true
    | _                       =>  false
  end.


Definition Def6_18_ProtocolUAFs (rl:ruleList) (EqOfEq:list terms) (uafList:facts): Prop :=
    forall r uaf eqClass rlProto rlSetup,      
                Def6_9_validRuleList rl /\ 
                eq rl (appendAny rlSetup rlProto) /\
                  Def_MinEqSet rl EqOfEq /\
                    (someCommonElements (Def_ListArgs uaf r) eqClass) /\
                      (member r rlProto) /\ (member eqClass EqOfEq) /\ (member uaf uafList).

(* (*Conver Def 6.18 and 6.19 to Function*)

Definition FinalProtocolUAFs (RL:ruleList) (uafList:facts) (EqOfEq:list terms): facts :=
  match uafList with
    | uaf1::uafs   =>  match (TermsFromUAFs uaf1) with
                              | tm1::tms  => match (someCommonElements (singleEqClass RL tm1) EqOfEq) with
                                                | True  =>  uaf1::(FinalProtocolUAFs RL uafs EqOfEq)
                                                | _     =>  FinalProtocolUAFs RL uafs EqOfEq
                                            end
                              | []        =>  []
                      end
   | []        =>  []
  end.

    forall r uaf eqClass rlProto rlSetup,      
                Def6_9_validRuleList rl /\ 
                eq rl (appendAny rlSetup rlProto) /\
                  Def_MinEqSet rl EqOfEq /\
                    (someCommonElements (Def_ListArgs uaf r) eqClass) /\
                      (member r rlProto) /\ (member eqClass EqOfEq) /\ (member uaf uafList).


Definition Def6_18_ProtocolUAFs (rl:ruleList) (EqOfEq:list terms): facts :=
  FinalProtocolUAFs (ProtocolUAFsFromRL rl) EqOfEq.
 *)

Fixpoint TermsInSameNameAndPositionUAF (uaf1:fact) (uaf2:fact) (t1:term) (t2:term) : Prop :=
  match uaf1, uaf2 with
   | STATE nm1 tm1, STATE nm2 tm2   => (eq_STATEname uaf1 uaf2) /\ (TermsInSamePosition tm1 tm2 t1 t2)
   | _, _                           => False
  end.


Definition TermsMatchSetupAndProtoUAFs (EqOfEq:list terms) (uafPList:facts) (uafSList:facts) : Prop :=
  forall tp1 tp2 ts eqClass uafS uafP1 uafP2, 
                          (member tp1 eqClass) /\  (member tp2 eqClass) /\ 
                            (member eqClass EqOfEq) /\ 
                                (member tp1 (TermsFromUAFs uafPList)) /\ (member tp2 (TermsFromUAFs uafPList)) /\ 
                                   (member uafP1 uafPList) /\  (member uafP2 uafPList) /\ 
                                      (TermsInSameNameAndPositionUAF uafP1 uafP2 tp1 tp2) /\
                                     (member uafS uafSList) -> 
                                        (TermsInSameNameAndPositionUAF uafP1 uafS tp1 ts) /\
                                        (TermsInSameNameAndPositionUAF uafP2 uafS tp2 ts).


Definition Def6_19_MatchingSetupUAFs (rl:ruleList) (EqOfEq:list terms) (uafSList:facts): Prop :=
    forall  uafPList,      
                Def6_9_validRuleList rl /\ 
                        Def_MinEqSet rl EqOfEq /\
                          Def6_18_ProtocolUAFs rl EqOfEq uafPList /\
                            (eq (SetupUAFsFromRL rl) uafSList) ->
                                  TermsMatchSetupAndProtoUAFs EqOfEq uafPList uafSList.


(* Define a 1-to-1 function from Eq to term  *)

(* Either replace all the terms in one go or use the function to return a specific term from each Eq class and use it in 
template for rewriting *)

Fixpoint EqToTerm_CaseA (eq:terms) (t:term): term :=
  match eq with
    | eq1::eqs  =>  if (b_termIsFunc eq1) then eq1 else (EqToTerm_CaseA eqs t)
    | []        =>  t
  end.


Fixpoint EqToTerm_CaseB (eq:terms) (t:term): term :=
  match eq with
    | eq1::eqs  =>  if (b_termIsPub eq1) then eq1 else (EqToTerm_CaseB eqs t)
    | []        =>  t
  end.


Fixpoint EqToTerm_CaseC (eq:terms) (t:term) : term :=
  match eq with
    | eq1::eqs  =>  eq1
    | []        =>  t
  end.


Inductive rewriteWithRules: label -> ruleList ->  label -> Prop :=  
  | lblcaseA   : forall t RL lbl1, ((In t (termsFromLabel lbl1)) /\
                  not (eq_term (EqToTerm_CaseA (singleEqClass RL t) t) t)) -> 
                  rewriteWithRules lbl1 RL (rewriteTermsInLabel lbl1 t (EqToTerm_CaseA (singleEqClass RL t) t))


  | lblcaseB   : forall t RL lbl1, ((In t (termsFromLabel lbl1)) /\
                  not (eq_term (EqToTerm_CaseB (singleEqClass RL t) t) t)) -> 
                  rewriteWithRules lbl1 RL (rewriteTermsInLabel lbl1 t (EqToTerm_CaseB (singleEqClass RL t) t))


  | lblcaseC   : forall t RL lbl1, ((In t (termsFromLabel lbl1)) /\
                      (eq_term (EqToTerm_CaseA (singleEqClass RL t) t) t)
                        /\
                        (eq_term (EqToTerm_CaseB (singleEqClass RL t) t) t))
                               -> 
                          rewriteWithRules lbl1 RL (rewriteTermsInLabel lbl1 t (EqToTerm_CaseC (singleEqClass RL t) t)).

Definition noOtherEquivalentTermsPresent (t1:term) (tmp:trace) (RL:ruleList)  := 
 not (exists t2, (In t2 (termsFromTemplate tmp)) 
                    /\ (In t2 (singleEqClass RL t1))  
                        /\  not (eq_term t1 t2)).



(*Need to continue rewriting till we have a template in its normal form *)
Inductive Def6_20_PreRewriteTemplate: trace -> ruleList -> trace -> Prop := 
   | Case_Base          : forall RL , Def6_20_PreRewriteTemplate [] RL []
   | case_Step          :  forall l1 l2 RL t1 t2, (rewriteWithRules l1 RL l2) 
                              -> Def6_20_PreRewriteTemplate t1 RL t2
                                  -> Def6_20_PreRewriteTemplate (l1::t1) RL (l2::t2).

(* "TemplateNormalForm" holds when for each term, there must be nothing else in the same equivalent class.
I.e., Any equivalence class generated here must only have a single member. *)

Definition Def_6_20_1_TemplateNormalForm (tmp:trace) (RL:ruleList)  := 
forall t1, (In t1 (termsFromTemplate tmp))  ->     (noOtherEquivalentTermsPresent t1 tmp RL) 

                                                  /\    exists tf, 
                                                          (In tf (singleEqClass RL t1)) /\ (termIsFunc tf) ->
                                                               (eq_termFuncName t1 tf)

                                                  /\    exists tp, 
                                                          (In tp (singleEqClass RL t1) /\ (termIsPub tp) ->
                                                               (eq_term t1 tp)).
 

(* Lemma: if RL is WF, exists tmp2 which is a product of 6.20 and leads to a normal form *)

Axiom normalFormExistsForEveryTmp : forall tmp f2 RL, 
    Def6_9_validRuleList RL /\
          Def6_2_wellformedRulesFromState f2 RL /\
            Def6_10_StdTemplate [RL] tmp  
               -> exists tmp1, 
                    Def6_20_PreRewriteTemplate tmp RL tmp1 /\
                                Def_6_20_1_TemplateNormalForm tmp1 RL.
(* Proof.
      intros. exists tmp. split. inversion H. inversion H1.
      + destruct RL.
        -  destruct tmp.
            * apply Case_Base.
            * destruct l.
 *) 

Definition Def_6_20_2_InstantiateTemplate (tmp1:trace) (RL:ruleList) (tmp2:trace): Prop := 
exists sigma, forall uafP, 
                  (In uafP (ProtocolUAFsFromRL RL)) ->
                      exists uafS,  
                            (In uafS (SetupUAFsFromRL RL)) /\
                              (eq_fact uafS (applySubFact sigma uafP)) /\
                                  eq_trace tmp2 (applySubTrace sigma tmp1).


Definition Def6_20_3_RewriteTemplate (tmp1:trace) (RL:ruleList) (tmp2:trace): Prop :=
  exists tmp, (Def6_20_PreRewriteTemplate tmp1 RL tmp) /\
                  Def_6_20_1_TemplateNormalForm tmp RL  /\
                    Def_6_20_2_InstantiateTemplate tmp RL tmp2.


(* Lemma 6.4: Given a valid rule list $RL$ and a template $T$, the rewritten template 
using $\rewriteTemp{T}{RL}$ from Def \ref{rewritetemp} does not contain any variable 
$v$ with a function equivalent representation present in any equivalence class,
 \ie, $\forall~v~ \nexists~f, \eqName{v}{f(\_)}$.
 *)

Axiom Lemma6_4_noVariableWithFnEquivInEquivalentClass : forall rl tempT v newT,
        exists fn ft,
        (Def6_13_Equivalent rl (Bterm (Var v)) (Func fn ft)) /\
                            (Def6_20_3_RewriteTemplate tempT rl newT) -> 
                                  not (member v (getVarsInTemplate newT)) .

(* Theorem 2:Given a well-formed and valid rule list RL, a template T generated using RL,
the substitution sigma applied on all the variables of the rewritten templates
trace_{template} generated using rewriteTemp{T}{RL} from Def 6.20, 
there exists a standard run of the system using RL which generates 
the same trace trace_{log} matching this substitution on trace_{template}. *)

Theorem Thm_6_2_ExistsStdRunForRewrittenTemplate : forall  allowSeq rlSetup rlp tr_template sigma f2, 
        (Def6_9_validRuleList rlp) /\ (Def6_2_wellformedRulesFromState f2 rlp) /\ (eq allowSeq (allPrefixs rlp))
                    ->  exists tr_new tr_log, (Def5_3_Valid_AllowSequences allowSeq rlp) 
                          /\ (Def6_10_StdTemplate allowSeq tr_template) 
                            /\ (Def6_20_3_RewriteTemplate tr_template rlp tr_new) 
                                 /\ (eq (applySubTrace sigma tr_new) tr_log) 
                        ->  exists sigmaList fs1 fs2, 
                                      (runInOrderSigma rlp rlSetup sigmaList fs1 tr_log fs2)
                                        /\ (member sigma sigmaList).

Fixpoint LabelAt {A:Type} (n:nat) (l:list A) (default:A) {struct l} : A :=
    match n, l with
      | O, x :: l' => x
      | O, other => default
      | S m, [] => default
      | S m, x :: t => LabelAt m t default
    end.

Fixpoint indexExists {A:Type} (m:nat) (l:list A) : Prop :=
    match m, l with
      | O, x :: l' => True
      | O, other => False
      | S n, [] => False
      | S n, x :: t => indexExists n t 
    end.

(* The predicate "prefixSubSequence t1 t2" holds if "t1" is a subsequnece of "t2" *)

Fixpoint subSequenceTrace (t1:trace) (t2:trace): Prop :=
  match t1, t2 with
    | t11::t1s, t21::t2s  =>  ((eq_label t11 t21) /\ (subSequenceTrace t1s t2s))
                                    \/
                                (subSequenceTrace t1s t2) 
    | [], _               =>  True
    | _, []               =>  False
  end.

(*Def 6.21 Correspondence*)
Definition Def6_21_Correspondence (tr_temp:trace) (tr_log:trace) (m:nat) (sigma:substitution) : Prop := 
 forall temp_m  lbl,
      (subSequenceTrace  (applySubTrace sigma tr_temp) tr_log) /\
        (eq_label (lastElement temp_m (applySubTrace sigma tr_temp)) (LabelAt m tr_log lbl)).


(*Def 6.22 Corr Restriction*)
Definition Def6_22_CorrespondenceRestriction (RL_proto:ruleList) (allowSeq: list ruleList) (tr_log:trace) (tr_tempsessions: trace) : Prop := 
  forall m, (indexExists m tr_log) /\
             Def6_12_StdSessionTemplate allowSeq tr_tempsessions ->
              exists sigma tr_rewrittenTemp , 
                (Def6_20_3_RewriteTemplate tr_tempsessions RL_proto tr_rewrittenTemp) ->
                  Def6_21_Correspondence tr_rewrittenTemp tr_log m sigma.


(*  Lemma 6.5*)
Axiom Lemma6_5_CorrespondenceRestrictionHoldsforAllStLookingTraces : 
      forall RL_proto allowSeq setupRules tr_tempsessions tr_log ,
            (eq allowSeq (allPrefixs RL_proto)) /\
            Def5_7_Standard_Looking_Trace allowSeq setupRules tr_log /\
             Def6_12_StdSessionTemplate allowSeq tr_tempsessions  -> 
               Def6_22_CorrespondenceRestriction RL_proto allowSeq tr_log tr_tempsessions.


(* Lemma 6.6 *)
Axiom Lemma6_6_CorrespondenceRestrictionImpliesTracesAndTemplatesMatch : 
      forall  RL_proto allowSeq setupRules tr_temp tr_log Log_tr Log_temp sigma,
      (eq allowSeq (allPrefixs RL_proto)) /\
       Def6_22_CorrespondenceRestriction RL_proto (AddSID allowSeq) tr_log tr_temp /\ 
            Def5_7_Standard_Looking_Trace allowSeq setupRules tr_log /\
             Def6_10_StdTemplate allowSeq (RemoveSID tr_temp) /\
                   (member Log_tr tr_log) /\ 
                     (member Log_temp tr_temp) ->
                        (eq_label Log_tr (applySubLabel sigma Log_temp)).

(*Def 6.23 Uniqueness Restriction*)
(*Whenever two Logs use same fresh name, they must come from same session*)

Definition Def6_23_UniquenessRestriction (RL_proto:ruleList) (tr_log:trace) : Prop := 
  forall Log_i Log_j x sid_1 sid_2 pars_i pars_j ,
      (member x (Def5_5_freshInRLProto RL_proto))
        /\ (LoggedLbl_in_Trace Log_i tr_log)
        /\ (LoggedLbl_in_Trace Log_j tr_log)
        /\ (getSID Log_i sid_1)
          /\ (getSID Log_j sid_2)
             /\ (getParsFromLog Log_i pars_i)
              /\ (getParsFromLog Log_j pars_j)
                 /\ (member x (commonFreshNames (getFreshProtoNamesinLabel Log_i) (getFreshProtoNamesinLabel Log_j)))
                    -> (eq_baseTerm sid_1 sid_2).

(* Lemma 6.7 *)
Axiom Lemma6_7_UniquenessRestrictionHoldsforAllStLookingTraces : 
      forall RL_proto allowSeq setupRules tr_log ,
            (eq allowSeq (allPrefixs RL_proto)) /\
            Def5_7_Standard_Looking_Trace allowSeq setupRules tr_log -> 
               Def6_23_UniquenessRestriction RL_proto tr_log .

(* Lemma 6.8 *)
Axiom Lemma6_8_TraceAndTemplateMatchImpliesBothRestrictionsHold : 
      forall  RL_proto allowSeq  tr_temp tr_log Log_tr Log_temp sigma,
            (eq allowSeq (allPrefixs RL_proto)) /\
             ((member Log_tr tr_log) /\ 
                 (member Log_temp tr_temp) /\
                     (eq_label Log_tr (applySubLabel sigma Log_temp))) -> 
                        (Def6_22_CorrespondenceRestriction RL_proto allowSeq tr_log tr_temp /\ 
                           Def6_23_UniquenessRestriction RL_proto tr_log).


Definition  noFreshProtoNamesInSetup (rl:ruleList) : Prop :=
            eq (Def5_5_freshInRLProto rl) [].

(*A valid setup rule list is one which uses only Basic labels (no custom Logged labels) 
and  uses only setup fresh names (no proto fresh names)*)

Definition  validSetupRuleList (rl:ruleList) : Prop :=
            onlyBasicLogsInRL rl
            /\ noFreshProtoNamesInSetup rl.


(*To be used in Definitions which do not mention RL as a rulelist 
but use rlProto and rlSetup separately*)

Definition WellFormedAndValidRLSetupProto (rlSetup: ruleList) (rlProto:ruleList) : Prop:=
                         validSetupRuleList rlSetup
                        /\ Def6_9_validRuleList rlProto
                        /\ Def6_2_wellformedRulesFromState [] (appendAny  rlSetup rlProto).

(*To be used in Definitions which use RL as a rulelist and 
do not mention rlProto and rlSetup separately*)

Definition WellFormedAndValidRuleList (RL: ruleList) : Prop:=
exists rlSetup rlProto, eq (appendAny rlSetup rlProto) RL
                       /\ WellFormedAndValidRLSetupProto rlSetup rlProto.


(* MAIN THEOREM - Theorem 6.3 *)
Theorem Thm_6_3_StealthAttackImpliesBothRestrictionsOnTraces : forall  allowSeq rlSetup attackTrace rlProto, 
                (WellFormedAndValidRLSetupProto  rlSetup rlProto
            /\  (eq allowSeq (allPrefixs rlProto)))
            ->
            ((Def5_9_Stealth_Attack allowSeq rlSetup (RemoveSID attackTrace))
        <-> exists tmplt_sessions tmplt_Rewritten,
               Def6_12_StdSessionTemplate allowSeq tmplt_sessions /\
               Def6_20_3_RewriteTemplate tmplt_sessions rlProto tmplt_Rewritten /\
               Def6_22_CorrespondenceRestriction rlProto  allowSeq tmplt_Rewritten attackTrace
                /\
                Def6_23_UniquenessRestriction rlProto attackTrace).