Bill Roscoe - Home Page (original) (raw)

OXFORD UNIVERSITY COMPUTING LABORATORY
Publications:Notes on Domain Theory PDF A theory of communicating sequential processes, Oxford University Computing Laboratory technical monograph PRG-16, May 1981 (with S.D. Brookes and C. A. R. Hoare) PDF A mathematical theory of communicating processes, Oxford University D. Phil. thesis, 1982. PDF Please note this is a 270 page, 118 Mb scanned file and will take some time to download. Criteria for metrisability, Proc. Amer. Math. Soc. 90 (April 1984), 631-640 (with P.J. Collins) http A theory of communicating sequential processes, Journal of the ACM 31, No. 3 (July 1984), 560-599 (with S.D. Brookes and C.A.R. Hoare) PDF Programs as executable predicates, Proceedings of FGCS84 (ICOT, editors) 220-228 (with C.A.R. Hoare). PDF Continuous analogues of axiomatised digital surfaces, Computer Vision, Graphics and Image Processing 29 (January 1985), 60-86 (with T.Y. Kong). PDF A lattice of conditions on topological spaces, Proc. Amer. Math. Soc. 94 (July 1985), 487-496 (with P.J. Collins, G.M. Reed and M.E. Rudin) http Proceedings of the Pittsburgh seminar on concurrency, Springer LNCS 197 (1985) (co-editor with S.D. Brookes and G. Winskel). http An improved failures model for communicating processes, in Proceedings of the Pittsburgh seminar on concurrency, Springer LNCS 197 (1985), 281-305 (with S.D. Brookes). PDF Denotational semantics for occam, in Proceedings of the Pittsburgh seminar on concurrency, Springer LNCS 197 (1985), 306-329. PDF Deadlock analysis in networks of communicating processes, in Logics and Models of Concurrent Systems (ed. K.R. Apt) NATO ASI series F, Vol. 13, Springer 1985, 305-324 (with S.D. Brookes). Characterisations of simply-connected finite polyhedra in 3-space, Bull. London Math. Soc. 17 (November 1985), 575-578 (with T.Y. Kong). PDF A theory of binary digital pictures, Computer Vision, Graphics and Image Processing 32 (November 1985), 221-243 (with T.Y. Kong). PDF Specifying problem one using the failures model for CSP and deriving CSP processes which meet this specification, in The Analysis of Concurrent Systems (ed. B.T. Denvir et al), Springer LNCS 207 (1985), 103-109.PDF A CSP solution to the ``trains'' problem, in The Analysis of Concurrent Systems (ed. B.T. Denvir et al), Springer LNCS 207 (1985), 384-388.PDF Local symmetry and triangle laws are sufficient for metrisability, Colloquia Mathematica Societatis Janos Bolyai 41, 177-181 (with P.J. Collins). PDF A timed model for communicating sequential processes, Proc.ICALP 86, Springer LNCS 226 (1986), 314-323 (with G.M. Reed).PDF The pursuit of deadlock freedom, Information and Computation 75, 3 (December 1987), 289-327 (with Naiem Dathi). PS Metric spaces as models for real-time concurrency, in Main et al, eds. Proceedings of the Third Workshop on the Mathematical Foundations of Programming Language Semantics (New Orleans, 1987) Springer LNCS 298 (1988), 331-343 (with G.M. Reed).PDF Laws of programming, Communications of the ACM 30, 8 (August 1987), 672-686 (with C.A.R. Hoare, He Jifeng, I.J. Hayes, C.C. Morgan, J.W. Sanders, I.H. Sorensen, J.M. Spivey and B.A. Sufrin). (Previously appeared as Oxford University Computing Laboratory Technical Report PRG-42.) PDF Routing messages through networks: an exercise in deadlock avoidance, in Muntean ed. et al. Programming of Transputer Based Machines: Proceedings of {7}th occam User Group Technical Meeting, (14-16 September 1987, Grenoble, France), IOS B.V., Amsterdam. PS Transforming occam programs, in The Design and Application of Parallel Digital Processors (IEE Conference Publication 298) (1988) (with M.H. Goldsmith). PDF A timed model for communicating sequential processes, Theoretical Computer Science 58 (1988), 249-261 (with G.M. Reed). PDF The laws of occam programming, Theoretical Computer Science 60 (1988), 177-229 (with C.A.R. Hoare). (Previously appeared as Oxford University Computing Laboratory Technical Report PRG-53, 1986.) PDF The decomposition of a rectangle into rectangles of minimal perimeter, University of Maryland Center for Automation Research CAR-TR-169 (1986) (with T.Y. Kong and D.M. Mount) (Also SIAM Journal of Computing 17, 6 pp1215-1231.) PDF An Operational Semantics for CSP (with S. D. Brookes and D. J. Walker) Technical Report 1986 PS An alternative order for the failures model, in `Two papers on CSP', technical monograph PRG-67, Oxford University Computing Laboratory, July 1988. Also appeared in Journal of Logic and Computation 2, 5 pp557-577. PS _Unbounded nondeterminism in CSP_, in `Two papers on CSP', technical monograph PRG-67, Oxford University Computing Laboratory, July 1988. Also Journal of Logic and Computation, Vol 3, No 2 pp131-172 (1993). PS Unbounded nondeterminism in CSP (with G.Barrett), in the Proceedings of MFPS89 (Springer LNCS 298). PS PDF Deadlock analysis in networks of communicating processes(with S.D. Brookes) Distributed Computing (1991) 4 209-230.PDF A lattice of conditions on topological spaces II(with P. Moody, G.M. Reed and P.J. Collins) Fundamenta Mathematicae 138 (1991) pp69-81 PDF The point-countable base problem, (with P.J. Collins and G.M. Reed) in `Problems in Topology' (G.M. Reed and J. van Mill, eds) Elsevier 1990.PDF _Maintaining consistency in distributed databases_, Technical Monograph PRG-87, Oxford University Computing Laboratory (1990).PS _Communication and correctness in Timed CSP_, (with S.A. Schneider, J.W. Davies, D.M. Jackson, and G.M. Reed), Technical Report to Esprit SPEC project, 1990. _A temporal logic for Timed CSP_ (with D.M. Jackson, J.W. Davies, G.M. Reed, and S.A. Schneider), Technical Report to Esprit SPEC project, 1990. _Topology, computer science and the mathematics of convergence_, in Topology and Category Theory in Computer Science (Reed, Roscoe, Wachter, eds) OUP 1991. PS _Topology and category theory in computer science,_ (co-edited with G.M. Reed and R.F. Wachter) OUP 1991, (proceedings of a special session at the 1989 Oxford Topology Conference). _Analysing TMFS: a study of nondeterminism in real-time concurrency_ (with G.M. Reed), in Concurrency: Theory Language and Architecture, (Yonezawa and Ito, eds) Springer LNCS 491. PS _CSP and timewise refinement_ (with G. M. Reed and S. A. Schneider), Proceedings of the BCS-FACS Refinement Workshop (Cambridge, 1991), LNCS. _Star covering properties_ (with E.K. van Douwen, G.M. Reed and I.J. Tree) Topology and its Applications 39 (1991) 71-103. PDF _Formal methods in the development of the H1 Transputer_(with A.D.B. Cox, M.H. Goldsmith and J.B. Scattergood), in Proceedings of Transputing 91 (IOS). _Concepts of digital topology_ (with T.Y. Kong) Topology and its applications 46 (1992) 219-262. PDF _Timed CSP: theory and practice_ (with J.Davies, D.Jackson, G.M.Reed, J.Reed and S.A. Schneider), Proceedings of REX Workshop, LNCS 600 (1992). _Acyclic monotone normality_ (with P. Moody), Topology and its Applications 47 (1992) 53-67. PDF _Occam in the specification and verification of microprocessors_Phil Trans R. Soc. Lond A (1992) 339, 137-151. Also in Mechanised Reasoning and Hardware Design, M.J.C. Gordon and C.A.R. Hoare, eds (Prentice-Hall, 1992). Original paper httpExtended Version PS _A semantic model for occam II_ (with M.H. Goldsmith and B.G.O. Scott) Proceedings of Transputing 93. _Denotational semantics for occam II_ (with M.H. Goldsmith and B.G.O. Scott) Oxford University Computing Laboratory Technical monograph PRG-108 (1993).PDF _Developing and verifying protocols in CSP_, Proceedings of Mierlo workshop on protocols, published by TU Eindhoven. _Fixed points without completeness_ (with M.W. Mislove and S.A. Schneider), Theoretical Computer Science 138, 2 pp273-314. _Model-checking CSP_, In _A Classical Mind: essays in Honour of C.A.R. Hoare_, Prentice-Hall 1994. PS _A Classical Mind: essays in Honour of C.A.R. Hoare_, Prentice-Hall 1994 (editor). _Denotational semantics for occam2, Part 1_ ( with M.H. Goldsmith and B.G.O. Scott) Transputer Communications 1, 2 pp65-91. _Denotational semantics for occam2, Part 2_(with M.H. Goldsmith and B.G.O. Scott) Transputer Communications 2. 1 pp25-67. _Non-interference through determinism_ (with J.C.P. Woodcock and L Wulf) in proceedings of ESORICS 94 (LNCS 875).PDF _Non-interference through determinism_ (with J.C.P. Woodcock and L Wulf) (revised version of above) Journal of Computer Security 4, 1 (pp27--54), 1996.PDF _CSP and determinism in security modelling_ Proceedings of 1995 IEEE Symposium on Security and Privacy (IEEE Computer Society Press) PS _Composing and decomposing systems under security properties_ (with L. Wulf) Proceedings of 1995 IEEE Computer Security Foundations Workshop (IEEE Computer Society Press) PS _Modelling and verifying key-exchange protocols using CSP and FDR_Proceedings of 1995 IEEE Computer Security Foundations Workshop (IEEE Computer Society Press) PS _Hierarchical compression for model-checking CSP, or How to check 1020 dining philosophers for deadlock_(with P.H.B. Gardiner, M.H. Goldsmith, J.R. Hulance, D.M.Jackson and J.B. Scattergood) In proceedings of TACAS 1995 (BRICS; also, revised, in a version of these proceedings published by LNCS) PS PDF _The timed failures-stability model for Timed CSP_(with G.M. Reed) Oxford University Computing Laboratory Technical Monograph PRG-119 (1996)`, also appeared in Theoretical Computer Science, Vol 211 (1999).PS PDF _Intensional specifications of security protocols_Proceedings of 1996 IEEE Computer Security Foundations Workshop (IEEE Computer Society Press) PS On transition systems and non-well-founded sets, (with R.S. Lazic) Annals of the New York Academiy of Sciences Vol 806, 1996. PS PDF The perfect spy for model-checking crypto-protocols, (with M.H. Goldsmith)} Proceedings of DIMACS workshop on the design and formal verification of crypto-protocols, 1997. (http://dimacs.rutgers.edu/workshops/program2/program.html)[ PDF](/oucl/work/bill.roscoe/publications/63.pdf) A Case Study of the Formal Specification of a Parallel System using CSP, (with S. Kiyamura) in "Correct Models of Parallel Computing"' (S. Noguchi and M. Ota, eds), IOS Press 1997 Using CSP to detect errors in the TMN protocol (with G. Lowe) University of Leicester Technical Report (1996) and IEEE transactions on Software Engineering Vol 23 (1997) PS Verifying Determinism of Concurrent Systems Which Use Unbounded Arrays, (with R. Lazic) Proceedings of INFINITY'98, Aalborg, Denmark, July 1998, extended version as Oxford University Computing Laboratory TR-2-98. PS (66a) Extended Abstract as aboveps file _Proving security protocols with model checkers by data independence techniques_Proceedings of CSFW 1998, IEEE Press. PS PDF The theory and practice of concurrency, Prentice Hall, 1998, ISBN 0-13-6774409-5, pp. xv+565.amended 2005 PS PDF What is intransitive noninterference? Proceedings of CSFW 1999, IEEE Press. (with M.H. Goldsmith) PS Proving security protocols with model checkers by data independence techniques, (with P.J. Broadfoot) Journal of Computer Security Vol 7 (1999) PS PDF Data independence with predicate symbols, (with R.S. Lazic) Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA'99), June 28 - July 1 1999, Las Vegas, Nevada, USA. Volume I. Published by CSREA Press. PS Verifying an infinite family of inductions simultaneously using data independence and FDR, (with S.J. Creese) In Formal Methods for Protocol Engineering and Distributed Systems, the proceedings of Formal Description Techniques for Distributed Systems and Communication Protocols and Protocol Specification, Testing and Verification (FORTE/PSTV'99), October 5-8 1999, Beijing, China. Published by Kluwer Academic Publishers. PS PDF Formal Verification of Arbitrary Network Topologies, (with S.J. Creese) Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA'99), June 28 - July 1 1999, Las Vegas, Nevada, USA. Volume II. Published by CSREA Press. PS PDF TTP: A case study in combining induction and data independence, (with S.J. Creese) Oxford University Computing Laboratory Technical Report, PRG-TR-1-99. PS Data independent induction over structured networks, (with S.J. Creese) Proceedings of PDPTA2000 PS Automating Data Independence, (with P.J. Broadfoot and G. Lowe) Proceedings of ESORICS2000, LNCS 1895. PS PDF Millennial Perspectives in Computer Science, (jointly edited with J. Davies and J. Woodcock), Palgrave 2000. The successes and failures of behavioural models(with R. Forster and G.M. Reed), in Millennial Perspectives in Computer Science, Palgrave 2000. PS PDF The Modelling and Analysis of Security Protocols, (with P. Ryan, S. Schneider, M. Goldsmith, G. Lowe) Addison-Wesley, 2001. On Model Checking Data-independent Systems with Arrays without Reset(abstract), (with R. S. Lazic and T. C. Newcomb), Proceedings of VCL 2001. PS What can you Decide about Resetable Arrays? , (with R. S. Lazic), Proceedings of VCL 2001. PS Compiling Shared Variable Programs into CSP, Proceedings of PROGRESS workshop 2001. PS Internalising Agents in CSP Protocol Models (Extended Abstract), (with P. J. Broadfoot) Proceedings of WITS 2002, Portland PS Capturing parallel attacks within the data independence framework, (with P. J. Broadfoot) Proceedings of CSFW 15 (IEEE Press, 2002) PS On Model Checking Data-independent Systems with Arrays without Reset, (with R. S. Lazic and T. C. Newcomb), Theory and Practice of Logic Programming 4(5 & 6), 659-693, 2004. PS PDF Embedding agents within the intruder to detect parallel attacks, (with P.J. Broadfoot) the Journal of Computer Security, vol 12 (3-4), 379-408, 2004. PS PDF Authentication in pervasive computing, (with S.J. Creese, M.H. Goldsmith and I.Zakiuddin), Proceedings of First International Conference on Pervasive Computing (March 2003), LNCS. PS Bisimulation and refinement reconciled, (with C.A.R. Hoare, C. Fournet, P.H.B. Gardiner, R. Milner, S.Rajamani and J. Rehof), Microsoft Technical Report, 2003. On the expressive power of CSP refinement, Preliminary version in Proceedings of AVoCS03, Southampton University Technical Report, April 2003, Formal Aspects of Computing, 17 (2), 93-112. PDF PS Polymorphic systems with arrays: decidability and undecidability(Extended abstract), (with R. S. Lazic and T. C. Newcomb), Proceedings of South-East Europe Workshop on Formal Methods, August 2003. PDF Watchdog transformations for property-oriented model checking(with M.H. Goldsmith, N.Moffat, T. Whitworth and I. Zakiuddin), in Proceedings of FME 2003. PDF The attacker in ubiquitous computing environments: formalising the threat model, (with S.J. Creese, M.H. Goldsmith and I.Zakiuddin), Proceedings of FAST 2003, Pisa. PDF Translating CSP trace refinement to UNITY unreachability : a study in data independence(with Xu Wang and R.S. Lazic), OUCL Research Report RR-03-08, April 2003. PS _Compiling Statemate Statecharts into CSP and verifying them using FDR_Extended Abstract January 2003 PS Seeing beyond divergence June 22, 2004. Communicating Sequential Processes, the first 25 years, Springer LNCS 3525,2005.. PS PDF _Finitary refinement checks for infinitary specifications_June 2004. Proceedings of CPA 2004. PDF Research directions for trust and security in human-centric computing, (with Sadie Creese, Michael Goldsmith and Irfan Zakiuddin) Proceedings of SPPC 2004. PDF Responsiveness of Interoperating Components, (with J. N. Reed and J. E. Sinclair) in FAC vol 16, pp 394-411 (2004). PS PDF Relating Data Independent Trace Checks in CSP with UNITY Reachability under a Normality Assumption, (with Xu Wang and R. S. Lazic), Proceedings of IFM 2004, Springer LNCS 2999 (2004). PDF Web Services Security: a preliminary study using Casper and FDR, (with E. Kleiner) In Proceedings of Automated Reasoning for Security Protocol Analysis (ARSPA 04), Cork, Ireland. PS PDF Polymorphic Systems with Arrays, 2-Counter Machines and Multiset Rewriting, (with R. S. Lazic and Tom Newcomb) Proceedings of INFINITY 2004. PS PDF On Model checking data-independent systems with arrays with whole-array operations, (with R. S. Lazic and Tom Newcomb) Communicating Sequential Processes Springer LNCS 3525,2005 PDF Exploiting Empirical Engagement in Authentication Protocol Design, (with Sadie Creese, Michael Goldsmith, Richard Harrison, Paul Whittaker and Irfan Zakiuddin) Proceedings of SPPC 2005 PDF On the relationship between Web Services Security and traditional protocols, (with Eldar Kleiner) to appear in the Proceedings of MFPS 2005 PS PDF Revivals,stuckness and the hierarchy of CSP Models, December 2007 (revision of 2005 draft) PDF The pursuit of buffer tolerance, May 2005, unpublished draft PS PDF Confluence thanks to extensional determinism, May 2005, In Proceedings of Bertinoro meeting on Concurrency, BRICS 2005. Revised version, publication reference ENTCS 1336, 2006 PDF Security and trust for ubiquitous communication, (with Sadie Creese, Mike Reed and Jeff Sanders) prepared for the ITU WSIS Thematic Meeting on Cybersecurity, Geneva, Switzerland June 2005 PDF Machine-Verifiable Responsiveness, (with J. N Reed and J. E Sinclair) Proceedings of AVOCS 2005 PDF Extending noninterference properties to the timed world,(with Jian Huang) To appear in the proceedings of SAC 2006PDF Bootstrapping Multi-Party Ad-Hoc Security,(with S. J. Creese, M. H. Goldsmith and Ming Xiao) To appear in the proceedings of SAC 2006, PDF A taxonomy of web services in CSP, (with A. Martin and L. Momtahan) Proceedings of Web Languages and Formal Methods 2005 PDF Human-centred computer security, Unpublished draft PDF Modelling unbounded parallel sessions of security protocols in CSP with E. Kleiner PDF Verifying Statemate Statecharts Using CSP and FDR with Zhenzhong Wu. To appear in the proceedings of ICFEM 2006PDF and scripts PDF PDF Efficient group authentication protocols based on human interaction. Proceedings of ARSPA 2006 (with L. H. Nguyen) PDF Responsiveness and stable revivals. (with J. N. Reed and J. E. Sinclair) In Formal Aspects of Computing Volume 19, Number 3, August 2007 PDF Nets with Tokens Which Carry Data. (with Ranko Lazic, Tom Newcomb, Joel Ouaknine and James Worrell) LNCS 3349 2007 PDF SVA, a tool for analysing shared-variable programms. (with David Hopkins) To appear in the proceedings of AVoCS 2007 pages 177 - 183 PDF Authenticating ad hoc networks by comparison of short digests. (with L. H. Nguyen) To appear in Information and Computation PDF For copies of papers marked HC please contact elizabeth.walsh@comlab.ox.ac.uk or sue.taylor@comlab.ox.ac.ukwith address details and a copy will be posted to you.

OXFORD UNIVERSITY COMPUTING LABORATORY

Publications:Notes on Domain Theory PDF A theory of communicating sequential processes, Oxford University Computing Laboratory technical monograph PRG-16, May 1981 (with S.D. Brookes and C. A. R. Hoare) PDF A mathematical theory of communicating processes, Oxford University D. Phil. thesis, 1982. PDF Please note this is a 270 page, 118 Mb scanned file and will take some time to download. Criteria for metrisability, Proc. Amer. Math. Soc. 90 (April 1984), 631-640 (with P.J. Collins) http A theory of communicating sequential processes, Journal of the ACM 31, No. 3 (July 1984), 560-599 (with S.D. Brookes and C.A.R. Hoare) PDF Programs as executable predicates, Proceedings of FGCS84 (ICOT, editors) 220-228 (with C.A.R. Hoare). PDF Continuous analogues of axiomatised digital surfaces, Computer Vision, Graphics and Image Processing 29 (January 1985), 60-86 (with T.Y. Kong). PDF A lattice of conditions on topological spaces, Proc. Amer. Math. Soc. 94 (July 1985), 487-496 (with P.J. Collins, G.M. Reed and M.E. Rudin) http Proceedings of the Pittsburgh seminar on concurrency, Springer LNCS 197 (1985) (co-editor with S.D. Brookes and G. Winskel). http An improved failures model for communicating processes, in Proceedings of the Pittsburgh seminar on concurrency, Springer LNCS 197 (1985), 281-305 (with S.D. Brookes). PDF Denotational semantics for occam, in Proceedings of the Pittsburgh seminar on concurrency, Springer LNCS 197 (1985), 306-329. PDF Deadlock analysis in networks of communicating processes, in Logics and Models of Concurrent Systems (ed. K.R. Apt) NATO ASI series F, Vol. 13, Springer 1985, 305-324 (with S.D. Brookes). Characterisations of simply-connected finite polyhedra in 3-space, Bull. London Math. Soc. 17 (November 1985), 575-578 (with T.Y. Kong). PDF A theory of binary digital pictures, Computer Vision, Graphics and Image Processing 32 (November 1985), 221-243 (with T.Y. Kong). PDF Specifying problem one using the failures model for CSP and deriving CSP processes which meet this specification, in The Analysis of Concurrent Systems (ed. B.T. Denvir et al), Springer LNCS 207 (1985), 103-109.PDF A CSP solution to the ``trains'' problem, in The Analysis of Concurrent Systems (ed. B.T. Denvir et al), Springer LNCS 207 (1985), 384-388.PDF Local symmetry and triangle laws are sufficient for metrisability, Colloquia Mathematica Societatis Janos Bolyai 41, 177-181 (with P.J. Collins). PDF A timed model for communicating sequential processes, Proc.ICALP 86, Springer LNCS 226 (1986), 314-323 (with G.M. Reed).PDF The pursuit of deadlock freedom, Information and Computation 75, 3 (December 1987), 289-327 (with Naiem Dathi). PS Metric spaces as models for real-time concurrency, in Main et al, eds. Proceedings of the Third Workshop on the Mathematical Foundations of Programming Language Semantics (New Orleans, 1987) Springer LNCS 298 (1988), 331-343 (with G.M. Reed).PDF Laws of programming, Communications of the ACM 30, 8 (August 1987), 672-686 (with C.A.R. Hoare, He Jifeng, I.J. Hayes, C.C. Morgan, J.W. Sanders, I.H. Sorensen, J.M. Spivey and B.A. Sufrin). (Previously appeared as Oxford University Computing Laboratory Technical Report PRG-42.) PDF Routing messages through networks: an exercise in deadlock avoidance, in Muntean ed. et al. Programming of Transputer Based Machines: Proceedings of {7}th occam User Group Technical Meeting, (14-16 September 1987, Grenoble, France), IOS B.V., Amsterdam. PS Transforming occam programs, in The Design and Application of Parallel Digital Processors (IEE Conference Publication 298) (1988) (with M.H. Goldsmith). PDF A timed model for communicating sequential processes, Theoretical Computer Science 58 (1988), 249-261 (with G.M. Reed). PDF The laws of occam programming, Theoretical Computer Science 60 (1988), 177-229 (with C.A.R. Hoare). (Previously appeared as Oxford University Computing Laboratory Technical Report PRG-53, 1986.) PDF The decomposition of a rectangle into rectangles of minimal perimeter, University of Maryland Center for Automation Research CAR-TR-169 (1986) (with T.Y. Kong and D.M. Mount) (Also SIAM Journal of Computing 17, 6 pp1215-1231.) PDF An Operational Semantics for CSP (with S. D. Brookes and D. J. Walker) Technical Report 1986 PS An alternative order for the failures model, in `Two papers on CSP', technical monograph PRG-67, Oxford University Computing Laboratory, July 1988. Also appeared in Journal of Logic and Computation 2, 5 pp557-577. PS _Unbounded nondeterminism in CSP_, in `Two papers on CSP', technical monograph PRG-67, Oxford University Computing Laboratory, July 1988. Also Journal of Logic and Computation, Vol 3, No 2 pp131-172 (1993). PS Unbounded nondeterminism in CSP (with G.Barrett), in the Proceedings of MFPS89 (Springer LNCS 298). PS PDF Deadlock analysis in networks of communicating processes(with S.D. Brookes) Distributed Computing (1991) 4 209-230.PDF A lattice of conditions on topological spaces II(with P. Moody, G.M. Reed and P.J. Collins) Fundamenta Mathematicae 138 (1991) pp69-81 PDF The point-countable base problem, (with P.J. Collins and G.M. Reed) in `Problems in Topology' (G.M. Reed and J. van Mill, eds) Elsevier 1990.PDF _Maintaining consistency in distributed databases_, Technical Monograph PRG-87, Oxford University Computing Laboratory (1990).PS _Communication and correctness in Timed CSP_, (with S.A. Schneider, J.W. Davies, D.M. Jackson, and G.M. Reed), Technical Report to Esprit SPEC project, 1990. _A temporal logic for Timed CSP_ (with D.M. Jackson, J.W. Davies, G.M. Reed, and S.A. Schneider), Technical Report to Esprit SPEC project, 1990. _Topology, computer science and the mathematics of convergence_, in Topology and Category Theory in Computer Science (Reed, Roscoe, Wachter, eds) OUP 1991. PS _Topology and category theory in computer science,_ (co-edited with G.M. Reed and R.F. Wachter) OUP 1991, (proceedings of a special session at the 1989 Oxford Topology Conference). _Analysing TMFS: a study of nondeterminism in real-time concurrency_ (with G.M. Reed), in Concurrency: Theory Language and Architecture, (Yonezawa and Ito, eds) Springer LNCS 491. PS _CSP and timewise refinement_ (with G. M. Reed and S. A. Schneider), Proceedings of the BCS-FACS Refinement Workshop (Cambridge, 1991), LNCS. _Star covering properties_ (with E.K. van Douwen, G.M. Reed and I.J. Tree) Topology and its Applications **39** (1991) 71-103. PDF _Formal methods in the development of the H1 Transputer_(with A.D.B. Cox, M.H. Goldsmith and J.B. Scattergood), in Proceedings of Transputing 91 (IOS). _Concepts of digital topology_ (with T.Y. Kong) Topology and its applications **46** (1992) 219-262. PDF _Timed CSP: theory and practice_ (with J.Davies, D.Jackson, G.M.Reed, J.Reed and S.A. Schneider), Proceedings of REX Workshop, LNCS 600 (1992). _Acyclic monotone normality_ (with P. Moody), Topology and its Applications **47** (1992) 53-67. PDF _Occam in the specification and verification of microprocessors_Phil Trans R. Soc. Lond A (1992) **339**, 137-151. Also in Mechanised Reasoning and Hardware Design, M.J.C. Gordon and C.A.R. Hoare, eds (Prentice-Hall, 1992). Original paper httpExtended Version PS _A semantic model for occam II_ (with M.H. Goldsmith and B.G.O. Scott) Proceedings of Transputing 93. _Denotational semantics for occam II_ (with M.H. Goldsmith and B.G.O. Scott) Oxford University Computing Laboratory Technical monograph PRG-108 (1993).PDF _Developing and verifying protocols in CSP_, Proceedings of Mierlo workshop on protocols, published by TU Eindhoven. _Fixed points without completeness_ (with M.W. Mislove and S.A. Schneider), Theoretical Computer Science **138**, 2 pp273-314. _Model-checking CSP_, In _A Classical Mind: essays in Honour of C.A.R. Hoare_, Prentice-Hall 1994. PS _A Classical Mind: essays in Honour of C.A.R. Hoare_, Prentice-Hall 1994 (editor). _Denotational semantics for occam2, Part 1_ ( with M.H. Goldsmith and B.G.O. Scott) Transputer Communications **1**, 2 pp65-91. _Denotational semantics for occam2, Part 2_(with M.H. Goldsmith and B.G.O. Scott) Transputer Communications **2**. 1 pp25-67. _Non-interference through determinism_ (with J.C.P. Woodcock and L Wulf) in proceedings of ESORICS 94 (LNCS 875).PDF _Non-interference through determinism_ (with J.C.P. Woodcock and L Wulf) (revised version of above) Journal of Computer Security **4**, 1 (pp27--54), 1996.PDF _CSP and determinism in security modelling_ Proceedings of 1995 IEEE Symposium on Security and Privacy (IEEE Computer Society Press) PS _Composing and decomposing systems under security properties_ (with L. Wulf) Proceedings of 1995 IEEE Computer Security Foundations Workshop (IEEE Computer Society Press) PS _Modelling and verifying key-exchange protocols using CSP and FDR_Proceedings of 1995 IEEE Computer Security Foundations Workshop (IEEE Computer Society Press) PS _Hierarchical compression for model-checking CSP, or How to check 1020 dining philosophers for deadlock_(with P.H.B. Gardiner, M.H. Goldsmith, J.R. Hulance, D.M.Jackson and J.B. Scattergood) In proceedings of TACAS 1995 (BRICS; also, revised, in a version of these proceedings published by LNCS) PS PDF _The timed failures-stability model for Timed CSP_(with G.M. Reed) Oxford University Computing Laboratory Technical Monograph PRG-119 (1996)`, also appeared in Theoretical Computer Science, Vol 211 (1999).PS PDF _Intensional specifications of security protocols_Proceedings of 1996 IEEE Computer Security Foundations Workshop (IEEE Computer Society Press) PS On transition systems and non-well-founded sets, (with R.S. Lazic) Annals of the New York Academiy of Sciences Vol 806, 1996. PS PDF The perfect spy for model-checking crypto-protocols, (with M.H. Goldsmith)} Proceedings of DIMACS workshop on the design and formal verification of crypto-protocols, 1997. (http://dimacs.rutgers.edu/workshops/program2/program.html)[ PDF](/oucl/work/bill.roscoe/publications/63.pdf) A Case Study of the Formal Specification of a Parallel System using CSP, (with S. Kiyamura) in "Correct Models of Parallel Computing"' (S. Noguchi and M. Ota, eds), IOS Press 1997 Using CSP to detect errors in the TMN protocol (with G. Lowe) University of Leicester Technical Report (1996) and IEEE transactions on Software Engineering Vol 23 (1997) PS Verifying Determinism of Concurrent Systems Which Use Unbounded Arrays, (with R. Lazic) Proceedings of INFINITY'98, Aalborg, Denmark, July 1998, extended version as Oxford University Computing Laboratory TR-2-98. PS (66a) Extended Abstract as aboveps file _Proving security protocols with model checkers by data independence techniques_Proceedings of CSFW 1998, IEEE Press. PS PDF The theory and practice of concurrency, Prentice Hall, 1998, ISBN 0-13-6774409-5, pp. xv+565.amended 2005 PS PDF What is intransitive noninterference? Proceedings of CSFW 1999, IEEE Press. (with M.H. Goldsmith) PS Proving security protocols with model checkers by data independence techniques, (with P.J. Broadfoot) Journal of Computer Security Vol 7 (1999) PS PDF Data independence with predicate symbols, (with R.S. Lazic) Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA'99), June 28 - July 1 1999, Las Vegas, Nevada, USA. Volume I. Published by CSREA Press. PS Verifying an infinite family of inductions simultaneously using data independence and FDR, (with S.J. Creese) In Formal Methods for Protocol Engineering and Distributed Systems, the proceedings of Formal Description Techniques for Distributed Systems and Communication Protocols and Protocol Specification, Testing and Verification (FORTE/PSTV'99), October 5-8 1999, Beijing, China. Published by Kluwer Academic Publishers. PS PDF Formal Verification of Arbitrary Network Topologies, (with S.J. Creese) Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA'99), June 28 - July 1 1999, Las Vegas, Nevada, USA. Volume II. Published by CSREA Press. PS PDF TTP: A case study in combining induction and data independence, (with S.J. Creese) Oxford University Computing Laboratory Technical Report, PRG-TR-1-99. PS Data independent induction over structured networks, (with S.J. Creese) Proceedings of PDPTA2000 PS Automating Data Independence, (with P.J. Broadfoot and G. Lowe) Proceedings of ESORICS2000, LNCS 1895. PS PDF Millennial Perspectives in Computer Science, (jointly edited with J. Davies and J. Woodcock), Palgrave 2000. The successes and failures of behavioural models(with R. Forster and G.M. Reed), in Millennial Perspectives in Computer Science, Palgrave 2000. PS PDF The Modelling and Analysis of Security Protocols, (with P. Ryan, S. Schneider, M. Goldsmith, G. Lowe) Addison-Wesley, 2001. On Model Checking Data-independent Systems with Arrays without Reset(abstract), (with R. S. Lazic and T. C. Newcomb), Proceedings of VCL 2001. PS What can you Decide about Resetable Arrays? , (with R. S. Lazic), Proceedings of VCL 2001. PS Compiling Shared Variable Programs into CSP, Proceedings of PROGRESS workshop 2001. PS Internalising Agents in CSP Protocol Models (Extended Abstract), (with P. J. Broadfoot) Proceedings of WITS 2002, Portland PS Capturing parallel attacks within the data independence framework, (with P. J. Broadfoot) Proceedings of CSFW 15 (IEEE Press, 2002) PS On Model Checking Data-independent Systems with Arrays without Reset, (with R. S. Lazic and T. C. Newcomb), Theory and Practice of Logic Programming 4(5 & 6), 659-693, 2004. PS PDF Embedding agents within the intruder to detect parallel attacks, (with P.J. Broadfoot) the Journal of Computer Security, vol 12 (3-4), 379-408, 2004. PS PDF Authentication in pervasive computing, (with S.J. Creese, M.H. Goldsmith and I.Zakiuddin), Proceedings of First International Conference on Pervasive Computing (March 2003), LNCS. PS Bisimulation and refinement reconciled, (with C.A.R. Hoare, C. Fournet, P.H.B. Gardiner, R. Milner, S.Rajamani and J. Rehof), Microsoft Technical Report, 2003. On the expressive power of CSP refinement, Preliminary version in Proceedings of AVoCS03, Southampton University Technical Report, April 2003, Formal Aspects of Computing, 17 (2), 93-112. PDF PS Polymorphic systems with arrays: decidability and undecidability(Extended abstract), (with R. S. Lazic and T. C. Newcomb), Proceedings of South-East Europe Workshop on Formal Methods, August 2003. PDF Watchdog transformations for property-oriented model checking(with M.H. Goldsmith, N.Moffat, T. Whitworth and I. Zakiuddin), in Proceedings of FME 2003. PDF The attacker in ubiquitous computing environments: formalising the threat model, (with S.J. Creese, M.H. Goldsmith and I.Zakiuddin), Proceedings of FAST 2003, Pisa. PDF Translating CSP trace refinement to UNITY unreachability : a study in data independence(with Xu Wang and R.S. Lazic), OUCL Research Report RR-03-08, April 2003. PS _Compiling Statemate Statecharts into CSP and verifying them using FDR_Extended Abstract January 2003 PS Seeing beyond divergence June 22, 2004. Communicating Sequential Processes, the first 25 years, Springer LNCS 3525,2005.. PS PDF _Finitary refinement checks for infinitary specifications_June 2004. Proceedings of CPA 2004. PDF Research directions for trust and security in human-centric computing, (with Sadie Creese, Michael Goldsmith and Irfan Zakiuddin) Proceedings of SPPC 2004. PDF Responsiveness of Interoperating Components, (with J. N. Reed and J. E. Sinclair) in FAC vol 16, pp 394-411 (2004). PS PDF Relating Data Independent Trace Checks in CSP with UNITY Reachability under a Normality Assumption, (with Xu Wang and R. S. Lazic), Proceedings of IFM 2004, Springer LNCS 2999 (2004). PDF Web Services Security: a preliminary study using Casper and FDR, (with E. Kleiner) In Proceedings of Automated Reasoning for Security Protocol Analysis (ARSPA 04), Cork, Ireland. PS PDF Polymorphic Systems with Arrays, 2-Counter Machines and Multiset Rewriting, (with R. S. Lazic and Tom Newcomb) Proceedings of INFINITY 2004. PS PDF On Model checking data-independent systems with arrays with whole-array operations, (with R. S. Lazic and Tom Newcomb) Communicating Sequential Processes Springer LNCS 3525,2005 PDF Exploiting Empirical Engagement in Authentication Protocol Design, (with Sadie Creese, Michael Goldsmith, Richard Harrison, Paul Whittaker and Irfan Zakiuddin) Proceedings of SPPC 2005 PDF On the relationship between Web Services Security and traditional protocols, (with Eldar Kleiner) to appear in the Proceedings of MFPS 2005 PS PDF Revivals,stuckness and the hierarchy of CSP Models, December 2007 (revision of 2005 draft) PDF The pursuit of buffer tolerance, May 2005, unpublished draft PS PDF Confluence thanks to extensional determinism, May 2005, In Proceedings of Bertinoro meeting on Concurrency, BRICS 2005. Revised version, publication reference ENTCS 1336, 2006 PDF Security and trust for ubiquitous communication, (with Sadie Creese, Mike Reed and Jeff Sanders) prepared for the ITU WSIS Thematic Meeting on Cybersecurity, Geneva, Switzerland June 2005 PDF Machine-Verifiable Responsiveness, (with J. N Reed and J. E Sinclair) Proceedings of AVOCS 2005 PDF Extending noninterference properties to the timed world,(with Jian Huang) To appear in the proceedings of SAC 2006PDF Bootstrapping Multi-Party Ad-Hoc Security,(with S. J. Creese, M. H. Goldsmith and Ming Xiao) To appear in the proceedings of SAC 2006, PDF A taxonomy of web services in CSP, (with A. Martin and L. Momtahan) Proceedings of Web Languages and Formal Methods 2005 PDF Human-centred computer security, Unpublished draft PDF Modelling unbounded parallel sessions of security protocols in CSP with E. Kleiner PDF Verifying Statemate Statecharts Using CSP and FDR with Zhenzhong Wu. To appear in the proceedings of ICFEM 2006PDF and scripts PDF PDF Efficient group authentication protocols based on human interaction. Proceedings of ARSPA 2006 (with L. H. Nguyen) PDF Responsiveness and stable revivals. (with J. N. Reed and J. E. Sinclair) In Formal Aspects of Computing Volume 19, Number 3, August 2007 PDF Nets with Tokens Which Carry Data. (with Ranko Lazic, Tom Newcomb, Joel Ouaknine and James Worrell) LNCS 3349 2007 PDF SVA, a tool for analysing shared-variable programms. (with David Hopkins) To appear in the proceedings of AVoCS 2007 pages 177 - 183 PDF Authenticating ad hoc networks by comparison of short digests. (with L. H. Nguyen) To appear in Information and Computation PDF For copies of papers marked HC please contact elizabeth.walsh@comlab.ox.ac.uk or sue.taylor@comlab.ox.ac.ukwith address details and a copy will be posted to you.