(** 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 Sec6_TamarinExample. (** ===================== *** 7: Definitions from Chapter 5 of the thesis ===================== **) (* Before defining standard traces we define a relation for running rules in a fixed order and a function give us just the logs from a trace *) (* 'runInOrder as sr f1 t f2' verifies that given a allowed sequences as and set up rules sr, facts f1 and trace t, whether it is possible to generate facts f2 or not by executing the rules from as in order and any rules from sr? *) 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. (* 'runInOrderSigmaProtocol as subs f1 t f2' verifies that given a allowed sequences as, facts f1 and trace t, whether it is possible to generate facts f2 or not by executing the rules from as in order? *) 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. (* runInOrderSigma executes multiple iterations of setup rules in any order followed by protocol rule execution once in the order mandated by any of the allowed sequences . Before passing the tist of facts (fsMid), produced by the setup rule list execution, to runInOrderSigmaProtocol, all the OUT and IN facts are removed from fsMid *) 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). Proof. intros. induction l1. + simpl in H. unfold not in H0. apply H0 in H. inversion H. + simpl. simpl in H. inversion H. left. apply H1. right. apply IHl1. assumption. Qed. Lemma memberAfterRemoveOne: forall fac1 fac2 facs, member fac1 (removeFact fac2 facs) -> member fac1 facs. Proof. intros. induction facs. + inversion H. + simpl. unfold removeFact in H. simpl in H. destruct ( fact_dec a fac2) in H. - right. assumption. - simpl in H. inversion H. * left. assumption. * right. apply IHfacs. unfold removeFact. apply H0. Qed. Lemma memberAfterRemove : forall fac facts1 facts2, member fac (removeFacts facts1 facts2) -> member fac facts2. Proof. intros. induction facts1. + simpl in H. assumption. + apply IHfacts1. simpl in H. apply memberAfterRemoveOne in H. assumption. Qed. 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. Proof. intros. induction factlist. inversion H. destruct (fact_dec fac (applySubFact sigma a)). - exists a. split. assumption. simpl. left. reflexivity. - simpl in H. inversion H. apply n0 in H0. inversion H0. apply IHfactlist in H0. inversion H0. exists x0. inversion H1. split;auto. + unfold member. right. apply H3. Qed. (* Unused *) 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). Proof. intros. inversion H. inversion H2. inversion H4. subst. apply memberOneOrOther in H0. inversion H2. inversion H6. subst. inversion H8. rewrite <- H9 in H0. destruct redRule. simpl. simpl in H0. + destruct f0. - inversion H0. - apply memberSigmaEquals in H0. inversion H0. exists x1. inversion H11. split. assumption. rewrite H12. reflexivity. + destruct f0. - inversion H0. - apply memberSigmaEquals in H0. inversion H0. exists x1. inversion H11. split. assumption. rewrite H12. reflexivity. + unfold not. intros. apply H1. eapply memberAfterRemove. apply H6. Qed. 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]. Proof. intros. induction (ts). + exists []. exists h. reflexivity. + inversion IHl. inversion H. destruct x0. - unfold appendAny in H0. inversion H0. exists [x1]. exists a. reflexivity. - exists (r::a::x0). exists x1. simpl. inversion H0. reflexivity. Qed. Lemma appendAnyAppendAny: forall {T:Type} (x1:T) x0 r, (appendAny (appendAny x0 [x1]) [r]) = (appendAny x0 [x1;r]). Proof. intros. induction x0. reflexivity. simpl. rewrite IHx0. reflexivity. Qed. (* Definitions from Chapter 5 of Thesis*) 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. (* A useful lemma, tells us we can extend the rulelist without problems: *) Lemma canExtendAllowSeq : forall rl rls r, Def5_3_Valid_AllowSequences rls rl -> Def5_3_Valid_AllowSequences rls (r::rl). Proof. intros. induction rls. - apply Empty_AS. - apply Step_AllowSeq. inversion H. inversion H3. split. + destruct a. apply Empty_O_SubList. apply Next_O_SubList. assumption. + apply IHrls. assumption. Qed. (* As examples of allowed sequences, we may use the list itself, all prefixes of the list. We now prove that these are Allowed Sequences *) Lemma idIsAllowSeq : forall rl, Def5_3_Valid_AllowSequences [rl] rl. Proof. intros. apply Step_AllowSeq. split. induction rl. apply Empty_O_SubList. apply Same_O_SubList. assumption. apply Empty_AS. Qed. 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. Proof. induction rl. + apply Empty_AS. + simpl. apply Step_AllowSeq. split. - apply idIsOrderedSublist. - apply canExtendAllowSeq. assumption. Qed. (* All list of rule lists are an allowed Sequence for some rulelist. Therefore we may just consider an arbitary list of rulelists in the following definitions *) Lemma allListsAllowedSeq : forall rll:(list ruleList), exists rl:ruleList, Def5_3_Valid_AllowSequences rll rl. Proof. induction rll. + exists []. apply Empty_AS. + inversion IHrll. exists (appendAny a x0). apply Step_AllowSeq. split. - induction a. apply Empty_O_SubList. apply Same_O_SubList. apply IHa. - induction a. assumption. apply canExtendAllowSeq. assumption. Qed. Lemma ginstSplit : forall rl1 rl2 r, ginsts r rl2 -> ginsts r (appendAny rl1 rl2). Proof. intros. induction rl1. + simpl. assumption. + simpl. apply GinstTail. assumption. Qed. 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.