[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 AccessControl
enrich gen-secdomain
 , 
       gen-systemstate
 , 
       gen-commands , 
       gen-value , 
       gen-name with
   functions 
      contents : systemstate × name → value;
      comment: Rushby Def. 5;
       
      obs : systemstate × secdomain → systemstate;
      step : systemstate × command → systemstate;
      cdom : command → secdomain;
   predicates 
      observe : name × secdomain;
      alter : name × secdomain;
       . ⇒ . : secdomain × secdomain;
      comment: security policy, interference relation;
       
      eqd : systemstate × secdomain × systemstate;
      comment: Rushby Reference Monitor Assumption.;
       
   
   axioms 
      eqd-def :  ⊦ eqd(sys, d, sys0) ↔ (∀ nam. observe(nam, d) → contents(sys, nam) = contents(sys0, nam));
      obs-in-domain :  ⊦ observe(nam, d) → contents(obs(sys, d), nam) = contents(sys, nam);
      used for : s, ls;
       
      obs-other-domain :  ⊦ ¬ observe(nam, d) → contents(obs(sys, d), nam) = null;
      used for : s, ls;
       
      extensionality :  ⊦ sys = sys0 ↔ (∀ nam. contents(sys, nam) = contents(sys0, nam));
      RMA-2
      : ⊦ 
          eqd(sys, cdom(co), sys0) ∧ contents(sys, nam) = contents(sys0, nam) ∧ alter(nam, cdom(co))
        → contents(step(sys, co), nam) = contents(step(sys0, co), nam);
      RMA-3 :  ⊦ contents(step(sys, co), nam) ≠ contents(sys, nam) → alter(nam, cdom(co));
      alter-observe-respects-policy :  ⊦ alter(nam, d) ∧ observe(nam, d0) → d ⇒ d0;
end enrich