enrich AccessControl4VarsTrans
 , 
       gen-command-list
 , 
       gen-secdomain-set
 with
comment: weaker version than in specification LanguageBaseNIF because only
         used names must be observed and need a domain. This may be useful
         since we have an infinite number of names.;
   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)));
      LanguageBasedNIF-run : eqd(sys, d, sys0) ⊦ ∀ nam. usedName(nam) ∧ cdom(nam) ⇒ d → contents(run(sys, cl), nam) = contents(run(sys0, cl), nam);
      used for : theorem;
       
      eqd-implies-LanguageBasedNIF : eqd(sys, d, sys0) ⊦ ∀ nam. usedName(nam) ∧ cdom(nam) ⇒ d → contents(sys, nam) = contents(sys0, nam);
      used for : theorem;
       
      LanguageBasedNIF-follows : obs(sys, d) = obs(sys0, d) ⊦ ∀ nam. usedName(nam) ∧ cdom(nam) ⇒ d → contents(sys, nam) = contents(sys0, nam);
      used for : theorem;
       
      Security :  ⊦ purge(cl, d) = purge(cl0, d) → obs(run(cl), d) = obs(run(cl0), d);
      comment:  This is the standard (generalized) purge security property. 
               Proved with RMA-1 and lemma1. ;
      used for : theorem;
       
      Security-without-initialstate :  ⊦ purge(cl, d) = purge(cl0, d) ∧ eqd(sys, d, sys0) → obs(run(sys, cl), d) = obs(run(sys0, cl0), d);
      comment:  This is the standard (generalized) purge security property 
               starting with two different states.
               Proved with RMA-1 and lemma1-gen. ;
      used for : theorem;
       
      Security-simple :  ⊦ obs(run(cl), d) = obs(run(purge(cl, d)), d);
      comment:  This is the standard (simple) purge security property. 
               Proved with RMA-1 and lemma1. ;
      used for : theorem;
       
      Security-simple-without-initialstate :  ⊦ obs(run(sys, cl), d) = obs(run(sys, purge(cl, d)), d);
      comment:  This is the standard (simple) purge security property
               without a fixed initial state.
               Proved with RMA-1 and lemma1-gen. ;
      used for : theorem;
       
end enrich