Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
%%% Non-interference in Constructive Authorization Logic %%% Proof of theorem 3 %%% Authors: Deepak Garg and Frank Pfenning principal: type. %name principal K. %%% just making this up so that principals are not %%% split during input coverage check prin_: principal -> principal. %%%% Predicates predicate: type. %name predicate P. %%%% Symbols, L ::= P | \perp | K.L %%%% We use K | F for K.F and bot for \perp symbol: type. %name symbol L. bot: symbol. | : principal -> symbol -> symbol. %infix right 2 | . basesym: predicate -> symbol. %%%% Formulas. F ::= L1 <= L2 | K.F %%%% We use K || F for K.F formula: type. %name formula F. <= : symbol -> symbol -> formula. || : principal -> formula -> formula. %infix none 1 <= . %infix right 2 || . %%%% Sequent calculus. %%%% Sequents have the form (F1 hyp), ... , (Fn hyp) ==> conc L1 L2, %%%% conc L1 L2 denotes L1 <= L2. hyp: formula -> type. %name hyp H. %%% conclusions : L1 <= L2 conc: symbol -> symbol -> type. %name conc D. %%% sequent calculus rules axiom: conc (basesym P) (basesym P). botL1: conc (bot) L. saysR: conc L1 L2 -> conc L1 (K | L2). saysL1: conc L1 (K | L2) -> conc (K | L1) (K | L2). saysL2: (hyp F -> conc L1 (K | L2)) -> (hyp (K || F) -> conc L1 (K | L2)). trans: conc L3 L1 -> conc L2 L4 -> hyp (L1 <= L2) -> conc L3 L4. %%%% Reflexivity. %%%% ==> conc L L. %%%% Proof by induction on L id: {L} conc L L -> type. %mode id +L -D. id_bot: id (bot) botL1. id_basesym: id (basesym P) axiom. id_dot: id (K | L) (saysL1 (saysR D)) <- id L D. %worlds () (id _ _). %total {L} (id L _). %%%% Completeness theorem. %%%% hyp (L1 <= L2) ==> conc L1 L2. completeness: hyp (L1 <= L2) -> conc L1 L2 -> type. %mode completeness +H -D. completeness_ : completeness (H: hyp (L1 <= L2)) (trans D1 D2 H) <- id L1 D1 <- id L2 D2. %worlds () (completeness _ _). %total {} (completeness _ _). %%%% Transtivity. %%%% ==> conc L1 L2 and ==> conc L2 L3 imply ==> conc L1 L3 %%%% Proof by simultaneous induction on both given derivations transitivity: conc L1 L2 -> conc L2 L3 -> conc L1 L3 -> type. %mode transitivity +D1 +D2 -D3. transitivity_hyp_l: transitivity axiom D D. transitivity_hyp_r: transitivity D axiom D. transitivity_botL1_l: transitivity botL1 D botL1. transitivity_saysL2_l: transitivity (saysL2 ([h] D1 h) H) D2 (saysL2 D H) <- {h} transitivity (D1 h) D2 (D h). transitivity_trans_l: transitivity (trans (D1: conc L3 L1) (D2: conc L2 L4) (H:hyp (L1 <= L2))) (D: conc L4 L5) (trans D1 E2 H) <- transitivity D2 D E2. transitivity_saysR_r: transitivity D1 (saysR (D2: conc L1 L2)) (saysR E) <- transitivity D1 D2 E. transitivity_trans_r: transitivity D1 (trans D2 D3 H) (trans E2 D3 H) <- transitivity D1 D2 E2. transitivity_saysL2_r: transitivity D1 (saysL2 ([h] D2 h) H) (saysL2 E2 H) <- {h} transitivity D1 (D2 h) (E2 h). transitivity_saysR_l_saysL1_r: transitivity (saysR D1) (saysL1 D2) E <- transitivity D1 D2 E. transitivity_saysL1_l_saysL1_r: transitivity (saysL1 D1) (saysL1 D2) (saysL1 E) <- transitivity D1 (saysL1 D2) E. %block blk_hyp: some {F: formula} block{h: hyp F}. %worlds (blk_hyp) (transitivity _ _ _). %total {[D1 D2]} (transitivity D1 D2 _). %%%% Admissibility of cut. %%%% ==> conc L1 L2 and hyp (L1 <= L2) ==> conc L3 L4 imply conc L3 L4. %%%% Proof by induction on second given derivation cut: conc L1 L2 -> (hyp (L1 <= L2) -> conc L3 L4) -> conc L3 L4 -> type. %mode cut +D1 +D2 -D3. cut_axiom: cut D1 ([h] axiom) axiom. cut_botL1: cut D1 ([h] botL1) botL1. cut_saysR: cut D1 ([h] saysR (D2 h)) (saysR E) <- cut D1 D2 E. cut_saysL1: cut D1 ([h] saysL1 (D2 h)) (saysL1 E) <- cut D1 D2 E. cut_saysL2: cut D1 ([h1] saysL2 ([h2] D2 h2 h1) H) (saysL2 E H) <- {h2} cut D1 (D2 h2) (E h2). cut_trans_prin: cut D1 ([h] trans (D2 h) (D3 h) h) E <- cut D1 D2 E2 <- cut D1 D3 E3 <- transitivity E2 D1 E2' <- transitivity E2' E3 E. cut_trans_nonprin: cut D1 ([h] trans (D2 h) (D3 h) H) (trans E2 E3 H) <- cut D1 D2 E2 <- cut D1 D3 E3. %worlds (blk_hyp) (cut _ _ _ ). %total {D2} (cut _ D2 _).