Refinement-closed security properties allow the verification of systems for all possible implementations. Some systems, however, have refinements that do not represent possible implementations. In particular, real instantiations of abstract systems comprising security-critical components surrounded by maximally hostile unrefined components are often characterised only by compositions of refinements of the abstract system's components, rather than all refinements of the abstract system. In this case, refinement-closed security properties that examine multiple behaviours of a system at once can be falsely violated by the presence of inconsistent pairs of behaviour arising from different, incompatible refinements of the system's components.
We show how to weaken a class of such properties, which includes both information flow and causation properties, to allow them to be applied to these sorts of abstract systems. The weakened properties ignore all pairs of inconsistent behaviour that would have violated the original property from which they are derived. We also show how to adapt existing automated tests for these properties to allow them to be used to test for their weakened counterparts instead. This enables greater flexibility in the application of these sorts of properties to compositions of nondeterministic components.
", author = "Toby Murray and Gavin Lowe", booktitle = "Proceedings of the Eighth International Workshop on Automated Verification of Critical Systems (AVoCS'08)", note = "To appear.", title = "On Refinement-Closed Security Properties and Nondeterministic Compositions", url = "http://web.comlab.ox.ac.uk/people/toby.murray/papers/nondet_compositions.pdf", year = "2008", } @article{temporal-logic, author = "Gavin Lowe", journal = "Formal Aspects of Computing", title = "Specification of communicating processes: temporal logic versus refusals-based refinement", year = "2008", } @conference{chris08csf, author = "Christopher Dilloway and Gavin Lowe", booktitle = "21st IEEE Computer Security Foundations Symposium (CSF 21)", title = "Specifying Secure Transport Layers", year = "2008", } @inproceedings{mazur:2007, abstract = "In this paper we consider an adaptation of counter abstraction for the CSP/FDR setting. The technique allows us to transform a concurrent system with an unbounded number of agents into a finite-state abstraction. The systems to which the method can be applied are composed of many identical node processes that run in parallel with a controller process. Refinement checks on the abstract state machine can be performed automatically in the traces and stable failures models using the model checker FDR. We illustrate the method on an example based on a multiprocessor operating system.", author = "Tomasz Mazur and Gavin Lowe", booktitle = "Proceedings of the Seventh International Workshop on Automated Verification of Critical Systems (AVoCS'07)", title = "Counter Abstraction in the CSP/FDR setting", url = "http://web.comlab.ox.ac.uk/people/tomasz.mazur/publications/counterabstraction_AVoCS.pdf", year = "2007", } Warning - the bibtex entry below may be invalid: Missing 'booktitle' @conference{harness, author = "Gavin Lowe", journal = "Proceedings of Workshop on Automated Verification of Critical Systems (AVoCS 2007)", title = "On CSP refinement tests that run multiple copies of a process", year = "2007", } @inproceedings{inproc/Lowe2007, author = "Gavin Lowe", booktitle = "{Proceedings of the Workshop on Issues in the Theory of Security (WITS '07)}", title = "On information Flow and refinement-closure", url = "http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Papers/NDC.pdf", year = "2007", } @inproceedings{inproc/Murray2007, abstract = "The rise of limited-privilege environments has been accompanied by the emergence of vulnerabilities in which a subject is able to maliciously wield their limited privileges to indirectly cause unwanted effects. Unfortunately, conventional safety analyses for access control systems are ill-equipped to deal with this problem because they do not detect the indirect effects that a subject can cause, but merely the permissions a subject can acquire. We present a technique that characterises a subject's authority as all of the effects they can cause to occur. Our technique is based on an analysis of causation, applied to a CSP model of a system. These analyses can be expressed as CSP refinements and, hence, automatically performed by a refinement-checker such as FDR. We demonstrate the ability of our technique to successfully identify excess authority by examining the 'Confused Deputy' scenario, whose vulnerability goes undetected with conventional safety analyses. ", author = "Toby Murray and Gavin Lowe", booktitle = "{Proceedings of Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (FCS-ARSPA'07)}", title = "Authority Analysis for Least Privilege Environments", url = "http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Papers/analysing_authority.pdf", year = "2007", } @conference{cdilloway2007spec, author = "Christopher Dilloway and Gavin Lowe", booktitle = "Proceedings of the Workshop on Issues in the Theory of Security (WITS '07)", title = "On the Specification of Secure Channels", year = "2007", } @article{journals/entcs/LoweO06, author = "Gavin Lowe and Jo{\"e}l Ouaknine", doi = "10.1016/j.entcs.2005.11.070", journal = "Electr. Notes Theor. Comput. Sci.", pages = "497-519", title = "On Timed Models and Full Abstraction", url = "http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Papers/timedTesting.ps", volume = "155", year = "2006", } @inproceedings{inproc/Newcomb, author = "Tom Newcomb and Gavin Lowe", booktitle = "{Proceedings of the Workshop on Issues in the Theory of Security (WITS '06)}", title = "A Computational Justification for Guessing Attack Formalisms", year = "2006", } @techreport{RR-05-05, abstract = "Recently attempts have been made to extend the Dolev-Yao security model by allowing an intruder to learn weak secrets, such as poorly-chosen passwords, by off-line guessing. In such an attack, the intruder is able to verify a guessed value g if he can use it to produce a value called a verifier. In such a case we say that g is verifier-producing. The definition was formed by inspection of known guessing attacks.
A more intuitive definition might be formed as follows: a value is verifiable if there exists some computational process that can somehow recognise a correct guess over any other value.
We formalise this intuitive definition, and use it to justify the soundness and completeness of the existing definition. Specifically we show that a value is recognisable if and only if the value is either already Dolev-Yao deducible or it is verifier-producing. In order to do this it was necessary to clarify the definition of verifier production slightly, revealing an ambiguity in the original definition.
", author = "Tom Newcomb and Gavin Lowe", institution = "Oxford University Computing Laboratory", month = "October", number = "RR-05-05", title = "A computational justification for guessing attack formalisms", year = "2005", } @article{journals/tcs/RohrmairL05, author = "Gordon Thomas Rohrmair and Gavin Lowe", doi = "10.1016/j.tcs.2005.03.004", journal = "Theor. Comput. Sci.", number = "1", pages = "82-101", title = "Using data-independence in the analysis of intrusion detection systems", url = "http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Security/Papers/intrusion.ps", volume = "340", year = "2005", } @article{journals/tcs/BoltonL05, author = "Christie Bolton and Gavin Lowe", doi = "10.1016/j.tcs.2004.10.004", journal = "Theoretical Computer Science", number = "3", pages = "407-438", title = "A hierarchy of failures-based models: theory and application", url = "http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Papers/EXPRESS.ps", volume = "330", year = "2005", } @article{journals/tcs/Lowe04, author = "Gavin Lowe", doi = "10.1016/j.tcs.2003.11.019", journal = "Theor. Comput. Sci.", number = "1", pages = "209-256", title = "Semantic models for information flow", url = "http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Security/Papers/infoflow.ps", volume = "315", year = "2004", } @article{journals/jcs/Lowe04a, author = "Gavin Lowe", journal = "Journal of Computer Security", number = "3-4", pages = "619-653", title = "Defining information flow quantity", url = "http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Security/Papers/capacityJCS.ps", volume = "12", year = "2004", } @article{journals/jcs/Lowe04, author = "Gavin Lowe", journal = "Journal of Computer Security", number = "1", pages = "83-98", title = "Analysing Protocol Subject to Guessing Attacks", url = "http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Security/Papers/guessing.ps", volume = "12", year = "2004", } @article{journals/ijisec/HopcroftL04, author = "Philippa J. Hopcroft and Gavin Lowe", doi = "10.1007/s10207-004-0040-1", journal = "Int. J. Inf. Sec.", note = "The {CSP} scripts associated with this paper are available here: \url{http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Security/Papers/TESLA/index.html}", number = "1", pages = "2-13", title = "Analysing a stream authentication protocol using model checking", url = "http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Security/Papers/TESLA.ps", volume = "3", year = "2004", } @article{journals/entcs/BoltonL04, author = "Christie Bolton and Gavin Lowe", doi = "10.1016/j.entcs.2004.04.025", journal = "Electr. Notes Theor. Comput. Sci.", pages = "129-152", title = "A Hierarchy of Failures-Based Models", volume = "96", year = "2004", } @inproceedings{conf/dsn/BoltonL04, author = "Christie Bolton and Gavin Lowe", booktitle = "2004 International Conference on Dependable Systems and Networks (DSN 2004), 28 June - 1 July 2004, Florence, Italy, Proceedings", isbn = "0-7695-2052-9", pages = "485-494", publisher = "IEEE Computer Society", title = "Analyses of the Reverse Path Forwarding Routing Algorithm", url = "http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Papers/RPF.ps", year = "2004", } @inproceedings{inproc/avis, author = "Gavin Lowe", booktitle = "{Proceedings of the Third International Workshop on Automatic Verification of Infinite-State Systems, (AVIS 2004)}", title = "On the Application of Counterexample-Guided Abstraction refinement and data independence to the parameterised model checking problem", url = "http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Papers/CEGAR.ps", year = "2004", } @techreport{RR-03-19, abstract = "The purpose of a grid is to enable large scale distributed computing over wide area networks, where entities (for example, users) can gain seamless access to computing resources across heterogeneous and geographically dispersed environments. There are a number of difficult issues that arise within the design and deployment of such a grid architecture; security has been a particularly difficult issue. In this paper, we will focus on the security implications arising through the introduction of delegation, an essential requirement to enable the sort of distributed collaboration and resource sharing for which the grid is designed. The precise impact of proposed delegation mechanisms upon security remains unclear within many grid projects. What security guarantees are required from the delegation architecture, and how does one determine whether a particular architecture provides those guarantees? In this paper, we aim to address these issues more precisely. We begin by identifying a number of security aspects of delegation. We then consider two existing architectures for secure delegation and evaluate what security requirements they meet. Finally, we discuss their applicability in practice within a grid environment, focusing mainly upon our observations within the European Union DataGrid project.", author = "Philippa J. Broadfoot and Gavin Lowe", institution = "Oxford University Computing Laboratory", month = "September", number = "RR-03-19", title = "Architectures for Secure Delegation Within Grids", year = "2003", } @article{journals/jcs/HeatherLS03, author = "James Heather and Gavin Lowe and Steve Schneider", journal = "Journal of Computer Security", number = "2", pages = "217-244", title = "How to Prevent Type Flaw Attacks on Security Protocols", url = "http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Security/Papers/typing.ps", volume = "11", year = "2003", } @article{journals/corr/cs-DC-0306004, author = "Roberto Alfieri and Roberto Cecchini and Vincenzo Ciaschini and Luca dell'Agnello and Alberto Gianoli and Fabio Spataro and Franck Bonnassieux and Philippa J. Broadfoot and Gavin Lowe and Linda Cornwall and Jens Jensen and David P. Kelsey and {\'A}kos Frohner and David L. Groep and Wim Som de Cerff and Martijn Steenbakkers and Gerben Venekamp and Daniel Kouril and Andrew McNab and Olle Mulmo and Mika Silander and Joni Hahkala and K{\'a}roly L{\"o}rentey", journal = "CoRR", title = "Managing Dynamic User Communities in a Grid of Autonomous Resources", url = "http://arxiv.org/abs/cs.DC/0306004", volume = "cs.DC/0306004", year = "2003", } @inproceedings{conf/iwfm/BoltonL03, author = "Christie Bolton and Gavin Lowe", booktitle = "6th International Workshop on Formal Methods, IWFM 2003, Dublin City University. 11 July, 2003", editor = "Joseph M. Morris and Benjamin Aziz and Fr{\'e}d{\'e}ric Oehl", publisher = "BCS", series = "Workshops in Computing", title = "On the Automatic Verification of Non-Standard Measures of Consistency", url = "http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Papers/IWFM.ps", year = "2003", } @inproceedings{conf/csfw/BroadfootL03, author = "Philippa J. Broadfoot and Gavin Lowe", booktitle = "16th IEEE Computer Security Foundations Workshop (CSFW-16 2003), 30 June - 2 July 2003, Pacific Grove, CA, USA", isbn = "0-7695-1927-X", pages = "141-", publisher = "IEEE Computer Society", title = "On Distributed Security Transactions that Use Secure Transport Protocols", url = "http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Security/Papers/layering.ps", year = "2003", } @inproceedings{conf/fasec/RohrmairL02, author = "Gordon Thomas Rohrmair and Gavin Lowe", booktitle = "Formal Aspects of Security, First International Conference, FASec 2002, London, UK, December 16-18, 2002, Revised Papers", editor = "Ali E. Abdallah and Peter Ryan and Steve Schneider", isbn = "3-540-20693-0", pages = "205-220", publisher = "Springer", series = "Lecture Notes in Computer Science", title = "Using CSP to Detect Insertion and Evasion Possibilities within the Intrusion Detection Area", url = "http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Security/Papers/IDS.ps", volume = "2629", year = "2002", } @inproceedings{conf/esorics/BroadfootL02, author = "Philippa J. Broadfoot and Gavin Lowe", booktitle = "Computer Security - ESORICS 2002, 7th European Symposium on Research in Computer Security, Zurich, Switzerland, October 14-16, 2002, Proceedings", editor = "Dieter Gollmann and G{\"u}nter Karjoth and Michael Waidner", isbn = "3-540-44345-2", pages = "146-161", publisher = "Springer", series = "Lecture Notes in Computer Science", title = "Analysing a Stream Authentication Protocol Using Model Checking", volume = "2502", year = "2002", } @inproceedings{conf/csfw/Lowe02, author = "Gavin Lowe", booktitle = "15th IEEE Computer Security Foundations Workshop (CSFW-15 2002), 24-26 June 2002, Cape Breton, Nova Scotia, Canada", isbn = "0-7695-1689-0", pages = "18-31", publisher = "IEEE Computer Society", title = "Quantifying Information Flow", url = "http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Security/Papers/capacity.ps", year = "2002", } @article{journals/jcs/HuiL01, author = "Mei Lin Hui and Gavin Lowe", journal = "Journal of Computer Security", number = "1/2", pages = "3-46", title = "Fault-Preserving Simplifying Transformations for Security Protocols", url = "http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Security/Papers/simplifyJCS.ps", volume = "9", year = "2001", } @book{book/Lowe, author = "Peter Ryan and Steve Schneider and Michael Goldsmith and Gavin Lowe and Bill Roscoe", publisher = "Addison-Wesley", title = "Modelling and analysis of security protocols", year = "2001", } @article{journals/entcs/RoscoeBL00, author = "A. W. Roscoe and Philippa J. Broadfoot and Gavin Lowe", journal = "Electr. Notes Theor. Comput. Sci.", title = "Data independent verification of crypto-protocols", url = "http://www.elsevier.com/gej-ng/31/29/23/97/27/show/Products/notes/index.htt\#034", volume = "40", year = "2000", } @article{journals/entcs/RoscoeBL00I, author = "A. W. Roscoe and Philippa J. Broadfoot and Gavin Lowe", journal = "Electr. Notes Theor. Comput. Sci.", title = "Data independent verification of crypto-protocols", url = "http://www.elsevier.com/gej-ng/31/29/23/97/27/show/Products/notes/index.htt\#034", volume = "40", year = "2000", } @inproceedings{conf/esorics/BroadfootLR00, author = "Philippa J. Broadfoot and Gavin Lowe and A. W. Roscoe", booktitle = "Computer Security - ESORICS 2000, 6th European Symposium on Research in Computer Security, Toulouse, France, October 4-6, 2000, Proceedings", doi = "10.1007/10722599_11", editor = "Fr{\'e}d{\'e}ric Cuppens and Yves Deswarte and Dieter Gollmann and Michael Waidner", isbn = "3-540-41031-7", pages = "175-190", publisher = "Springer", series = "Lecture Notes in Computer Science", title = "Automating Data Independence", url = "http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Security/Papers/BLR_esorics00.ps", volume = "1895", year = "2000", } @inproceedings{conf/csfw/HeatherLS00, author = "James Heather and Gavin Lowe and Steve Schneider", booktitle = "CSFW", pages = "255-268", title = "How to Prevent Type Flaw Attacks on Security Protocols", url = "http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Security/Papers/typingJCS.ps", year = "2000", } @article{journals/jcs/Lowe99, author = "Gavin Lowe", journal = "Journal of Computer Security", number = "1", title = "Towards a Completeness Result for Model Checking of Security Protocols", url = "http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Security/Papers/completeness.ps", volume = "7", year = "1999", } @inproceedings{inproc/Donovan/99, author = "Ben Donovan and Paul Norris and Gavin Lowe", booktitle = "{Proceedings of the Workshop on Formal Methods and Security Protocols}", note = "Some of the {Casper} scripts are available here: \url{http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Security/Papers/prots.tar.gz}", title = "Analyzing a Library of Security Protocols using {Casper} and {FDR}", year = "1999", } @article{journals/dc/LoweD99, author = "Gavin Lowe and Jim Davies", journal = "Distributed Computing", number = "2-3", pages = "91-103", title = "Using CSP to Verify Sequential Consistency", url = "http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Papers/cache.ps.gz", volume = "12", year = "1999", } @inproceedings{conf/csfw/Lowe99, author = "Mei Lin Hui and Gavin Lowe", booktitle = "CSFW", pages = "32-43", title = "Safe Simplifying Transformations for Security Protocols", url = "http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Security/Papers/simplify.ps", year = "1999", } @article{journals/jcs/Lowe98, author = "Gavin Lowe", journal = "Journal of Computer Security", number = "1-2", pages = "53-84", title = "Casper: A Compiler for the Analysis of Security Protocols", url = "http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Security/Casper/casper.ps", volume = "6", year = "1998", } @inproceedings{conf/csfw/Lowe98, author = "Gavin Lowe", booktitle = "Computer Security Foundations Workshop", pages = "96-105", title = "Towards a Completeness Result for Model Checking of Security Protocols", url = "http://dlib.computer.org/conferen/csfw/8488/pdf/84880096.pdf", year = "1998", } @inproceedings{conf/csfw/GorrieriSAFGLM98, author = "Roberto Gorrieri and Paul F. Syverson and Mart\'{\i}n Abadi and Riccardo Focardi and Dieter Gollmann and Gavin Lowe and Catherine Meadows", booktitle = "Computer Security Foundations Workshop", pages = "79-82", title = "Panel Introduction: Varieties of Authentication", url = "http://dlib.computer.org/conferen/csfw/8488/pdf/84880079.pdf", year = "1998", } @article{journals/tse/LoweR97, author = "Gavin Lowe and A. W. Roscoe", journal = "IEEE Trans. Software Eng.", number = "10", pages = "659-669", title = "Using CSP to Detect Errors in the TMN Protocol", url = "http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Security/Papers/TMN.ps", volume = "23", year = "1997", } @inproceedings{conf/csfw/Lowe97a, author = "Gavin Lowe", booktitle = "10th Computer Security Foundations Workshop (CSFW '97), June 10-12, 1997, Rockport, Massachusetts, USA", pages = "31-44", publisher = "IEEE Computer Society", title = "A Hierarchy of Authentication Specification", url = "http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Security/Papers/authentication.ps", year = "1997", } @inproceedings{conf/csfw/Lowe97, author = "Gavin Lowe", booktitle = "10th Computer Security Foundations Workshop (CSFW '97), June 10-12, 1997, Rockport, Massachusetts, USA", pages = "18-30", publisher = "IEEE Computer Society", title = "Casper: A Compiler for the Analysis of Security Protocols", url = "http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Security/Casper/casper.ps", year = "1997", } @techreport{tr/Lowe1997/5, author = "Gavin Lowe", institution = "Department of Mathematics and Computer Science, University of Leicester", number = "1997/5", title = "A Family of Attacks upon Authentication Protocols", url = "http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Security/Papers/multiplicityTR.ps", year = "1997", } @article{journals/stp/Lowe96, author = "Gavin Lowe", journal = "Software - Concepts and Tools", number = "3", pages = "93-102", title = "Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR", url = "http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Security/Papers/NSFDR.ps", volume = "17", year = "1996", } @article{journals/scp/CurtisL96, author = "Sharon Curtis and Gavin Lowe", journal = "Sci. Comput. Program.", number = "1-3", pages = "197-216", title = "Proofs with Graphs", url = "http://cms.brookes.ac.uk/staff/SharonCurtis/publications/graphSCP.ps.gz", volume = "26", year = "1996", } @inproceedings{conf/tacas/Lowe96, author = "Gavin Lowe", booktitle = "Tools and Algorithms for Construction and Analysis of Systems, Second International Workshop, TACAS '96, Passau, Germany, March 27-29, 1996, Proceedings", editor = "Tiziana Margaria and Bernhard Steffen", isbn = "3-540-61042-1", pages = "147-166", publisher = "Springer", series = "Lecture Notes in Computer Science", title = "Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR", url = "http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Security/Papers/NSFDR.ps", volume = "1055", year = "1996", } @inproceedings{conf/csfw/Lowe96, author = "Gavin Lowe", booktitle = "Ninth IEEE Computer Security Foundations Workshop, March 10 - 12, 1996, Dromquinna Manor, Kenmare, County Kerry, Ireland", pages = "162-169", publisher = "IEEE Computer Society", title = "Some new attacks upon security protocols", url = "http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Security/Papers/attacks.ps", year = "1996", } @article{journals/tcs/Lowe95, author = "Gavin Lowe", doi = "10.1016/0304-3975(94)00171-E", journal = "Theor. Comput. Sci.", number = "2", pages = "315-352", title = "Probabilistic and Prioritized Models of Timed CSP", url = "http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Papers/Probs/MFPS.ps.gz", volume = "138", year = "1995", } @inproceedings{/inproc/mpc/Lowe95II, author = "Sharon Curtis and Gavin Lowe", booktitle = "{Mathematics of Program Construction}", publisher = "Lecture Notes in Computer Science", title = "A Graphical Calculus", url = "http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Papers/graph.ps.gz", volume = "947", year = "1995", } @article{journals/ipl/Lowe95, author = "Gavin Lowe", doi = "10.1016/0020-0190(95)00144-2", journal = "Information Processing Letters", number = "3", pages = "131-133", title = "An Attack on the Needham-Schroeder Public-Key Authentication Protocol", url = "http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Security/Papers/NSPKP.ps", volume = "56", year = "1995", } @article{journals/cj/Lowe95, author = "Gavin Lowe", journal = "The Computer Journal", number = "6", pages = "443-456", title = "Scheduling-Oriented Models for Real-Time Systems", url = "http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Papers/TAM/scheduling.ps.gz", volume = "38", year = "1995", } @article{journals/cj/LoweZ95, author = "Gavin Lowe and Hussein Zedan", journal = "The Computer Journal", number = "10", pages = "785-800", title = "Refinement of Complex Systems: A Case Study", url = "http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Papers/TAM/casestudy.ps.gz", volume = "38", year = "1995", } @phdthesis{/thesis/Lowe93, author = "Gavin Lowe", school = "Oxford University Computing Laboratory", title = "{Probabilities and Priorities in Timed CSP}", url = "http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Papers/Probs/thesis.ps.gz", year = "1993", }