[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Specification LanguageBasedNIFIntrans
enrich MeydenIntrans
 with
   functions 
      cdom : name → secdomain;
   predicates 
      eqlb : systemstate × secdomain × systemstate;
      eqlbs : systemstate × secdomainset × systemstate;
   
   axioms 
      eqlb-def :  ⊦ eqlb(sys, d, sys0) ↔ (∀ nam. cdom(nam) ⇒ d → contents(sys, nam) = contents(sys0, nam));
      eqlbs-def :  ⊦ eqlbs(sys, ds, sys0) ↔ (∀ d. d ∈ ds → eqlb(sys, d, sys0));
      no-read-up :  ⊦ observe(nam, d) → cdom(nam) ⇒ d;
      comment: this connects observe to the 
                      language based attacker model 
                      (who can see all low variables).;
       
      no-write-down :  ⊦ alter(nam, d) → d ⇒ cdom(nam);
      comment: this follows from alter-observe-respects-policy
                         if we have observe(nam, cdom(nam)) 
                         (this follows from observe-all-names and d ⇒ d);
       
      observe-all-names :  ⊦ cdom(nam) ⇒ d → observe(nam, d);
      LanguageBasedNIF-run : eqlbs(sys, sources(cl, d), sys0) ⊦ eqlb(run(sys, cl), d, run(sys0, cl));
      comment: requires observe-all-names.;
      used for : theorem;
       
      LanguageBasedNIF-run-observe : eqds(sys, sources(cl, d), sys0) ⊦ eqd(run(sys, cl), d, run(sys0, cl));
      comment: holds without observe-all-names.;
      used for : theorem;
       
      eqd-implies-lbnif : eqd(sys, d, sys0) ⊦ ∀ nam. cdom(nam) ⇒ d → contents(sys, nam) = contents(sys0, nam);
      comment: uses observe-all-names.
            This is identical to LanguageBasedNIF-follows below
            because eqd is equivalent to obs (see spec AccessControl).;
      used for : theorem;
       
      obs-implies-lbnif : obs(sys, d) = obs(sys0, d) ⊦ ∀ nam. cdom(nam) ⇒ d → contents(sys, nam) = contents(sys0, nam);
      comment: uses observe-all-names.;
      used for : theorem;
       
      obs-implies-lbnif-observe : obs(sys, d) = obs(sys0, d) ⊦ ∀ nam. cdom(nam) ⇒ d ∧ observe(nam, d) → contents(sys, nam) = contents(sys0, nam);
      comment: holds without observe-all-names.;
      used for : theorem;
       
end enrich