Description

This is a publicly available part of the Event-B specification of the Hierarchical Integrated Model of Access Control and Information Flows (the HIMACF model, previously known as the MROSL DP-model). This part contains specification of the role-based access control and is described in the following book (in Russian): Моделирование и верификация политик безопасности управления доступом в операционных системах.

Citation

For citing or referencing this work, please use the following BibTeX entry:

@book{devyanin_security_monograph_2019,
    author = {Devyanin, P. N. and Efremov, D. V. and Kuliamin, V. V. and Petrenko, A. K. and Khoroshilov, A. V. and Shchepetkov, I. V.},
    title = {Modeling and Verification of Access Control Security Policies in Operating Systems},
    publisher = {Goryachaya Liniya -- Telekom},
    year = {2019},
    address = {Moscow, Russian Federation},
    pages = {214},
    isbn = {978-5-9912-0787-4},
    url = {http://www.ispras.ru/publications/2018/security_policy_modeling_and_verification/}
}