(**************************************************************** Michel St-Martin and Amy Felty December 2015, Coq version V8.4 A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules, Michel St-Martin and Amy P. Felty, In Proceedings of the Fifth ACM SIGPLAN Conference on Certified Programs and Proofs (CPP), January 2016. ***************************************************************) Require Export RuleSet. Open Scope Z_scope. Lemma ThreePm_rc : 0 <= 54000 < MIDNIGHT. Proof. unfold MIDNIGHT; omega. Qed. Definition ThreePm:Z'NM := (exist _ 54000 ThreePm_rc). Definition Request1 := (intReq 123)::(intReq 2):: (intReq 0)::(timeReq ThreePm)::(intReq 1):: (intReq 2)::(intReq 1)::nil. Lemma ThreeAm_rc : 0 <= 10800 <= MIDNIGHT. Proof. unfold MIDNIGHT; omega. Qed. Lemma FourAm_rc : 0 <= 14400 <= MIDNIGHT. Proof. unfold MIDNIGHT; omega. Qed. Lemma SixAm_rc : 0 <= 21600 <= MIDNIGHT. Proof. unfold MIDNIGHT; omega. Qed. Lemma FivePm_rc : 0 <= 61200 <= MIDNIGHT. Proof. unfold MIDNIGHT; omega. Qed. Lemma ElevenPm_rc : 0 <= 82800 <= MIDNIGHT. Proof. unfold MIDNIGHT; omega. Qed. Definition intEq (z:Z)(n:nat):srac := single (intInRange z z) n. Definition G123: srac := intEq 123 1. Definition AILab := intEq 0 2. Definition FMLab := intEq 1 2. Definition GradLab := intEq 2 2. Definition AnyLocation := single (any (intReq 0)) 2. Definition Enter: srac := intEq 0 3. Definition ThreeAm:Z' := (exist _ 10800 ThreeAm_rc). Definition FourAm:Z' := (exist _ 14400 FourAm_rc). Definition SixAm:Z' := (exist _ 21600 SixAm_rc). Definition FivePm:Z' := (exist _ 61200 FivePm_rc). Definition ElevenPm:Z' := (exist _ 82800 ElevenPm_rc). Definition GlabHours:srac := not (single (timeInRange ThreeAm FourAm) 4). Definition FMlabHours:srac := single (timeInRange SixAm ElevenPm) 4. Definition After5:srac := single (timeInRange FivePm Z'MIDNIGHT) 4. Definition AnyTime: srac := single (any (timeReq Z'NM0)) 4. Definition NotRegistered := intEq 0 5. (* Definition Violations := single (intGt 0) 6. *) Definition Violations := intEq 123 1. Definition Professors: srac := intEq 2 6. Definition Grads: srac := intEq 1 6. Definition Rule1 := ruleCons permit (and (and (and (single (any (intReq 0)) 1) (intEq 4 2)) Enter) FMlabHours). Definition Rule2 := ruleCons permit (and (and (and (or Grads Professors) GradLab) Enter) GlabHours). Definition Rule3 := ruleCons permit (and (and (and G123 FMLab) Enter) FMlabHours). Definition Rule4 := ruleCons permit (and (and (and (intEq 456 1) AILab) Enter) GlabHours). Definition Rule5 := ruleCons deny (and (and (and NotRegistered (or FMLab AILab)) Enter) AnyTime). Definition Rule6 := ruleCons deny (and (and (and Violations AnyLocation) Enter) After5). Definition setOfRules := Rule1::Rule2::Rule3::Rule4::Rule5::Rule6::nil. Open Scope nat_scope. Lemma test: (find_conflicts setOfRules) = (0, 5) :: (1, 5) :: (2, 4) :: (2, 5) :: (3, 4) :: nil. Proof. unfold setOfRules. unfold find_conflicts. unfold conflicts_aux. simpl. unfold toLists. unfold convertDNF. unfold Grads, Professors, GradLab, Enter, GlabHours, Violations, AnyLocation, After5. unfold G123, AnyTime, NotRegistered, FMLab, FMlabHours, AILab. unfold intEq. repeat unfoldRemoveNotsG. simpl. trivial. Qed.