Abstract
We address the proof-based development of (system) models satisfying a security policy. The security policy is expressed in a model called OrBAC, which allows one to state permissions and prohibitions on actions and activities and belongs to the family of role-based access control formalisms. The main question is to validate the link between the security policy expressed in OrBAC and the resulting system; a first abstract B model is derived from the OrBAC specification of the security policy and then the model is refined to introduce properties that can be expressed in OrBAC. The refinement guarantees that the resulting B (system) model satisfies the security policy. We present a generic development of a system with respect to a security policy and it can be instantiated later for a given security policy.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Abou El Kalam, A., El Baida, R., Balbiani, P., Benferhat, S., Cuppens, F., Deswarte, Y., Miège, A., Saurel, C., Trouessin, G.: Organization Based Access Control. In: 4th IEEE International Workshop on Policies for Distributed Systems and Networks (Policy 2003) (June 2003)
Abrial, J.-R.: Etude systéme: méthode et exemple, http://www.atelierb.societe.com/documents.html
Abrial, J.R.: The B Book - Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)
Back, R.-J., von Wright, J.: Refinement Calculus. Springer, Heidelberg (1998)
Bell, D.E., LaPadula, L.J.: Secure computer systems: Unified exposition and multics interpretation. MTR-2997 (ESD-TR-75-306), available as NTIS AD-A023 588, MITRE Corporation (1976)
Biba, K.: Integrity consideration for secure computer systems. Technical Report MTR-3153, MITRE Corporation (1975)
Cansell, D., Méry, D.: Logical foundations of the B method. Computers and Informatics 22 (2003)
Chandy, K.M., Misra, J.: Parallel Program Design A Foundation. Addison-Wesley, Reading (1988)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (2000)
ClearSy. Web site B4free set of tools for development of B models (2004)
Cuppens, F.: Orbac web page, http://www.orbac.org
Ferraiolo, D.F., Sandhu, R., Gavrila, S., Kuhn, D.R., Chandramouli, R.: Proposed nist standard for role-based access control. ACM Transactions on Information and System Security 4(3), 222–274 (2001)
Gavrila, S.I., Barkley, J.F.: Formal specification for role based access control user/role and role/role relationship management. In: ACM Workshop on Role-Based Access Control, pp. 81–90 (1998)
Lampson, B.: Protection. In: Proceedings of the 5th Annual Princeton Conference on Information Sciences and Systems, pp. 437–443. Princeton University (1971)
Sandhu, R., Coyne, E.J., Feinstein, H.L., Youman, C.E.: Role-based access control models. IEEE Computer 29(2), 38–47 (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Benaïssa, N., Cansell, D., Méry, D. (2006). Integration of Security Policy into System Modeling. In: Julliand, J., Kouchnarenko, O. (eds) B 2007: Formal Specification and Development in B. B 2007. Lecture Notes in Computer Science, vol 4355. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11955757_19
Download citation
DOI: https://doi.org/10.1007/11955757_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-68760-3
Online ISBN: 978-3-540-68761-0
eBook Packages: Computer ScienceComputer Science (R0)