Research / Groupings / Formal Verification And Security / Publications

Publications

A selection of publications produced by group members are listed below.

[Sort by: date, type]

62 publications:

2010

[CabukChenPlaquinRyan2010] Serdar Cabuk, Liqun Chen, David Plaquin and Mark Ryan. Trusted Integrity Measurement and Reporting for Virtualized Platforms. In Proceedings of the International Conference on Trusted Systems (INTRUST'09), Springer. 2010.
[ChenRyan2010Authdata] Liqun Chen and Mark 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), Springer. 2010.

2009

[DinhChothiaRyan2009] Tien Tuan Anh Dinh, Tom Chothia and Mark Ryan. A Trusted Infrastructure for P2P-Based Marketplaces. In 9th IEEE International Conference on Peer-to-Peer Computing (P2P'09), pages 151-154. 2009.
[DelauneKremerRyan2009EVoting] Stéphanie Delaune, Steve Kremer and Mark Ryan. Verifying Privacy-type Properties of Electronic Voting Protocols. Journal of Computer Security, pages 435-487, IOS Press. 2009.
[DelauneKremerRyan2010Bisimulation] Stéphanie Delaune, Steve Kremer and Mark Ryan. Symbolic Bisimulation for the Applied Pi Calculus. Journal of Computer Security. To appear. 2009.

2008

[DinhRyan2008P2P] 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). 2008.
[DelauneRyanSmyth2008VeriPriv] Stéphanie Delaune, Mark Ryan and Ben 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), pages 263-278, Springer. 2008.
[MukhamedovRyan2008] Aybek Mukhamadov and Mark Ryan. Fair Multi-party Contract Signing using Private Contract Signatures. Information and Computation, pages 272-290. 2008.
[ChenRyan2008] Liqun Chen and Mark Ryan. Offline dictionary attack on TCG TPM weak authorisation data, and solution. In D. Grawrock and H. Reimer and A. Sadeghi and C. Vishik (editors) Future of Trust in Computing, Vieweg & Teubner. 2008.
[BrownRyan2008] Andrew Brown and Mark Ryan. Synthesising Monitors from High-level Policies for the Safe Execution of Untrusted Software. In Fourth Information Security Practice and Experience Conference (ISPEC 2008), Springer. 2008.
[SalaiwarakulRyan2008] Anongporn Salaiwarakul and Mark Ryan. Verification of Integrity and Secrecy Properties of a biometric Authentication Protocol. In Fourth Information Security Practice and Experience Conference (ISPEC'08), Springer. 2008.
[DelauneKremerRyan2008Bisimulation] Stéphanie Delaune, Steve Kremer and Mark Ryan. Symbolic Bisimulation for the applied pi Calculus. Submitted JCS. 2008.
[MukhamedovRyan2008Escrow] Aybek Mukhamedov and Mark Ryan. Anonymity protocol with identity escrow, and analysis in the applied pi calculus. Submitted TSC. 2008.
[DelauneKremerRyan2008] Stéphanie Delaune, Steve Kremer and Mark Ryan. Composition of Password-based Protocols. In 21st IEEE Computer Security Foundations Symposium, IEEE Computer Society Press. 2008.
[LiDengWang08] Tieyan Li, Robert H Deng, and Guilin Wang. The Security and Improvement of an Ultra-lightweight RFID Authentication Protocol. Journal of Security and Communication Networks, 1(2), pages 135--146, Wiley. 2008.
[BrownRyan2008MobileDevices] Andrew Brown and Mark Ryan. Monitoring the Execution of Third-party Software on Mobile Devices (Extended Abstract). In 11th International Symposium On Recent Advances In Intrusion Detection (RAID'08), Springer. 2008.
[SalaiwarakulRyan2008Biometric] Anongporn Salaiwarakul and Mark Ryan. Analysis of a Biometric Authentication Protocol for Signature Creation Application. In Third International Workshop on Security (IWSEC'08), Springer. 2008.
[GaoWWL08] Wei Gao, Guilin Wang, Xueli Wang and Fei Li. One-Round ID-Based Blind Signature Scheme without ROS Assumption. In Pairing, pages 316-331. 2008.
[ICICS08] Liqun Chen and Mark Dermot Ryan and Guilin Wang. Information and Communications Security. 2008.
[LiWD08] Tieyan Li, Guilin Wang and Robert H. Deng. Security Analysis on a Family of Ultra-lightweight RFID Authentication Protocols. JSW, 3(3), pages 1-10. 2008.

2007

[DAAsrc07] Ben Smyth, Mark Ryan and Liqun Chen. Direct Anonymous Attestation (DAA): Ensuring privacy with corrupt administrators. In F. Stajano (editor) ESAS'07: Fourth European Workshop on Security and Privacy in Ad hoc and Sensor Networks, volume 4572 of Lecture Notes in Computer Science, pages 218--231, Springer-Verlag. 2007. [pdf] [bib]
[ZhangGuelevRyan2008] Nan Zhang, Dimitar P. Guelev and Mark Ryan. Synthesising Verified Access Control Systems through Model Checking. Journal of Computer Security, 16(1), pages 1-61. 2007.
[GorogiannisRyan2007] Nikos Gorogiannis and Mark Ryan. Requirements, specifications and minimal refinement. Formal Aspects of Computing, 19(4), pages 417-444. 2007.
[MarganiecRyan2007] Stephan Reiff-Marganiec and Mark Ryan. Special Issue on Feature Integration. Computer Networks. 2007.
[DelauneKremerRyan2007] Stéphanie Delaune, Steve Kremer and Mark Ryan. Symbolic bisimulation for the applied pi calculus. In Foundations of Software Technology and Theoretical Computer Science (FSTTCS'07), Springer. 2007.
[DelauneKremerRyan2007abs] Stéphanie Delaune, Steve Kremer and Mark Ryan. Symbolic bisimulation for the applied pi calculus (extended abstract). In International Workshop on Security Issues in Concurrency, Springer. 2007.
[GuelevRyanSchobbens2007] Dimitar P. Guelev, Mark 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), pages 53-62, IOS Press. 2007.
[MukhamedovRyan2007Escrow] Aybek Mukhamedov and Mark Ryan. Anonymity protocol with identity escrow, and analysis in the applied pi calculus. In G. Barthe and C. Fournet (editors) Trustworthy Global Computing, Springer. 2007.
[LiuWHWHMS07] Dennis Y. W. Liu, Duncan S. Wong, Xinyi Huang, Guilin Wang, Qiong Huang, Yi Mu and Willy Susilo. Formal Definition and Construction of Nominative Signature. In ICICS, pages 57-68. 2007.
[MukhamedovRyan2007Contract] Aybek Mukhamedov and Mark Ryan. Improved multi-party contract signing. In Financial Cryptography and Data Security, volume 4889 of LNCS, pages 179-191, Springer. 2007.

2006

[MukhamedovRyan2006] Aybek Mukhamedov and Mark Ryan. Resolve-Impossibility for a Contract-Signing Protocol. In 19th Computer Security Foundations Workshop (CSFW), pages 167-176, IEEE Computer Society Press. 2006.
[DelauneKremerRyan2006Coercion] Stéphanie Delaune, Steve Kremer and Mark Ryan. Coercion-resistance and Receipt-freeness in Electronic Voting. In 19th Computer Security Foundations Workshop (CSFW), pages 28-42, IEEE Computer Society Press. 2006.
[DelauneKremerRyan2006VerifyingVoting] Stéphanie Delaune, Steve Kremer and Mark Ryan. Verifying properties of electronic voting protocols. In David Chaum and Ron Rivest and Markus Jakobsson and Berry Schoenmakers and Peter Ryan and Josh Benaloh and Mirek Kutylowski (editors) Towards Trustworthy Election Systems. 2006.

2005

[MukhamedovRyan2005] Aybek Mukhamedov and Mark Ryan. On Anonymity with Identity Escrow. In Proceedings of the Third international Workshop on Formal Aspects in Security and Trust (FAST2005), volume 3866 of LNCS, pages 235-243, Springer. 2005.
[ZhangRyanGuelev2005] Nan Zhang, Mark Ryan and Dimitar Guelev. Evaluating Access Control Policies Through Model Checking. In Eighth Information Security Conference (ISC'05). Lecture Notes in Computer Science volume 3650:446-460. 2005.
[KremerRyan2005] Steve Kremer and Mark Ryan. Analysis of an Electronic Voting Protocol in the Applied Pi Calculus. In Proceedings of the European Symposium on Programming (ESOP'05), pages 186-200, Springer. Lecture Notes in Computer Science series. 2005.
[mukhamedov2005amp] A. Mukhamedov, S. Kremer and E. Ritter. Analysis of a Multi-Party Fair Exchange Protocol and Formal Proof of Correctness in the Strand Space Model. LNCS, 3570, pages 255--269, Springer. 2005.
[GuelevRyanSchobbens2005] Dimitar P. Guelev, Mark Ryan and Pierre-Yves Schobbens. Synthesising Features by Games. In R. Lazic and R. Nagarajan (editors) Proceedings of the 5th International Workshop on Automated Verification of Critical Systems (AVoCS 2005). Electronic Notes in Theoretical Computer Science volume 145:79-93. 2005.
[HardingRyanSchobbens2005] Aidan Harding, Mark Ryan and Yves Schobbens. A New Algorithm for Strategy Synthesis in LTL Games. In Nicolas Halbwachs and Lenore D. Zuck (editors) Eleventh International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'05), volume 3440 of LNCS, pages 477-492, Springer. 2005.

2004

[KremerRyan2004] Steve Kremer and Mark Ryan. Analysing the vulnerability of protocols to produce known-pair and chosen-text attacks. In Proceedings of the 2nd International Workshop on Security Issues in Coordination Models, Languages, and Systems (SecCo 2004), pages 87-104. Electronic Notes in Theoretical Computer Science - Special Issue for CONCUR'04 Workshop on Security Issues in Coordination Models, Languages and Systems (SecCo'04). 2004.
[ZhangRyanGuelev2004] Nan Zhang, Mark Ryan and Dimitar P. Guelev. Synthesising Verified Access Control Systems in XACML. In 2nd ACM Workshop on Formal Methods in Security Engineering, pages 56-65, Springer. 2004.
[HuthRyan2004] Michael Huth and Mark Ryan. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press. Second Edition with major revisions and updates. 2004.
[GuelevRyanSchobbens2004Integration] Dimitar P. Guelev, Mark Ryan and Pierre-Yves Schobbens. Model-checking the Preservation of Temporal Properties upon Feature Integration. In Proceedings of the Fouth International Workshop on Automated Verification of Critical Systems (CONCUR Workshop AVoCS 2004), pages 311-324. Electronic Notes in Theoretical Computer Science, Volume 128 Issue 6. 2004.
[GuelevRyanSchobbens2004AccessControl] Dimitar P. Guelev, Mark Ryan and Pierre-Yves Schobbens. Model-checking Access Control Policies. In Seventh Information Security Conference (ISC'04), Springer. Lecture notes in Computer Science. 2004.
[RyanMeyerEhrich] Objects, Agents and Features: Structuring mechanisms for contemporary software. In Mark Ryan and John-Jules Meyer and Hans-Dieter Ehrich (editors) , Springer. Lecture Notes in Computer Science, vol. 2975. 2004.

2003

[HarrisRyen2003] Hannah Harris and Mark Ryan. Theoretical Foundations of Updating Systems. In Proceedings of Automated Software Engineering 2003, 18th IEEE International Conference, IEEE Computer Society Press. 2003.
[GuelevSchobbensRyan2003] Dimitar P. Guelev, Pierre-Yves Schobbens and Mark Ryan. Feature Integration by Substitution. In D. Amyot and L. Logrippo (editors) Feature Interactions in Telecommunications and Software Systems VII, pages 275-291, IOS Press. 2003.

2002

[HarrisRyan2002] Hannah Harris and Mark Ryan. Feature Integration as an Operation of Theory Change. In F. van Harmelen (editor) Proceedings of ECAI 2002, 15th European Conference on Artificial Intelligence, pages 546-550, IOS Press. 2002.
[RyanSchobbens2002] Mark Ryan and Pierre-Yves Schobbens. Agents and Roles: Refinement in Alternating-Time Temporal Logic. In John-Jules Meyer (editor) International Workshop on Agent Theories Architectures and Languages (ATAL-01), pages 100-114, Springer. 2002.
[AndrekaRyanSchobbens2002] Hajnal Andr'eka, Mark Ryan and Pierre-Yves Schobbens. Operators and Laws for Combining Preference Relations. Journal of Logic and Computation, 12(1), pages 13-53. 2002.
[GorogiannisRyan2002BeliefChange] Nikos Gorogiannis and Mark Ryan. Implementation of Belief Change Operators using BDDs. Studia Logica, 70(1), pages 131-156. 2002.
[PlathRyan2001FeatureConstruct] Malte Plath and Mark Ryan. Feature Integration using a Feature Construct. Science of Computer Programming, 41(1), pages 53-84. Code to support the paper: ftp://ftp.cs.bham.ac.uk/pub/authors/M.D.Ryan/00-scp-data.tar.gz. 2002.
[GorogiannisRyan2002Refinement] Nikos Gorogiannis and Mark Ryan. Requirements, Specifications and Minimal Refinement. In 9th Workshop on Logic, Language, Information and Computation. Volume 67 of Electronic Notes in Theoretical Computer Science. 2002.
[HardingSchobbensRyan2002] Aidan Harding, Mark Ryan and Pierre-Yves Schobbens. Approximating ATL* in ATL. In Third International Workshop on Verification, Model Checking and Abstract Interpretation, volume 2294 of Lecture Notes in Computer Science, pages 289-301, Springer. 2002.

2001

[GilmoreRyan2001] Stephen Gilmore and Mark Ryan. Language Constructs for Describing Features. 2001.
[CassezJardRozoyRyan2001] Franck Cassez, Claude Jard, Brigitte Rozoy and Mark Ryan. Modelling and Verification of Parallel Processes. 2001.
[PlathRyan2001CSPFeatures] Malte Plath and Mark Ryan. Defining Features for CSP: Reflections on the Feature Interaction Contest. In Language Constructs for Describing Features, Springer. 2001.
[CassezRyanSchobbens2001] Franck Cassez, Mark Ryan and Pierre-Yves Schobbens. Proving feature non-interaction with Alternating-Time Temporal Logic. In Stephen Gilmore and Mark Ryan (editors) Language Constructs for Describing Features, Springer. 2001.

2000

[HuthRyan2000] Michael Huth and Mark Ryan. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press. Foreword by Ed Clarke. 2000.
[PlathRyan2000Contest] Malte Plath and Mark Ryan. Entry for FIW'00 Feature Interaction Contest. Technical report , University of Birmingham. 2000.
[LomuscioMeydenRyan2000] Alessio Lomuscio, Ron van der Meyden and Mark Ryan. Knowledge in Multi-Agent Systems: Initial Configurations and Broadcast. ACM Transactions on Computational Logic (TOCL), 1(2), pages 247-284, ACM Press. 2000.
[PlathRyan2000Semantics] Malte Plath and Mark Ryan. The feature construct of SMV semantics. In Sixth International Workshop on Feature Interactions in Telecommunications and Software Systems, IOS Press. 2000.

Instructions for submitting publications to this list

If you wish to add your publications to this list please submit the bibtex file and paper to Ben Smyth. All bibtex entries should have an additional field cats = VALUE which corresponds to the category in which the publication belongs. VALUE is a | separated list of categories chosen from the set {prot, crypto, acs, soft}. For example, if the publication belongs in the security protocols and applied cryptography then the following would be defined: cats = |prot|crypto|.

University of Birmingham