Load Sec6_TamarinExample.

Inductive runInOrder : ruleList -> ruleList -> substitution -> facts -> trace -> facts -> Prop :=
     | Run_Stop_O : forall f1 rls sigma, runInOrder [] rls sigma f1 [] f1
     | Run_Step_O : forall r rls rlp sigma f1 t f2 f3 l, (reduceWithGroundRule (applySubRule sigma r) f1 l f2)
                          -> (runInOrder rlp rls sigma f2 t f3) -> runInOrder (r::rlp) rls sigma f1 (l::t) f3
     | Run_Step_Silent_O : forall r rls rlp sigma f1 t f2 f3, (reduceWithGroundRule (applySubRule sigma r) f1 emptyLabel f2)
                          -> (runInOrder rlp rls sigma f2 t f3) -> runInOrder (r::rlp) rls sigma f1 t f3
     | Run_FreshStep_O : forall rls rlp sigma f1 t f2 f3 fn, (reduceWithRule (freshRuleP fn) f1 emptyLabel f2)
                         -> (runInOrder rlp rls sigma f2 t f3) -> runInOrder rlp rls sigma f1 t f3
     | Run_Step_S : forall rls rlp sigma f1 l f2 f3 t, (reduceWithRules rls f1 l f2)
                         -> (runInOrder rlp rls sigma f2 t f3) -> runInOrder rlp rls sigma f1 (l::t) f3
     | Run_Step_Silent_S : forall rls rlp sigma f1 t f2 f3, (reduceWithRules rls f1 emptyLabel f2)
                         -> (runInOrder rlp rls sigma f2 t f3) -> runInOrder rlp rls sigma f1 t f3
     | Run_FreshStep_S : forall rls rlp sigma f1 t f2 f3 fn, (reduceWithRule (freshRuleS fn) f1 emptyLabel f2)
                         -> (runInOrder rlp rls sigma f2 t f3) -> runInOrder rlp rls sigma f1 t f3
     | Run_Comm_O : forall rls rlp sigma f1 t f2 trm, (subList [OUT trm] f1) ->
                            runInOrder rlp rls sigma ((IN trm)::(removeFacts [OUT trm] f1)) t f2 ->
                               runInOrder rlp rls sigma f1 t f2.



Inductive runInOrderSigmaProtocol : ruleList -> substitutions -> facts -> trace -> facts -> Prop :=
     | Sigma_Run_Stop_P : forall f1 sigma, runInOrderSigmaProtocol [] sigma f1 [] f1

     | Sigma_Run_Step_P : forall r rlp sigmaNow sigmaPrev f1 t f2 f3 l,
                                  groundRule (applySubRule sigmaNow r)
                                    -> reduceWithGroundRule (applySubRule sigmaNow r) f1 l f2
                                      -> (runInOrderSigmaProtocol rlp sigmaPrev f2 t f3)
                                        -> runInOrderSigmaProtocol (r::rlp) (sigmaNow::sigmaPrev) f1 (l::t) f3

     | Sigma_Run_Step_Silent_P : forall r rlp sigmaNow sigmaPrev f1 t f2 f3,
                                    groundRule (applySubRule sigmaNow r)
                                      -> reduceWithGroundRule (applySubRule sigmaNow r) f1 emptyLabel f2
                                        -> (runInOrderSigmaProtocol rlp sigmaPrev f2 t f3)
                                          -> runInOrderSigmaProtocol (r::rlp) (sigmaNow::sigmaPrev)f1 t f3

     | Sigma_Run_Comm_P : forall rlp sigmaPrev f1 t f2 trm, (subList [OUT trm] f1) ->
                            runInOrderSigmaProtocol rlp sigmaPrev ((IN trm)::(removeFacts [OUT trm] f1)) t f2 ->
                               runInOrderSigmaProtocol rlp sigmaPrev f1 t f2.


Fixpoint runInOrderSigma (rlProto:ruleList) (rlSetup:ruleList) (sigmaAll:substitutions) (fsInitial:facts) (tr:trace) (fsFinal:facts) : Prop :=
forall fsMid trSetup trProto,
  run rlSetup fsInitial trSetup fsMid
  /\ runInOrderSigmaProtocol rlProto sigmaAll (removeOutInfromFactList fsMid) tr fsFinal
        /\ (eq_trace tr (appendAny trSetup trProto)).

Lemma memberOneOrOther : forall {T:Type} (e:T) (l1:list T) (l2:list T),
  member e (appendAny l1 l2) -> not (member e l2) -> (member e l1).


Lemma memberAfterRemoveOne: forall fac1 fac2 facs,
  member fac1 (removeFact fac2 facs) -> member fac1 facs.

Lemma memberAfterRemove : forall fac facts1 facts2, member fac (removeFacts facts1 facts2) -> member fac facts2.

Lemma memberSigmaEquals : forall (fac:fact) (sigma:substitution) (factlist:list fact),
  member fac (applySubFacts sigma factlist)
    -> exists (facTemplate:fact), fac = applySubFact sigma facTemplate
                                         /\ member facTemplate factlist.

Lemma factFromReduction : forall sigma redRule f1 f2 l fac,
   reduceWithRuleSigma redRule sigma f1 l f2
     -> member fac f2 -> not (member fac f1)
       -> exists facTemplate, ( member facTemplate (conclFacts redRule)
             /\ applySubFact sigma facTemplate = fac).

Axiom destructReduceSigma : forall r f1 l f2 sigma,
  groundRule (applySubRule sigma r) ->
    reduceWithGroundRule (applySubRule sigma r) f1 l f2 ->
      reduceWithRuleSigma r sigma f1 l f2.

Axiom subListOneOrOther : forall f1 f fs,
  subList [f1] (f::fs) -> not (eq_fact f1 f) -> subList [f1] fs.

Fixpoint memberAtSamePos {T1:Type} {T2:Type} (e1:T1) (e2:T2) (list1: list T1) (list2: list T2) : Prop :=
  match list1 with
    | [] => False
    | h1::ts1 => match list2 with
                   | [] => False
                   | h2::ts2 => (e1=h1 /\ e2=h2) \/ memberAtSamePos e1 e2 ts1 ts2
                  end
   end.

Axiom factFromRule : forall fac (f1:facts) protocolRules sigmas f1 t f2,
 runInOrderSigmaProtocol protocolRules sigmas f1 t f2 -> member fac f2 -> not(member fac f1)
      -> exists r sigma facTemplate, memberAtSamePos r sigma protocolRules sigmas
             /\ member facTemplate (conclFacts r) /\ applySubFact sigma facTemplate = fac.

Lemma reverseHeadList : forall (h:rule) (ts:list rule), exists listPart last, (h::ts) = appendAny listPart [last].

Lemma appendAnyAppendAny: forall {T:Type} (x1:T) x0 r,
(appendAny (appendAny x0 [x1]) [r]) = (appendAny x0 [x1;r]).


Inductive Def5_3_Valid_AllowSequences : (list ruleList) -> ruleList -> Prop :=
  | Empty_AS : forall rs, Def5_3_Valid_AllowSequences [] rs
  | Step_AllowSeq : forall rl rlsHead rlsTail,
              orderedSubList rlsHead rl /\ Def5_3_Valid_AllowSequences rlsTail rl
                              -> Def5_3_Valid_AllowSequences (rlsHead::rlsTail) rl.

Lemma canExtendAllowSeq : forall rl rls r, Def5_3_Valid_AllowSequences rls rl
                                                   -> Def5_3_Valid_AllowSequences rls (r::rl).

Lemma idIsAllowSeq : forall rl, Def5_3_Valid_AllowSequences [rl] rl.

Fixpoint allPrefixs (rl:ruleList) : list ruleList :=
  match rl with
    | [] => []
    | h::ts => (h::ts):: (allPrefixs ts)
  end.

Lemma prefixIsAllowSeq : forall rl:ruleList, Def5_3_Valid_AllowSequences (allPrefixs rl) rl.


Lemma allListsAllowedSeq : forall rll:(list ruleList), exists rl:ruleList, Def5_3_Valid_AllowSequences rll rl.

Lemma ginstSplit : forall rl1 rl2 r, ginsts r rl2 -> ginsts r (appendAny rl1 rl2).

Inductive Def_Standard_Trace : list ruleList -> ruleList -> substitutions-> trace -> Prop :=
  | StandRun_Head : forall rl rls t f2 setupRules sigmas, (runInOrderSigma rl setupRules sigmas [] t f2 ) -> Def_Standard_Trace (rl::rls) setupRules sigmas t
  | StandRun_Tail : forall rl rls t setupRules sigmas, Def_Standard_Trace rls setupRules sigmas t -> Def_Standard_Trace (rl::rls) setupRules sigmas t.

Definition Def5_7_Standard_Trace(allowSeq:list ruleList) (setupRules: ruleList) (sigmas : substitutions) (thisTr:trace) : Prop :=
                      (Def_Standard_Trace allowSeq setupRules sigmas thisTr).

Inductive Subset_of_Standard_Traces : list ruleList -> ruleList -> substitutions -> list trace -> Prop :=
  | StandTraces_Empty : forall rlp setupRules sigmas, Subset_of_Standard_Traces rlp setupRules sigmas []
  | StandTraces_Next : forall rlp setupRules t ts sigmas, Def5_7_Standard_Trace rlp setupRules sigmas t /\ Subset_of_Standard_Traces rlp setupRules sigmas ts -> Subset_of_Standard_Traces rlp setupRules sigmas (t::ts).

Inductive mergeTrace : trace -> trace -> trace -> Prop :=
  | PMerge_nil : mergeTrace [] [] []
  | PMerge_left : forall x l l1 l2 , mergeTrace l1 l2 l -> mergeTrace (x::l1) l2 (x::l)
  | PMerge_right : forall x l l1 l2, mergeTrace l1 l2 l -> mergeTrace l1 (x::l2) (x::l).

Inductive merge : list trace -> trace -> Prop :=
  | PMerge_Base : forall lstTR TR, In TR lstTR -> merge lstTR TR
  | PMerge_Step : forall lst1 tr1 tr2 trnew, (merge lst1 tr1 /\ In tr2 lst1 /\ mergeTrace tr1 tr2 trnew)
                                                                              -> merge lst1 trnew.

Fixpoint applySubRuleListWise (sigmas : list substitution) (rl:ruleList) : ruleList :=
match sigmas, rl with
  | sig1::sigs, r1::rs => (applySubRule sig1 r1)::(applySubRuleListWise sigs rs)
  | _, _ => []
end.

Fixpoint Def5_5_freshInRLProto (rl: ruleList) : list freshNameProto :=
  match rl with
    | [] => []
    | rl1::rls => appendAny (getFrNamesPremiseProto (getFrFactProtoRule rl1)) (Def5_5_freshInRLProto rls)
  end.

Fixpoint Def5_5_freshInRLSetup (rl: ruleList) : list freshNameSetup :=
  match rl with
    | [] => []
    | rl1::rls => appendAny (getFrNamesPremiseSetup (getFrFactSetupRule rl1)) (Def5_5_freshInRLSetup rls)
  end.

Definition Def5_6_FreshFromRL_In_Trace (sigmas:substitutions) (rl:ruleList) (tr: trace) : list freshNameProto :=
          commonFreshNames (Def5_5_freshInRLProto (applySubRuleListWise sigmas rl)) (getFreshProtoNamesinTrace tr).

Definition ConditionOnFreshNames (sigmas:substitutions) (allowSeq:list ruleList) (logFromTraces:list trace) : Prop :=
forall tr_i tr_j rl_i rl_j, noCommonElements (Def5_6_FreshFromRL_In_Trace sigmas rl_i tr_i)
                                              (Def5_6_FreshFromRL_In_Trace sigmas rl_j tr_j)
                                     /\ (member rl_i allowSeq)
                                      /\ (member rl_j allowSeq)
                                       /\ (member tr_i logFromTraces)
                                         /\ (member tr_j logFromTraces)
                                          /\ not (eq tr_i tr_j).

Definition Def5_7_Standard_Looking_Trace (allowSeq:list ruleList) (setupRules:ruleList) (testTrace:trace) : Prop :=
 exists sigmas sometraces, (Subset_of_Standard_Traces allowSeq setupRules sigmas sometraces)
                       /\ (merge (map getLogTrace sometraces) (getLogTrace testTrace))
                         /\ ConditionOnFreshNames sigmas allowSeq (map getLogTrace sometraces).

Definition Def5_8_Attack_Trace (attackTrace:trace) : Prop := True.

Definition Def5_9_Stealth_Attack (allowSeq:list ruleList) (setupRules:ruleList) (testTrace:trace) : Prop :=
            Def5_7_Standard_Looking_Trace allowSeq setupRules testTrace /\ Def5_8_Attack_Trace testTrace.