(** 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 3B: 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 Sec4_Groundterms. (** ==================== ** 5: Tamarin Reduction ======================= **) (* This section defines Tamarin rule for generating traces *) (* N.B. Tamarin enforces additional constrainst of allowed traces, i.e., freshnames do not repeat. We do not enforce these here, but we can add them later if needed *) (* This section defines how a term can be reduced with a particular rule set *) (** "reduceWithRule r f1 l f2" means that the rule "r" can match the facts "f1" and produce the facts "f2" with the label "label"**) Inductive reduceWithGroundRule : rule -> facts -> label -> facts -> Prop := | R_match : forall r s1, (subList (premiseFacts r) s1) -> reduceWithGroundRule r s1 (labelR r) (appendAny (conclFacts r) (removeFacts (premiseFacts r) s1)). Definition reduceWithRule (r1:rule) (f:facts) (l:label) (f2:facts) : Prop := exists r2, (ginst r2 r1) /\ reduceWithGroundRule r2 f l f2. Definition reduceWithRules (rs:ruleList) (f:facts) (l:label) (f2:facts) : Prop := exists r2, (ginsts r2 rs) /\ reduceWithGroundRule r2 f l f2. (** "reduceWithRuleSigma r f1 l f2" means that the rule "r" can match the facts "f1" and produce the facts "f2" with the label "label"**) Definition reduceWithRuleSigma (r1:rule) (sigma:substitution) (f:facts) (l:label) (f2:facts) : Prop := exists r2, (ginstWithSigma r2 sigma r1) /\ reduceWithGroundRule r2 f l f2. Definition reduceWithRulesSigma (rs:ruleList) (sigma:substitution) (f:facts) (l:label) (f2:facts) : Prop := exists r2, (ginstsWithSigma r2 sigma rs) /\ reduceWithGroundRule r2 f l f2. Definition freshRuleS (n:freshNameSetup) : rule := (RuleSetup [] emptyLabel [FR_P (Name (Fresh_S n))]). Definition freshRuleP (n:freshNameProto) : rule := (RuleProto [] emptyLabel [FR_P (Name (Fresh_P n))]). (* This is the key reduction definition that tells us how a list of protocol rules can be used to generate a trace *) Inductive run : ruleList -> facts -> trace -> facts -> Prop := | Run_Stop : forall rl f1, run rl f1 [] f1 | Run_Step : forall rl f1 t f2 f3 l, (reduceWithRules rl f1 l f2) -> (run rl f2 t f3) -> run rl f1 (l::t) f3 | Run_Step_Silent : forall rl f1 t f2 f3, (reduceWithRules rl f1 emptyLabel f2) -> (run rl f2 t f3) -> run rl f1 t f3 | Run_FreshStepP : forall rl f1 t f2 f3 fn, (reduceWithRule (freshRuleP fn) f1 emptyLabel f2) -> (run rl f2 t f3) -> run rl f1 t f3. (* <-- this seems like a hack, but I'm not sure of a better way ... *) (* N.B. this does not enforce the conditions needed in Tamarin, e.g. fresh names do not repeat, these restrictions need to be added *) (* This is the key reduction definition that tells us how a list of protocol rules can be used to generate a trace using substitution*) Inductive runSigma : ruleList -> substitutions -> facts -> trace -> facts -> Prop := | SigmaRun_Stop : forall rl f1, runSigma rl [] f1 [] f1 | SigmaRun_Step : forall rl sigmaPrev f1 t f2 f3 l sigmaNow, (reduceWithRulesSigma rl sigmaNow f1 l f2) -> (runSigma rl sigmaPrev f2 t f3) -> runSigma rl (sigmaNow::sigmaPrev) f1 (l::t) f3 | SigmaRun_Step_Silent : forall rl sigmaPrev f1 t f2 f3 sigmaNow, (reduceWithRulesSigma rl sigmaNow f1 emptyLabel f2) -> (runSigma rl sigmaPrev f2 t f3) -> runSigma rl (sigmaNow::sigmaPrev) f1 t f3 | SigmaRun_FreshStepP : forall rl f1 t f2 f3 fn sigmaPrev sigmaNow, (reduceWithRuleSigma (freshRuleP fn) sigmaNow f1 emptyLabel f2) -> (runSigma rl sigmaPrev f2 t f3) -> runSigma rl (sigmaNow::sigmaPrev) f1 t f3. (* <-- this seems like a hack, but I'm not sure of a better way ... *) (** Some useful Lemmas about traces **) Lemma reduceWithFirstRule : forall r rl f1 f2 l, reduceWithRule r f1 l f2 -> reduceWithRules (r::rl) f1 l f2. Proof. intros. unfold reduceWithRules. inversion H. inversion H0. exists x0. split. - apply GinstHead. assumption. - assumption. Qed. Lemma reduceWithSecondRule : forall r1 r2 rl f1 f2 l, reduceWithRule r2 f1 l f2 -> reduceWithRules (r1::r2::rl) f1 l f2. Proof. intros. unfold reduceWithRules. inversion H. inversion H0. exists x0. split. - apply GinstTail. apply GinstHead. assumption. - assumption. Qed. Lemma FreshRulePIsAGroundRule : forall fn, groundRule (freshRuleP fn). Proof. intros. unfold groundRule. unfold freshRuleP. split. + reflexivity. + split. - unfold groundFacts. split. * reflexivity. * auto. - reflexivity. Qed. Lemma ProtoFreshNameStep (fn:freshNameProto) : forall fs, reduceWithRule (freshRuleP fn) fs emptyLabel ((FR_P (Name (Fresh_P fn)))::fs). Proof. unfold reduceWithRule. exists (freshRuleP fn). split. + apply Ginst. split. - exists subs_empty. reflexivity. - apply FreshRulePIsAGroundRule. + unfold freshRuleP. apply R_match. simpl. auto. Qed. Lemma FreshRuleSIsAGroundRule : forall fn, groundRule (freshRuleS fn). Proof. intros. unfold groundRule. unfold freshRuleS. split. + reflexivity. + split. - unfold groundFacts. split. * reflexivity. * auto. - reflexivity. Qed. Lemma SetupFreshNameStep (fn:freshNameSetup) : forall fs, reduceWithRule (freshRuleP fn) fs emptyLabel ((FR_P (Name (Fresh_P fn)))::fs). Proof. unfold reduceWithRule. exists (freshRuleP fn). split. + apply Ginst. split. - exists subs_empty. reflexivity. - apply FreshRulePIsAGroundRule. + unfold freshRuleP. apply R_match. simpl. auto. Qed. Lemma ProtoFreshNameStepEmpty (fn:freshNameProto) : reduceWithRule (freshRuleP fn) [] emptyLabel [ FR_P (Name (Fresh_P fn)) ]. Proof. apply ProtoFreshNameStep. Qed. Lemma SetupFreshNameStepEmpty (fn:freshNameSetup) : reduceWithRule (freshRuleP fn) [] emptyLabel [ FR_P (Name (Fresh_P fn)) ]. Proof. apply SetupFreshNameStep. Qed. Lemma reduceRulesLessImpliesMore : forall r rl f1 l f2, reduceWithRules rl f1 l f2 -> reduceWithRules (r::rl) f1 l f2. Proof. intros. inversion H. inversion H0. unfold reduceWithRules. exists x0. split. - apply GinstTail. assumption. - assumption. Qed. Lemma runRulesLessImpliesMore : forall r rl f1 t f2, run rl f1 t f2 -> run (r::rl) f1 t f2. Proof. intros. induction H. - apply Run_Stop. - eapply Run_Step. apply reduceRulesLessImpliesMore. apply H. assumption. - eapply Run_Step_Silent. apply reduceRulesLessImpliesMore. apply H. assumption. - eapply Run_FreshStepP. apply H. assumption. Qed. Lemma runTransitive : forall rl s1 s2 s3 l1 l2, run rl s1 l1 s2 /\ run rl s2 l2 s3 -> run rl s1 (appendAny l1 l2) s3. Proof. intros rl s1 s2 s3 l1 l2 H. destruct H. induction H ; simpl. + apply H0. + eapply Run_Step. apply H. auto. + eapply Run_Step_Silent. apply H. auto. + eapply Run_FreshStepP. apply H. auto. Qed. (** The same Lemmas with substitution**) Lemma reduceWithFirstRuleSigma : forall r rl f1 f2 l sigma, reduceWithRuleSigma r sigma f1 l f2 -> reduceWithRulesSigma (r::rl) sigma f1 l f2. Proof. intros. unfold reduceWithRulesSigma. inversion H. inversion H0. exists x0. split. - apply GinstHeadSigma. assumption. - assumption. Qed. Lemma reduceWithSecondRuleSigma : forall r1 r2 rl f1 f2 l sigma, reduceWithRuleSigma r2 sigma f1 l f2 -> reduceWithRulesSigma (r1::r2::rl) sigma f1 l f2. Proof. intros. unfold reduceWithRulesSigma. inversion H. inversion H0. exists x0. split. - apply GinstTailSigma. apply GinstHeadSigma. assumption. - assumption. Qed. Lemma ProtoFreshNameStepSigma (fn:freshNameProto) : forall fs sigma, reduceWithRuleSigma (freshRuleP fn) sigma fs emptyLabel ((FR_P (Name (Fresh_P fn)))::fs). Proof. unfold reduceWithRuleSigma. exists (freshRuleP fn). split. + apply GinstSigma. split. - reflexivity. - apply FreshRulePIsAGroundRule. + unfold freshRuleP. apply R_match. simpl. auto. Qed. Lemma SetupFreshNameStepSigma (fn:freshNameSetup) : forall fs sigma, reduceWithRuleSigma (freshRuleP fn) sigma fs emptyLabel ((FR_P (Name (Fresh_P fn)))::fs). Proof. unfold reduceWithRuleSigma. exists (freshRuleP fn). split. + apply GinstSigma. split. - reflexivity. - apply FreshRulePIsAGroundRule. + unfold freshRuleS. apply R_match. simpl. auto. Qed. Lemma ProtoFreshNameStepEmptySigma (fn:freshNameProto) : reduceWithRuleSigma (freshRuleP fn) subs_empty [] emptyLabel [ FR_P (Name (Fresh_P fn)) ]. Proof. apply ProtoFreshNameStepSigma. Qed. Lemma SetupFreshNameStepEmptySigma (fn:freshNameSetup) : reduceWithRuleSigma (freshRuleP fn) subs_empty [] emptyLabel [ FR_P (Name (Fresh_P fn)) ]. Proof. apply SetupFreshNameStepSigma. Qed. Lemma reduceRulesLessImpliesMoreSigma : forall r rl f1 l f2 sigma, reduceWithRulesSigma rl sigma f1 l f2 -> reduceWithRulesSigma (r::rl) sigma f1 l f2. Proof. intros. inversion H. inversion H0. unfold reduceWithRulesSigma. exists x0. split. - apply GinstTailSigma. assumption. - assumption. Qed. Lemma runRulesLessImpliesMoreSigma : forall r rl f1 t f2 sigmas, runSigma rl sigmas f1 t f2 -> runSigma (r::rl) sigmas f1 t f2. Proof. intros. induction H. - apply SigmaRun_Stop. - eapply SigmaRun_Step. apply reduceRulesLessImpliesMoreSigma. apply H. assumption. - eapply SigmaRun_Step_Silent. apply reduceRulesLessImpliesMoreSigma. apply H. assumption. - eapply SigmaRun_FreshStepP. apply H. assumption. Qed. Lemma runTransitiveSigma : forall rl f1 f2 f3 l1 l2 sigmas1 sigmas2, runSigma rl sigmas1 f1 l1 f2 /\ runSigma rl sigmas2 f2 l2 f3 -> runSigma rl (appendAny sigmas1 sigmas2) f1 (appendAny l1 l2) f3. Proof. intros rl s1 s2 s3 l1 l2 sigmas1 sigmas2 H. destruct H. induction H ; simpl. + apply H0. + eapply SigmaRun_Step. apply H. apply IHrunSigma. auto. + eapply SigmaRun_Step_Silent. apply H. auto. + eapply SigmaRun_FreshStepP. apply H. auto. Qed.