{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T19:40:03Z","timestamp":1750362003592,"version":"3.41.0"},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2025,5,24]],"date-time":"2025-05-24T00:00:00Z","timestamp":1748044800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,5,24]],"date-time":"2025-05-24T00:00:00Z","timestamp":1748044800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2025,6]]},"DOI":"10.1007\/s11334-025-00611-7","type":"journal-article","created":{"date-parts":[[2025,5,24]],"date-time":"2025-05-24T08:33:43Z","timestamp":1748075623000},"page":"475-499","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formal model-driven security combining B-method and process algebra"],"prefix":"10.1007","volume":"21","author":[{"given":"Akram","family":"Idani","sequence":"first","affiliation":[]},{"given":"Yves","family":"Ledru","sequence":"additional","affiliation":[]},{"given":"German","family":"Vega","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,5,24]]},"reference":[{"key":"611_CR1","doi-asserted-by":"publisher","unstructured":"Probst CW, Hunker J, Gollmann D, Bishop M (eds.) (2010) Insider Threats in Cyber Security. Advances in Information Security, vol. 49. Springer. https:\/\/doi.org\/10.1007\/978-1-4419-7133-3","DOI":"10.1007\/978-1-4419-7133-3"},{"key":"611_CR2","doi-asserted-by":"publisher","unstructured":"Greitzer FL (2019) Insider Threats: It\u2019s the HUMAN, Stupid! In: Proceedings of the Northwest Cybersecurity Symposium. NCS \u201919. Association for Computing Machinery, New York, NY, USA. https:\/\/doi.org\/10.1145\/3332448.3332458","DOI":"10.1145\/3332448.3332458"},{"key":"611_CR3","doi-asserted-by":"crossref","unstructured":"Homoliak I, Toffalini F, Guarnizo J, Elovici Y, Ochoa M (2019) Insight Into Insiders and IT: A Survey of Insider Threat Taxonomies, Analysis, Modeling, and Countermeasures. ACM Computing Surveys 52(2)","DOI":"10.1145\/3303771"},{"key":"611_CR4","unstructured":"Kont M, Pihelgas M, Wojtkowiak J, Trinberg L, Osula A-M (2018) Insider Threat Detection Study. The NATO Cooperative Cyber Defence Centre of Excellence"},{"key":"611_CR5","doi-asserted-by":"publisher","unstructured":"Idani A, Ledru Y, Vega G (2023) A process-centric approach to insider threats identification in information systems. In: Wakrime, A.A., Navarro-Arribas, G., Cuppens, F., Cuppens, N., Benaini, R. (eds.) 18th International Conference on Risks and Security of Internet and Systems - , (CRiSIS\u201923). LNCS, vol. 14529, pp. 231\u2013247. Springer, Morocco. https:\/\/doi.org\/10.1007\/978-3-031-61231-2_15","DOI":"10.1007\/978-3-031-61231-2_15"},{"key":"611_CR6","doi-asserted-by":"crossref","unstructured":"Idani A, Ledru Y (2015) B for Modeling Secure Information Systems - The B4MSecure Platform. In: International Conference on Formal Engineering Methods (ICFEM). LNCS, vol. 9407, pp. 312\u2013318. Springer","DOI":"10.1007\/978-3-319-25423-4_20"},{"key":"611_CR7","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 (1996) The B-book: Assigning Programs to Meanings. Cambridge University Press, UK"},{"key":"611_CR8","doi-asserted-by":"crossref","unstructured":"Ferraiolo DF, Sandhu RS, Gavrila SI, Kuhn DR, Chandramouli R (2001) Proposed NIST standard for Role-based Access Control. In: ACM Transactions on Information and System Security (TISSEC\u2019-01), pp. 224\u2013274","DOI":"10.1145\/501978.501980"},{"key":"611_CR9","doi-asserted-by":"publisher","unstructured":"Basin D, Doser J, Lodderstedt T (2006) Model driven security: From UML models to access control infrastructures. ACM Trans. Softw. Eng. Methodol. 15(1), https:\/\/doi.org\/10.1145\/1125808.1125810","DOI":"10.1145\/1125808.1125810"},{"key":"611_CR10","doi-asserted-by":"crossref","unstructured":"Basin D, Clavel M, Doser J, Egea M (2009) Automated analysis of security-design models. Information & Software Technology 51","DOI":"10.1016\/j.infsof.2008.05.011"},{"key":"611_CR11","doi-asserted-by":"publisher","unstructured":"Basin D, Clavel M, Egea M (2011) A Decade of Model-Driven Security. In: Proceedings of the 16th ACM Symposium on Access Control Models and Technologies. SACMAT\u201911, pp. 1\u201310. ACM. https:\/\/doi.org\/10.1145\/1998441.1998443","DOI":"10.1145\/1998441.1998443"},{"issue":"1","key":"611_CR12","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1145\/1125808.1125811","volume":"15","author":"C Snook","year":"2006","unstructured":"Snook C, Butler M (2006) UML-B: Formal Modeling and Design Aided by UML. ACM Transactions of Software Engineering Methodologies 15(1):92\u2013122","journal-title":"ACM Transactions of Software Engineering Methodologies"},{"key":"611_CR13","unstructured":"Bandara A, Shinpei H, Jurjens J, Kaiya H, Kubo A, Laney R, Mouratidis H, Nhlabatsi A, Nuseibeh B, Tahara Y, Tun T, Washizaki H, Yoshioka N, Yu Y (2010) Security Patterns: Comparing Modeling Approaches. IGI Global"},{"key":"611_CR14","doi-asserted-by":"crossref","unstructured":"Lodderstedt T, Basin D, Doser J (2002) SecureUML: A UML-Based Modeling Language for Model-Driven Security. In: Proceedings of the 5th International Conference on The Unified Modeling Language. UML \u201902. Springer, London, UK, UK. http:\/\/dl.acm.org\/citation.cfm?id=647246.719477","DOI":"10.1007\/3-540-45800-X_33"},{"key":"611_CR15","doi-asserted-by":"publisher","unstructured":"Idani A (2022) The B method meets MDE: review, progress and future. In: Guizzardi, R.S.S., Ralyt\u00e9, J., Franch, X. (eds.) 16th International Conference on Research Challenges in Information Science (RCIS\u201922). LNCS, vol. 446, pp. 495\u2013512. Springer, Spain. https:\/\/doi.org\/10.1007\/978-3-031-05760-1_29","DOI":"10.1007\/978-3-031-05760-1_29"},{"issue":"7","key":"611_CR16","doi-asserted-by":"publisher","first-page":"924","DOI":"10.1109\/TKDE.2008.28","volume":"20","author":"K Sohr","year":"2008","unstructured":"Sohr K, Drouineaud M, Ahn G-J, Gogolla M (2008) Analyzing and managing role-based access control policies. IEEE Transactions on Knowledge and Data Engineering 20(7):924\u2013939. https:\/\/doi.org\/10.1109\/TKDE.2008.28","journal-title":"IEEE Transactions on Knowledge and Data Engineering"},{"key":"611_CR17","doi-asserted-by":"crossref","unstructured":"Leuschel M, Butler M (2003) ProB: A Model Checker for B. In: FME 2003: Formal Methods Europe. LNCS, vol. 2805. Springer","DOI":"10.1007\/978-3-540-45236-2_46"},{"key":"611_CR18","doi-asserted-by":"crossref","unstructured":"Wildmoser M, Nipkow T (2004) Certifying machine code safety: Shallow versus deep embedding. In: Slind, K., Bunker, A., Gopalakrishnan, G. (eds.) Theorem Proving in Higher Order Logics (TPHOLs 2004). LNCS, vol. 3223, pp. 305\u2013320. Springer","DOI":"10.1007\/978-3-540-30142-4_22"},{"key":"611_CR19","doi-asserted-by":"crossref","unstructured":"Butler MJ, Leuschel M (2005) Combining CSP and B for specification and property verification. In: International Symposium of Formal Methods - FM 2005. Lecture Notes in Computer Science, vol. 3582, pp. 221\u2013236. Springer","DOI":"10.1007\/11526841_16"},{"issue":"3","key":"611_CR20","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/s10817-022-09546-9","volume":"68","author":"G Paolo","year":"2022","unstructured":"Paolo G, Pasquale M (2022) Optimizing theorem proving for security policies: A machine learning approach. Journal of Automated Reasoning 68(3):275\u2013298. https:\/\/doi.org\/10.1007\/s10817-022-09546-9","journal-title":"Journal of Automated Reasoning"},{"key":"611_CR21","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2023.103856","volume":"310","author":"Y Bengio","year":"2023","unstructured":"Bengio Y, Lavoie A, Dupont M (2023) Neural theorem proving: Learning to guide formal proofs. Artificial Intelligence Journal 310:103856. https:\/\/doi.org\/10.1016\/j.artint.2023.103856","journal-title":"Artificial Intelligence Journal"},{"issue":"2","key":"611_CR22","first-page":"321","volume":"47","author":"E Clarke","year":"2021","unstructured":"Clarke E, Kroening D (2021) Model checking: State-space reduction techniques. IEEE Transactions on Software Engineering 47(2):321\u2013339","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"8","key":"611_CR23","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R Bryant","year":"1986","unstructured":"Bryant R (1986) Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers 35(8):677\u2013691","journal-title":"IEEE Transactions on Computers"},{"issue":"4","key":"611_CR24","first-page":"1","volume":"26","author":"C Gehrmann","year":"2023","unstructured":"Gehrmann C, Zhao J (2023) Ai-driven security policy verification. ACM Transactions on Privacy and Security 26(4):1\u201320","journal-title":"ACM Transactions on Privacy and Security"},{"key":"611_CR25","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2020.110697","volume":"169","author":"J Geismann","year":"2020","unstructured":"Geismann J, Bodden E (2020) A systematic literature review of model-driven security engineering for cyber-physical systems. Journal of Systems and Software 169:110697. https:\/\/doi.org\/10.1016\/j.jss.2020.110697","journal-title":"Journal of Systems and Software"},{"issue":"1","key":"611_CR26","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 DP (2008) Synthesising verified access control systems through model checking. Journal of Computer Security 16(1):1\u201361","journal-title":"Journal of Computer Security"},{"key":"611_CR27","doi-asserted-by":"crossref","unstructured":"Koleini M, Ryan M (2011) A knowledge-based verification method for dynamic access control policies. In: 13th International Conference on Formal Engineering Methods, ICFEM. LNCS, vol. 6991, pp. 243\u2013258. Springer","DOI":"10.1007\/978-3-642-24559-6_18"},{"issue":"2","key":"611_CR28","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 (2015) Proof-based verification approaches for dynamic properties: application to the information system domain. Formal Asp. Comput. 27(2):335\u2013374. https:\/\/doi.org\/10.1007\/s00165-014-0323-x","journal-title":"Formal Asp. Comput."},{"key":"611_CR29","doi-asserted-by":"crossref","unstructured":"Ledru Y, Idani A, Milhau J, Qamar N, Laleau R, Richier J-L, Labiadh M-A (2014) Validation of IS security policies featuring authorisation constraints. International Journal of Information System Modeling and Design (IJISMD)","DOI":"10.4018\/ijismd.2015010102"},{"key":"611_CR30","doi-asserted-by":"crossref","unstructured":"Radhouani A, Idani A, Ledru Y, Rajeb NB (2015) Symbolic Search of Insider Attack Scenarios from a Formal Information System Modeling. LNCS Transactions on Petri Nets and Other Models of Concurrency 10:131\u2013152","DOI":"10.1007\/978-3-662-48650-4_7"},{"issue":"5","key":"611_CR31","first-page":"835","volume":"36","author":"K Sohr","year":"2010","unstructured":"Sohr K, Drouineaud M, Ahn G (2010) Analyzing and managing role-based access control policies in uml. IEEE Transactions on Software Engineering 36(5):835\u2013856","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"1","key":"611_CR32","first-page":"55","volume":"21","author":"L Baresi","year":"2023","unstructured":"Baresi L, Pasquale M (2023) Machine learning for automated security analysis. IEEE Security & Privacy 21(1):55\u201367","journal-title":"IEEE Security & Privacy"},{"key":"611_CR33","unstructured":"Huang W, Li T (2022) Parallel execution of csp models for large-scale security verification. Journal of Formal Methods in Computer Science 19(3):102\u2013121"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-025-00611-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11334-025-00611-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-025-00611-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T19:02:57Z","timestamp":1750359777000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11334-025-00611-7"}},"subtitle":["The B4MSecure Platform"],"short-title":[],"issued":{"date-parts":[[2025,5,24]]},"references-count":33,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2025,6]]}},"alternative-id":["611"],"URL":"https:\/\/doi.org\/10.1007\/s11334-025-00611-7","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"type":"print","value":"1614-5046"},{"type":"electronic","value":"1614-5054"}],"subject":[],"published":{"date-parts":[[2025,5,24]]},"assertion":[{"value":"31 October 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 May 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 May 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}]}}