{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T15:51:14Z","timestamp":1781106674039,"version":"3.54.1"},"reference-count":47,"publisher":"IGI Global Scientific Publishing","issue":"1","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015,1,1]]},"abstract":"<p>Designing a security policy for an information system (IS) is a non-trivial task. Variants of the RBAC model can be used to express such policies as access-control rules associated to constraints. In this paper, we advocate that currently available tools do not take sufficiently into account the functional description of the application and its impact on authorisation constraints and dynamic aspects of security. The authors suggest translating both security and functional models into a formal language, such as B, whose analysis and animation tools will help validate a larger set of security scenarios. The authors describe how various kinds of constraints can be expressed and animated in this context. The authors also present a tool support which performs this translation and report on a case study where animation and testing techniques were used to validate the security policy of a medical emergency information system.<\/p>","DOI":"10.4018\/ijismd.2015010102","type":"journal-article","created":{"date-parts":[[2015,2,18]],"date-time":"2015-02-18T07:18:03Z","timestamp":1424243883000},"page":"24-46","source":"Crossref","is-referenced-by-count":8,"title":["Validation of IS Security Policies Featuring Authorisation Constraints"],"prefix":"10.4018","volume":"6","author":[{"given":"Yves","family":"Ledru","sequence":"first","affiliation":[{"name":"University Grenoble Alpes, LIG, Grenoble, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Akram","family":"Idani","sequence":"additional","affiliation":[{"name":"University Grenoble Alpes, LIG, Grenoble, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"J\u00e9r\u00e9my","family":"Milhau","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris-Est, LACL, UPEC, IUT S\u00e9nart-Fontainebleau, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nafees","family":"Qamar","sequence":"additional","affiliation":[{"name":"University Grenoble Alpes, LIG, Grenoble, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"R\u00e9gine","family":"Laleau","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris-Est, LACL, UPEC, IUT S\u00e9nart-Fontainebleau, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jean-Luc","family":"Richier","sequence":"additional","affiliation":[{"name":"CNRS, LIG, Grenoble, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mohamed Amine","family":"Labiadh","sequence":"additional","affiliation":[{"name":"University Grenoble Alpes, LIG, Grenoble, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"2432","reference":[{"key":"ijismd.2015010102-0","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162"},{"key":"ijismd.2015010102-1","doi-asserted-by":"publisher","DOI":"10.1145\/1266840.1266875"},{"key":"ijismd.2015010102-2","unstructured":"Autrel, F., Cuppens, F., Cuppens-Boulahia, N., & Coma-Brebel, C. (2008). MotOrBAC 2: a security policy tool. In SARSSI\u201908: 3\u00e8me conf. sur la S\u00e9curit\u00e9 des Architectures R\u00e9seaux et des Syst\u00e8mes d\u2019Information."},{"key":"ijismd.2015010102-3","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2008.05.011"},{"key":"ijismd.2015010102-4","doi-asserted-by":"publisher","DOI":"10.1145\/1998441.1998443"},{"key":"ijismd.2015010102-5","doi-asserted-by":"publisher","DOI":"10.1145\/1125808.1125810"},{"key":"ijismd.2015010102-6","first-page":"184","article-title":"A Comparison of Commercial and Military Computer Security Policies.","author":"D. D.Clark","year":"1987","journal-title":"IEEE Symposium on Security and Privacy"},{"key":"ijismd.2015010102-7","first-page":"130","article-title":"A Methodology for Secure Software Design.","author":"E. B.Fern\u00e1ndez","year":"2004","journal-title":"Proceedings of the International Conference on Software Engineering Research and Practice, SERP\u201904"},{"key":"ijismd.2015010102-8","author":"D. F.Ferraiolo","year":"2003","journal-title":"Role-Based Access Control"},{"key":"ijismd.2015010102-9","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2011.11.017"},{"key":"ijismd.2015010102-10","unstructured":"Frappier, M., Gervais, F., Laleau, R., & Fraikin, B. (2008). Algebraic State Transition Diagrams (Tech.Rep.No.24). Sherbrooke, Qu\u00e9bec, Canada: Universit\u00e9 de Sherbrooke, D\u00e9partement d\u2019informatique. Available from http:\/\/www.dmi.usherb.ca\/gril\/doc\/eb3pai\/pdf\/08-TR24.pdf"},{"key":"ijismd.2015010102-11","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-008-0064-1"},{"key":"ijismd.2015010102-12","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-003-0024-z"},{"key":"ijismd.2015010102-13","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.01.013"},{"key":"ijismd.2015010102-14","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90035-9"},{"key":"ijismd.2015010102-15","author":"C. A. R.Hoare","year":"1985","journal-title":"CSP \u2013 Communicating Sequential Processes"},{"key":"ijismd.2015010102-16","article-title":"Automated Checking of SAP Security Permissions.","author":"S.H\u00f6hn","year":"2003","journal-title":"6th Working Conference on Integrity and Internal Control in Information Systems (IICIS)"},{"key":"ijismd.2015010102-17","doi-asserted-by":"publisher","DOI":"10.1145\/1368088.1368228"},{"issue":"3","key":"ijismd.2015010102-18","doi-asserted-by":"crossref","first-page":"87","DOI":"10.3166\/isi.15.3.87-112","article-title":"Infrastructure dirig\u00e9e par les mod\u00e8les pour une int\u00e9gration adaptable et \u00e9volutive de UML et B.","volume":"15","author":"A.Idani","year":"2010","journal-title":"Ing\u00e9nierie des Syst\u00e8mes d\u2019Information"},{"key":"ijismd.2015010102-19","doi-asserted-by":"publisher","DOI":"10.1145\/505145.505149"},{"key":"ijismd.2015010102-20","author":"J.J\u00fcrjens","year":"2004","journal-title":"Secure Systems Development with UML"},{"key":"ijismd.2015010102-21","doi-asserted-by":"publisher","DOI":"10.1109\/ICECCS.2005.61"},{"key":"ijismd.2015010102-22","article-title":"Model-based security analysis for mobile communications.","author":"J.J\u00fcrjens","year":"2008","journal-title":"Proceedings of the 30th International Conference on Software Engineering (ICSE 2008)"},{"key":"ijismd.2015010102-23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78743-3_21"},{"key":"ijismd.2015010102-24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22056-2_62"},{"key":"ijismd.2015010102-25","doi-asserted-by":"publisher","DOI":"10.1145\/1998441.1998471"},{"key":"ijismd.2015010102-26","doi-asserted-by":"crossref","unstructured":"Leuschel, M., & Butler, M. (2003). ProB: A Model Checker for B. In FME 2003: Formal methods (LNCS Vol. 2805, pp. 855\u2013874). Springer.","DOI":"10.1007\/978-3-540-45236-2_46"},{"key":"ijismd.2015010102-27","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-007-0063-9"},{"key":"ijismd.2015010102-28","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2005.05.002"},{"key":"ijismd.2015010102-29","unstructured":"Matulevi\u010dius, R., & Dumas, M. (2011). Towards Model Transformation between SecureUML and UMLsec for Role-based Access Control. In Proceedings of the 2011 conference on Databases and Information, DB&IS 2010, pages 339\u2013352, IOS Press Amsterdam."},{"key":"ijismd.2015010102-30","unstructured":"Milhau, J. (2011). Un processus formel d\u2019int\u00e9gration de politiques de contr\u00f4le d\u2019acc\u00e8s dans les syst\u00e8mes d\u2019information. Doctoral dissertation, Universit\u00e9 de Sherbrooke - Universit\u00e9 Paris Est. http:\/\/tel.archives-ouvertes.fr\/docs\/00\/67\/48\/65\/PDF\/TH2011PEST1038_complete.pdf"},{"key":"ijismd.2015010102-31","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16265-7_18"},{"key":"ijismd.2015010102-32","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-011-0166-z"},{"key":"ijismd.2015010102-33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11811-1_31"},{"key":"ijismd.2015010102-34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19125-1_2"},{"key":"ijismd.2015010102-35","doi-asserted-by":"publisher","DOI":"10.1145\/990036.990054"},{"key":"ijismd.2015010102-36","unstructured":"Salabert, K., Milhau, J., Fraikin, B., Frappier, M., Gervais, F., & Laleau, R. (2010). iASTD: un interpr\u00e9teur pour les ASTD. In AFADL 2010, Poitiers, France."},{"key":"ijismd.2015010102-37","article-title":"Policy analysis for security-enhanced Linux.","author":"B.Sarna-Starosta","year":"2004","journal-title":"Proceedings of the 2004 Workshop on Issues in the Theory of Security (WITS2004)"},{"key":"ijismd.2015010102-38","doi-asserted-by":"publisher","DOI":"10.1145\/507712.507714"},{"key":"ijismd.2015010102-39","doi-asserted-by":"publisher","DOI":"10.1145\/1125808.1125811"},{"key":"ijismd.2015010102-40","doi-asserted-by":"publisher","DOI":"10.1109\/TKDE.2008.28"},{"key":"ijismd.2015010102-41","author":"J. M.Spivey","year":"1992","journal-title":"Z Notation \u2013 a reference manual"},{"key":"ijismd.2015010102-42","doi-asserted-by":"publisher","DOI":"10.1145\/1542207.1542212"},{"key":"ijismd.2015010102-43","author":"J. B.Warmer","year":"1998","journal-title":"The Object Constraint Language: Precise Modeling with UML"},{"key":"ijismd.2015010102-44","doi-asserted-by":"crossref","unstructured":"Wildmoser, M., & Nipkow, T. (2004). Certifying Machine Code Safety: Shallow versus DeepEmbedding. In K. Slind, A. Bunker, & G. Gopalakrishnan (Eds.), Theorem Proving in Higher Order Logics (LNCS Vol. 3223, p. 305\u2013320). Springer.","DOI":"10.1007\/978-3-540-30142-4_22"},{"key":"ijismd.2015010102-45","doi-asserted-by":"publisher","DOI":"10.1109\/ICECCS.2009.16"},{"key":"ijismd.2015010102-46","unstructured":"Zao, J., Wee, H., Chu, J., & Jackson, D. (2003). RBAC Schema Verification Using Lightweight Formal Model and Constraint Analysis. In SACMAT 2003,8th ACM symposium on Access Control Models and Technologies. ACM."}],"container-title":["International Journal of Information System Modeling and Design"],"original-title":[],"language":"ng","link":[{"URL":"https:\/\/www.igi-global.com\/viewtitle.aspx?TitleId=123606","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,6,1]],"date-time":"2022-06-01T21:38:24Z","timestamp":1654119504000},"score":1,"resource":{"primary":{"URL":"https:\/\/services.igi-global.com\/resolvedoi\/resolve.aspx?doi=10.4018\/ijismd.2015010102"}},"subtitle":[""],"short-title":[],"issued":{"date-parts":[[2015,1,1]]},"references-count":47,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,1]]}},"URL":"https:\/\/doi.org\/10.4018\/ijismd.2015010102","relation":{},"ISSN":["1947-8186","1947-8194"],"issn-type":[{"value":"1947-8186","type":"print"},{"value":"1947-8194","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,1,1]]}}}