{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,10]],"date-time":"2026-03-10T20:35:18Z","timestamp":1773174918959,"version":"3.50.1"},"publisher-location":"Cham","reference-count":51,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031197611","type":"print"},{"value":"9783031197628","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-19762-8_28","type":"book-chapter","created":{"date-parts":[[2022,10,19]],"date-time":"2022-10-19T08:03:09Z","timestamp":1666166589000},"page":"382-405","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Towards a\u00a0Methodology for\u00a0Formally Analyzing Federated Identity Management Systems"],"prefix":"10.1007","author":[{"given":"Katerina","family":"Ksystra","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maria","family":"Dimarogkona","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nikolaos","family":"Triantafyllou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Petros","family":"Stefaneas","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Petros","family":"Kavassalis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,10,17]]},"reference":[{"key":"28_CR1","doi-asserted-by":"crossref","unstructured":"Chadwick, D.W., Inman, G.: Attribute Aggregation in Federated Identity Management. IEEE Computer Society (2009). https:\/\/ieeexplore.ieee.org\/document\/5070036\/references#references","DOI":"10.1109\/MC.2009.143"},{"key":"28_CR2","doi-asserted-by":"crossref","unstructured":"Carretero, J., et al.: Federated Identity Architecture of the European eID System (2018). https:\/\/ieeexplore.ieee.org\/abstract\/document\/8543142","DOI":"10.1109\/ACCESS.2018.2882870"},{"key":"28_CR3","unstructured":"EduGain. https:\/\/edugain.org\/"},{"key":"28_CR4","unstructured":"eIDAS Netowrk. https:\/\/ec.europa.eu\/cefdigital\/wiki\/pages\/viewpage.action?pageId=82773030"},{"key":"28_CR5","unstructured":"Fusion Middleware Administrator\u2019s Guide for Oracle Identity Federation. https:\/\/docs.oracle.com\/en\/middleware\/"},{"key":"28_CR6","unstructured":"LEPS. D7.2 - Cost-benefit assessment of CEF eID uptake by private sector. Petros Kavassalis (2018). http:\/\/www.leps-project.eu\/node\/359"},{"key":"28_CR7","first-page":"11","volume":"71, C","author":"E Ghazizadeh","year":"2016","unstructured":"Ghazizadeh, E., Manan, J.A., Zamani, M., Pashang, A.: A survey of security issues for cloud computing. J. Netw. Comput. Appl. 71, C, 11\u201329 (2016)","journal-title":"J. Netw. Comput. Appl."},{"key":"28_CR8","unstructured":"Gro\u00df, T.: Security analysis of the SAML single sign-on browser\/artifact profile. In: Proceedings ACSAC 2003 (19th Annual Computer Security Applications Conference)"},{"key":"28_CR9","unstructured":"Rodriguez, U.F., Laurent-Maknavicius, M., Incera-Dieguez, J.: Federated identity architectures. In: Proceedings MCIS 2006 (Mediterranean Conference of Information Systems)"},{"key":"28_CR10","doi-asserted-by":"crossref","unstructured":"Pfitzmann, B., Waidner, M.: Federated identity-management protocols. In: Proceedings of the 11th International Conference on Security, pp. 153\u2013174 (2003)","DOI":"10.1007\/11542322_20"},{"key":"28_CR11","doi-asserted-by":"crossref","unstructured":"You, J.H., Jun, M.S.: A mechanism to prevent RP phishing in OpenID system. In: Proceedings of 9th International Conference on Computer and Information Science (2010)","DOI":"10.1109\/ICIS.2010.63"},{"key":"28_CR12","unstructured":"Sun, S.T.: Simple but not secure: an empirical security analysis of OAuth 2.0-based single sign-on systems. In: Proceedings of ACM Conference on Computer and Communications (2012)"},{"key":"28_CR13","unstructured":"IBM Tivoli Federated Identity Manager Data Sheet. [8] J. Carretero. Federated Identity Architecture of the European eID System. IEEE Access (2018)"},{"key":"28_CR14","doi-asserted-by":"crossref","unstructured":"Gro\u00df, T., Pfitzmann, B., Sadeghi, A.: Proving a WS-federation passive requestor profile with a browser model. In: Proceedings of SWS 2004 (Workshop on Secure Web Service), pp. 77\u201386","DOI":"10.1145\/1111348.1111357"},{"key":"28_CR15","unstructured":"Formal Methods Europe (FME) industry oriented website. https:\/\/fme-industry.github.io\/"},{"issue":"1","key":"28_CR16","first-page":"83","volume":"22","author":"J Wuang","year":"2013","unstructured":"Wuang, J., Hongxin, H.U., Bo, Z., Fei, Y., Huanguo, Z., Qianhong, W.U.: Formal analysis of information card federated identity-management protocol. Chinese J. Electron. 22(1), 83\u201388 (2013)","journal-title":"Chinese J. Electron."},{"key":"28_CR17","unstructured":"Avispa. http:\/\/www.avispa-project.org\/"},{"key":"28_CR18","unstructured":"Clavel, M., et al.: All About Maude - a High-performance Logical Framework: How to Specify, Program and Verify Systems in Rewriting Logic"},{"key":"28_CR19","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-6687-0","volume-title":"Designing Reliable Distributed Systems","author":"PC Olveczky","year":"2017","unstructured":"Olveczky, P.C.: Designing Reliable Distributed Systems. Springer, London (2017). https:\/\/doi.org\/10.1007\/978-1-4471-6687-0"},{"key":"28_CR20","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th Annual Symposium on Foundations of Computer Science (SFCS 1977), pp. 46\u201357. IEEE Computer Society, Washington, DC (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"28_CR21","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems","author":"Z Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/978-1-4612-0931-7"},{"key":"28_CR22","unstructured":"Meseguer, J., et al.: Maude Manual Version 2.7.1 (2016)"},{"key":"28_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-642-16310-4_11","volume-title":"Rewriting Logic and Its Applications","author":"M Sun","year":"2010","unstructured":"Sun, M., Meseguer, J., Sha, L.: A formal pattern architecture for safe medical systems. In: \u00d6lveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 157\u2013173. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16310-4_11"},{"key":"28_CR24","unstructured":"Lamport, L.: Specifying Systems (2002)"},{"key":"28_CR25","unstructured":"Lamport, L.: The Operators of TLA+. SRC Technical Note (1997)"},{"key":"28_CR26","unstructured":"Lamport, L.: Specifying Concurrent Systems with TLA+ (2000)"},{"key":"28_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/978-3-540-72952-5_6","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"A Riesco","year":"2007","unstructured":"Riesco, A., Verdejo, A.: Distributed applications implemented in Maude with parameterized skeletons. In: Bonsangue, M.M., Johnsen, E.B. (eds.) FMOODS 2007. LNCS, vol. 4468, pp. 91\u2013106. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-72952-5_6"},{"key":"28_CR28","unstructured":"LEPS. D4.2 - eIDAS Interconnection Supporting Service. Petros Kavassalis (2018). http:\/\/www.leps-project.eu\/node\/347"},{"key":"28_CR29","unstructured":"$$\\lambda $$-ForM Formal Methods Research Group. http:\/\/fsvg.math.ntua.gr\/"},{"key":"28_CR30","unstructured":"Lamport, L.: The TLA+ Home Page. https:\/\/lamport.azurewebsites.net\/tla\/tla.html"},{"key":"28_CR31","unstructured":"Applications of Maude. http:\/\/maude.cs.illinois.edu\/w\/index.php\/Applications"},{"key":"28_CR32","unstructured":"How to Evaluate the Suitability of a Formal Method for Industrial Deployment? A Survey Technical Report, SCCH-TR-1603 - 2016"},{"key":"28_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/978-3-319-12904-4_13","volume-title":"Rewriting Logic and Its Applications","author":"A Riesco","year":"2014","unstructured":"Riesco, A.: An integration of CafeOBJ into full Maude. In: Escobar, S. (ed.) WRLA 2014. LNCS, vol. 8663, pp. 230\u2013246. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-12904-4_13"},{"key":"28_CR34","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1016\/j.scico.2016.04.014","volume":"131","author":"D Hansen","year":"2016","unstructured":"Hansen, D., Leuschell, M.: Translating B to TLA+ for validation with TLC. Sci. Comput. Program. 131, 40\u201355 (2016)","journal-title":"Sci. Comput. Program."},{"key":"28_CR35","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1016\/j.entcs.2004.06.016","volume":"117","author":"IA Mason","year":"2005","unstructured":"Mason, I.A., Talcott, C.L.: IOP: the interoperability platform and IMaude: an interactive extension of Maude. Electron. Notes Theoret. Comput. Sci. 117, 315\u2013333 (2005)","journal-title":"Electron. Notes Theoret. Comput. Sci."},{"key":"28_CR36","doi-asserted-by":"crossref","unstructured":"Aoumer, N., Barkaoui, K., Saake, G.: Towards MAUDE-TLA based foundation for complex concurrent systems specification and certification. In: Proceedings of the 5th International Conference on Information Technology: New Generations, pp. 1305\u20131307 (2008)","DOI":"10.1109\/ITNG.2008.268"},{"key":"28_CR37","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1016\/S1571-0661(04)00037-4","volume":"4","author":"M Clavel","year":"1996","unstructured":"Clavel, M., Meseguer, J.: Reflection and strategies in rewriting logic. Electron. Notes Theoret. Comput. Sci. 4, 126\u2013148 (1996)","journal-title":"Electron. Notes Theoret. Comput. Sci."},{"key":"28_CR38","unstructured":"ProB animator for TLA+. https:\/\/www3.hhu.de\/stups\/prob\/index.php\/TLA"},{"issue":"4","key":"28_CR39","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1145\/2699417","volume":"58","author":"C Newcombe","year":"2015","unstructured":"Newcombe, C., Rath, T., Zhang, F., Munteanu, B., Brooker, M., Deardeuff, M.: How Amazon web services uses formal methods. Commun. ACM 58(4), 66\u201373 (2015)","journal-title":"Commun. ACM"},{"key":"28_CR40","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1016\/S1571-0661(05)80134-3","volume":"36","author":"PC Olveczky","year":"2000","unstructured":"Olveczky, P.C., Meseguer, J.: Real-Time Maude: a tool for simulating and analyzing real-time and hybrid systems. Electron. Notes Theoret. Comput. Sci. 36, 361\u2013382 (2000)","journal-title":"Electron. Notes Theoret. Comput. Sci."},{"key":"28_CR41","unstructured":"Parallel Statistical Model Checking and Quantitative Analysis Tool. http:\/\/maude.cs.uiuc.edu\/tools\/pvesta\/"},{"key":"28_CR42","unstructured":"MultiVeStA: Distributed Statistical Model Checking for Discrete Event Simulators. https:\/\/sysma.imtlucca.it\/tools\/toolmultivesta\/"},{"issue":"3","key":"28_CR43","doi-asserted-by":"publisher","first-page":"695","DOI":"10.1016\/j.camwa.2010.05.017","volume":"60","author":"H Zhang","year":"2010","unstructured":"Zhang, H., Merz, S., Gu, M.: Specifying and verifying PLC systems with TLA+: a case study. Comput. Math. Appl. 60(3), 695\u2013705 (2010)","journal-title":"Comput. Math. Appl."},{"key":"28_CR44","unstructured":"Barjaktarovic M.: The state-of-the-art in formal methods. Technical report\/Wilkes University and WetStone Technologies (1998). http:\/\/www.cs.utexas.edu\/users\/csed\/formal-methods\/docs\/StateFM.pdf. Accessed 20 May 2019"},{"issue":"4","key":"28_CR45","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1145\/242223.242257","volume":"28","author":"JEM Clarke","year":"1996","unstructured":"Clarke, J.E.M., et al.: Formal methods: state of the art and future directions. ACM Comput. Surv. 28(4), 626\u2013643 (1996)","journal-title":"ACM Comput. Surv."},{"key":"28_CR46","unstructured":"Leveraging eID in the Private Sector. LEPS EU-funded project website. http:\/\/www.leps-project.eu\/"},{"key":"28_CR47","doi-asserted-by":"crossref","unstructured":"Lamport, L.: The PlusCal Algorithm Language (2009)","DOI":"10.1007\/978-3-642-03466-4_2"},{"key":"28_CR48","unstructured":"Student and Citizen Identities Linked. SEAL EU-funded project website. https:\/\/project-seal.eu\/about"},{"key":"28_CR49","unstructured":"Increasing trust with eID for developing business. GRIDS EU-funded project website. https:\/\/www.grids-cef.eu\/"},{"key":"28_CR50","series-title":"IFIP Advances in Information and Communication Technology","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/978-3-030-42504-3_28","volume-title":"Privacy and Identity Management. Data for Better Living: AI and Privacy","author":"A Satybaldy","year":"2020","unstructured":"Satybaldy, A., Nowostawski, M., Ellingsen, J.: Self-sovereign identity systems. In: Friedewald, M., \u00d6nen, M., Lievens, E., Krenn, S., Fricker, S. (eds.) Privacy and Identity 2019. IAICT, vol. 576, pp. 447\u2013461. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-42504-3_28"},{"key":"28_CR51","doi-asserted-by":"crossref","unstructured":"Naik, N., Jenkins, P.: Governing principles of self-sovereign identity applied to blockchain enabled privacy preserving identity management systems. In: 2020 IEEE International Symposium on Systems Engineering (ISSE), pp. 1\u20136 (2020)","DOI":"10.1109\/ISSE49799.2020.9272212"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation. Practice"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-19762-8_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,19]],"date-time":"2022-10-19T23:16:04Z","timestamp":1666221364000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-19762-8_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031197611","9783031197628"],"references-count":51,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-19762-8_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"17 October 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ISoLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Leveraging Applications of Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rhodes","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 October 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 October 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"isola2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.isola-conference.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}