Library Sec10_Chap6Defs

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").

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.

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.

Lemma emptyReduceGround : forall r f1 f2, reduceWithGroundRule r f1 emptyLabel f2
                                    -> (labelR r) = emptyLabel.

Lemma emptyReduce : forall r f1 f2, reduceWithRule r f1 emptyLabel f2
                                    -> (labelR r) = emptyLabel.

Lemma LoggedLabelGroundReduce : forall r f1 f2 lg1 l1, reduceWithGroundRule r f1 (LoggedLabel lg1 l1) f2
                                    -> exists lg2 l2, (labelR r) = (LoggedLabel lg2 l2).

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).

Lemma LoggedLabelReduce : forall r f1 f2 lg1 l1, reduceWithRule r f1 (LoggedLabel lg1 l1) f2
                                    -> exists lg2 l2, (labelR r) = (LoggedLabel lg2 l2).

Lemma emptyLabelSigmaEq : forall sigma l, ((applySubLabel sigma l) = emptyLabel) -> (l = emptyLabel).

Lemma setupRulesBasicLabels : forall rls f1 l f2,
wellFormedSetupRules rls -> reduceWithRules rls f1 l f2 -> exists al, l = BasicLabel al.

Lemma StdTracesHaveTemplates : forall t allowSequence sigma setupRules f1 f2,
        wellFormedSetupRules setupRules
          -> runInOrder allowSequence setupRules sigma f1 t f2
            -> (getLogTrace t) =
                       (applySubTrace sigma (StdTemplateForRuleList allowSequence)).

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.

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).

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.

Fixpoint uniqueArgumentsFact (f:fact) (r: rule) (rs:list rule) : Prop :=
  match f with
   | STATE n ts => (uniqueTermsForRule ts n r rs)
   | _ => False
  end.

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.

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.

Global Index

other

(1 entry)

Library Index

other

(1 entry)

Global Index

S

Sec10_Chap6Defs [library]

Library Index

S

Sec10_Chap6Defs

Global Index

other

(1 entry)

Library Index

other

(1 entry)

This page has been generated by coqdoc