Анализ в рамках базовой ролевой ДП-модели безопасности систем с простыми траекториями функционирования

Тип работы:
Реферат
Предмет:
ТЕХНИЧЕСКИЕ НАУКИ


Узнать стоимость

Детальная информация о работе

Выдержка из работы

2010 Математические основы компьютерной безопасности № 1(7)
МАТЕМАТИЧЕСКИЕ ОСНОВЫ КОМПЬЮТЕРНОЙ БЕЗОПАСНОСТИ
УДК 004. 94
АНАЛИЗ В РАМКАХ БАЗОВОЙ РОЛЕВОЙ ДП-МОДЕЛИ БЕЗОПАСНОСТИ СИСТЕМ С ПРОСТЫМИ ТРАЕКТОРИЯМИ
ФУНКЦИОНИРОВАНИЯ1
П. Н. Девянин
Институт криптографии, связи и информатики, г. Москва, Россия E-mail: peter_devyanin@hotmail. com
В рамках базовой ролевой ДП-модели анализируются условия передачи прав доступа и реализации информационных потоков по памяти. При этом рассматриваются только простые траектории функционирования системы, когда взаимодействует произвольное число субъект-сессий, и они не получают доступа владения друг к другу с использованием информационных потоков по памяти к функционально ассоциированным с субъект-сессиями сущностям.
Ключевые слова: компьютерная безопасность, ролевая модель, ДП-модели.
1. Основные элементы базовой ролевой ДП-модели
На основе базовой ролевой ДП-модели (БР ДП-модели) [1, 2] рассмотрим условия передачи прав доступа и реализации информационных потоков по памяти для случая, когда на траекториях функционирования системы субъект-сессии не получают доступа владения друг к другу с использованием информационных потоков по памяти к функционально ассоциированным с субъект-сессиями сущностям.
Основными элементами БР ДП-модели являются:
E = O U C — множество сущностей, где O — множество объектов, C — множество контейнеров и O П C = 0-
U — множество пользователей-
Lu — множество доверенных пользователей-
Nu — множество недоверенных пользователей-
S С E — множество субъект-сессий пользователей-
Ls — множество доверенных субъект-сессий-
Ns — множество недоверенных субъект-сессий-
R — множество ролей-
AR — множество административных ролей-
Rr = {readr, writer, appendr, executer, ownr} - множество видов прав доступа-
Ra = {reada, writea, appenda, owna} -множество видов доступа-
Rf = {writem, writet} -множество видов информационных потоков-
A С S х E х Ra — множество доступов субъект-сессий к сущностям-
F С E х E х Rf — множество информационных потоков между сущностями-
P С E х Rr — множество прав доступа к сущностям-
1 Работа выполнена при поддержке гранта МД-2. 2010. 10.
UA: U ^ 2R — функция авторизованных ролей пользователей-
AUA: U ^ 2ar — функция авторизованных административных ролей пользователей-
PA: R ^ 2р — функция прав доступа ролей-
user: S ^ U — функция принадлежности субъект-сессии пользователю- roles: S ^ 2r U 2ar — функция текущих ролей субъект-сессий- can_manage_rights: AR ^ 2r — функция администрирования прав доступа ролей-
He: E ^ 2е — функция иерархии сущностей-
Hr: R ^ 2r — функция иерархии ролей-
Har: AR ^ 2ar — функция иерархии административных ролей-
G = (PA, user, roles, A, F, He) — состояние системы-
E (G*, OP) -система, при этом G* -множество всех возможных состояний, OP — множество правил преобразования состояний-
G ~ap G'- - переход системы T,(G*, OP) из состояния G в состояние G'- с использованием правила преобразования состояний op Е OP-
T,(G*, OP, G0) -система T,(G*, OP) с начальным состоянием G0-
[s] С E U U — множество сущностей, функционально ассоциированных с субъект-сессией s (при этом по определению выполняется условие s Е [s]), и пользователей, каждый из которых может создать субъект-сессию, являющуюся функционально ассоциированной сущностью с субъект-сессией s-
fa: U х E ^ 2е U 2U — функция, задающая множества сущностей, функционально ассоциированных с субъект-сессией, при ее создании пользователем (или от имени пользователя другой субъект-сессией) из сущности. При этом если пользователь u Е U или субъект-сессия от имени пользователя u не могут создать из сущности e Е E новую субъект-сессию, то по определению fa (u, e) = 0. Кроме того, если для пользователя u Е U и сущности e Е E существует пользователь x Е U, такой, что выполняется условие x Е fa (u, e), то по определению будем считать, что пользователь x может создать субъект-сессию, которая будет являться функционально ассоциированной сущностью с субъект-сессией, создаваемой пользователем u из сущности e. По определению выполняется условие: для каждой субъект-сессии s Е S существует единственная сущность es Е E, такая, что справедливо равенство fa (user (s), es) = [s]-
y (E) С Ls х E — множество пар вида (доверенная субъект-сессия, сущность), относительно которых корректна доверенная субъект-сессия y-
de_facto_roles: S ^ 2Rl& gt-ar — функция фактических текущих ролей субъект-сессий, при этом по определению в каждом состоянии системы G = (PA, user, roles, A, F, He) для каждой субъект-сессии si Е S выполняется равенство:
de_facto_roles (s) = roles (s1) U {r Е R U AR: 3s2 Е S [(s1, s2, owna) Е A & amp- & amp- r Е roles (s2)]}-
de_facto_rights: S ^ 2P — функция фактических текущих прав доступа субъект-сессий, при этом по определению в каждом состоянии системы G = (PA, user, roles, A, F, He) для каждой субъект-сессии s Е S выполняется равенство:
de_facto_rights (s) = {p Е P: 3r Е de_facto_roles (s) [p Е PA®]}- de_facto_actions: S ^ 2P х 2r — функция фактических возможных дей-
ствий субъект-сессий, при этом по определению в каждом состоянии системы G = (PA, user, roles, A, F, He) для каждой субъект-сессии s1 Е S выполняется равенство:
de_facto_actions (s1) = (PA (roles (s1)) х can _manage _rights (roles (s1) П AR)) U U{(p, r) Е PxR: 3s2 Е S 3^, s2, owna) Е A [r Е can_manage_rights (roles (s2)nAR) & amp- & amp- p Е PA (roles (s2))]}.
В БР ДП-модели определены следующие правила преобразования состояний:
— монотонные: take_role (x, r), grant_right (x, r, (y, ar)), create_entity (x, r, y, z), create_first_session (u, r, y, z), create_session (x, w, r, y, z), rename_entity (x, y, z), control (x, y, z), access_own (x, y), take_access_own (x, y, z), access_read (x, y), access_write (x, y), access_append (x, y), flow (x, y, y'-, z), find (x, y, z), post (x, y, z), pass (x, y, z), take_flow (x, y) —
— немонотонные: remove_role (x, r), remove_right (x, r, (y, ar)), delete_entity (x, y, z). Используем следующие предположение и определения БР ДП-модели. Предположение 1. Каждые пользователь или субъект-сессия системы T,(G*, OP)
вне зависимости от имеющихся у них авторизованных ролей являются либо доверенными, либо недоверенными. Доверенные пользователи или субъект-сессии не создают новых субъект-сессий. Каждые недоверенный пользователь или субъект-сессия могут создать только недоверенную субъект-сессию.
Определение 1. Назовем траекторию функционирования системы T. (G*, OP) траекторией без кооперации доверенных и недоверенных субъект-сессий для передачи прав доступа, если при ее реализации используются только монотонные правила преобразования состояний и доверенные субъект-сессии:
— не берут роли в множество текущих ролей-
— не дают другим ролям права доступа к сущностям-
— не получают доступа владения к субъект-сессиям.
Определение 2. Траекторию без кооперации доверенных и недоверенных субъект-сессий для передачи прав доступа G0 ~opi G1 ~op2 … ^~oPN Gn, где N ^ 0, назовем простой, если при ее реализации для 0 ^ i ^ N каждое правило op i не является правилом вида control (x, y, z), использующим для получения доступа владения субъект-сессией x к субъект-сессии y информационный поток по памяти (x, z, writem), где z Е [y].
Определение 3. Пусть G0 = (PA0,user0,roles0, A0, F0, HEo) -состояние системы E (G*, OP), в котором существуют недоверенный пользователь x Е Nu и субъект-сессия или недоверенный пользователь y Е Nu U S0, такие, что x = y. Определим предикат simple_can_access_own (x, y, G0), который будет истинным тогда и только тогда, когда существуют состояния G1,…, Gn и правила преобразования состояний op1,…, opN, такие, что G0 ~opi G1 hop2 … ~opN GN, где N ^ 0, является простой траекторией без кооперации доверенных и недоверенных субъект-сессий для передачи прав доступа, и существуют субъект-сессии sx, sy Е Sn, такие, что user'-N (sx) = x, или sy = y, или userN (sy) = y и выполняется условие (sx, sy, owna) Е An.
Определение 4. Пусть G = (PA, user, roles, A, F, He) -состояние системы
E (G*, OP), в котором существуют субъект-сессии или недоверенные пользователи x, y Е NU U S. Определим предикат simple_directly_access_own (x, y, G), который будет истинным тогда и только тогда, когда или x = y, или выполняется одно из следующих условий 1−6.
1. Если y Е Nu и x Е Nu, то существуют сущность ey Е E и роль ry Е R, такие, что (ey, executer) Е PA (UA (y)), ry Е can_manage_rights (AUA (y)) и выполняется одно из условий:
— ry Е UA (x) —
— x Е fa (y, ey).
2. Если y Е Nu и x Е Ns П S, то существуют сущность ey Е E и роль ry Е R, такие, что (ey, executer) Е PA (UA (y)), ry Е can_manage_rights (AUA (y)) и выполняется одно из условий:
— ry Е UA (user (x)) —
— x Е fa (y, ey).
3. Если y Е Nu и x Е Ls П S, то существуют сущность ey Е E и роль ry Е R, такие, что (ey, executer) Е PA (UA (y)), ry Е can_manage_rights (AUA (y)) и выполняется одно из условий:
— ry Е roles (x) —
— x Е fa (y, ey).
4. Если y Е S и x Е Nu, то выполняется одно из условий:
— (y, ownr) Е PA (UA (x)) —
— x Е [y].
5. Если y Е S и x Е Ns П S, то выполняется одно из условий:
— (y, ownr) Е PA (UA (user (x))) —
— x Е [y]-
— (x, y, owna) Е A.
6. Если y Е S и x Е Ls П S, то выполняется одно из условий:
— (y, ownr) Е PA (roles (x)) —
— x Е [y]-
— (x, y, owna) Е A.
Определение 5. Пусть G = (PA, user, roles, A, F, He) -состояние системы
E (G*, OP), в котором существует субъект-сессия или недоверенный пользователь x Е Nu U S. Назовем множество X С Nu U S островом субъект-сессии или недоверенного пользователя x, если X = {x} U {y Е (NU U S) {x}: существует последовательность s1 = x и s2,…, sm Е (Nu U S) {x}, где sm = y и m ^ 2, такая, что для каждого i, 1 ^ i & lt- m, истинен предикат simple_directly_access_own (si, si+1, G)}. Определим функцию island: Nu U S ^ 2NuUS, задающую для каждых субъект-сессии или недоверенного пользователя соответствующий им остров. При этом используются следующие обозначения:
island_roles: NU U (NS П S) ^ 2r U 2ar — функция, задающая для каждых недоверенного пользователя или недоверенной субъект-сессии x Е Nu U (Ns П S) роли, которыми обладают все субъект-сессии или недоверенные пользователи, принадлежащие острову x. При этом по определению справедливо равенство island_roles (x) = = {r Е R U AR: 3y Е island (x) [(y Е NU & amp- r Е UA (y) U AUA (y)) V (y Е NS П S & amp- & amp- r Е UA (user (y)) U AUA (user (y))) V (y Е Ls П S& amp- r Е roles (y))]}-
island_rights: Nu U (Ns П S) ^ 2P — функция, задающая для каждых недоверенного пользователя или недоверенной субъект-сессии x Е Nu U (Ns П S) права доступа, которыми обладают все субъект-сессии или недоверенные пользователи, принадлежащие острову x. При этом по определению справедливо равенство island_rights (x) = {p Е P: 3r Е island_roles (x) [p Е PA®]}-
island_actions: NU U (NS П S) ^ 2P x 2r — функция, задающая для каждых недоверенного пользователя или недоверенной субъект-сессии x Е Nu U
U (Ns П S) возможные действия, которыми обладают все субъект-сессии или недоверенные пользователи, принадлежащие острову x. При этом по определению справедливо равенство island_actions (x) = {(p, r) Е P х R: 3y Е island (x)
[(y Е NU & amp- (p, r) Е PA (UA (y)) х can_manage_rights (AUA (y))) V (y Е NS П S & amp- & amp- (p, r) Е PA (UA (user (y))) х can_manage_rights (AUA (user (y)))) V (y Е Ls П S & amp-
& amp- (p, r) Е PA (roles (y)) х can_manage_rights (roles (y) П AR))]}.
Определение 6. Пусть G = (PA, user, roles, A, F, He) -состояние системы
E (G*, OP), в котором существуют недоверенная субъект-сессия или недоверенный пользователь x Е Nu U (Ns П S) и субъект-сессии или недоверенные пользователи y, z Е Nu U S. Будем говорить, что субъект-сессия или недоверенный пользователь y соединяются простым мостом с субъект-сессией или недоверенным пользователем z через недоверенную субъект-сессию или недоверенного пользователя x, если z Е island (x) и существует роль ry Е R, такая, что выполняются следующие два условия.
1. Или y Е NU и ry Е UA (y), или y Е NS П S и ry Е UA (user (y)), или y Е Ls П S и ry Е roles (y).
2. Или z Е NU и ry Е can_manage_rights (AUA (z)), или z Е NS П S и ry Е can_manage_rights (AUA (user (z))), или z Е Ls П S и ry Е can_manage_-rights (roles (z) П AR).
При этом используется следующее обозначение:
is_simple_bridge: (NU U (NS П S)) х (NU U S) х (NU U S) ^ {true, false} - функция, для которой по определению справедливо равенство is_simple_bridge (x, y, z) = true тогда и только тогда, когда y соединен простым мостом с z через x, где x Е Nu U U (Ns П S), y, z Е Nu U S.
Определение 7. Пусть G = (PA, user, roles, A, F, He) -состояние системы
E (G*, OP), в котором существуют недоверенная субъект-сессия или недоверенный пользователь x Е Nu U (Ns П S) и субъект-сессии или недоверенные пользователи y, z Е Nu US. Будем говорить, что субъект-сессия или недоверенный пользователь y соединяются мостом с субъект-сессией или недоверенным пользователем z через недоверенную субъект-сессию или недоверенного пользователя x, когда существуют субъект-сессии или недоверенные пользователи v, w Е Nu U S и роли rv, ry Е R, такие, что v, w, z Е island (x), w, z Е island (v), z Е island (w) и выполняются следующие условия.
1. Или y Е NU и ry Е UA (y), или y Е NS П S и ry Е UA (user (y)), или y Е Ls П S и ry Е roles (y).
2. Или v Е NU и rv Е UA (v), ry Е can_manage_rights (AUA (v)), или v Е NS П S и rv Е UA (user (v)), ry Е can_manage_rights (AUA (user (v))), или v Е Ls П S и rv Е roles (v), ry Е can_manage_rights (roles (v) П AR).
3. Или w Е NU и rv Е can_manage_rights (AUA (w)), или w Е S и (w, ownr) Е Е PA (rv).
При этом используется следующее обозначение:
is_bridge: (Nu U (NS П S)) х (Nu U S) х (N?j U S) ^ {true, false} - функция, для которой по определению справедливо равенство is_bridge (x, y, z) = true тогда и только тогда, когда y соединен мостом с z через x, где x Е NU U (NS П S), y, z Е NU U S.
В [2] обоснованы алгоритмически проверяемые необходимые и достаточные условия истинности предиката simple_can_access_own (x, y, G0).
Утверждение 1. Пусть G0 = (PA0,user0,roles0, A0, F0, HEo) — состояние системы E (G*, OP), в котором существуют недоверенный пользователь или недоверенная
субъект-сессия x Е Nu U (Ns П S0) и субъект-сессия или недоверенный пользователь у Е island (x) {x}. Тогда справедливо одно из предложений:
— если x Е Nu, то истинен предикат simple_can_access_own (x, у, G0) —
— если x Е Ns П So, то истинен предикат simple_can__access_own (user0(x), y, G0).
Следствие 1. Пусть G0 = (PAo, nsero, roleso, A0, F0, HEo) -состояние системы E (G*, OP), в котором существуют недоверенный пользователь или недоверенная субъект-сессия x Е Nu U (Ns П So). Тогда существуют состояния Gi,…, Gn и правила преобразования состояний opi,…, opN, такие, что G0 ~opi Gi ~op2 … ^~opN Gn, где N ^ 0, является простой траекторией без кооперации доверенных и недоверенных субъект-сессий для передачи прав доступа, и существует недоверенная субъект-сессия sx Е Ns П Sn, такая, что-либо userN (sx) = x, либо sx = x и выполняются условия:
— island_roles (x) = island_roles (sx) С de_facto_rolesN (sx) (множество фактических ролей субъект-сессии sx включает все роли субъект-сессий или пользователей, принадлежащих ее острову) —
— island_rights (x) = island_rights (sx) С de_facto_rightsN (sx) (множество фактических прав доступа субъект-сессии sx включает все права доступа субъект-сессий или пользователей, принадлежащих ее острову) —
— island_actions (x) = island_actions (sx) С de facto actionsN (sx) (множество фактических возможных действий субъект-сессии sx включает все возможные действия субъект-сессий или пользователей, принадлежащих ее острову).
Теорема 1. Пусть G0 = (PA0,user0,roles0, A0, Fo, HEo) -состояние системы
E (G*, OP), в котором существуют недоверенный пользователь x Е Nu и субъект-сессия или недоверенный пользователь у Е Nu U S0, такие, что x = у. Предикат simple_can_access_own (x, у, G0) является истинным тогда и только тогда, когда существуют последовательности недоверенных субъект-сессий или недоверенных пользователей xi,…, xm Е NuU (NsnS0) и субъект-сессий или недоверенных пользователей у1,…, ут Е NuUS0, где m ^ 1, таких, что xi = x, ут = у, уг Е island (xi) для 1 ^ i ^ m и выполняются следующие условия.
1. Если m ^ 2, то справедливо равенство is_bridge (xm, ym-l, y) = true.
2. Если m ^ 3, то для каждого i, 2 ^ i & lt- m, или is^ridge^. i^^^j) = true, или is_simple_bridge (xi, уг-1, уг) = true.
2. Условия передачи прав доступа
В рамках БР ДП-модели рассмотрим условия передачи прав доступа с участием произвольного числа субъект-сессий для простых траекторий функционирования системы. Дадим определение.
Определение 8. Пусть G0 = (PA0,user0,roles0, A0, Fo, HEo) -состояние системы T,(G*, OP), в котором существуют пользователь x Е U0 и право доступа к сущности (e, a) Е P0. Определим предикат simple_can_share ((e, a), x, G0), который будет истинным тогда и только тогда, когда существуют состояния Gi,…, Gn и правила преобразования состояний opi,…, opN, такие, что G0 ~opi Gi hop2 … ~opN Gn, где N ^ 0, является простой траекторией без кооперации доверенных и недоверенных субъект-сессий для передачи прав доступа, и существует субъект-сессия sx Е Sn, такая, что userN (sx) = x и выполняется условие (e, a) Е de_facto_rightsN (sx).
Определим и обоснуем алгоритмически проверяемые необходимые и достаточные условия истинности предиката simple_can_share ((e, a), x, G0) для случая, когда x Е Nu.
Теорема 2. Пусть G0 = (PA0,user0,roles0, A0, Fo, HEo) -состояние системы
T,(G*, OP), в котором существуют недоверенный пользователь x Е Nu и право доступа к сущности (e, a) Е P0. Предикат simple_can_share ((e, a), x, G0) является истинным тогда и только тогда, когда выполняется одно из условий.
1. Выполняется условие (e, 5) Е PAo (UAo (x)), где 5 Е {a, ownr}.
2. Существует субъект-сессия или недоверенный пользователь у Е Nu U S0, истинен предикат simple_can_access_own (x, у, G0) и выполняется одно из условий:
— у Е Nu и (e, a) Е PAo (UAo (y)) —
— у Е Ns П So и (e, a) Е PAo (UAo (usero (y))) —
— у Е Ls П So и (e, a) Е PAo (roleso (у)).
3. Существуют последовательности недоверенных субъект-сессий или недоверенных пользователей xi,…, xm Е Nu U (Ns П So), субъект-сессий или недоверенных пользователей у1,…, ym Е Nu U S0, где m ^ 2, таких, что xi = x, уi Е island (xi), где 1 ^ i ^ m, и выполняется одно из условий:
— Уm Е Nu и (e, ownr) Е PA^UA^ym))'--
ym Е NS П S0 и (e, ownr) Е P A0(UA0 (user0(ym
))) —
— ym Е Ls П So и (e, own) Е PAo (roleso (ym)).
При этом справедливо равенство is_simple_bridge (xm, ym-i, ym) = true, и для каждого 2 ^ i ^ m справедливо равенство или is_bridge (xi, yi-i, yi) = true, или is_simple_bridge (xi, yi-i, yi) = true.
Доказательство. Докажем достаточность выполнения условий теоремы для истинности предиката simple_can_share ((e, a), x, G0) при x Е Nu.
Пусть выполнено условие 1 теоремы. Тогда по предположению 1 существуют сущность ex Е E0, административная роль arx Е AUA0(x) и роль rx Е can_-manage_rights (arx), такие, что (ex, executer) Е PAo (UAo (x)). Положим opi = create_first_session (x, rx, ex, sx).
По условию 1 существует роль re Е UA0(x), такая, что (e, 5) Е PA0(re), где 5 Е { a, ownr }. Тогда положим op2 = take_role (sx, re).
Если 5 = a, то положим N = 2.
Если 5 = ownr, то положим
op3 = take_role (sx, arx) —
op4 = grant_right (sx, re, (e, a)) —
N = 4.
Таким образом, существует G0 ~opi … ~opN Gn — простая траектория без кооперации доверенных и недоверенных субъект-сессий для передачи прав доступа, и в состоянии Gn выполняется условие userN (sx) = x и право доступа к сущности (e, a) Е de_facto_rightsN (sx). Следовательно, по определению 8 предикат simple_can_share ((e, a), x, G0) является истинным.
Пусть выполнено условие 2 теоремы. Тогда существует субъект-сессия или недоверенный пользователь у Е Nu U S0, истинен предикат simple_can_access_own (x, у, G0) и по определению 3 существуют состояния Gi,…, Gm и правила преобразования состояний opi,…, opM, такие, что G0 ~opi … ^~opM Gm, где M ^ 0, является простой траекторией без кооперации доверенных и недоверенных субъект-сессий для передачи прав доступа, существуют субъект-сессии sx, sy Е Sm, такие, что userM (sx) = x, или sy = у, или userM (sy) = у, и выполняется условие (sx, sy, owna) Е Am. По условию 1 теоремы возможны три случая.
Первый случай: выполняются условия у Е Nu и (e, a) Е PAo (UAo (у)). Тогда существует роль ry Е UA0(у) = UAM (userM (sy)), такая, что (e, a) Е PA0(ry). Положим opM+i = take _role (sy, ry) —
N = M + 1.
Второй случай: выполняются условия у Е Ns П So и (e, a) Е PA0(UA0(user0(y))). Тогда существует роль ry Е UA0(user0(y)), такая, что (e, a) Е PA0(ry). Положим opM+i = take_role (y, ry) —
N = M + 1.
Третий случай: выполняется условие у Е Ls П So и (e, a) Е PA0(roles0(y)). Тогда положим N = M. Следовательно, траектория G0 ~opi … ~opN Gn, где N ^ 0, является простой траекторией без кооперации доверенных и недоверенных субъект-сессий для передачи прав доступа и выполняется условие (e, a) Е de_facto_rightsN (sx). Значит, по определению 8 предикат simple_can_share ((e, a), x, G0) является истинным.
Пусть выполнено условие 3 теоремы, тогда выполняются условия m ^ 2 и is_simple_bridge (xm, ym-i, ym) = true. Выберем минимальное 2 ^ k ^ m, такое, что справедливы равенства is_simple_bridge (xi, yi-i, yi) = true, где k ^ l ^ m. Для каждого простого моста, соединяющего субъект-сессию или недоверенного пользователя yi-i с субъект-сессией или недоверенным пользователем yi через недоверенную субъект-сессию или недоверенного пользователя xl, выполняется условие yi Е island (xi) и существует роль ryi_i, удовлетворяющая условиям определения 6, где k ^ l ^ m.
По утверждению 1 и определению 3 существуют состояния Gi,…, Gm и правила преобразования состояний opi,…, opM, такие, что G0 ~opi … ~opM Gm, где M ^ 0, является простой траекторией без кооперации доверенных и недоверенных субъект-сессий для передачи прав доступа, и для каждого k ^ l ^ m существует субъект-сессия sxi Е Sm, такая, что или userM (sxi) = xi, или sxi = xi, существует субъект-сессия syi Е Sm, такая, что userM (syi) = у или syi = yi, и выполняется условие (sxi, syi, owna) Е AM. Положим
opM+i = grant _right (sxm, rym_i, (e, own)) —
opM+m-k = grant_right (sxk+i, fyk, (e, own)) — opM+m-k+i = grant _right (sxk, ryk-i, (e, a)) —
K = M + m — k + 1.
Возможны два случая.
Первый случай: справедливо равенство k = 2. По условию теоремы yi Е island (x), следовательно, по утверждению 1 существуют состояния Gk+i,…, Gn и правила преобразования состояний opK+i,…, opN, такие, что GK ~opK+i GK+i ~opK+2 … ~opN GN, где N ^ K, является простой траекторией без кооперации доверенных и недоверенных субъект-сессий для передачи прав доступа, существуют субъект-сессии sx, syi Е Sn, такие, что выполняются условия:
— userN (sx) = x или sx = x-
— существует субъект-сессия syi Е Sn, такая, что userN (syi) = yi или syi = yi-
— (sx, syi, owna) Е An.
Второй случай: выполняется неравенство k & gt- 2. Тогда выполняется условие is_bridge (xk-i, yk-2,yk-i) = true и последовательность недоверенных субъект-сессий или недоверенных пользователей xi,…, xk-i Е Nu U (Ns П So), субъект-сессий или недоверенных пользователей yi,…, yk-i Е Nu U So удовлетворяет условиям теоремы 1.
Следовательно, истинен предикат simple_can_access_own (x, yk-i, G0), и по определению 3 существуют состояния Gk+1 ,…, Gn и правила преобразования состояний opK+i,.., opN, такие, что Gk -opK+i Gk+i -opK+2 … -opN Gn, где N ^ K, является простой траекторией без кооперации доверенных и недоверенных субъект-сессий для передачи прав доступа, существуют субъект-сессии sx, syk_i Е Sn, такие, что выполняются условия:
— userN (sx) = x-
— syk-i = yk-i или userN (syk-i) = yk-i-
(sx, syk-i, owna) Е AN.
Таким образом, в обоих случаях выполняется условие (e, a) Е de_ facto _rightsN (sx), и траектория G0 -opi … -opN Gn является простой траекторией без кооперации доверенных и недоверенных субъект-сессий для передачи прав доступа. Значит, по определению 8 предикат simple_can_share ((e, a), x, G0) является истинным.
Обоснована достаточность выполнения условий теоремы для истинности предиката simple_can_share ((e, a), x, G0) при x Е Nu.
Докажем необходимость выполнения условий теоремы для истинности предиката simple_can_share ((e, a), x, G0) при x Е Nu. По определению 8 существуют состояния Gi,…, Gn и правила преобразования состояний opi,…, opN, такие, что G0 -opi … -opN Gn, где N ^ 0, является простой траекторией без кооперации доверенных и недоверенных субъект-сессий для передачи прав доступа, и существует субъект-сессия sx Е Sn, такая, что userN (sx) = x и выполняется условие (e, a) Е Е de_facto_rightsN (sx).
Среди всех траекторий выберем ту, у которой длина N является минимальной. Проведем доказательство индукцией по длине траекторий N.
Пусть N = 0, тогда существует недоверенная субъект-сессия sx Е Ns П So, такая, что user0(sx) = x, и выполняется условие (e, a) Е de_facto_rights0(sx). Значит, существует роль r Е R U AR, такая, что (e, a) Е PA0®. Возможны два случая.
Первый случай: выполняется условие r Е roles0(sx) С UA0(x). Следовательно, условие 1 теоремы выполнено.
Второй случай: существует субъект-сессия у Е S0, такая, что r Е roles0(у) и (sx, y, owna) Е A0. Следовательно, по определению 3 истинен предикат simple_can_ access_own (x, у, G0). Таким образом, условие 2 теоремы выполнено.
Пусть N = 1, тогда из минимальности N следует, что выполняются условия (e, a) Е de_facto_rights0(sx) и (e, a) Е de_facto_rightsi (sx). Возможны пять случаев.
Первый случай: существует недоверенная субъект-сессия у Е Ns П So, такая, что-либо у = sx, либо (sx, y, owna) Е A0, и существует роль re Е UA0(user0(y)), такая, что (e, a) Е PA0(re) и opi = take_role (y, re). Если у = sx, то выполнено условие 1 теоремы. Если (sx, y, owna) Е A0, то по определению 3 предикат simple_can_access_own (x, у, G0) является истинным. Следовательно, условие 2 теоремы выполнено.
Второй случай: существует субъект-сессия yi Е S0, такая, что-либо yi = sx, либо (sx, yi, owna) Е A0, и существуют недоверенная субъект-сессия x2 Е Ns П So и роль re Е roles0(yi), такие, что ((e, ownr), re) Е de_facto_actions0(x2), и opi = grant_right (x2,re, (e, a)). Значит, существует субъект-сессия y2 Е S0, такая, что-либо у2 = x2, либо (x2,y2,owna) Е A0, и выполняются условия
(e, ownr) Е PA0(roles0(y2)) и re Е can_manage_rights (roles0(y2) П AR)). Следова-
тельно, справедливо равенство is_simple_bridge (x2,yi, y2) = true. По определению 5 выполняются условия yi Е island (x) и у2 Е island (x2). Положим m = 2. Следовательно, условие 3 теоремы выполнено.
Третий случай: существуют субъект-сессии y, z Е S0, такие, что z Е [у] и либо sx = z, либо (sx, z, owna) Е A0, и (e, a) Е PA0(roles0(у)), opi = control (sx, y, z).
Четвертый случай: существует субъект-сессия у Е S0, такая, что (y, ownr) Е Е de_facto_rights0(sx), (e, a) Е PA0(roles0(y)) и opi = access_own (sx, у). Значит, существует субъект-сессия z Е So, такая, что (sx, z, owna) Е A0 и (y, ownr) Е Е PA0(roles0(z)).
Пятый случай: существуют субъект-сессии y, z Е S0, такие, что {(sx, z, owna), (z, y, owna)} Е A0, и (e, a) Е PA0(roles0(y)), opi = take_access_own (sx, z, y).
В третьем, четвертом и пятом случаях по определению 5 выполняется условие у Е island (x) {x}. Следовательно, по утверждению 1 истинен предикат simple_can_access_own (x, у, G0), и условие 2 теоремы выполнено.
Пусть N & gt- 1 и утверждение теоремы верно для всех траекторий длины
l & lt- N. Докажем, что при длине траектории N если истинен предикат simple_-can_share ((e, a), x, G0), то выполняются условия теоремы.
Из минимальности N следует, что существует недоверенная субъект-сессия sx Е Ns П Sn-i, такая, что user'-N-i (sx) = x, и выполняются условия (e, a) Е de_-facto_rightsN-i (sx) и (e, a) Е de_facto_rightsN (sx). Возможны пять случаев.
Первый случай: существует недоверенная субъект-сессия sy' Е NsПSN-i, такая, что-либо sy = sx, либо (sx, sy& gt-, owna) Е An-i, и существует роль re Е UAn-i (userN-i (sy'-)), такая, что (e, a) Е PAN-i (re) и opN = take_role (sy, re). Положим у'- = userN-i (sy& gt-), тогда по предположению 1 выполняется условие re Е UA0(y'-). Возможны две ситуации.
Первая ситуация: выполняется условие (e, a) Е PA0(re). Если sy' = sx, то выполняется условие (e, a) Е PAo (UAo (x)) и выполнено условие 1 теоремы. Если (sx, sy, owna) Е An-i, то положим у = у'-. Тогда (e, a) Е PA0(UA0(y)) и по определению 3 истинен предикат simple_can_access_own (x, у, G0). Следовательно, выполнено условие 2 теоремы.
Вторая ситуация: выполняется условие (e, a) Е PA0(re). Если sy' = sx, то положим k = 1, yi = sy& gt-. Пусть (sx, sy& gt-, owna) Е An-i, тогда по определению 3 истинен предикат simple_can_access_own (x, у'-, G0). Следовательно, по теореме 1 существуют последовательности недоверенных субъект-сессий или недоверенных пользователей xi,…, xk Е Nu U (Ns П So), субъект-сессий или недоверенных пользователей yi,…, yk Е NuUSo, где k ^ 1, таких, что xi = x, yk = sy, yi Е island (xi), где 1 ^ i ^ m, и выполняются условия:
— если k ^ 2, то справедливо равенство is_bridge (xk, yk-i, yk) = true-
— если k ^ 3, то для каждого 2 ^ i & lt- k справедливо равенство или is_bridge (xi,
yi-i, yi) = true, или is_simple_bridge (xi, yi-i, yi) = true.
При этом существуют 1 ^ M & lt- N и недоверенная субъект-сессия sx' Е Ns ПM-i, такие, что ((e, ownr), re) Е de_facto_actionsM-i (sx/) и opM = grant_right (sx, re, (e, a)). Значит, существует субъект-сессия sy" Е Sm-i, такая, что-либо sxj = sy", либо (sx/, sy", owna) Е Am-i. При этом выполняются условия re Е can_manage_-rights (rolesM-i (sy") П AR)) и (e, ownr) Е PAM-i (rolesM-i (sy")). Положим x'- = = userM-i (sx'-) Е Nu. Если sy& quot- Е Ns, то положим yk+i = userM-i (sy& quot-) Е Nu. Тогда выполняется условие re Е can_manage_rights (UA0(yk+i) П AR)). Если sy" Е Ls, то положим yk+i = sy", по предположению 1 выполняются условия yk+i Е Ls П So и
re Е can_manage_rights (roles0(yk+i) П AR)). Значит, либо x'- = yk+i_, либо истинен предикат simple_can_access_own (x'-, уk+i, G0), и по теореме 1 существует недоверенный пользователь xk+i Е Nu, такой, что yk+i Е island (xk+i). Следовательно, по определению 6 справедливо равенство is_simple_bridge (xk+i, yk, yk+i) = true. При этом так как yk+i Е island (xk+i), то возможен выбор такого xk+i, что истинен предикат simple_can_share ((e, ownr), xk+i, G0) с длиной траектории меньше N.
Значит, по предположению индукции для предиката simple_can_share ((e, ownr), xk+i, Go) и из выполнения одного из условий
— yk+i Е Nu и (e, ownr) Е PAm-i (UAm-i (yk+i)) —
— yk+i Е Ls П So и (e, own) Е PAm-i (rolesM-i (yk+i))
следует, что для предиката simple_can_share ((e, ownr), xk+i, G0) выполнено условие 1 или условие 3 теоремы.
Если для предиката simple_can_share ((e, ownr), xk+i, Go) выполнено условие 1 теоремы, то (e, ownr) Е PAo (UA0(xk+i)) и yk+i = xk+i. Положим m = k + 1.
Если для предиката simple_can_share ((e, ownr), xk+i, Go) выполнено условие 3 теоремы, то существуют последовательности недоверенных субъект-сессий или недоверенных пользователей xk+i,…, xm Е Nu U (Ns П S0), субъект-сессий или недоверенных пользователей yk+]_,…, ym Е Nu U So, где m ^ k +1, таких, что yi Е island (xi), где k + 1 ^ i ^ m, и выполняется одно из условий:
— УmЕ Nu и (e, ownr) Е PAo (UAo (ym)) —
ym Е NS П S0 и (e, ownr) Е P A0(UA0 (user0(ym
))) —
ym Е LS П S0 и (e, ownr) Е P-A0(roles0(y
m)).
При этом справедливо равенство is_simple_bridge (xm, ym-i, ym) = true, и для каждого k + 2 ^ i ^ m справедливо равенство или is_bridge (xi, yi-i, yi) = true, или is _simple _bridge (xi, yi-i, yi) = true.
Таким образом, в первом случае во второй ситуации выполнено условие 3 теоремы. Второй случай: существует субъект-сессия sy Е Sn-i, такая, что-либо sy = sx, либо (sx, sy, owna) Е An-i, и существуют недоверенная субъект-сессия sxj Е Ns П Sn-i и роль re Е rolesN-i (sy), такие, что ((e, ownr), re) Е de_facto_actionsN-i (sx/), и opN = grant_right (sx& gt-, re, (e, a)). Значит, существует субъект-сессия sy Е SN-i, такая, что-либо sy = sx& gt-, либо (sx& gt-, sy, owna) Е An-i, и выполняются условия (e, ownr) Е PAn-i (rolesN-i (sy)), re Е can_manage_rights (rolesN-i (sy& gt->-) П AR)).
Если sy = sx, то положим k = 1, yi = sy. Пусть (sx, sy, owna) Е An-i, тогда по определению 3 истинен предикат simple _can_access _own (x, sy, G0). Следовательно, по теореме 1 существуют последовательности недоверенных субъект-сессий или недоверенных пользователей xi,…, xk Е Nu U (Ns П S0), субъект-сессий или недоверенных пользователей yi,…, yk Е NuUSo, где k ^ 1, таких, что xi = x, yk = sy, yi Е island (xi), где 1 ^ i ^ m, и выполняются условия:
— если k ^ 2, то справедливо равенство is_bridge (xk, yk-i, yk) = true-
— если k ^ 3, то для каждого 2 ^ i & lt- k справедливо равенство или is_bridge (xi, yi-i, yi) = true, или is_simple_bridge (xi, yi-i, yi) = true.
Положим x'- = userN-i (sx'-) Е Nu. Если sy Е Ns, то положим yk+i = userN-i (sy) Е Е Nu. Тогда выполняется условие re Е can_manage_rights (UA0(yk+i) П AR)). Если sy Е Ls, то положим yk+i = sy, по предположению 1 выполняются условия yk+i Е Ls П So и re Е can_manage_rights (roles0(yk+i) П AR)). Значит, либо x'- = yk+i_,
либо истинен предикат simple_can_access_own (x'-, yk+i, Go), и по теореме 1 существует недоверенный пользователь xk+i Е Nu, такой, что yk+i Е island (xk+i). Следовательно, по определению 6 справедливо равенство is_simple_bridge (xk+i, yk, yk+i). При этом так как yk+i Е island (xk+i), то возможен выбор такого xk+i, что истинен предикат simple_can_share ((e, ownr), xk+i, G0) с длиной траектории меньше N.
Значит, по предположению индукции для предиката simple_can_share ((e, ownr), xk+i, Go) и из выполнения одного из условий
— yk+i Е Nu и (e, ownr) Е PAn-i (UAn-i (yk+i)) —
— yk+i Е Ls П So и (e, ownr) Е PAn-i (rolesN-i (yk+i))
следует, что для предиката simple_can_share ((e, ownr), xk+i, G0) выполнено условие 1 или условие 3 теоремы.
Если для предиката simple_can_share ((e, ownr), xk+i, Go) выполнено условие 1 теоремы, то (e, ownr) Е PAo (UA0(xk+i)) и yk+i = xk+i. Положим m = k + 1.
Если для предиката simple_can_share ((e, ownr), xk+i, Go) выполнено условие 3 теоремы, то существуют последовательности недоверенных субъект-сессий или недоверенных пользователей xk+i,…, xm Е Nu U (Ns П S0), субъект-сессий или недоверенных пользователей yk+]_,…, ym Е Nu П So, где m ^ k +1, таких, что yi Е island (xi), где k + 1 ^ i ^ m, и выполняется одно из условий:
— УmЕ Nu и (e, ownr) Е PAo (UAo (ym)) —
— УmЕ Ns П So и (e, own) Е PAo (UAo (usero (ym))) —
— УmЕ Ls П So и (e, own) Е PAo (roleso (ym)).
При этом справедливо равенство is_simple_bridge (xm, ym-i, ym) = true и для каждого k + 2 ^ i ^ m справедливо равенство или is_bridge (xi, yi-i, yi) = true, или is _simple _bridge (xi, yi-i, yi) = true.
Таким образом, во втором случае выполнено условие 3 теоремы.
Третий случай: существуют субъект-сессии sy, sz Е Sn-i, такие, что sz Е [sy] и либо sx = sz, либо (sx, sz, owna) Е An-i, и (e, a) Е PAN-i (rolesN-i (sy& gt-)), opN =
= control (sx, sy& gt-, sz).
Четвертый случай: существует субъект-сессия sy Е Sn-i, такая, что (sy, ownr) Е Е de_facto_rightsN^(s^, (e, a) Е PAN-i (rolesN-i (sy)) и opN = access_own (sx, sy).
Пятый случай: существуют субъект-сессии sy, sz Е Sn-i, такие, что {(sx, sz, owna), (sz, sy, owna)} С An-i, и (e, a) Е PAn-i (roles0(sy& gt-)), opN = take_access_own (sx, sz, sy).
Таким образом, в третьем, четвертом и пятом случае существует роль re Е UAn-i (userN-i (sy)), такая, что (e, a) Е PAN-i (re). При этом, если sy Е Ns, то положим у'- = userN-i (sy), если sy Е Ls, то у'- = sy и по предположению 1 у'- Е LsПSo. Значит, истинен предикат simple_can_access_own (x, у'-, G0), и выполнение условия 2 или 3 теоремы обосновывается аналогично первому случаю.
Следовательно, доказан шаг индукции при длине траектории, равной N. Доказательство необходимости выполнения условия теоремы для истинности предиката simple_can_share ((e, a), x, G0) при x Е Nu выполнено.
Теорема доказана. ¦
Определим и обоснуем алгоритмически проверяемые необходимые и достаточные условия истинности предиката simple_can_share ((e, a), x, G0) для случая, когда x Е Lu.
Теорема 3. Пусть G0 = (PA0,user0,roles0, A0, F0, HEo) -состояние системы
E (G*, OP), в котором существуют доверенный пользователь x Е Lu и право доступа
к сущности (e, a) Е Po. Предикат simple_can_share ((e, a), x, Go) является истинным тогда и только тогда, когда существует доверенная субъект-сессия sx Е Ls П So, такая, что usero (sx) = x и выполняется одно из следующих условий:
1. Выполняется условие (e, a) Е PAo (roleso (sx)).
2. Существуют последовательности недоверенных субъект-сессий или недоверенных пользователей x,…, xm Е Nj U (Ns П So), субъект-сессий или недоверенных пользователей yl,…, ym Е NuUS0, где m ^ 1, таких, что yi Е island (xi), где 1 ^ i ^ m, и выполняется одно из условий:
— УтЕ Nu и (e, ownr) Е PAo (UAo (ym)) —
— УтЕ Ns П So и (e, ownr) Е PAo (UAo (usero (ym))) —
— УmЕ Ls П So и (e, ownr) Е PAo (roleso (ym)).
При этом справедливо равенство is_simple_bridge (xl, sx, y) = true и для каждого
2 ^ i ^ m справедливо равенство is_simple_bridge (xi, yi-i, yi) = true.
Доказательство. Докажем достаточность выполнения условий теоремы для истинности предиката simple_can_share ((e, a), x, Go) при x Е Ljj.
Пусть выполнено условие 1 теоремы. Тогда по определению 8 предикат simple_ can_share ((e, a), x, Go) является истинным.
Пусть выполнено условие 2 теоремы. Докажем истинность предиката simple_can_ share ((e, a), x, Go) индукцией по длине m последовательностей субъект-сессий или недоверенных пользователей.
Пусть m = 1. Тогда по условию теоремы справедливо равенство is_simple_
bridge (xl, sx, y) = true, и по определению 6 yl Е island (xl) и существует роль
re Е roleso (sx), такая, что выполняется одно из условий:
— y Е Nu и (e, ownr) Е PAo (UAo (yi)) и re Е can_manage_rights (AUAo (yl)) —
— yl Е Ns П So и (e, ownr) Е PAo (UAo (usero (yl))) и re Е can_manage_ rights (AU Ao (usero (yl))) —
— yl Е Ls П So и (e, ownr) Е PAo (roleso (yl)) и re Е can_manage_rights (roleso (yl) П ПAR).
По утверждению следствия 1 существуют состояния Go,…, Gm и правила преобразования состояний opo,…, opM, такие, что Go … ~apM Gm, где M ^ 0, является
простой траекторией без кооперации доверенных и недоверенных субъект-сессий для передачи прав доступа, и существует недоверенная субъект-сессия sxi Е Ns П Sm, такая, что-либо User'-M (sxi) = xl, либо sxi = xl, и в состоянии Gm выполняется условие island_actions (xl) = island_actions (sxi) Е de_facto_actionsM (sxi). Значит, выполняется условие ((e, ownr), re) Е de_facto_actionsM (sxi). Положим opM+l = grant_right (sxi, re, (e, a)).
Тогда в состоянии Gm+i, таком, что Gm Ьорм Gm+l, выполняется условие (e, a) Е PAM+l (re) Е PAM+l (rolesM+l (sx)). Так как траектория Go bopi Gl Ьор2 … bopM+i Gm+l является простой траекторией без кооперации доверенных и недоверенных субъект-сессий для передачи прав доступа, то по определению 8 является истинным предикат simple_can_share ((e, a), x, Go).
Заметим, что при m = 1 условие sx Е Ls П So не является существенным, т. е. передача прав доступа возможна в случае, когда sx Е Ns П So.
Пусть m & gt- 1 и утверждение верно для всех последовательностей длины l & lt- m. Докажем достаточность условий теоремы при длине последовательности, равной m.
С учетом сделанного замечания и из предположения индукции следует, что существуют состояния Go,…, Gm и правила преобразования состояний opo,…, opM, такие,
что G0 ~oPi … ~арм Gm, где M ^ 0, является простой траекторией без кооперации доверенных и недоверенных субъект-сессий для передачи прав доступа, и существует субъект-сессия syi Е Sm, такая, что-либо user'-M (syi) = yi, либо syi = yi, и в состоянии Gm выполняется условие (e, a) Е PAm (rolesM (syi)). При этом по условию теоремы и по определению 6 справедливо равенство is_simple_bridge (xi, sx, syi) = true. Выполняя рассуждения, аналогичные использованным при обосновании случая m = 1, получаем, что предикат simple_can_share ((e, a), x, G0) является истинным.
Таким образом, для x Е Lu доказана достаточность выполнения условий теоремы для истинности предиката simple_can_share ((e, a), x, G0).
Докажем для x Е Lu необходимость выполнения условий теоремы для истинности предиката simple_can_share ((e, a), x, G0).
Пусть истинен предикат simple_can_share ((e, a), x, G0). Тогда по определению 8 существуют состояния Gi,…, Gn = (PAn, usern, rolesN, An, Fn, Hen) и правила преобразования состояний opi,…, opN, такие, что G0 ~opi … ~oPN Gn, где N ^ 0, является простой траекторией без кооперации доверенных и недоверенных субъект-сессий для передачи прав доступа, и существует субъект-сессия sx Е Sn, такая, что usern (sx) = x и выполняется условие (e, a) Е de_facto_rightsN (sx). Так как x Е Lu, то по предположению 1 и по определениям 1 и 2 выполняются условия sx Е Ls П So и (e, a) Е PAn (rolesN (sx)).
Среди всех траекторий выберем ту, у которой длина N является минимальной. Проведем доказательство индукцией по длине траекторий N.
Пусть N = 0, тогда (e, a) Е PA0(roles0(sx)). Следовательно, выполнено условие 1 теоремы.
Пусть N = 1, тогда из минимальности N следует, что (e, a) Е PA0(roles0(sx)). Тогда существуют недоверенная субъект-сессия xi Е Ns П So и роль re Е roles0(sx), такие, что ((e, ownr), re) Е de_facto_actions0(xi), и opi = grant_right (xi, re, (e, a)). Значит, существует субъект-сессия yi Е S0, такая, что-либо yi = xi, либо (xi, yi, owna) Е A0, и выполняются условия (e, ownr) Е PA0(roles0(yi)) и re Е can_manage_ rights (roles0(yi) П AR)). Следовательно, справедливо равенство is_simple_bridge (xi, sx, yi) = true. По определению 5 выполняется условие yi Е island (xi). Положим m = 1. Следовательно, условие 2 теоремы выполнено.
Пусть N & gt- 1 и утверждение теоремы верно для всех траекторий длины l & lt- N. Докажем, что при длине траектории N если истинен предикат simple_ can_share ((e, a), x, Go), то выполняются условия теоремы.
Тогда существуют недоверенная субъект-сессия sxj Е Ns П Sn-i и роль re Е rolesN^(s^, такие, что ((e, ownr), re) Е de_facto_actionsN-i (sx/), и opN = = grant_right (sx& gt-, re, (e, a)). Значит, существует субъект-сессия sy Е Sn-i, такая, что-либо sy = sx& gt-, либо (sx& gt-, sy, owna) Е An-i, и выполняются условия (e, ownr) Е Е PAN-i (rolesN-i (sy)), re Е can_manage_rights (rolesN-i (sy& gt-) П AR)).
Положим x'- = userN-i (sxf) Е Nu. Если sy Е Ns, то положим yi = userN-i (sy) Е Nu. Тогда выполняется условие re Е can_manage_rights (UA0(yi) П AR)). Если sy Е Ls, то положим yi = sy, по предположению 1 выполняются условия yi Е Ls П So и re Е can_manage_rights (roles0(yi) П AR)). Значит, либо x'- = yi, либо истинен предикат simple_can_access_own (x'-, yi, G0), и по теореме 1 существует недоверенный пользователь xi Е Nu, такой, что yi Е island (xi). Следовательно, по определению 6 справедливо равенство is_simple_bridge (xi, sx, yi).
Если выполняется одно из условий:
— yi Е Nu и (e, ownr) Е PAo (UAo (yi)) —
— уг Е N3* П 50 И (е, ошщ) Е РЛо (иЛо (ивего (у1))) —
— Уг Е Ья П Бо и (е, о/шпг) Е РЛо (то1ево (у1)),
то положим т = 1, и условие 2 теоремы выполнено.
Пусть ни одно из данных условий не выполняется, тогда заметим, что доверенность субъект-сессии 8х не является существенной при получении принадлежащей ей ролью те права доступа (е, а). Следовательно, так как (е, о/шпг) Е РЛN-г (то1е8м-(8у')), где-либо уг Е N0- и уг = ивегм-1(ву), либо уг = 8 у.е. Ья П Бо, то, многократно повторяя выполненные рассуждения, получаем, что существуют последовательности недоверенных субъект-сессий или недоверенных пользователей х2,.. , хт Е N0 и (N3 П 50), субъект-сессий или недоверенных пользователей у2, …, ут Е N0иБо, где т ^ 2, таких, что уг Е г81апд,(хг), где 2 ^ г ^ т, и выполняется одно из условий:
— утЕ N0 и (е, ОтПг) Е РЛо (иЛо (ут)) —
ут Е NS П 50 и (e, о™пт) Е Р Л0(иЛо (и8его (ут))) —
ут Е П 50 и (e, о™пт) Е Р-Л0(то1е80(у
т)).
При этом справедливо равенство г8 _8гтгр1е _Ътгв, де (х2, уг, у2) = 1гие, и для каждого
3 ^ г ^ т справедливо равенство г8_8гтр1е_Ъггд1де (хг, уг-г, уг) =ие.
Таким образом, выполнено условие 2 теоремы. Следовательно, доказан шаг индукции при длине траектории, равной N.
Доказательство необходимости выполнения условия теоремы для истинности предиката 8%тр1е_сап_8Ъ, ате ((е, а), х, О0) при х Е Ь0 выполнено.
Теорема доказана. ¦
3. Условия реализации информационных потоков по памяти
В рамках БР ДП-модели рассмотрим условия реализации информационных потоков по памяти с участием произвольного числа субъект-сессий для простых траекторий функционирования системы. Дадим определение.
Определение 9. Пусть Оо = (РЛ0,и8ег0,го1е80, Ло, Го, НЕо) -состояние системы Е (О*, ОР), в котором существуют сущности или недоверенные пользователи х, у Е ^ и Ео, где х = у. Определим предикат 8гтр1е_сап_'-штИе_тетоту (х, у, О0), который будет истинным тогда и только тогда, когда существуют состояния Ог,…, Ом и правила преобразования состояний орг,…, орм, такие, что Оо Ьор1 … Ьорм Ом, где N ^ 0, является простой траекторией без кооперации доверенных и недоверенных субъект-сессий для передачи прав доступа, и выполняется условие (х'-, у'-, ттИет) Е Гм, где верно следующее:
— если х Е Ео, то х'- = х- если х Е, то х'- Е Бм и и8етм (х'-) = х-
— если у Е Ео, то у'- = у- если у Е, то у'- Е Бм и и8етм (у'-) = у.
Так как недоверенный пользователь может создать субъект-сессию, то в отличие от дискреционных или мандатных ДП-моделей в рамках БР ДП-модели он может являться источником или приемником информационного потока. С учетом условий функционирования существующих и перспективных КС будем считать, что в дальнейшем выполняется следующее предположение.
Предположение 2. У каждой доверенной субъект-сессии всегда имеется роль, обладающая правами доступа на чтение и запись к некоторой сущности. У каждого недоверенного пользователя имеется авторизованная роль, обладающая правами доступа на чтение и запись к некоторой сущности.
Обоснуем необходимые и достаточные условия истинности предиката 81тр1е_сап_ '-штИе_тетоту (х, у, Оо).
Теорема 4. Пусть G0 = (PA0,user0,roles0, A0, F0, HEo) -состояние системы
E (G*, OP), в котором существуют сущности или недоверенные пользователи x, y Е Nu U E0, где x = у. Предикат simple_can_write_memory (x, у, G0) истинен тогда и только тогда, когда существует последовательность недоверенных пользователей или сущностей ei,…, em Е Nu U Eo, где ei = x, em = у и m ^ 2, таких, что выполняется одно из условий.
1. m = 2 и (x'-, y'-, writem) Е F0, где выполняются условия:
— если x Е E0, то x'- = x- если x Е Nu, то x'- Е S0 и user0(x'-) = x-
— если у Е E0, то у'- = у- если у Е Nu, то у'- Е S0 и user0(y'-) = у.
2. Для каждого i = 1,…, m — 1 выполняется одно из условий:
— ei Е Nu U S0, ei+i Е Nu U Eo и (ei, ei+i, writem) Е F0, где верно следующее:
• если ei Е S0, то ei = ei- если ei Е NU, то ei Е S0 и user0(ei) = ei-
• если ei+i Е Eo, то e! i+i = ei+i- если ei+i Е Nu, то e! i+i Е So и usero (ei+i) = ei+i-
— ei Е Nu U So, ei+i Е E0 S0 и истинен предикат simple_can_share ((ei+i, a), ei, G0), где a Е {writer, appendr}, и верно следующее:
• если ei Е NU, то ei = ei-
• если ei Е S0, то ei = user0(ei) —
— ei+i Е NuUSo, ei Е E0S0 и истинен предикат simple_can_share ((ei, readr), e'-i+1, G0), где верно следующее:
• если ei+i Е Nu, то e! i+i = ei+i-
• если ei+i Е So, то ei+i = usero (ei+i) —
— ei Е Nu U (Ns П S0), ei+i Е Nu U So и истинен simple_can_access_own (ei, ei+i, G0), где верно следующее:
• если ei Е Nu, то ei = ei-
• если ei Е Ns П S0, то ei = user0(ei) —
— ei+i Е NuU (NsПS0), ei Е NuUSo и истинен предикат simple_can_access_own (e'-i+i, ei, G0), где верно следующее:
• если ei+i Е Nu, то e'-i+i = ei+i-
• если ei+i Е Ns П So, то eJi+i = usero (ei+i).
Доказательство. Докажем достаточность выполнения условий теоремы для истинности предиката simple_can_write_memory (x, у, G0).
Пусть выполнено условие 1 теоремы. Тогда по определению 9 предикат simple_can_ write_memory (x, y, G0) является истинным.
Пусть выполнено условие 2 теоремы. Тогда осуществим доказательство индукцией по длине m последовательности недоверенных пользователей или сущностей.
Пусть m = 2. Возможны пять случаев.
Первый случай: x Е Nu U S0, у Е Nu U E0 и (x'-, у'-, writem) Е F0, где выполняются условия:
— если x Е S0, то x'- = x- если x Е Nu, то x'- Е S0 и user0(x'-) = x-
— если у Е E0, то у'- = у- если у Е Nu, то у'- Е S0 и user0(y'-) = у.
Следовательно, по определению 9 предикат simple_can_write_memory (x, у, G0)
является истинным.
Второй случай: x Е NuUSo, у Е E0S0 и истинен предикат simple_can_share ((y, a), x'-, G0), где a Е {writer, appendr}, и верно следующее:
— если x Е Nu, то x'- = x-
— если x Е S0, то x'- = user0(x).
Тогда по определению 8 существуют состояния Gi,…, Gm и правила преобразования состояний op]_,…, opM, такие, что G0 ~opi … ~opM Gm, где M ^ 0, является простой траекторией без кооперации доверенных и недоверенных субъект-сессий для передачи прав доступа, и существует субъект-сессия sx Е Sm, такая, что userM (sx) = x'- и выполняется условие (у, a) Е de_facto_rightsM (sx), где a Е {writer, appendr}. Если a = writer, то положим
opM+i = access _write (sx, y) —
N = M + 1.
Если a = appendr, то положим opM+i = access_append (sx, у) —
N = M + 1.
Таким образом, существует G0 ~opi … ~opN Gn — простая траектория без кооперации доверенных и недоверенных субъект-сессий для передачи прав доступа, и в состоянии Gn выполняется условие (sx, y, writem) Е Fn, где user'-M (sx) = x, либо sx = x. Следовательно, по определению 9 предикат simple_can_write_memory (x, у, G0) является истинным.
В третьем случае: у Е Nu U S0, x Е E0 S0 и истинен предикат simple_can_sha-re ((x, readr), y'-, G0), где верно следующее:
— если у Е Nu, то у'- = у-
— если у Е S0, то у'- = user0(y),
истинность предиката simple_can_write_memory (x, у, G0) обосновывается аналогично второму случаю.
Четвертый случай: x Е Nu U (Ns П So), у Е Nu U S0 и истинен simple_can_access_ own (x'-, y, G0), где верно следующее:
— если x Е Nu, то x'- = x-
— если x Е Ns П So, то x'- = user0(x).
Тогда по определению 3 существуют состояния Gi,…, Gm и правила преобразования состояний opi,…, opM, такие, что G0 ~opi … ~& lt-pM Gm, где M ^ 0, является простой траекторией без кооперации доверенных и недоверенных субъект-сессий для передачи прав доступа, и существуют субъект-сессии sx, sy Е Sm, такие, что user'-M (sx) = x'-, или sy = у, или userM (sy) = у и выполняется условие (sx, sy, owna) Е AM.
Если sy Е Ls П Sm, то по предположению 2 существуют роль r Е rolesM (sy) и сущность e Е EM, такие, что {(e, readr), (e, writer)} С PAM®. Положим opM+i = access _write (sy, e) — opM+2 = take_flow (sx, sy) —
opM+3 post (sx, e,) sy) —
N = M + 3.
Если sy Е Ns П Sm, то по предположению 2 существуют роль r Е UAm (userM (sy)) и сущность e Е EM, такие, что {(e, readr), (e, writer)} С PAM®. Положим opM+i = take _role (sy, r) — opM+2 = access _write (sy, e) — opM+з = take_flow (sx, sy) —
opM+4 post (sx, e,) sy) —
N = M + 4.
Таким образом, существует G0 ~opi … ~opN Gn -простая траектория без кооперации доверенных и недоверенных субъект-сессий для передачи прав доступа, и в состоянии Gn выполняется условие (sx, sy, writem) Е Fn, где верно следующее:
— или sx = x, или userM (sx) = x-
— или sy = у, или userN (sy) = у.
Следовательно, по определению 9 предикат simple_can_write_memory (x, у, G0) является истинным.
В пятом случае: у Е Nu U (Ns П So), x Е Nu U So и истинен simple_can_access_ own (y'-, x, G0), где верно следующее:
— если у Е Nu, то у'- = у-
— если у Е Ns П So, то у'- = user0(y),
истинность предиката simple_can_write_memory (x, у, G0) обосновывается аналогично четвертому случаю.
Пусть m & gt- 2 и утверждение верно для всех последовательностей длины l & lt- m. Докажем достаточность условий теоремы при длине последовательности, равной m.
По условию теоремы существует последовательность недоверенных пользователей или сущностей ei,…, em Е Nu U E0, где ei = x, em = у, таких, что выполняется
условие 2. Возможны четыре случая.
Первый случай: x Е Nu U S0, em-i Е Nu U So. Тогда по предположению индукции истинны предикаты simple_can_write_memory (x, em-i, G0) и simple_can_ write_memory (em-i, y, G0), и по определению 9 существуют состояния Gi,…, Gm и правила преобразования состояний opi,…, opM, такие, что G0 ~opi … ~& lt-pM Gm, где M ^ 0, является простой траекторией без кооперации доверенных и недоверенных субъект-сессий для передачи прав доступа, и выполняется условие (x'-, e'-m_i, writem) Е FM и (e'-m-i, y'-, writem) Е FM, где выполняются условия:
— если x Е S0, то x'- = x- если x Е Nu, то x'- Е SM и userM (x'-) = x-
— если em-i Е So, то e'-m-i = em-i- если e'-m-i Е Nu, то e'-m-i Е Sm и user M (e'-m-i) =
— em-i-
— если у Е E0, то у'- = у- если у Е Nu, то у'- Е SM и userM (у'-) = у.
Положим
opM+i = find (x'-, e'-m-i, у'-) —
N = M +1.
Таким образом, существует G0 ~opi … ~opN Gn -простая траектория без кооперации доверенных и недоверенных субъект-сессий для передачи прав доступа, и в состоянии Gn выполняется условие (x'-, у'-, writem) Е Fn. Следовательно, по определению 9 предикат simple_can_write_memory (x, у, G0) является истинным.
Второй случай: x Е Nu U S0, em-i Е E0 S0. Тогда по предположению индукции истинен предикат simple_can_write_memory (x, em-i, G0) и по определению 9 существуют состояния Gi,…, Gk и правила преобразования состояний op]_,…, opK, такие, что G0 ~opi … ^~opK Gk, где K ^ 0, является простой траекторией без кооперации доверенных и недоверенных субъект-сессий для передачи прав доступа, и выполняется условие (x'-, e'-m-i, writem) Е FK, где, если x Е S0, то x'- = x- если x Е Nu, то x'- Е SK и
userK (x'-) = x.
Кроме того, по условию теоремы у Е Nu U S0 и выполняется одно из условий:
— у Е So и (em-i, readr) Е PAo (roleso (y)) —
— у Е Nu и истинен предикат simple_can_share ((em-i, readr), y, G0) —
— у Е Ns П S0 и истинен предикат simple_can_share ((em-i, readr), user0(y), G0).
При выполнении первого условия положим у'- = у и M = K. При выполнении
второго или третьего условия по определению 8 существуют состояния Gk+i,…, Gm и правила преобразования состояний opK+i,…, opM, такие, что Gk ~opK+i Gk+1 ^~opK+2
… ~opM Gm, где M ^ K, является простой траекторией без кооперации доверенных и недоверенных субъект-сессий для передачи прав доступа, и существует субъект-сессия у'- Е Sm, такая, что или у'- = у, или userM (у'-) = У, и выполняется условие (em-i, readr) Е de_facto_rightsM (у'-). Положим
opM+i = post (x'-, e'-m-i, у'-) —
N = M +1.
Таким образом, существует G0 ~opi … ~opN Gn -простая траектория без кооперации доверенных и недоверенных субъект-сессий для передачи прав доступа, и в состоянии Gn выполняется условие (x'-, у'-, writem) Е Fn. Следовательно, по определению 9 предикат simple_can_write_memory (x, у, G0) является истинным.
Индуктивный шаг в третьем случае: x Е E0 S0, em-i Е Nu U So, обосновывается аналогично второму случаю.
Четвертый случай: x, em-i Е E0 S0. Тогда по условию теоремы m ^ 4 и em-2,y Е Е Nu U S0. Далее индуктивный шаг обосновывается аналогично второму случаю.
Таким образом, доказана достаточность выполнения условий теоремы для истинности предиката simple_can_write_memory (x, у, G0).
Докажем необходимость выполнения условий теоремы для истинности предиката simple_can_write_memory (x, у, G0). По определению 9 существуют состояния G1,…, Gn и правила преобразования состояний opi,…, opN, такие, что G0 ~opi … ~opN Gn, где N ^ 0, является простой траекторией без кооперации доверенных и недоверенных субъект-сессий для передачи прав доступа, и выполняется условие (x'-, у'-, writem) Е Fn, где верно следующее:
— если x Е E0, то x'- = x- если x Е Nu, то x'- Е SN и userN (x'-) = x-
— если у Е E0, то у'- = у- если у Е Nu, то у'- Е SN и userN (у'-) = у.
Среди всех траекторий выберем ту, у которой длина N является минимальной. Проведем доказательство индукцией по длине траекторий N.
Пусть N = 0, тогда (x'-, у'-, writem) Е F0 и выполнено условие 1 теоремы.
Пусть N = 1, тогда из минимальности N следует, что x'-, у'- Е E0, (x'-, у'-, writem) Е F0 и (x'-, у'-, writem) Е Fi. Возможны семь случаев.
Первый случай: у'- Е S0 и opi = access_read (y'-, x), где x'- = x Е E0 S0. Тогда (x, readr) Е de_facto_rights0(y'-) и по определению 8 истинен предикат simple_can_share ((x, readr), user0(y'-), G0). Положим m = 2. Следовательно, условие 2 теоремы выполнено.
Во втором случае: x'- Е S0 и opi = access_write (x'-, у), и третьем случае: x'- Е S0 и opi = access_append (x'-, у), где у'- = у Е E0 S0, выполнение условий теоремы обосновывается аналогично первому случаю.
Четвертый случай: x'- Е S0 и существует субъект-сессия e2 Е S0, такая, что opi = find (x'-, e2, y'-). Тогда (x'-, e2, writem) Е F0, и или (e2,y'-, writem) Е F0, или у'- = у Е E0 S0, (у, в) Е de_facto_rights0(e2), где в Е {writer, appendr}. Значит, либо (e2,y'-, writem) Е F0, либо у'- = у Е E0 S0, (у, в) Е de_facto_rights0(e2) и по определению 8 истинен предикат simple_can_share ((y, в), user0(e2), G0). Положим m = 3. Следовательно, условие 2 теоремы выполнено.
В пятом случае: существует субъект-сессия e2 Е S0, такая, что opi = pass (x'-, e2, y'-), и шестом случае: x'-, y'- Е S0 и существует сущность e2 Е E0, такая, что opi = post (x'-, e2, y'-), выполнение условий теоремы обосновывается аналогично четвертому случаю.
Седьмой случай: x'- Е Ns П So и существует субъект-сессия e2 Е S0, такая, что opi = take_flow (x'-, e2). Тогда (x'-, e2, owna) Е A0 и (e2,y'-, writem) Е F0. Следовательно, по определению 3 истинен предикат simple_can_access_own (user0(x'-), e2, G0). Положим m = 3. Следовательно, условие 2 теоремы выполнено.
Пусть N & gt- 1 и утверждение теоремы верно для всех траекторий длины l & lt- N. Докажем, что при длине траектории N если истинен предикат simple_ can_write_memory (x, y, G0), то выполняются условия теоремы.
Из минимальности N следует, что выполняется условие (x'-, у'-, writem) Е Fn-i. Возможны семь случаев.
Первый случай: у'- Е SN-i и opN = access_read (y'-, x), где x'- = x Е E0 S0. Тогда (x, readr) Е de_facto_rightsN-i (y'-). Если у'- Е Ls П Sn-i, то по предположению 1 выполняются условия у = у'- Е Ls П So и по определению 8 истинен предикат simple_can_share ((x, readr), user0(y), G0). Если у'- Е Ns П SN-i, то либо у = = userN-i (y'-) и по определению 8 истинен предикат simple_can_share ((x, readr), y, G0), либо у = у'- Е Ns^So и по определению 8 истинен предикат simple_can_share ((x, readr), user0(y), G0). Положим m = 2. Следовательно, условие 2 теоремы выполнено.
Во втором случае: x'- Е Sn-i и opN = access_write (x'-, у), и третьем случае: x'- Е SN-i и opN = access_append (x'-, у), где у'- = у Е E0 S0, выполнение условий теоремы обосновывается аналогично первому случаю.
Четвертый случай: x'- Е Sn-1 и существует субъект-сессия s'- Е Sn-i, такая, что opN = find (x'-, s'-, у'-). Тогда (x'-, s'-, writem) Е FN-i, и или (s'-, y'-, writem) Е FN-i, или у'- = у Е E0 S0, (у, в) Е de_facto_rightsN-i (s'-), где в Е {writer, appendr}.
Так как (x'-, s'-, writem) Е FN-i, то истинен предикат simple_can_write_memory (x, s, G0) с длиной траектории меньше N, где-либо s = s'- Е S0, либо s = userN-i (s'-) Е Nu. По предположению индукции существует последовательность недоверенных пользователей или сущностей ei,…, ek Е Nu U Eo, где ei = x, ek = s и k ^ 2, удовлетворяющих условию 1 или 2 теоремы.
Если (s'-, у'-, writem) Е Fn-i, то аналогично существует последовательность недоверенных пользователей или сущностей ek,…, em Е Nu U Eo, где ek = s, em = у и m — k ^ 1, удовлетворяющих условию 1 или 2 теоремы, где-либо s = s'- Е S0, либо s = userN-i (s'-) Е Nu.
Если у'- = у Е E0 S0, (у, в) Е de_facto_rightsN-i (s'-), где в Е {writer, appendr}, то по определению 8 истинен предикат simple_can_share ((y, в), s, G0), где s = userN-i (s'-). Положим m = k + 1, em = y.
Таким образом, в четвертом случае существует последовательность недоверенных пользователей или сущностей ei,…, em Е Nu U Eo, где ei = x, em = у и m ^ 2, удовлетворяющих условию 2 теоремы.
В пятом случае: существует субъект-сессия s'- Е Sn-i, такая, что opN = pass (x'-, s'-, у'-), выполнение условий теоремы обосновывается аналогично четвертому случаю.
Шестой случай: x'-, y'- Е Sn-i и существует сущность e Е En-i, такая, что opN = post (x'-, e, y'-). Из минимальности N и предположения 2 следует, что e Е E0. Значит, выполнение условий теоремы обосновывается аналогично четвертому случаю.
Седьмой случай: x'- Е Ns П Sn-i и существует субъект-сессия s'- Е Sn-i, такая, что opN = take_flow (x'-, s'-). Тогда (x'-, s'-, owna) Е AN-i и (s'-, y'-, writem) Е FN-i. Если s'- Е So, то положим s = s'-- если s'- Е S0, то положим s = userN-i (s'-) Е Nu. Следовательно, либо x = userN-i (x'-) и по определению 3 истинен предикат simple_can_access_own (x, s, G0), либо x = x'- Е Ns П S0 и по определению 3 исти-
нен предикат simple_can_access_own (user0(x), s, G0). Далее обоснование выполнения условий теоремы осуществляется аналогично четвертому случаю.
Значит, доказан шаг индукции при длине траектории, равной N. Доказательство необходимости выполнения условия теоремы для истинности предиката simple_can_write_memory (x, y, G0) выполнено.
Теорема доказана. ¦
Таким образом, в рамках БР ДП-модели для систем с простыми траекториями функционирования обоснованы необходимые и достаточные условия передачи прав доступа или реализации информационных потоков по памяти. В дальнейшем с применением техники доказательства теорем 1−4 планируется описать и обосновать условия передачи прав доступа, реализации информационных потоков по памяти и по времени для произвольных траекторий функционирования систем.
ЛИТЕРАТУРА
1. Девянин П. Н. Базовая ролевая ДП-модель // Прикладная дискретная математика. 2008. № 1(1). С. 64−70.
2. Девянин П. Н. Анализ условий получения доступа владения в рамках базовой ролевой ДП-модели без информационных потоков по памяти // Прикладная дискретная математика. 2009. № 3(5). С. 69−84.

ПоказатьСвернуть
Заполнить форму текущей работой