(** 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 Sec9_LemmasOnWellformedness. (** ============================================ *** 10: Definitions from Chapter 6 of the thesis =============================================== **) Definition StdTemplateForRuleList : ruleList -> trace := getLogRL. Definition Def_StdTemplates : (list ruleList) -> (list trace) := map getLogRL. Definition Def6_10_StdTemplate (allowSeq:list ruleList) (thisTemp:trace) : Prop := (In thisTemp (Def_StdTemplates allowSeq)). Fixpoint StdTracesfromTemplates (sigma:substitution) (allowSeq: list ruleList) : list trace := applySubTraces sigma (Def_StdTemplates allowSeq). Definition StdTracefromTemplate (sigma:substitution) (allRules:list ruleList) (thisTrace:trace) : Prop := (In thisTrace (StdTracesfromTemplates sigma allRules)). Definition SID : baseTerm := (Var "sid"). (* "updateLabel l1" adds session ID 'sid' to front of action label parameters in every logged label. *) Fixpoint updateLabel (l1 : label ) : label := match l1 with | (LoggedSIDLabel t al lb) => (LoggedSIDLabel t al lb) | (LoggedLabel al lb) => (LoggedSIDLabel SID al lb) | (BasicLabel als) => (BasicLabel als) end. (** While annotating rules, annotation of first rule modifies all three parts of a rule while with other rules only the premise and labels are modified *) Fixpoint annotateFirstRule (firstRule : rule) : rule := match firstRule with | RuleProto f1 lbl f2 => RuleProto (FR_P SID::f1) (updateLabel lbl) ((OUT [Bterm SID])::f2) | RuleSetup f1 lbl f2 => RuleSetup f1 lbl f2 end. Fixpoint annotateOtherRules (rl : ruleList) : ruleList := match rl with | (RuleSetup f1 lbl f2)::rls => (RuleSetup f1 lbl f2) :: (annotateOtherRules rls) | (RuleProto ppat lbl cpat)::t => (RuleProto ((IN [(Bterm SID)])::ppat) (updateLabel lbl) ((OUT [(Bterm SID)])::cpat))::(annotateOtherRules t) | [] => [] end. (** "annotateRules rl " add the session IDs to the ruleList rl **) Fixpoint annotateRules (rl : ruleList) : ruleList := match rl with | [] => [] | r::t => (annotateFirstRule r) ::(annotateOtherRules t) end. Definition AddSID :(list ruleList) -> (list ruleList) := map annotateRules. Definition AddSIDTrace: trace -> trace := map updateLabel. Definition Def6_11_SessionsRL (allowSeq:list ruleList) : (list trace) := Def_StdTemplates (AddSID allowSeq). Definition Def6_12_StdSessionTemplate (allowSeq:list ruleList) (thisTemp:trace) : Prop := (In thisTemp (Def6_11_SessionsRL allowSeq)). Fixpoint subTrace_genFrom_Template (sigma:substitution) (tr:trace) (StdTmp:trace) : Prop := match tr, StdTmp with | [],[] => True | t1::ts, o1::os => eq_label t1 (applySubLabel sigma o1) /\ (subTrace_genFrom_Template sigma ts os) | _,_ => False end. (** Remove the session IDs from a trace **) Fixpoint RemoveSIDfromLabel (l1 : label) : label := match l1 with | (LoggedSIDLabel t al lb) => (LoggedLabel al lb) | (LoggedLabel al lb) => (LoggedLabel al lb) | (BasicLabel als) => (BasicLabel als) end. Definition RemoveSID : trace -> trace := map RemoveSIDfromLabel. (** "sameSID t1 t2" verifies if terms "t1" and "t2" contain the same SID **) Fixpoint sameSID (tm1:terms) (tm2:terms): Prop := match tm1, tm2 with | sid1::pars1, sid2::pars2 => eq_term sid1 sid2 | _,_ => False end. (** "al_Only_OnceNMAL al Tstd" verifies if every "al" present in template "tm", is present only once.**) Fixpoint al_Only_OnceNMAL (al:actionLabel) (Tstd:trace) : Prop := match Tstd with | nil => False | lbl1:: lbls => ((inLabelwithName al lbl1) /\ not (ALinTemplatewithName al lbls)) \/ (not (inLabelwithName al lbl1) /\ al_Only_OnceNMAL al lbls) end. (** "everyLogUniqueinTemplate Tstd" holds only if every "al" present in template is present only once.**) Definition everyLogUniqueinTemplate (Tstd:trace) : Prop := forall al, (al_in_Trace al Tstd) -> al_Only_OnceNMAL al Tstd. (* "WellFormedTemplate Tstd " verifies that there are no repeated log names in any of the templates *) Fixpoint WellFormedTemplate (Tstd:list trace) : Prop:= match Tstd with | tm1::tmRestList => (everyLogUniqueinTemplate tm1) /\ (WellFormedTemplate tmRestList) | [] => True end. Lemma emptyLabelsLemma : forall sigma l, applySubLabel sigma l = emptyLabel -> l = emptyLabel. Proof. intros. destruct l; inversion H; destruct l. - reflexivity. - inversion H1. Qed. Lemma emptyReduceGround : forall r f1 f2, reduceWithGroundRule r f1 emptyLabel f2 -> (labelR r) = emptyLabel. Proof. intros. destruct r. + inversion H. reflexivity. + inversion H. reflexivity. Qed. Lemma emptyReduce : forall r f1 f2, reduceWithRule r f1 emptyLabel f2 -> (labelR r) = emptyLabel. Proof. intros. destruct r. + simpl. inversion H. inversion H0. inversion H1. subst. inversion H3. inversion H4. unfold applySubRule in H6. inversion H2. rewrite H7. rewrite <- H6 in H7. simpl in H7. destruct l. apply emptyLabelsLemma in H7. rewrite H7. reflexivity. inversion H7. inversion H7. + simpl. inversion H. inversion H0. inversion H1. subst. inversion H3. inversion H4. unfold applySubRule in H6. inversion H2. rewrite H7. rewrite <- H6 in H7. simpl in H7. destruct l. apply emptyLabelsLemma in H7. rewrite H7. reflexivity. inversion H7. inversion H7. Qed. Lemma LoggedLabelGroundReduce : forall r f1 f2 lg1 l1, reduceWithGroundRule r f1 (LoggedLabel lg1 l1) f2 -> exists lg2 l2, (labelR r) = (LoggedLabel lg2 l2). Proof. intros. destruct r; inversion H; subst; exists lg1; exists l1; reflexivity. Qed. Lemma LoggedSIDLabelGroundReduce : forall r f1 f2 lg1 l1 t, reduceWithGroundRule r f1 (LoggedSIDLabel t lg1 l1) f2 -> exists lg2 l2 t, (labelR r) = (LoggedSIDLabel t lg2 l2). Proof. intros. destruct r; inversion H; subst; exists lg1; exists l1; exists t; reflexivity. Qed. Lemma LoggedLabelReduce : forall r f1 f2 lg1 l1, reduceWithRule r f1 (LoggedLabel lg1 l1) f2 -> exists lg2 l2, (labelR r) = (LoggedLabel lg2 l2). Proof. intros. destruct r. + simpl. inversion H. inversion H0. apply LoggedLabelGroundReduce in H2. inversion H2. inversion H3. inversion H1. subst. inversion H5. inversion H6. destruct l. - subst. simpl in H4. inversion H4. - exists a. exists l. reflexivity. - subst. simpl in H4. inversion H4. + simpl. inversion H. inversion H0. apply LoggedLabelGroundReduce in H2. inversion H2. inversion H3. inversion H1. subst. inversion H5. inversion H6. destruct l. - subst. simpl in H4. inversion H4. - exists a. exists l. reflexivity. - subst. simpl in H4. inversion H4. Qed. Lemma emptyLabelSigmaEq : forall sigma l, ((applySubLabel sigma l) = emptyLabel) -> (l = emptyLabel). Proof. intros. destruct l; unfold applySubLabel in H; inversion H. destruct l. - reflexivity. - inversion H1. Qed. Lemma setupRulesBasicLabels : forall rls f1 l f2, wellFormedSetupRules rls -> reduceWithRules rls f1 l f2 -> exists al, l = BasicLabel al. Proof. intros. inversion H0. inversion H1. induction H2. destruct l. - exists l. reflexivity. - apply LoggedLabelGroundReduce in H3. inversion H3. inversion H4. inversion H2. subst. inversion H6. inversion H7. destruct r2; destruct r1. + simpl in H9. inversion H9. simpl in H5. rewrite H5 in H12. destruct l0. * inversion H12. * inversion H. inversion H10. inversion H15. inversion H18. * inversion H12. + inversion H9. + inversion H9. + simpl in H9. inversion H9. simpl in H5. rewrite H5 in H12. destruct l0. * inversion H12. * inversion H. inversion H10. * inversion H12. - apply LoggedSIDLabelGroundReduce in H3. inversion H3. inversion H4. inversion H5. inversion H2. subst. inversion H7. inversion H8. destruct r1; destruct r2. + simpl in H6. simpl in H10. inversion H10. rewrite H6 in H13. destruct l1. * inversion H13. * inversion H13. * inversion H. inversion H11. inversion H16. inversion H19. + inversion H10. + inversion H10. + simpl in H6. simpl in H10. inversion H10. rewrite H6 in H13. destruct l1. * inversion H13. * inversion H13. * inversion H. inversion H11. - apply wellFormedTail in H. apply IHginsts in H. + assumption. + unfold reduceWithRules. exists r1. split. assumption. assumption. + split; assumption. + assumption. Qed. Lemma StdTracesHaveTemplates : forall t allowSequence sigma setupRules f1 f2, wellFormedSetupRules setupRules -> runInOrder allowSequence setupRules sigma f1 t f2 -> (getLogTrace t) = (applySubTrace sigma (StdTemplateForRuleList allowSequence)). Proof. intros. induction H0; intros. + (* Run_Stop_O *) reflexivity. + (* Run_Step_O *) apply IHrunInOrder in H. clear IHrunInOrder. inversion_clear H0. destruct r; destruct l0; simpl; try assumption. - apply listEqHead. assumption. - apply listEqHead. assumption. + (* Run_Step_Silent_O *) apply IHrunInOrder in H. clear IHrunInOrder. apply emptyReduceGround in H0. destruct r; simpl in H0; apply emptyLabelSigmaEq in H0; subst; assumption. + (* Run_FreshStep_O *) apply IHrunInOrder in H. assumption. + (* Run_Step_S *) destruct l. - simpl. apply IHrunInOrder in H. assumption. - apply setupRulesBasicLabels with (f1:=f1) (l:=LoggedLabel a l) (f2:=f2) in H. * inversion H. inversion H2. * assumption. - apply setupRulesBasicLabels with (f1:=f1) (l:=LoggedSIDLabel b a l) (f2:=f2) in H. * inversion H. inversion H2. * assumption. + (* Run_Step_Silent_S *) apply IHrunInOrder. assumption. + (* Run_FreshStep_S *) apply IHrunInOrder. assumption. + (* Run_Comm_O *) apply IHrunInOrder in H. assumption. Qed. (**======================================================= **** Definitions and Proofs from Chapter 6 ==========================================================**) (* Setup rules only produce single unique state facts or non unique facts that have unique parameters (or outputs which we ignore). Setup Rule facts : * All Non unique facts must have a unique construction, unique for a principal name Definition of a Step in a Path : * A step exists if : - from a variable that appears in a particular position in an input to the same position in the previous output - from a variable that appears in a position in a unique state fact to the a variable in same position in a previous occurence of that unique fact. - from a variable in any fact in a rule to the same variable to another fact in that rule. A path is zero or more steps. *) (* New validity conditions for a variable in Protocol ruleList : A variable in a protocol ruleList is valid, if this variable x * is a new variable in any rule. * while appearing in a unique state has a path from this variable back to a constant or a variable and a previous path for another occurence of this variable also leads to the same constant or a variable. * while appearing in a non unique state fact F, it is paired with another variable that has a path to a value v then there exists a previous non unique state fact F which has variable in the same position as x which also has a path to v, and is paired with a variable of the same name. *) (* Handling Public and Private keys in a model A Public key has two different nomenclatures in a Tamarin file : !Pk($A, pk(~ltkA)) and !Pk($A, pkA) For their equivalence, we can add a restriction stating Given !Pk(X, pk(ltkX)) AND !Pk(Y, pkY) EQ(X,Y) -> EQ(PkX,pkY) i.e. Given STATE PkFact [B; Func PkName [ltkB_var]] and STATE PkFact [B; pkB] EQ(Func PkName [ltkB_var], pkB) is true It flows from the fact that the setup rules generate a fresh key for each Principal which is unique Any rule can consist of one of the following facts : * Fresh fact - Fr() is for new variable so it is always valid. Fr() is not allowed more to exist more than once for any variable i.e. Each instance of Fr() must use a new variable. * Input/Output fact - Any input via In() is required to match all the varibales used herein with the variables used in previous output Out(). Variables are matched by position and in the case of different names, they are treated as equal. * Unique state fact (appears only once) - Appears in pair at conclusion of previous rule and premise of the current rule. Every variable and their corresponding positions are matched. * Non-unique state fact (appears multiple times but uniquely for a Principal) - such as "STATE PkFact [B; Func PkName [ltkB_var]]" and "STATE PkFact [B; pkB]" are matched based on their occurrence in the outputs and inputs. Values such as "Func PkName [ltkB_var]" and "pkB" are considered same if there exists a set of output and input that is supposed to match on account of them being equal. e.g. If "aenc{'1', ~ni, $I}pkR" and "aenc{'1', ni, I}pk(ltkR)" appear in output and inputrespectively => "pkR" and "pk(ltkR)" are equal. *) (**================================================= 10A: Types of Facts allowed in the system ================================================== *) (* We define a uniqueStateFact as one that is only product in one rule. This is useful to us because if a fact is uniquely produced then we can be sure that every rule that uses this fact as an input will get the same values *) Fixpoint uniqueStateFact (f:fact) (rl:list rule) : Prop := match rl, f with | r::rlt, STATE n ts => ( stateAppearsOnce f (conclFacts r) /\ NameDoesNotAppearInFacts n (allConclFacts rlt) ) \/ ( NameDoesNotAppearInFacts n (conclFacts r) /\ uniqueStateFact f rlt ) | _ , _ => False end. (* This requires that the unique fact is used with all vars the same, however this could be weaken to only requiring that variable in question is the same *) Fixpoint variableInUniqueStateFact (v:variable) (newRule:rule) (pastRules: list rule) : Prop := exists n ts, (uniqueStateFact (STATE n ts) pastRules) /\ (member (STATE n ts) (premiseFacts newRule)) /\ member v (variablesInTerms ts). (* We also define a uniqueArugmentsFact as one that can be product in many places but always has different arguments. Often this will be for setting up principals key e.g. Fact('C', key). For two occurences of such a fact, if we can show that if one of the argument terms match then we can conclude that the other terms must *) (* A term in OK as a unique state argument if it is fresh, or if it is a constant that no other states with a the same name use *) Fixpoint uniqueTermsForRule (ts:terms) (n:name) (r:rule) (rs:list rule) : Prop := match ts with | [] => True | th::tst => ( termIsOnlyConstant th n rs \/ termIsFresh th r ) /\ (uniqueTermsForRule tst n r rs) end. (* Constant must also not appear in other places*) Fixpoint uniqueArgumentsFact (f:fact) (r: rule) (rs:list rule) : Prop := match f with | STATE n ts => (uniqueTermsForRule ts n r rs) | _ => False end. (*Rajiv:How to model UAF_gen and UAF_used?*) Fixpoint collectUniqueStateFacts (fls:facts) (rlst:ruleList) : facts := match fls with | f1::fs => match (uniqueStateFact f1 rlst) with | True => (f1 :: (collectUniqueStateFacts fs rlst)) end | [] => [] end. Fixpoint collectUniqueArgFacts (fls:facts) (r:rule) (rls:ruleList) : facts := match fls with | f1::fs => match (uniqueArgumentsFact f1 r rls) with | True => (f1 :: (collectUniqueArgFacts fs r rls)) end | [] => [] end. Fixpoint PresentInSamePositionUSF (RL:list rule) (usf:fact) (t1:term) (t2:term) : Prop := CheckFactsInUSF (collectUniqueStateFacts (collectStateFacts RL) RL) usf t1 t2. Fixpoint PresentInSamePositionUAF (RL:list rule) (uaf:fact) (t1:term) (t2:term) : Prop := match RL with | r::rs => ((CheckFactsInUAF (collectUniqueArgFacts (collectStateFacts RL) r rs) uaf t1 t2) /\ PresentInSamePositionUAF rs uaf t1 t2) | [] => True end. (* This is an update to the model that allows any number of steps between an input and an output for variables linked by input and outputs *) Fixpoint varMatchInLastOutput (x:variable) (ts:terms) (revRules: list rule) : Prop := match revRules with | [] => False | r::rs => member (OUT ts) (conclFacts r) \/ ((noOutputRule r) /\ varMatchInLastOutput x ts rs) end. Fixpoint variableLinkedInputOutput (x:variable) (newRule:rule) (pastRules: list rule) : Prop := exists ts, (member (IN ts) (premiseFacts newRule)) /\ varMatchInLastOutput x ts (rev pastRules). Definition Def6_4_allowedFactType (f:fact) (r: rule) (rs:list rule) : Prop := (exists t, (member (FR_P t) (premiseFacts r)) /\ (eq_fact f (FR_P t))) \/ (exists ts, (member (IN ts) (premiseFacts r) /\ (eq_fact f (IN ts)) \/ (member (OUT ts) (conclFacts r)) /\ (eq_fact f (OUT ts)))) \/ (uniqueStateFact f (r::rs)) \/ (uniqueArgumentsFact f r rs). Definition Def6_5_variableDirectlyLinked (var: variable) (newRule:rule) (pastRules: list rule) : Prop := (variableLinkedInputOutput var newRule pastRules) \/ (variableInUniqueStateFact var newRule pastRules). Fixpoint Def6_6_variableIndirectlyLinked (v:variable) (newRule:rule) (pastRules: list rule) : Prop := exists n ts, uniqueArgumentsFact (STATE n ts) newRule pastRules /\ member (STATE n ts) (premiseFacts newRule) /\ (exists RuleA, member (STATE n ts) (conclFacts RuleA) /\ (member RuleA pastRules)) /\ member v (variablesInTerms ts) /\ (exists t, member t (variablesInTerms ts) /\ Def6_5_variableDirectlyLinked t newRule pastRules) /\ (exists c, member c (constantsInTerms ts)). Definition variableIsNew (var:variable) (pastRules: list rule) : Prop := trueForAll (fun x => (NotIn var (variablesInRule x))) pastRules. Definition Def6_7_validVariable (newRule:rule) (pastRules: list rule) (var: variable) : Prop := (variableIsNew var pastRules) \/ (Def6_5_variableDirectlyLinked var newRule pastRules) \/ (Def6_6_variableIndirectlyLinked var newRule pastRules). Fixpoint Def6_7_validVariables (newRule:rule) (pastRules: list rule) (vs:variables) : Prop := trueForAll (Def6_7_validVariable newRule pastRules) vs. Definition Def6_8_validRule (newRule:rule) (pastRules: list rule): Prop := (forall f, (member f (allFactsRL (appendAny pastRules [newRule]))) /\ (Def6_4_allowedFactType f newRule pastRules)) /\ (forall vs, trueForAll (Def6_7_validVariable newRule pastRules) vs). Fixpoint Def6_9_validRuleList (rs : list rule) : Prop := match rs with | [] => True | r::rst => (Def6_9_validRuleList rst) /\ (Def6_7_validVariables r rst (variablesInRule r)) end. Fixpoint Def6_9_validRuleLists (allowSeq : list ruleList) : Prop := trueForAll Def6_9_validRuleList allowSeq.