Publications

Please feel free to ask me for papers which are not linked from this page (e.g. drafts)

2023

  1. Vincent Cheval, José Moreira, and Mark D. Ryan. Automatic verification of transparency protocols. In 8th IEEE European Symposium on Security and Privacy (EuroS&P'23), 2023.
  2. Daniel Fentham, David Parker, and Mark D. Ryan. Using Reed-Muller codes for classification with rejection and recovery. In International Symposium on Foundations and Practice of Security, 2023.

2022

  1. José Moreira, Mark D. Ryan, and Flavio D. Garcia. Protocols for a Two-Tiered Trusted Computing Base. In 27th European Symposium on Research in Computer Security (ESORICS), 2022.
  2. Thalia Laing, Eduard Marin, Mark D. Ryan, Joshua Schiffman, and Gaëtan Wattiau. Symbolon: Enabling Flexible Multi-device-based User Authentication. In IEEE Conference on Dependable and Secure Computing (IEEE DSC), 2022.
  3. Rujia Li, Qin Wang, Qi Wang, David Galindo, and Mark Ryan. SoK: TEE-assisted Confidential Smart Contract. In Privacy Enhancing Technology Symposium (PETS), 2022.

2021

  1. Georgios Fotiadis, José Moreira, Thanassis Giannetsos, Liqun Chen, Peter B Rønne, Mark D Ryan, and Peter YA Ryan. Root-of-Trust Abstractions for Symbolic Analysis: Application to Attestation Protocols. In International Workshop on Security and Trust Management, pages 163-184. Springer, 2021.
  2. Robert H. Deng, Feng Bao, Guilin Wang, Jian Shen, Mark Ryan, Weizhi Meng, and Ding Wang. Proceedings of Information Security Practice and Experience. In 16th International Conference on Information Security Practice and Experience (ISPEC 2021), Nanjing, China, December 2021. Lecture Notes in Computer Science 13107, Springer 2021.

2020

  1. Rajiv Ranjan Singh, José Moreira, Tom Chothia, and Mark D Ryan. Modelling of 802.11 4-way handshake attacks and analysis of security properties. In International Workshop on Security and Trust, 2020.
  2. Michael Oxford, David Parker, and Mark Ryan. Quantitative verification of certificate transparency gossip protocols. In IEEE Conference on Communications and Network Security (CNS), Pages 1-9, 2020.

2019

  1. Mihai Ordean, Mark Ryan, and David Galindo. CAOS: Concurrent-Access Obfuscated Store. In Proceedings of the 24th ACM Symposium on Access Control Models and Technologies, pages 13-24, 2019.

2018

  1. Michael Denzel, and Mark D. Ryan. Malware tolerant (mesh-) networks. In International Conference on Cryptology and Network Security, Pages 133-153, Springer, 2018.
  2. Jiangshan Yu, Mark Ryan, Cas Cremers. DECIM: Detecting endpoint compromise in messaging. In IEEE Transactions on Information Forensics and Security, 13, 1, pp. 106-118. 2017.

2017

  1. Jiangshan Yu, and Mark Ryan. Evaluating web PKIs. In Software Architecture for Big Data and the Cloud, 105-126, 2017.
  2. Matteo Maffei, and Mark Ryan. Proceedings of Principles of Security and Trust. In 6th International Conference on Principles of Security and Trust (POST 2017), European Joint Conferences on Theory and Practice of Software (ETAPS 2017) Uppsala, Sweden, April 2017, Lecture Notes in Computer Science 10204, Springer 2017.

2016

  1. M. Aparpinis, L. Mancini, E. Ritter, M. D. Ryan. Analysis of privacy in mobile telephony systems. In International Journal of Information Security, 1-33, 2016. Springer open-access version.
  2. Jiangshan Yu, Vincent Cheval, and Mark Ryan. DTKI: a new formalized PKI with verifiable trusted parties. In The Computer Journal, 2016. Official version.

2015

  1. Jiangshan Yu and Mark D. Ryan. Device attacker models: fact and fiction. In Security Protocols XXIII, 2015.
  2. Ben Smyth, Mark D. Ryan and Liqun Chen. Formal analysis of privacy in Direct Anonymous Attestation schemes. In Science of Computer Programming Volume 111, Part 2, 2015.
  3. Gurchetan S. Grewal, Mark D. Ryan, Liqun Chen and Michael R. Clarkson. Du-Vote: Remote Electronic Voting with Untrusted Computers. In 28th IEEE Computer Security Foundations Symposium (CSF), 2015.

2014

  1. Jia Liu, Mark D. Ryan and Liqun Chen. Balancing Societal Security and Individual Privacy: Accountable Escrow System. In 27th IEEE Computer Security Foundations Symposium (CSF), 2014.
  2. Mark D. Ryan. Enhanced certificate transparency and end-to-end encrypted mail. In Network and Distributed System Security (NDSS), 2014.
  3. Myrto Arapinis, Loretta I. Mancini, Mark D. Ryan and Eike Ritter. Privacy through Pseudonymity in Mobile Telephony Systems. In Network and Distributed System Security (NDSS), 2014.
  4. Myrto Arapinis, Sergiu Bursuc, and Mark D. Ryan. Privacy-supporting cloud computing by in-browser key translation. In Journal of Computer Security, 2014.
  5. Myrto Arapinis, Joshua Phillips, Mark D. Ryan and Eike Ritter. StatVerif: Verification of Stateful Processes. In Journal of Computer Security, 2014.
  6. Myrto Arapinis, Jia Liu, Eike Ritter, Mark Ryan. Stateful applied pi calculus. In POST'14.

2013

  1. Shiwei Xu, Ian Batten, Mark Ryan. Dynamic Measurement and Protected Execution: Model and Analysis. In Trustworthy Global Computing, 2013.
  2. Mark Dermot Ryan. Cloud computing security: The scientific challenge, and a survey of solutions. In Journal of Systems and Software 86(9): 2263-2268, 2013.
  3. Masoud Koleini and Mark D. Ryan. Model checking agent knowledge in dynamic access control policies. In TACAS, 2013. (Longer tech report.)
  4. Gurchetan S. Grewal, Mark D. Ryan, Sergiu Bursuc and Peter Y. A. Ryan. Caveat Coercitor: coercion-evidence in electronic voting. In IEEE Symposium on Security and Privacy, 2013.
  5. Myrto Arapinis, Veronique Cortier, Steve Kremer, Mark Ryan. Practical Everlasting Privacy. In POST'13.

2012

  1. Myrto Arapinis, Ravishankar Borgaonkar, Nico Golde, Loretta Mancini, Kevin Redon, Eike Ritter and Mark Ryan. New privacy issues in mobile telephony: fix and verification. In CCS'12.
  2. Myrto Arapinis, Sergiu Bursuc and Mark Ryan. Privacy-Supporting Cloud Computing: ConfiChair, a case study. In POST 2012.
  3. Myrto Arapinis, Sergiu Bursuc and Mark Ryan. Reduction of equational theories for verification of trace equivalence: re-encryption, associativity and commutativity. In POST 2012.

2011

  1. Sergiu Bursuc, Gurchetan Grewal and Mark Ryan. Trivitas: Voters Directly Verifying Votes. In VoteID 2011.
  2. Ben Smyth, Mark Ryan and Liqun Chen. Formal analysis of anonymity in ECC-based Direct Anonymous Attestation schemes. In Proceedings of the Eighth International Workshop on Formal Aspects of Security and Trust (FAST'11).
  3. Masoud Koleini and Mark Ryan. A knowledge-based verification method for dynamic access control policies. In Proceedings of the 13th International Conference on Formal Engineering Methods (ICFEM 2011).
  4. Mark Ryan. Cloud Computing Privacy Concerns on our Doorstep. In Communications of the ACM, 54(1), pp. 36-38. January 2011.
  5. Mark Ryan and Ben Smyth. The Applied Pi Calculus. In Véronique Cortier and Steve Kremer editors, Formal Models and Techniques for Analyzing Security Protocols, chapter 6, IOS Press.
  6. Myrto Arapinis, Eike Ritter and Mark Ryan. StatVerif: Verification of Stateful Processes. In Proceedings of the 24th IEEE Computer Security Foundations Symposium (CSF 2011), pp. 33-47.
  7. Stéphanie Delaune, Steve Kremer, Mark Ryan and Graham Steel. Formal analysis of protocols based on TPM state registers. In Proceedings of the 24th IEEE Computer Security Foundations Symposium (CSF 2011), pp. 66-82.

2009

  1. M. Koleini, H. Qunoo and M. Ryan. Towards Modelling and Verifying Dynamic Access Control Policies for Web-Based Collaborative Systems. W3C Workshop on Access Control Application Scenarios, 2009.
  2. S. Delaune, S. Kremer and M. D. Ryan. Verifying Privacy-type Properties of Electronic Voting Protocols. In Journal of Computer Security, 17(4), pages 435-487. IOS Press, 2009.
  3. T. T. A. Dinh, T. Chothia and M. D. Ryan. A Trusted Infrastructure for P2P-Based Marketplaces. In 9th IEEE International Conference on Peer-to-Peer Computing (P2P'09), 2009. Pages 151-154.
  4. L. Chen and M. D. Ryan. Offline dictionary attack on TCG TPM weak authorisation data, and solution. In D. Grawrock,  H. Reimer, A. Sadeghi, C. Vishik, editors, Future of Trust in Computing, Vieweg & Teubner, 2009.
  5. A. Mukhamedov, A. Gordon and M. D. Ryan. Towards a Verified Reference Implementation of the Trusted Platform Module. In 19th International Workshop on Security Protocols, LNCS, Springer, 2009.

2008

  1. A. Mukhamedov and M. D. Ryan. Fair Multi-party Contract Signing using Private Contract Signatures. Information and Computation. 206(2-4), pages 272-290, Academic Press, 2008.
  2. N. Zhang, D. P. Guelev and Mark Ryan. Synthesising Verified Access Control Systems through Model Checking. Journal of Computer Security 16(1):1-61. 2008
  3. S. Delaune, S. Kremer and M. D. Ryan. Composition of Password-based Protocols. In 21st IEEE Computer Security Foundations Symposium (CSF'08), IEEE Comp. Soc. Press, 2008.
  4. A. Brown and M. D. Ryan. Synthesising Monitors from High-level Policies for the Safe Execution of Untrusted Software, in Fourth Information Security Practice and Experience Conference (ISPEC 2008). LNCS, Springer, 2008.
  5. A. Salaiwarakul and M. D. Ryan. Verification of Integrity and Secrecy Properties of a Biometric Authentication Protocol, in Fourth Information Security Practice and Experience Conference (ISPEC'08). LNCS, Springer, 2008.
  6. A. Brown and M. D. Ryan. Monitoring the Execution of Third-party Software on Mobile Devices (Extended Abstract). 11th International Symposium On Recent Advances In Intrusion Detection (RAID'08), LNCS, Springer, 2008.
  7. A. Salaiwarakul and M. D. Ryan. Analysis of a Biometric Authentication Protocol for Signature Creation Application. Third International Workshop on Security (IWSEC'08), LNCS, Springer, 2008.
  8. S. Delaune, M. Ryan and B. Smyth. Automatic verification of privacy properties in the applied pi calculus. In Proceedings of the 2nd Joint iTrust and PST Conferences on Privacy, Trust Management and Security (IFIPTM'08). IFIP International Federation for Information Processing, volume 263, pp. 263-278, Springer-Verlag 2008.
  9. Tien Tuan Anh Dinh and Mark Ryan. A Sybil-Resilient Reputation Metric for P2P Applications. In Third International Workshop on Dependable and Sustainable Peer-to-Peer Systems (DAS-P2P 2008), in conjunction with the 2008 International Symposium on Applications and the Internet (SAINT2008).

2007

  • Nikos Gorogiannis and Mark Ryan. Requirements, specifications and minimal refinement. Formal Aspects of Computing 19(4), pp.417-444, Springer-Verlag 2007.  (DOI:10.1007/s00165-006-0014-3).
    Code supporting the paper: ACTL tableau generator, by Nikos Gorogrannis.  It outputs SMV or DOT code for the resulting finite state automaton. Written in C++, should work under Unix or Windows without significant changes.
  • D. P. Guelev, Mark D. Ryan and Pierre-Yves Schobbens. Model-checking the Preservation of Temporal Properties upon Feature Integration. International Journal on Software Tools for Technlogy Transfer, 9(1), 53-62,  2007.
  • Stephan Reiff-Marganiec and Mark Ryan (eds). Computer Networks, 51(2). Special issue on Feature Integration. Guest Editorial. Elsevier, 2007.
  • A. Mukhamedov and M. Ryan. Anonymity protocol with identity escrow, and analysis in the applied pi calculus. In G. Barthe and C.  Fournet, eds, Trustworthy Global Computing, LNCS, Springer-Verlag, 2007
  • S. Delaune, S. Kremer and M. Ryan. Symbolic bisimulation for the applied pi calculus.  Foundations of Software Technology and Theoretical Computer Science (FSTTCS'07), Springer-Verlag, 13pp, 2007.
  • S. Delaune, S. Kremer and M. Ryan. Symbolic bisimulation for the applied pi calculus (extended abstract). International Workshop on Security Issues in Concurrency, LNCS, Springer-Verlag, 2007.
  • B. Smyth, L. Chen,  and M. D. Ryan, Direct Anonymous Attestation: ensuring privacy with corrupt administrators. F. Stajano et al. (eds.), Procedings of the Fourth European Workshop on Security and Privacy in Ad hoc and Sensor Networks, pp. 218-­231, LNCS 4572, Springer-Verlag 2007.
  • A. Mukhamedov and M. D. Ryan. Improved multi-party contract signing. Financial Cryptography and Data Security, LNCS 4889, Springer, pages 179-191,  2007.

2006

2005

  • Dimitar P. Guelev, Mark Ryan, and Pierre Yves Schobbens. Synthesising Features by Games. Proceedings of the 5th International Workshop on Automated Verification of Critical Systems (AVoCS 2005), edited by R. Lazic and R. Nagarajan.  Electronic Notes in Theoretical Computer Science volume 145, pages 79-93. 2005.
  • Aybek Mukhamedov and Mark D. Ryan, On Anonymity with Identity Escrow. Proceedings of the Third international Workshop on Formal Aspects in Security and Trust (FAST2005).  LNCS volume 3866, pages 235-243. Springer-Verlag, 2005.
  • N. Zhang, Mark D. Ryan and Dimitar Guelev, Evaluating Access Control Policies Through Model Checking. Eighth Information Security Conference (ISC'05). Lecture Notes in Computer Science volume 3650, pages 446-460, Springer-Verlag, 2005.
  • Aidan Harding, Mark Ryan and Pierre Yves Schobbens. A New Algorithm for Strategy Synthesis in LTL Games.  Eleventh International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'05). Lecture Notes in Computer Science volume 3440, edited by Nicolas Halbwachs and Lenore D. Zuck. Pages 477-492. Springer-Verlag.
  • Steve Kremer and Mark D. Ryan. Analysis of an Electronic Voting Protocol in the Applied Pi Calculus. In Proceedings of the European Symposium on Programming (ESOP'05),  Lecture Notes in Computer Science volume 3444, pages 186-200. Springer Verlag, 2005.

2004

2003

  • H. Harris and M. D. Ryan, Theoretical Foundations of Updating Systems. In Proceedings of Automated Software Engineering 2003, 18th IEEE International Conference. IEEE Computer Society Press, 2003. 8 pages.
  • D. P. Guelev, P. Y. Schobbens and M. D. Ryan, Feature Integration by Substitution. In D. Amyot and L. Logrippo (editors), Feature Interactions in Telecommunications and Software Systems VII, IOS Press, pp. 275-291, 2003.

2002

2001

2000

1999

  • A. Lomuscio and M. D. Ryan, An algorithmic approach to knowledge evolution. Artificial Intelligence for Engineering Design, Analysis and Manufacturing (AIEDAM), Vol. 13, No. 2 (Special issue on Temporal Logic in Engineering), pp.119-132, 1999. (RAE2001)
  • M. C. Plath and M. D. Ryan. SFI: a feature integration tool. In R. Berghammer and Y. Lakhnech, editors, Tool Support for System Specification, Development and Verification, Advances in Computing Science, pages 201-216. Springer, 1999.
  • Alessio Lomuscio and Mark Ryan.  A Spectrum of Modes of Knowledge Sharing between Agents. Sixth International Workshop on Agent Theories Architectures and Languages (ATAL-99), pages 13-26, LNCS, Springer-Verlag, 1999.

1998

  • Malte Plath and Mark Ryan, A Feature Construct for Promela. In SPIN'98 -- Proceedings of the 4th SPIN workshop, November 1998.
  • M. Plath and M. Ryan, Plug and Play Features, 28pp, Fifth International Workshop on Feature Interactions in Telecommunications and Software Systems, IOS Press, 1998.
  • A. Lomuscio and M. Ryan. Model refinement and model checking for S5n. Proceedings of the ECAI-98 Workshop on Practical Reasoning and Rationality, Brighton (UK), 1998.
  • A. Lomuscio and M. Ryan. Ideal agents sharing (some!) knowledge. In Proceedings of ECAI-98, 13th European Conference on Artificial Intelligence. John Wiley & Sons, 5pp, 1998.
  • F. Miguel Dionisio, Stefan Brass, Mark Ryan and Udo W. Lipeck, Hypothetical Reasoning with Defaults. Workshop on Computational Aspects of Nonmonotonic Reasoning-CNMR'98 (Held in conjunction with the Seventh International Workshop on Nonmonotonic Reasoning), 1998

1997

1996
  • M. d'Inverno, M. Fisher, A. Lomuscio, M. Luck, M. de Rijke, M. Ryan and M. Wooldridge. Formalisms for multi-agent systems. The Knowledge Engineering Review, Vol. 12:3, 1997, 315-321.
  • M. Ryan and P.-Y. Schobbens. Intertranslating counterfactuals and updates. In W. Wahlster, editor, 12th European Conference on Artificial Intelligence (ECAI), pages 100--104. John Wiley & Sons, Ltd., 1996.
  • A. S. Guerra and M. Ryan. Feature- and object-oriented specifications. In P.-Y. Schobbens, editor, ModelAge'96: Proceedings of the Esprit WG Workshop, 1996.
  • M. Ryan, P.-Y. Schobbens, and O. Rodrigues. Counterfactuals and updates as inverse modalities. In Y. Shoham, editor, TARK'96: Proc. Theoretical Aspects of Rationality and Knowledge, pages 163--173. Morgan Kaufmann, 1996.
  • A. Finkelstein, M. Ryan, and G. Spanoudakis. Software package requirements and procurement. In Proc. 8th International Workshop on Software Specification and Design (IWSSD-8). IEEE CS Press, 1996.

1994

  • M. D. Ryan. Belief revision and ordered theory presentations. In A. Fuhrmann and H. Rott, editors, Logic, Action and Information. De Gruyter Publishers, 1994. Also in Proc. Eighth Amsterdam Colloquium on Logic, University of Amsterdam, 1991.

1993

  • M. D. Ryan. Prioritising preference relations. In G.L. Burn, S.J. Gay, and M.D. Ryan, editors, Theory and Formal Methods 1993: Proceedings of the First Imperial College, Department of Computing, Workshop on Theory and Formal Methods, Isle of Thorns Conference Centre, Chelwood Gate, Sussex, UK, 29--31 March 1993. Springer-Verlag Workshops in Computer Science.
  • G. L. Burn, S. J. Gay, and M. D. Ryan, editors. Theory and Formal Methods 1993: Proceedings of the First Imperial College, Department of Computing, Workshop on Theory and Formal Methods, Isle of Thorns Conference Centre, Chelwood Gate, Sussex, UK, 29--31 March 1993. Springer-Verlag Workshops in Computer Science.
  • M. D. Ryan. Defaults in specifications. In A. Finkelstein, editor, Proc. IEEE International Symposium on Requirements Engineering (RE'93), pages 142--149, 1993.
  • M. D. Ryan. Towards specifying norms. Annals of Mathematics and Artificial Intelligence, 9:49--67, 1993.
  • M. D. Ryan and M. R. Sadler. Valuation systems and consequence relations. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, volume 1. Oxford University Press, 1992.

1992

1991

  • M. D. Ryan, J. Fiadeiro, and T. Maibaum. Sharing actions and attributes in modal action logic. In T. Ito and A. Meyer, editors, Theoretical Aspects of Computer Software, pages 569--593. Lecture Notes in Computer Science 526, Springer Verlag, 1991.
  • M. D. Ryan. Defaults and revision in structured theories. In Proc. Sixth IEEE Symposium on Logic in Computer Science (LICS), pages 362--373. Morgan Kaufmann, 1991.
  • H. Fuks, M. Ryan, and M. Sadler. Outline of a commitment logic for legal reasoning. In Proc 3rd International Conference on Logics, Informatics and Law, volume 44, pages 167--207, 1990.