enrich AccessControl
 , 
       gen-command-list
 , 
       gen-secdomain-set
 with
   functions 
      run : systemstate × commandlist → systemstate;
      run : commandlist → systemstate;
      ipurge : commandlist × secdomain → commandlist;
      sources : commandlist × secdomain → secdomainset;
   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);
      sources-base :  ⊦ sources([], d) = ∅ ++ d;
      used for : s, ls;
       
      sources-rec :  ⊦ sources(co ' + cl, d) = (((∃ d0. d0 ∈ sources(cl, d) ∧ cdom(co) ⇒ d0) ⊃ sources(cl, d) ++ cdom(co); sources(cl, d)));
      ipurge-base :  ⊦ ipurge([], d) = [];
      used for : s, ls;
       
      ipurge-rec :  ⊦ ipurge(co ' + cl, d) = ((cdom(co) ∈ sources(co + cl, d) ⊃ co + ipurge(cl, d); ipurge(cl, d)));
      Security-strong :  ⊦ ipurge(cl, d) = ipurge(cl0, d) ∧ eqds(sys, sources(cl, d), sys0) → obs(run(sys, cl), d) = obs(run(sys0, cl0), d);
      comment: 
    comment :  This is the standard (generalized) purge security property 
               starting with two different states.
               Proved with RMA-1 and lemma1-gen. 

            Because of sources-ipurge the eqds precondition is equivalent to
            eqds(sys, sources(ipurge(cl, d), d), sys0) and
            eqds(sys, sources(ipurge(cl0, d), d), sys0) and
            eqds(sys, sources(cl0, d), sys0)
            ;
      used for : theorem;
       
      Security :  ⊦ ipurge(cl, d) = ipurge(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-simple :  ⊦ obs(run(cl), d) = obs(run(ipurge(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, ipurge(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