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

2017

  1. Myrto Arapinis, Loretta Ilaria Mancini, Eike Ritter, Mark D. Ryan. Analysis of privacy in mobile telephony systems. In International Journal of Information Security, 16(5): 491-523, 2017. Springer version.
  2. Kevin Milner, Cas Cremers, Jiangshan Yu, Mark Ryan Automatically Detecting the Misuse of Secrets: Foundations, Design Principles, and Applications. In IEEE Computer Security Foundations Symposium (CSF), 2017.
  3. Jiangshan Yu, Mark Ryan and Liqun Chen. Authenticating compromisable storage systems. In 16th IEEE International Conference on Trust, Security and Privacy in Computing and Communications (IEEE TrustCom-17), 2017.
  4. Mark D. Ryan. Making Decryption Accountable. In 25th Security Protocols Workshop, Springer LNCS, 2017.
  5. Michael Denzel, Mark D. Ryan and Eike Ritter. A malware-tolerant, self-healing industrial control system framework. In 32nd International Conference on ICT Systems Security and Privacy Protection (IFIP-SEC 2017), 2017.
  6. Jia Liu, Myrto Arapinis, Eike Ritter and Mark Ryan. Stateful applied pi calculus: observational equivalence and labelled bisimilarity. In Journal of Logical and Algebraic Methods in Programming, 89: 95-149, 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.

2010

  1. A. Mukhamedov and M. D. Ryan. Anonymity Protocol with Identity Escrow and Analysis in the Applied pi-calculus. In ACM Transactions on Information and System Security (TISSEC). 13(4), article 41. December 2010.
  2. H. Qunoo and M. Ryan. Modelling Dynamic Access Control Policies for Web-Based Collaborative Systems. In S. Foresti and S. Jajodia editors, Proceedings of the 24th Annual IFIP WG 11.3 Working Conference on Data and Applications Security and Privacy. LNCS 6166, Springer, pp. 295-302, 2010.
  3. T. T. A. Dinh and M. Ryan. Verifying Security Property of Peer-to-Peer Systems Using CSP. In Proceedings of the fifteenth European Symposium on Research in Computer Security (ESORICS'10). LNCS, Springer, pp. 319-339, 2010.
  4. M. Arapinis, T. Chothia, E. Ritter and M. Ryan. Analysing unlinkability and anonymity using the applied pi calculus. In Proceedings of the 23rd IEEE Computer Security Foundations symposium (CSF 2010). IEEE Computer Society, pp. 107-121, 2010.
  5. S. Delaune, S. Kremer, M. D. Ryan and G. Steel. A formal analysis of authentication in the TPM. In Proceedings of Seventh International Workshop on Formal Aspects in Security and Trust (FAST'10). LNCS, Springer.
  6. S. Kremer, M. D. Ryan and B. Smyth. Election verifiability in electronic voting protocols. In Proceedings of the fifteenth European Symposium on Research in Computer Security (ESORICS'10). LNCS, Springer, volume 6345, pp. 389-404, 2010.
  7. K. Ables and M. D. Ryan. Escrowed data and the digital envelope. In Trust and Trustworthy Computing (TRUST 2010), pages 246-256. LNCS, Springer, 2010.
  8. L. Chen and M. D. Ryan. Attack, solution and verification for shared authorisation data in TCG TPM. In Proceedings of the Sixth International Workshop on Formal Aspects in Security and Trust (FAST'09). LNCS, Springer, 2010.
  9. S. Cabuk, L. Chen, D. Plaquin and M. D. Ryan. Trusted Integrity Measurement and Reporting for Virtualized Platforms. In Proceedings of International Conference on Trusted Systems (INTRUST'09). LNCS, Springer, 2010.
  10. S. Delaune, S. Kremer and M. D. Ryan. Symbolic bisimulation for the applied pi calculus. In Journal of Computer Security, 18(2), pp. 317-377, 2010.

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.

1995

  • Riccardo Poli, Mark Ryan, and Aaron Sloman. A new continuous propositional logic. In C. Pinto-Ferreira and N. J. Mamede, editors, Progress in Artificial Intelligence: Seventh Portuguese Conference on Artificial Intelligence, EPIA'95, volume 990 of Lecture Notes in Artificial Intelligence, pages 17--26, 1995.
  • H. Andreka, M. D. Ryan, and P.-Y. Schobbens. Operators and laws for combining preference relations. In R. J. Wieringa and R. B. Feenstra, editors, Information Systems: Correctness and Reusability (Selected Papers). World Scientific Publishing Co., 1995.
  • M. D. Ryan, A. Sernadas, and C. Sernadas. Adjunctions between default frameworks. In R. J. Wieringa and R. B. Feenstra, editors, Information Systems: Correctness and Reusability (Selected Papers). World Scientific Publishing Co., 1995.
  • M. D. Ryan and P.-Y. Schobbens. Belief revision and verisimilitude. Notre Dame Journal of Formal Logic, 36(1), 1995.

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.