{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T15:46:32Z","timestamp":1784216792303,"version":"3.55.0"},"reference-count":129,"publisher":"Oxford University Press (OUP)","issue":"1","license":[{"start":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T00:00:00Z","timestamp":1770681600000},"content-version":"vor","delay-in-days":40,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Horizon Europe program","award":["101070351"],"award-info":[{"award-number":["101070351"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026,1,31]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>The revolutionary opportunities presented by eXtended Reality (XR) technologies will only materialize if modeling and analysis activities, undertaken during the engineering process of XR systems, are directed towards ensuring their social acceptance. By this, we mean integrating human and technical aspects during system development to ensure that the system guarantees communication security and data privacy, and is trusted by end users. One approach to achieve these guarantees is through rigorous, formal specification and verification during system modeling and analysis, explicitly considering the human factor. Accordingly, in this survey, we systematically investigate 6 mainstream formalisms for modeling and analyzing socio-technical security concerns, encompassing privacy and trust, in XR systems. We consider both desired concerns (e.g., requirements, properties) and undesired ones (e.g., threats, attacks). Our investigation incorporates 34 state-of-the-art approaches comprising languages, techniques, frameworks, and tools, leveraging these formalisms, which we compare against a diverse set of criteria: (1) expressivity, (2) modeling and analysis complexity, (3) modeling and analysis constructs, (4) power of inference, (5) user-friendliness, (6) applicability. Based on our findings, we identify the current gaps and considerable challenges and suggest an agenda for future research. To guide our investigation from a more practical perspective, we also present two real-world pilot studies that illustrate the potential application of formal methods in specific XR applications. This work thus aims to provide insights from a twofold perspective: for formal methods researchers seeking to learn more about socio-technical security in XR systems, and for security practitioners focused on socio-technical aspects in XR who are interested in formal approaches.<\/jats:p>","DOI":"10.1093\/cybsec\/tyag004","type":"journal-article","created":{"date-parts":[[2026,1,18]],"date-time":"2026-01-18T12:33:26Z","timestamp":1768739606000},"source":"Crossref","is-referenced-by-count":1,"title":["Formal methods for socio-technical security in eXtended Reality (XR): state-of-the-art and research agenda"],"prefix":"10.1093","volume":"12","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9380-6916","authenticated-orcid":false,"given":"Megha","family":"Quamara","sequence":"first","affiliation":[{"name":"King\u2019s College London Department of Informatics, , London, WC2B 4BG ,","place":["United Kingdom"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9916-271X","authenticated-orcid":false,"given":"Luca","family":"Vigan\u00f2","sequence":"additional","affiliation":[{"name":"King\u2019s College London Department of Informatics, , London, WC2B 4BG ,","place":["United Kingdom"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4308-1352","authenticated-orcid":false,"given":"Viktor","family":"Schmuck","sequence":"additional","affiliation":[{"name":"King\u2019s College London Department of Engineering, , London, WC2R 2LS ,","place":["United Kingdom"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7213-6359","authenticated-orcid":false,"given":"Oya","family":"Celiktutan","sequence":"additional","affiliation":[{"name":"King\u2019s College London Department of Engineering, , London, WC2R 2LS ,","place":["United Kingdom"]}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"286","published-online":{"date-parts":[[2026,2,10]]},"reference":[{"key":"2026021004191006200_bib1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3652595","article-title":"Extended Reality (XR) Toward Building Immersive Solutions: The Key to Unlocking Industry 4.0","volume":"56","author":"Alhakamy","year":"2024","journal-title":"ACM Comput Surv"},{"key":"2026021004191006200_bib2","doi-asserted-by":"publisher","first-page":"107289","DOI":"10.1016\/j.chb.2022.107289","article-title":"What is XR? Towards a framework for augmented and virtual reality","volume":"133","author":"Rauschnabel","year":"2022","journal-title":"Comput Hum Behav"},{"key":"2026021004191006200_bib3","doi-asserted-by":"crossref","first-page":"282","DOI":"10.1117\/12.197321","article-title":"Augmented reality: A class of displays on the reality-virtuality continuum","volume-title":"Telemanipulator and telepresence technologies","author":"Milgram","year":"1995"},{"key":"2026021004191006200_bib4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3472303","article-title":"A systematic literature review of virtual, augmented, and mixed reality game applications in healthcare","volume":"3","author":"Fu","year":"2022","journal-title":"ACM T. Comput. Healthcare (HEALTH)"},{"key":"2026021004191006200_bib5","doi-asserted-by":"publisher","first-page":"101863","DOI":"10.1016\/j.tele.2022.101863","article-title":"Extended reality applications in industry 4.0.-A systematic literature review","volume":"73","author":"Cardenas-Robledo","year":"2022","journal-title":"Telemat Inform"},{"key":"2026021004191006200_bib6","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1109\/EXPAT.2019.8876559","article-title":"Extended reality in iot scenarios: Concepts, applications and future trends","volume-title":"2019 5th Experiment International Conference (exp. at\u201919)","author":"Andrade","year":"2019"},{"key":"2026021004191006200_bib7","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1109\/MTS.2024.3370023","article-title":"The social implications of XR: Promises, perils, and potential","volume":"43","author":"Michael","year":"2024","journal-title":"IEEE Technol Soc Mag"},{"key":"2026021004191006200_bib8","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/978-3-030-62655-6_3","article-title":"User experience in collaborative extended reality: overview study","volume-title":"Virtual Reality and Augmented Reality: 17th EuroVR International Conference, EuroVR 2020, Valencia, Spain, November 25\u201327, 2020, Proceedings 17","author":"Nguyen","year":"2020"},{"key":"2026021004191006200_bib9","first-page":"1","article-title":"Satisfied or not: user experience of mobile augmented reality in using natural language processing techniques on review comments","volume":"26","author":"Jang","year":"2022","journal-title":"Virt Real"},{"key":"2026021004191006200_bib10","first-page":"360","article-title":"Super-immersive Remote Working via Virtual Reality Controlled Robotics","volume-title":"Proceedings of the Augmented Humans International Conference 2023","author":"Naik","year":"2023"},{"key":"2026021004191006200_bib11","doi-asserted-by":"publisher","first-page":"102923","DOI":"10.1016\/j.cose.2022.102923","article-title":"Rise of the metaverse\u2019s immersive virtual reality malware and the man-in-the-room attack and defenses","volume":"127","author":"Vondr\u00e1\u010dek","year":"2023","journal-title":"Comput Secur"},{"key":"2026021004191006200_bib12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3614426","article-title":"Secure and trustworthy artificial intelligence-extended reality (AI-XR) for metaverses","volume":"56","author":"Qayyum","year":"2024","journal-title":"ACM Comput Surv"},{"key":"2026021004191006200_bib13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3696015","article-title":"From Embodied Abuse to Mass Disruption: Generative, Inter-Reality Threats in Social, Mixed-Reality Platforms","volume":"5","author":"Baldry","year":"2024","journal-title":"Digital Threats: Research and Practice"},{"key":"2026021004191006200_bib14","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1109\/VRW52623.2021.00085","article-title":"Privacy-certification standards for extended-reality devices and services","volume-title":"2021 IEEE Conference on Virtual Reality and 3D User Interfaces Abstracts and Workshops (VRW)","author":"Happa","year":"2021"},{"key":"2026021004191006200_bib15","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/s44163-024-00190-9","article-title":"Biometrics in extended reality: a review","volume":"4","author":"Agarwal","year":"2024","journal-title":"Disc Artif Intell"},{"key":"2026021004191006200_bib16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3659945","article-title":"Deceived by immersion: A systematic analysis of deceptive design in extended reality","volume":"56","author":"Hadan","year":"2024","journal-title":"ACM Comput Surv"},{"key":"2026021004191006200_bib17","doi-asserted-by":"publisher","first-page":"563","DOI":"10.3233\/JCS-150536","article-title":"Service security and privacy as a socio-technical problem","volume":"23","author":"Bella","year":"2015","journal-title":"J Comput Secur"},{"key":"2026021004191006200_bib18","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1109\/DSN-S50200.2020.00041","article-title":"A framework for risk assessment in augmented reality-equipped socio-technical systems","volume-title":"2020 50th Annual IEEE-IFIP International Conference on Dependable Systems and Networks-Supplemental Volume (DSN-S)","author":"Bahaei","year":"2020"},{"key":"2026021004191006200_bib19","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1016\/j.compeleceng.2015.02.019","article-title":"Security analysis of socio-technical physical systems","volume":"47","author":"Lenzini","year":"2015","journal-title":"Comput Elect Eng"},{"key":"2026021004191006200_bib20","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1007\/978-3-319-07881-6_20","article-title":"Dealing with security requirements for socio-technical systems: A holistic approach","volume-title":"Advanced Information Systems Engineering: 26th International Conference, CAiSE 2014, Thessaloniki, Greece, June 16-20, 2014. Proceedings 26","author":"Li","year":"2014"},{"key":"2026021004191006200_bib21","doi-asserted-by":"crossref","first-page":"502","DOI":"10.1109\/CIC.2016.077","article-title":"Privacy by socio-technical design: A collaborative approach for privacy friendly system design","volume-title":"2016 IEEE 2nd International Conference on Collaboration and Internet Computing (CIC)","author":"Degeling","year":"2016"},{"key":"2026021004191006200_bib22","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1007\/978-3-319-70241-4_16","article-title":"Toward GDPR-compliant socio-technical systems: Modeling language and reasoning framework","volume-title":"The Practice of Enterprise Modeling: 10th IFIP WG 8.1. Working Conference, PoEM 2017, Leuven, Belgium, November 22-24, 2017, Proceedings 10","author":"Robol","year":"2017"},{"key":"2026021004191006200_bib23","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1592434.1592436","article-title":"Formal methods: Practice and experience","volume":"41","author":"Woodcock","year":"2009","journal-title":"ACM Comput Surv (CSUR)"},{"key":"2026021004191006200_bib24","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3522582","article-title":"A survey of practical formal methods for security","volume":"34","author":"Kulik","year":"2022","journal-title":"Form Asp Comput"},{"key":"2026021004191006200_bib25","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/978-3-031-08143-9_1","article-title":"Formal Methods for Socio-technical Security (Formal and Automated Analysis of Security Ceremonies)","volume-title":"Coordination Models and Languages: 24th IFIP WG 6.1 International Conference, COORDINATION 2022, Held as Part of the 17th International Federated Conference on Distributed Computing Techniques, DisCoTec 2022, Lucca, Italy, June 13-17, 2022, Proceedings","author":"Vigan\u00f2","year":"2022"},{"key":"2026021004191006200_bib26","article-title":"Uppaal","year":"2023"},{"key":"2026021004191006200_bib27","article-title":"Alloy","year":"2023"},{"key":"2026021004191006200_bib28","article-title":"Rodin","year":"2023"},{"key":"2026021004191006200_bib29","article-title":"Tamarin","year":"2023"},{"key":"2026021004191006200_bib30","article-title":"ProVerif","year":"2023"},{"key":"2026021004191006200_bib31","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1145\/2580723.2580730","article-title":"Security and privacy for augmented reality systems","volume":"57","author":"Roesner","year":"2014","journal-title":"Commun ACM"},{"key":"2026021004191006200_bib32","doi-asserted-by":"publisher","first-page":"103127","DOI":"10.1016\/j.cose.2023.103127","article-title":"A systematic threat analysis and defense strategies for the metaverse and extended reality systems","volume":"128","author":"Qamar","year":"2023","journal-title":"Comput Secur"},{"key":"2026021004191006200_bib33","article-title":"Formal methods in human-computer interaction","author":"Harrison","year":"1990"},{"key":"2026021004191006200_bib34","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s11948-014-9621-1","article-title":"The convergence of virtual reality and social networks: threats to privacy and autonomy","volume":"22","author":"O\u2019Brolch\u00e1in","year":"2016","journal-title":"Sci Eng Ethics"},{"key":"2026021004191006200_bib35","article-title":"Security and Privacy in Virtual Reality\u2013A Literature Survey","author":"Giaretta","year":"2022"},{"key":"2026021004191006200_bib36","doi-asserted-by":"crossref","first-page":"102951","DOI":"10.1016\/j.cose.2022.102951","article-title":"Virtually secure: A taxonomic assessment of cybersecurity challenges in virtual reality environments","volume":"124","author":"Odeleye","year":"2022","journal-title":"Comput Secur"},{"key":"2026021004191006200_bib37","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1109\/AINS50155.2020.9315127","article-title":"A survey on privacy issues of augmented reality applications","volume-title":"2020 IEEE Conference on Application, Information and Network Security (AINS)","author":"King","year":"2020"},{"key":"2026021004191006200_bib38","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3359626","article-title":"Security and privacy approaches in mixed reality: A literature survey","volume":"52","author":"De\u00a0Guzman","year":"2019","journal-title":"ACM Comput Surv (CSUR)"},{"key":"2026021004191006200_bib39","doi-asserted-by":"publisher","first-page":"103989","DOI":"10.1016\/j.jnca.2024.103989","article-title":"Privacy preservation in Artificial Intelligence and Extended Reality (AI-XR) metaverses: A survey","volume":"231","author":"Alkaeed","year":"2024","journal-title":"J Netw Comput Appl"},{"key":"2026021004191006200_bib40","doi-asserted-by":"publisher","first-page":"1229","DOI":"10.1080\/10447318.2019.1619259","article-title":"Seven HCI grand challenges","volume":"35","author":"Stephanidis","year":"2019","journal-title":"Int J Hum\u2013Comput Int"},{"key":"2026021004191006200_bib41","doi-asserted-by":"publisher","first-page":"1251","DOI":"10.1080\/10447318.2022.2138826","article-title":"A systematic literature review of user trust in AI-enabled systems: An HCI perspective","volume":"40","author":"Bach","year":"2024","journal-title":"Int J Hum\u2013Comput Int"},{"key":"2026021004191006200_bib42","doi-asserted-by":"crossref","first-page":"1151","DOI":"10.1145\/3543873.3587584","article-title":"Federated learning for metaverse: A survey","volume-title":"Companion Proceedings of the ACM Web Conference 2023","author":"Chen","year":"2023"},{"key":"2026021004191006200_bib43","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1109\/TBDATA.2024.3362191","article-title":"Decentralized Federated Learning: A Survey on Security and Privacy","volume":"10","author":"Hallaji","year":"2024","journal-title":"IEEE T Big Data"},{"key":"2026021004191006200_bib44","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1177\/0018720811417254","article-title":"A meta-analysis of factors affecting trust in human-robot interaction","volume":"53","author":"Hancock","year":"2011","journal-title":"Hum Fact"},{"key":"2026021004191006200_bib45","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1177\/2050157919843961","article-title":"The privacy implications of social robots: Scoping review and expert interviews","volume":"7","author":"Lutz","year":"2019","journal-title":"Mobile Media Commun"},{"key":"2026021004191006200_bib46","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/s43154-020-00029-y","article-title":"Trust in robots: Challenges and opportunities","volume":"1","author":"Kok","year":"2020","journal-title":"Curr Robot Rep"},{"key":"2026021004191006200_bib47","doi-asserted-by":"publisher","first-page":"1179","DOI":"10.1007\/s12369-020-00659-4","article-title":"A systematic review of attitudes, anxiety, acceptance, and trust towards social robots","volume":"12","author":"Naneva","year":"2020","journal-title":"Int J Soc Robot"},{"key":"2026021004191006200_bib48","doi-asserted-by":"publisher","first-page":"181","DOI":"10.3390\/computers11120181","article-title":"A Systematic Review on Social Robots in Public Spaces: Threat Landscape and Attack Surface","volume":"11","author":"Oruma","year":"2022","journal-title":"Computers"},{"key":"2026021004191006200_bib49","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1007\/s10207-021-00545-8","article-title":"Robotics cyber security: Vulnerabilities, attacks, countermeasures, and recommendations","volume":"21","author":"Yaacoub","year":"2022","journal-title":"Int J Inf Secur"},{"key":"2026021004191006200_bib50","first-page":"1","article-title":"Procedures for performing systematic reviews","volume":"33","author":"Kitchenham","year":"2004","journal-title":"Keele UK Keele University"},{"key":"2026021004191006200_bib51","first-page":"230","article-title":"Google Scholar\u2019s ranking algorithm: an introductory overview","volume-title":"Proceedings of the 12th international conference on scientometrics and informetrics (ISSI\u201909)","author":"Beel","year":"2009"},{"key":"2026021004191006200_bib52","article-title":"Formal methods for security","author":"Chong","year":"2016"},{"key":"2026021004191006200_bib53","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1007\/978-3-642-41010-9_5","article-title":"Study on the barriers to the industrial adoption of formal methods","volume-title":"Formal Methods for Industrial Critical Systems: 18th International Workshop, FMICS 2013, Madrid, Spain, September 23-24, 2013. Proceedings 18","author":"Davis","year":"2013"},{"key":"2026021004191006200_bib54","doi-asserted-by":"crossref","first-page":"676","DOI":"10.1109\/INDIN.2016.7819246","article-title":"A study on user-friendly formal specification languages for requirements formalization","volume-title":"2016 IEEE 14th International Conference on Industrial Informatics (INDIN)","author":"Pang","year":"2016"},{"key":"2026021004191006200_bib55","first-page":"21","article-title":"Attack trees","volume":"24","author":"Schneier","year":"1999","journal-title":"Dr Dobb\u2019s J"},{"key":"2026021004191006200_bib56","doi-asserted-by":"publisher","first-page":"4127","DOI":"10.1109\/TDSC.2021.3121216","article-title":"Modeling and defense of social virtual reality attacks inducing cybersickness","volume":"19","author":"Valluripally","year":"2021","journal-title":"IEEE T Depend Secure Comput"},{"key":"2026021004191006200_bib57","doi-asserted-by":"crossref","first-page":"2559","DOI":"10.1109\/TSC.2022.3216539","article-title":"Detection of security and privacy attacks disrupting user immersive experience in virtual reality learning environments","volume":"16","author":"Valluripally","year":"2022","journal-title":"IEEE T Serv Comput"},{"key":"2026021004191006200_bib58","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1007\/978-3-319-29968-6_4","article-title":"How to generate security cameras: Towards defence generation for socio-technical systems","volume-title":"Graphical Models for Security: Second International Workshop, GraMSec 2015, Verona, Italy, July 13, 2015, Revised Selected Papers 2","author":"Gadyatskaya","year":"2016"},{"key":"2026021004191006200_bib59","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1007\/978-3-319-27810-0_3","article-title":"Formal modelling and analysis of socio-technical systems","volume":"9560","author":"Probst","year":"2016","journal-title":"Semantics, Logics, and Calculi: Essays Dedicated to Hanne Riis Nielson and Flemming Nielson on the Occasion of Their 60th Birthdays"},{"key":"2026021004191006200_bib60","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1109\/JSYST.2012.2221933","article-title":"Security policy alignment: A formal approach","volume":"7","author":"Pieters","year":"2012","journal-title":"IEEE Syst J"},{"key":"2026021004191006200_bib61","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1007\/978-3-319-24018-3_16","article-title":"Attack tree generation by policy invalidation","volume-title":"Information Security Theory and Practice: 9th IFIP WG 11.2 International Conference, WISTP 2015, Heraklion, Crete, Greece, August 24-25, 2015. Proceedings 9","author":"Ivanova","year":"2015"},{"key":"2026021004191006200_bib62","doi-asserted-by":"crossref","DOI":"10.3990\/1.9789036546256","article-title":"Truth or dare: quantitative security risk analysis via attack trees","author":"Kumar","year":"2018"},{"key":"2026021004191006200_bib63","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1007\/978-3-319-24249-1_25","article-title":"Sequential and parallel attack tree modelling","volume-title":"Computer Safety, Reliability, and Security: SAFECOMP 2015 Workshops, ASSURE, DECSoS. ISSE, ReSA4CI, and SASSUR, Delft, The Netherlands, September 22, 2015, Proceedings 34","author":"Arnold","year":"2015"},{"key":"2026021004191006200_bib64","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1109\/STAST.2015.11","article-title":"Regression Nodes: Extending attack trees with data from social sciences","volume-title":"2015 Workshop on Socio-Technical Aspects in Security and Trust","author":"Bull\u00e9e","year":"2015"},{"key":"2026021004191006200_bib65","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","article-title":"A theory of timed automata","volume":"126","author":"Alur","year":"1994","journal-title":"Theor Comput Sci"},{"key":"2026021004191006200_bib66","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1145\/2808783.2808787","article-title":"Modelling social-technical attacks with timed automata","volume-title":"Proceedings of the 7th ACM CCS international workshop on managing insider security threats","author":"David","year":"2015"},{"key":"2026021004191006200_bib67","first-page":"1","article-title":"Attack trees for security and privacy in social virtual reality learning environments","volume-title":"2020 IEEE 17th Annual Consumer Communications and Networking Conference (CCNC)","author":"Valluripally","year":"2020"},{"key":"2026021004191006200_bib68","first-page":"402","article-title":"Probabilistic Analysis of Security Protocols Using Probabilistic Timed Automata","author":"Siedlecka-Lamch","year":"2022","journal-title":"ETHICOMP 2022"},{"key":"2026021004191006200_bib69","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1109\/ETFA.2019.8869381","article-title":"AI, connectivity and cyber-security in avionics","volume-title":"2019 24th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA)","author":"Gatti","year":"2019"},{"key":"2026021004191006200_bib70","article-title":"Bayesian theory","author":"Bernardo","year":"2009"},{"key":"2026021004191006200_bib71","first-page":"6226","article-title":"Trust Dynamics and Transfer across Human-Robot Interaction Tasks: Bayesian and Neural Computational Models","volume-title":"IJCAI","author":"Soh","year":"2019"},{"key":"2026021004191006200_bib72","doi-asserted-by":"publisher","first-page":"101908","DOI":"10.1016\/j.cose.2020.101908","article-title":"Insider threat risk prediction based on Bayesian network","volume":"96","author":"Elmrabit","year":"2020","journal-title":"Comput Secur"},{"key":"2026021004191006200_bib73","first-page":"1","article-title":"Detecting human vulnerably in socio-technical systems: a naval case study","volume-title":"Proceedings of the 23rd ACM\/IEEE International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings","author":"Perrotin","year":"2020"},{"key":"2026021004191006200_bib74","first-page":"144","article-title":"Modelling Responsible Digital Security Behaviour for Countering Social Media Manipulation","volume-title":"ECSM 2023 10th European Conference on Social Media","author":"Maathuis","year":"2023"},{"key":"2026021004191006200_bib75","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2166956.2166962","article-title":"Epistemic temporal logic for information flow security","volume-title":"Proceedings of the ACM SIGPLAN 6th Workshop on Programming Languages and Analysis for Security","author":"Balliu","year":"2011"},{"key":"2026021004191006200_bib76","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1109\/CSFW.1989.40587","article-title":"A logic of knowledge and belief for reasoning about computer security","volume-title":"Proceedings of the Computer Security Foundations Workshop II","author":"Moser","year":"1989"},{"key":"2026021004191006200_bib77","doi-asserted-by":"publisher","first-page":"275","DOI":"10.3389\/fpsyg.2014.00275","article-title":"A perceptual account of symbolic reasoning","volume":"5","author":"Landy","year":"2014","journal-title":"Front Psychol"},{"key":"2026021004191006200_bib78","doi-asserted-by":"publisher","first-page":"509","DOI":"10.3233\/JCS-16891","article-title":"Invalid certificates in modern browsers: A socio-technical analysis","volume":"26","author":"Giustolisi","year":"2018","journal-title":"J Comput Secur"},{"key":"2026021004191006200_bib79","doi-asserted-by":"publisher","first-page":"102259","DOI":"10.1016\/j.sysarc.2021.102259","article-title":"A security policy hardening framework for Socio-Cyber-Physical Systems","volume":"119","author":"Ouchani","year":"2021","journal-title":"J Syst Archit"},{"key":"2026021004191006200_bib80","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1007\/978-3-319-17016-9_18","article-title":"Probabilistic modelling of humans in security ceremonies","volume-title":"Data Privacy Management, Autonomous Spontaneous Security, and Security Assurance: 9th International Workshop, DPM 2014, 7th International Workshop, SETOP 2014, and 3rd International Workshop, QASA 2014, Wroclaw, Poland, September 10-11, 2014. Revised Selected Papers 9","author":"Johansen","year":"2015"},{"key":"2026021004191006200_bib81","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1007\/978-3-642-30436-1_23","article-title":"Layered analysis of security ceremonies","volume-title":"Information Security and Privacy Research: 27th IFIP TC 11 Information Security and Privacy Conference, SEC 2012, Heraklion, Crete, Greece, June 4-6, 2012. Proceedings 27","author":"Bella","year":"2012"},{"key":"2026021004191006200_bib82","doi-asserted-by":"publisher","first-page":"411","DOI":"10.3233\/JCS-210059","article-title":"Modelling human threats in security ceremonies","volume":"30","author":"Bella","year":"2022","journal-title":"J Comput Secur"},{"key":"2026021004191006200_bib83","first-page":"927","article-title":"Formal methods for modeling socio-technical innovation between adversaries","volume-title":"2011 Eighth International Conference on Information Technology: New Generations","author":"Thomas","year":"2011"},{"key":"2026021004191006200_bib84","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1109\/CSF.2016.30","article-title":"Modeling human errors in security protocols","volume-title":"2016 IEEE 29th Computer Security Foundations Symposium (CSF)","author":"Basin","year":"2016"},{"key":"2026021004191006200_bib85","doi-asserted-by":"publisher","first-page":"100239","DOI":"10.1016\/j.osnem.2022.100239","article-title":"The HEIC application framework for implementing XAI-based socio-technical systems","volume":"32","author":"Paredes","year":"2022","journal-title":"Online Social Networks and Media"},{"key":"2026021004191006200_bib86","article-title":"Systems engineering with SysML\/UML: modeling, analysis, design","author":"Weilkiens","year":"2011"},{"key":"2026021004191006200_bib87","doi-asserted-by":"crossref","first-page":"1553","DOI":"10.1109\/TrustCom.2013.190","article-title":"Studies in socio-technical security analysis: authentication of identities with TLS certificates","volume-title":"2013 12th IEEE International Conference on Trust, Security and Privacy in Computing and Communications","author":"Ferreira","year":"2013"},{"key":"2026021004191006200_bib88","doi-asserted-by":"crossref","first-page":"306","DOI":"10.1007\/978-3-319-07620-1_27","article-title":"Socio-technical security analysis of wireless hotspots","volume-title":"Human Aspects of Information Security, Privacy, and Trust: Second International Conference, HAS 2014, Held as Part of HCI International 2014, Heraklion, Crete, Greece, June 22-27, 2014. Proceedings 2","author":"Ferreira","year":"2014"},{"key":"2026021004191006200_bib89","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/s12652-015-0269-8","article-title":"Generating attacks in SysML activity diagrams by detecting attack surfaces","volume":"6","author":"Ouchani","year":"2015","journal-title":"J Amb Intel Hum Comput"},{"key":"2026021004191006200_bib90","first-page":"1","article-title":"Addressing Early Life Cycle Privacy Risk","volume-title":"2017 International Workshop on Privacy Engineering-IWPE","author":"Shapiro","year":"2017"},{"key":"2026021004191006200_bib91","first-page":"e148944","article-title":"FedAssess: Analysis for Efficient Communication and Security Algorithms over Various Federated Learning Frameworks and Mitigation of Label Flipping Attack","author":"Anusuya","year":"2014","journal-title":"Bull Pol Acad Sci Tech Sci"},{"key":"2026021004191006200_bib92","doi-asserted-by":"publisher","first-page":"103740","DOI":"10.1016\/j.cose.2024.103740","article-title":"Shadow Backdoor Attack: Multi-intensity Backdoor Attack Against Federated Learning","volume":"139","author":"Ren","year":"2024","journal-title":"Comput Secur"},{"key":"2026021004191006200_bib93","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1016\/S0927-0507(05)80172-0","article-title":"Markov decision processes","volume":"2","author":"Puterman","year":"1990","journal-title":"Handbooks Oper Res Manage Sci"},{"key":"2026021004191006200_bib94","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1016\/j.comcom.2022.07.038","article-title":"Towards enhanced threat modelling and analysis using a Markov Decision Process","volume":"194","author":"Malik","year":"2022","journal-title":"Comput Commun"},{"key":"2026021004191006200_bib95","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1109\/SP.2012.21","article-title":"Formalizing and enforcing purpose restrictions in privacy policies","volume-title":"2012 IEEE Symposium on Security and Privacy","author":"Tschantz","year":"2012"},{"key":"2026021004191006200_bib96","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1109\/MoWNet.2017.8045953","article-title":"A Markov game privacy preserving model in retail applications","volume-title":"2017 International Conference on Selected Topics in Mobile and Wireless Networking (MoWNeT)","author":"Sfar","year":"2017"},{"key":"2026021004191006200_bib97","doi-asserted-by":"publisher","first-page":"109949","DOI":"10.1109\/ACCESS.2022.3213711","article-title":"Markov Decision Process for Modeling Social Engineering Attacks and Finding Optimal Attack Strategies","volume":"10","author":"Abri","year":"2022","journal-title":"IEEE Access"},{"key":"2026021004191006200_bib98","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/s10009-014-0361-y","article-title":"Uppaal SMC tutorial","volume":"17","author":"David","year":"2015","journal-title":"Int J Softw Tools Tech Trans"},{"key":"2026021004191006200_bib99","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3342355","article-title":"Formal specification and verification of autonomous robotic systems: A survey","volume":"52","author":"Luckcuck","year":"2019","journal-title":"ACM Comput Surv (CSUR)"},{"key":"2026021004191006200_bib100","doi-asserted-by":"crossref","first-page":"479","DOI":"10.1109\/ISMAR52148.2021.00065","article-title":"Arena: The augmented reality edge networking architecture","volume-title":"2021 IEEE International Symposium on Mixed and Augmented Reality (ISMAR)","author":"Pereira","year":"2021"},{"key":"2026021004191006200_bib101","doi-asserted-by":"crossref","first-page":"369","DOI":"10.32604\/iasc.2023.036052","article-title":"Spatial Multi-Presence System to Increase Security Awareness for Remote Collaboration in an Extended Reality Environment","volume":"37","author":"Lee","year":"2023","journal-title":"Int Autom Soft Comput"},{"key":"2026021004191006200_bib102","doi-asserted-by":"publisher","first-page":"293","DOI":"10.3233\/JCS-210075","article-title":"A mutation-based approach for the formal and automated analysis of security ceremonies","volume":"31","author":"Sempreboni","year":"2023","journal-title":"J Comput Secur"},{"key":"2026021004191006200_bib103","doi-asserted-by":"crossref","first-page":"242","DOI":"10.1007\/978-3-030-05297-3_17","article-title":"Theorizing about socio-technical approaches to HCI","volume-title":"Human Work Interaction Design. Designing Engaging Automation: 5th IFIP WG 13.6 Working Conference, HWID 2018, Espoo, Finland, August 20-21, 2018, Revised Selected Papers 5","author":"Abdelnour-Nocera","year":"2019"},{"key":"2026021004191006200_bib104","doi-asserted-by":"crossref","first-page":"34","DOI":"10.1109\/HST.2011.5954992","article-title":"Security checkers: Detecting processor malicious inclusions at runtime","volume-title":"2011 IEEE International Symposium on Hardware-Oriented Security and Trust","author":"Bilzor","year":"2011"},{"key":"2026021004191006200_bib105","doi-asserted-by":"publisher","first-page":"13089","DOI":"10.1109\/ACCESS.2022.3146390","article-title":"An Integrated Formal Method Combining Labeled Transition System and Event-B for System Model Refinement","volume":"10","author":"Rao","year":"2022","journal-title":"IEEE Access"},{"key":"2026021004191006200_bib106","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1109\/SOSE55472.2022.9812648","article-title":"Using the architecture of Socio-Technical System to analyse its vulnerability","volume-title":"2022 17th Annual System of Systems Engineering Conference (SOSE)","author":"Perrotin","year":"2022"},{"key":"2026021004191006200_bib107","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1093\/comjnl\/bxq042","article-title":"Run-time security traceability for evolving systems","volume":"54","author":"Bauer","year":"2011","journal-title":"Comput J"},{"key":"2026021004191006200_bib108","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1109\/EDOC49727.2020.00026","article-title":"Continuous security testing: A case study on integrating dynamic security testing tools in ci\/cd pipelines","volume-title":"2020 IEEE 24th International Enterprise Distributed Object Computing Conference (EDOC)","author":"Rangnau","year":"2020"},{"key":"2026021004191006200_bib109","doi-asserted-by":"crossref","first-page":"1","DOI":"10.13031\/jash.15756","article-title":"Safety Risk Assessment of an Autonomous Agricultural Machine","volume":"30","author":"Aby","year":"2024","journal-title":"J Agric Saf Health"},{"key":"2026021004191006200_bib110","doi-asserted-by":"publisher","first-page":"7","DOI":"10.3390\/info8010007","article-title":"Model based safety analysis with smartIflow","volume":"8","author":"H\u00f6nig","year":"2017","journal-title":"Information"},{"key":"2026021004191006200_bib111","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1145\/3276954.3276958","article-title":"Protecting chatbots from toxic content","volume-title":"Proceedings of the 2018 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software","author":"Baudart","year":"2018"},{"key":"2026021004191006200_bib112","first-page":"99","article-title":"{HeapHopper}: Bringing bounded model checking to heap implementation security","volume-title":"27th USENIX Security Symposium (USENIX Security 18)","author":"Eckert","year":"2018"},{"key":"2026021004191006200_bib113","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/978-3-031-48495-7_6","article-title":"AR Patterns: Event-Driven Design Patterns in Creating Augmented Reality Experiences","volume-title":"International Conference on Virtual Reality and Mixed Reality","author":"Ackermann","year":"2023"},{"key":"2026021004191006200_bib114","first-page":"1324","article-title":"Design patterns for situated visualization in augmented reality","volume":"30","author":"Lee","year":"2023","journal-title":"IEEE T Vis Comput Graph"},{"key":"2026021004191006200_bib115","first-page":"30","article-title":"Patterns of Information Security Postures for Socio-Technical Systems and Systems-of-Systems","author":"Storer","year":"2012","journal-title":"Cyberpatterns 2012"},{"key":"2026021004191006200_bib116","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1145\/1040291.1040292","article-title":"Flow analysis for verifying properties of concurrent software systems","volume":"13","author":"Dwyer","year":"2004","journal-title":"ACM T Softw Eng Methodol (TOSEM)"},{"key":"2026021004191006200_bib117","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1145\/2775054.2694372","article-title":"A hardware design language for timing-sensitive information-flow security","volume":"50","author":"Zhang","year":"2015","journal-title":"Acm Sigplan Notices"},{"key":"2026021004191006200_bib118","article-title":"Isabelle: A generic theorem prover","author":"Paulson","year":"1994"},{"key":"2026021004191006200_bib119","doi-asserted-by":"crossref","DOI":"10.6028\/NIST.IR.8539.ipd","article-title":"Security Property Verification by Transition Model","author":"Hu","year":"2024"},{"key":"2026021004191006200_bib120","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","article-title":"The model checker SPIN","volume":"23","author":"Holzmann","year":"1997","journal-title":"IEEE T Softw Eng"},{"key":"2026021004191006200_bib121","doi-asserted-by":"crossref","first-page":"495","DOI":"10.1007\/3-540-48683-6_44","article-title":"NuSMV: A new symbolic model verifier","volume-title":"Computer Aided Verification: 11th International Conference, CAV\u201999 Trento, Italy, July 6\u201310, 1999 Proceedings 11","author":"Cimatti","year":"1999"},{"key":"2026021004191006200_bib122","doi-asserted-by":"crossref","first-page":"180","DOI":"10.1007\/3-540-46425-5_12","article-title":"Secure information flow as typed process behaviour","volume-title":"Programming Languages and Systems: 9th European Symposium on Programming, ESOP 2000 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000 Berlin, Germany, March 25\u2013April 2, 2000 Proceedings 9","author":"Honda","year":"2000"},{"key":"2026021004191006200_bib123","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/11787006_1","article-title":"Differential privacy","volume-title":"International colloquium on automata, languages, and programming","author":"Dwork","year":"2006"},{"key":"2026021004191006200_bib124","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1109\/EuroSP48549.2020.00014","article-title":"X-men: A mutation-based approach for the formal analysis of security ceremonies","volume-title":"2020 IEEE European Symposium on Security and Privacy (EuroS&P)","author":"Sempreboni","year":"2020"},{"key":"2026021004191006200_bib125","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/s00200-005-0170-3","article-title":"Process-algebraic approaches for multi-agent systems: an overview","volume":"16","author":"Viroli","year":"2005","journal-title":"Appl Algebra Eng Commun Comput"},{"key":"2026021004191006200_bib126","doi-asserted-by":"publisher","first-page":"671","DOI":"10.1016\/B978-0-444-53726-3.00013-X","article-title":"Dynamic epistemic logic","volume":"337","author":"Kooi","year":"2011","journal-title":"Handbook of logic and language"},{"key":"2026021004191006200_bib127","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1007\/BF01211247","article-title":"Real space process algebra","volume":"5","author":"Baeten","year":"1993","journal-title":"Formal Aspects of Computing"},{"key":"2026021004191006200_bib128","doi-asserted-by":"publisher","first-page":"100758","DOI":"10.1016\/j.cosrev.2025.100758","article-title":"The Beauty and the Beast: A survey on process algebras and cybersecurity","volume":"57","author":"Costa","year":"2025","journal-title":"Comput Sci Rev"},{"key":"2026021004191006200_bib129","doi-asserted-by":"publisher","first-page":"9313239","DOI":"10.1155\/ahci\/9313239","article-title":"A Systematic Literature Review: Cognitive Workload Assessment in Human Factors Research","volume":"2025","author":"Tierney","year":"2025","journal-title":"Adv Hum-Comput Int"}],"container-title":["Journal of Cybersecurity"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/academic.oup.com\/cybersecurity\/article-pdf\/12\/1\/tyag004\/66838300\/tyag004.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/academic.oup.com\/cybersecurity\/article-pdf\/12\/1\/tyag004\/66838300\/tyag004.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T09:19:28Z","timestamp":1770715168000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/cybersecurity\/article\/doi\/10.1093\/cybsec\/tyag004\/8470988"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"references-count":129,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2026,1,31]]}},"URL":"https:\/\/doi.org\/10.1093\/cybsec\/tyag004","relation":{},"ISSN":["2057-2085","2057-2093"],"issn-type":[{"value":"2057-2085","type":"print"},{"value":"2057-2093","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2026]]},"published":{"date-parts":[[2026]]},"article-number":"tyag004"}}