diff -r 8779d321cc2e -r f27882976251 Flask.thy --- a/Flask.thy Wed May 15 11:21:39 2013 +0800 +++ b/Flask.thy Wed May 15 15:42:46 2013 +0800 @@ -1017,6 +1017,23 @@ (Some u, Some r, Some t) \ Some (u, r, t) | _ \ None)" +fun init_role_of_obj :: "t_object \ role_t option" +where + "init_role_of_obj (O_proc p) = init_role_of_proc p" +| "init_role_of_obj _ = Some R_object" + +definition init_sectxt_of_obj :: "t_object \ security_context_t option" +where + "init_sectxt_of_obj obj \ + (case (init_user_of_obj obj, init_role_of_obj obj, init_type_of_obj obj) of + (Some u, Some r, Some t) \ Some (u,r,t) + | _ \ None)" + +definition sec_of_root :: "security_context_t" +where + "sec_of_root \ (case (init_user_of_obj (O_dir []), init_type_of_obj (O_dir [])) of + (Some u, Some t) \ (u, R_object, t))" + (******* flask granting ******** * involves three kinds of rules: * 1. allow rule of types, allowed_rule_list_t, main