{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T19:24:21Z","timestamp":1750361061596},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662486498"},{"type":"electronic","value":"9783662486504"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-48650-4_7","type":"book-chapter","created":{"date-parts":[[2015,11,23]],"date-time":"2015-11-23T14:25:07Z","timestamp":1448288707000},"page":"131-152","source":"Crossref","is-referenced-by-count":3,"title":["Symbolic Search of Insider Attack Scenarios from a Formal Information System Modeling"],"prefix":"10.1007","author":[{"given":"Amira","family":"Radhouani","sequence":"first","affiliation":[]},{"given":"Akram","family":"Idani","sequence":"additional","affiliation":[]},{"given":"Yves","family":"Ledru","sequence":"additional","affiliation":[]},{"given":"Narjes","family":"Ben Rajeb","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,11,24]]},"reference":[{"key":"7_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book: Assigning Programs to Meanings","author":"J-R Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/BFb0053357","volume-title":"B\u201998: Recent Advances in the Development and Use of the B Method","author":"J-R Abrial","year":"1998","unstructured":"Abrial, J.-R., Mussat, L.: Introducing dynamic constraints in B. In: Bert, D. (ed.) B 1998. LNCS, vol. 1393, pp. 83\u2013128. Springer, Heidelberg (1998)"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1007\/978-3-540-75209-7_30","volume-title":"Model Driven Engineering Languages and Systems","author":"K Anastasakis","year":"2007","unstructured":"Anastasakis, K., Bordbar, B., Georg, G., Ray, I.: UML2Alloy: a challenging model transformation. In: Engels, G., Opdyke, B., Schmidt, D.C., Weil, F. (eds.) MODELS 2007. LNCS, vol. 4735, pp. 436\u2013450. Springer, Heidelberg (2007)"},{"key":"7_CR4","doi-asserted-by":"publisher","first-page":"815","DOI":"10.1016\/j.infsof.2008.05.011","volume":"51","author":"D Basin","year":"2009","unstructured":"Basin, D., Clavel, M., Doser, J., Egea, M.: Automated analysis of security-design models. Inf. Softw. Technol. 51, 815\u2013831 (2009)","journal-title":"Inf. Softw. Technol."},{"issue":"1","key":"7_CR5","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1145\/1125808.1125810","volume":"15","author":"D Basin","year":"2006","unstructured":"Basin, D., Doser, J., Lodderstedt, T.: Model driven security: from UML models to access control infrastructures. ACM Trans. Softw. Eng. Methodol. 15(1), 39\u201391 (2006)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"issue":"3","key":"7_CR6","doi-asserted-by":"publisher","first-page":"20:1","DOI":"10.1145\/1805974.1805976","volume":"13","author":"MY Becker","year":"2010","unstructured":"Becker, M.Y., Nanz, S.: A logic for state-modifying authorization policies. ACM Trans. Inf. Syst. Secur. 13(3), 20:1\u201320:28 (2010)","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/11415787_18","volume-title":"ZB 2005: Formal Specification and Development in Z and B","author":"D Bert","year":"2005","unstructured":"Bert, D., Potet, M.-L., Stouls, N.: GeneSyst: a tool to reason about behavioral aspects of B event specifications. Application to security properties. In: Treharne, H., King, S., Henson, M., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455, pp. 299\u2013318. Springer, Heidelberg (2005)"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"Fisler, K., Krishnamurthi, S., Meyerovich, L.A., Tschantz, M.C.: Verification and change-impact analysis of access-control policies. In: Proceedings of the 27th International Conference on Software Engineering, ICSE 2005, pp. 196\u2013205. ACM, New York (2005)","DOI":"10.1145\/1062455.1062502"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-642-24559-6_18","volume-title":"Formal Methods and Software Engineering","author":"M Koleini","year":"2011","unstructured":"Koleini, M., Ryan, M.: A knowledge-based verification method for dynamic access control policies. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 243\u2013258. Springer, Heidelberg (2011)"},{"issue":"4","key":"7_CR10","doi-asserted-by":"publisher","first-page":"796","DOI":"10.1017\/S0960129512000266","volume":"23","author":"M Kuhlmann","year":"2013","unstructured":"Kuhlmann, M., Sohr, K., Gogolla, M.: Employing UML and OCL for designing and analysing role-based access control. Math. Struct. Comput. Sci. 23(4), 796\u2013833 (2013)","journal-title":"Math. Struct. Comput. Sci."},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-540-24756-2_11","volume-title":"Integrated Formal Methods","author":"K Lano","year":"2004","unstructured":"Lano, K., Clark, D., Androutsopoulos, K.: UML to B: formal verification of object-oriented models. In: Boiten, E.A., Derrick, J., Smith, G. (eds.) IFM 2004. LNCS, vol. 2999, pp. 187\u2013206. Springer, Heidelberg (2004)"},{"key":"7_CR12","series-title":"Lecture Notes in Business Information Processing","doi-asserted-by":"publisher","first-page":"592","DOI":"10.1007\/978-3-642-22056-2_62","volume-title":"Advanced Information Systems Engineering Workshops","author":"Y Ledru","year":"2011","unstructured":"Ledru, Y., Idani, A., Milhau, J., Qamar, N., Laleau, R., Richier, J.-L., Labiadh, M.-A.: Taking into account functional models in the validation of IS security policies. In: Salinesi, C., Pastor, O. (eds.) CAiSE Workshops 2011. LNBIP, vol. 83, pp. 592\u2013606. Springer, Heidelberg (2011)"},{"key":"7_CR13","doi-asserted-by":"publisher","first-page":"24","DOI":"10.4018\/ijismd.2015010102","volume":"6","author":"Y Ledru","year":"2014","unstructured":"Ledru, Y., Idani, A., Milhau, J., Qamar, N., Laleau, R., Richier, J.-L., Labiadh, M.-A.: Validation of IS security policies featuring authorisation constraints. Int. J. Inf. Syst. Model. Des. (IJISMD) 6, 24\u201346 (2014)","journal-title":"Int. J. Inf. Syst. Model. Des. (IJISMD)"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Ledru, Y., Qamar, N., Idani, A., Richier, J.-L., Labiadh, M.-A.: Validation of security policies by the animation of Z specifications. In: Proceedings of the 16th ACM Symposium on Access Control Models and Technologies, SACMAT 2011. ACM, New York (2011)","DOI":"10.1145\/1998441.1998471"},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"Ledru, Y., Idani, A., Richier, J.-L.: Validation of a security policy by the test of its formal B specification - a case study. In: 3rd International Workshop on Formal Methods in Software Engineering (FormaliSE 2015), Colocated with International Conference on Software Engineering, pp. 13\u201322. IEEE Computer Society (2015)","DOI":"10.1109\/FormaliSE.2015.9"},{"key":"7_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"855","DOI":"10.1007\/978-3-540-45236-2_46","volume-title":"FME 2003: Formal Methods","author":"M Leuschel","year":"2003","unstructured":"Leuschel, M., Butler, M.: ProB: a model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855\u2013874. Springer, Heidelberg (2003)"},{"issue":"2","key":"7_CR17","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/s00165-014-0323-x","volume":"27","author":"A Mammar","year":"2015","unstructured":"Mammar, A., Frappier, M.: Proof-based verification approaches for dynamic properties: application to the information system domain. Formal Aspects Comput. 27(2), 335\u2013374 (2015)","journal-title":"Formal Aspects Comput."},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"Qamar, N., Ledru, Y., Idani, A.: Evaluating RBAC supported techniques and their validation and verification. In: 6th International Conference on Availability, Reliability and Security (ARES 2011). IEEE Computer Society, Vienna, Autriche, August 2011","DOI":"10.1109\/ARES.2011.112"},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"Radhouani, A., Idani, A., Ledru, Y., Rajeb, N.B.: Extraction of insider attack scenarios from a formal information system modeling. In: 5th International Workshop on Formal Methods for Security (FMS) (2014)","DOI":"10.1007\/978-3-662-48650-4_7"},{"issue":"1","key":"7_CR20","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1145\/1125808.1125811","volume":"15","author":"C Snook","year":"2006","unstructured":"Snook, C., Butler, M.: UML-B: formal modeling and design aided by UML. ACM Trans. Softw. Eng. Methodol. 15(1), 92\u2013122 (2006)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"7_CR21","doi-asserted-by":"crossref","unstructured":"Toahchoodee, M., Ray, I., Anastasakis, K., Georg, G., Bordbar, B.: Ensuring spatio-temporal access control for real-world applications. In: Proceedings of the 14th ACM Symposium on Access Control Models and Technologies, SACMAT 2009, pp. 13\u201322. ACM, New York (2009)","DOI":"10.1145\/1542207.1542212"},{"issue":"4","key":"7_CR22","doi-asserted-by":"publisher","first-page":"19:1","DOI":"10.1145\/1592434.1592436","volume":"41","author":"J Woodcock","year":"2009","unstructured":"Woodcock, J., Larsen, P.G., Bicarregui, J., Fitzgerald, J.: Formal methods: practice and experience. ACM Comput. Surv. 41(4), 19:1\u201319:36 (2009)","journal-title":"ACM Comput. Surv."},{"key":"7_CR23","unstructured":"Zao, J., Wee, H., Chu, J., Jackson, D.: RBAC schema verification using lightweight formal model and constraint analysis. In: Proceedings of the 8th ACM Symposium on Access Control Models and Technologies, SACMAT 2003. ACM (2003)"},{"key":"7_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"446","DOI":"10.1007\/11556992_32","volume-title":"Information Security","author":"N Zhang","year":"2005","unstructured":"Zhang, N., Ryan, M.D., Guelev, D.P.: Evaluating access control policies through model checking. In: Zhou, J., L\u00f3pez, J., Deng, R.H., Bao, F. (eds.) ISC 2005. LNCS, vol. 3650, pp. 446\u2013460. Springer, Heidelberg (2005)"},{"issue":"1","key":"7_CR25","doi-asserted-by":"publisher","first-page":"1","DOI":"10.3233\/JCS-2008-16101","volume":"16","author":"N Zhang","year":"2008","unstructured":"Zhang, N., Ryan, M., Guelev, D.P.: Synthesising verified access control systems through model checking. J. Comput. Secur. 16(1), 1\u201361 (2008)","journal-title":"J. Comput. Secur."}],"container-title":["Lecture Notes in Computer Science","Transactions on Petri Nets and Other Models of Concurrency X"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-48650-4_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T16:56:47Z","timestamp":1559321807000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-48650-4_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662486498","9783662486504"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-48650-4_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}