[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 MeydenTrans
enrich AccessControlTrans
 , 
       gen-command-list
 , 
       gen-secdomain-set
 with
   functions 
      run : systemstate × commandlist → systemstate;
      run : commandlist → systemstate;
      purge : commandlist × secdomain → commandlist;
   predicates 
      eqds : systemstate × secdomainset × systemstate;
      secure : systemstate;
   
   axioms 
      eqds-def :  ⊦ eqds(sys, ds, sys0) ↔ (∀ d. d ∈ ds → eqd(sys, d, sys0));
      run-base :  ⊦ run(sys, []) = sys;
      used for : s, ls;
       
      run-rec :  ⊦ run(sys, co ' + cl) = run(step(sys, co), cl);
      used for : s, ls;
       
      run-initial :  ⊦ run(cl) = run(initialstate, cl);
      purge-base :  ⊦ purge([], d) = [];
      used for : s, ls;
       
      purge-rec :  ⊦ purge(co ' + cl, d) = ((cdom(co) ⇒ d ⊃ co + purge(cl, d); purge(cl, d)));
end enrich