[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 path-permission
enrich
   permission-param
, 
   permission
with
   

   
   
   
   predicates  px : user × path × state;
               px-parent : user × path × state;
               py : user × path × state;
               pr : user × path × state;
               pw : user × path × state;
   
   
   
   

   

   axioms px :  ⊦ px(user, p, st) ↔ (∀ q. q ⊑ p → px(user, meta(q, st)));
          px-parent :  ⊦ px-parent(user, p, st) ↔ p ≠ ε → px(user, parent(p), st);
          used for: ls;
          pr :  ⊦ pr(user, p, st) ↔ pr(user, meta(p, st)) ∧ px-parent(user, p, st);
          pw :  ⊦ pw(user, p, st) ↔ pw(user, meta(p, st)) ∧ px-parent(user, p, st);
          py :  ⊦ py(user, p, st) ↔ pw(user, p, st) ∧ px(user, p, st);
          used for: ls;

   

   
end enrich