Bill Roscoe : Publications
-
[0]
Notes on Domain Theory
A. W. Roscoe
1989.
These notes were written for the Oxford Domain Theory course between 1984 and 1989. I originally planned to publish them as half of "Domains for denotational semantics".
Details about Notes on Domain Theory | BibTeX data for Notes on Domain Theory | Download (pdf) of Notes on Domain Theory
-
[1]
A theory of communicating sequential processes
A. W. Roscoe‚ S.D. Brookes and C. A. R. Hoare
No. PRG−16. Oxford University Computing Laboratory. May, 1981.
Details about A theory of communicating sequential processes | BibTeX data for A theory of communicating sequential processes | Download (pdf) of A theory of communicating sequential processes
-
[2]
A mathematical theory of communicating processes
A. W. Roscoe
PhD Thesis , type= D. Phil. Thesis. Oxford University. 1982.
Please note this is a 270 page‚ 118 Mb scanned file and will take some time to download.
Details about A mathematical theory of communicating processes | BibTeX data for A mathematical theory of communicating processes | Download (pdf) of A mathematical theory of communicating processes
-
[3]
Criteria for metrisability
A. W. Roscoe and P.J. Collins
In Proc. Amer. Math. Soc.. No. 90. Pages 631−640. April, 1984.
Details about Criteria for metrisability | BibTeX data for Criteria for metrisability | Link to Criteria for metrisability
-
[4]
A theory of communicating sequential processes
A. W. Roscoe‚ S.D. Brookes and C.A.R. Hoare
In Journal of the ACM. No. 3. Pages 560–599. July, 1984.
Details about A theory of communicating sequential processes | BibTeX data for A theory of communicating sequential processes | Download (pdf) of A theory of communicating sequential processes
-
[5]
Programs as executable predicates
A. W. Roscoe and C.A.R. Hoare
In Proceedings of FGCS84 (ICOT‚ editors). Pages 220–228. 1984.
Details about Programs as executable predicates | BibTeX data for Programs as executable predicates | Download (pdf) of Programs as executable predicates
-
[6]
Continuous analogues of axiomatised digital surfaces
A. W. Roscoe and T.Y. Kong
In Computer Vision‚ Graphics and Image Processing. No. 29. Pages 60–86. January, 1985.
Details about Continuous analogues of axiomatised digital surfaces | BibTeX data for Continuous analogues of axiomatised digital surfaces | Download (pdf) of Continuous analogues of axiomatised digital surfaces
-
[7]
A lattice of conditions on topological spaces
A. W. Roscoe‚ P.J. Collins‚ G.M. Reed and M.E. Rudin
In Proc. Amer. Math. Soc.. No. 94. Pages 487–496. July, 1985.
Details about A lattice of conditions on topological spaces | BibTeX data for A lattice of conditions on topological spaces | Link to A lattice of conditions on topological spaces
-
[8]
Proceedings of the Pittsburgh seminar on concurrency
A. W. Roscoe‚ S.D. Brookes and G. Winskel, editors
Details about Proceedings of the Pittsburgh seminar on concurrency | BibTeX data for Proceedings of the Pittsburgh seminar on concurrency | Link to Proceedings of the Pittsburgh seminar on concurrency
-
[9]
An improved failures model for communicating processes
A. W. Roscoe and S.D. Brookes
In Proceedings of the Pittsburgh seminar on concurrency. No. 197. Pages 281–305. Springer. 1985.
Details about An improved failures model for communicating processes | BibTeX data for An improved failures model for communicating processes | Download (pdf) of An improved failures model for communicating processes
-
[10]
Denotational semantics for occam
A. W. Roscoe
In Proceedings of the Pittsburgh seminar on concurrency. No. 197. Pages 306–329. Springer. 1985.
Details about Denotational semantics for occam | BibTeX data for Denotational semantics for occam | Download (pdf) of Denotational semantics for occam
-
[11]
Deadlock analysis in networks of communicating processes
A. W. Roscoe and S.D. Brookes
In K.R. Apt, editor, Logics and Models of Concurrent Systems. Vol. 13 of NATO ASI series F. Pages 305–324. Springer. 1985.
Details about Deadlock analysis in networks of communicating processes | BibTeX data for Deadlock analysis in networks of communicating processes
-
[12]
Characterisations of simply−connected finite polyhedra in 3−space
A. W. Roscoe and T.Y. Kong
In Bull. London Math. Soc.. No. 17. Pages 575–578. November, 1985.
Details about Characterisations of simply−connected finite polyhedra in 3−space | BibTeX data for Characterisations of simply−connected finite polyhedra in 3−space | Download (pdf) of Characterisations of simply−connected finite polyhedra in 3−space
-
[13]
A theory of binary digital pictures
A. W. Roscoe and T.Y. Kong
In Computer Vision‚ Graphics and Image Processing. No. 32. Pages 221–243. November, 1985.
Details about A theory of binary digital pictures | BibTeX data for A theory of binary digital pictures | Download (pdf) of A theory of binary digital pictures
-
[14]
Specifying problem one using the failures model for CSP and deriving CSP processes which meet this specification
A. W. Roscoe
In B.T. Denvir et al, editor, The Analysis of Concurrent Systems. No. 207. Pages 103–109. Springer. 1985.
Details about Specifying problem one using the failures model for CSP and deriving CSP processes which meet this specification | BibTeX data for Specifying problem one using the failures model for CSP and deriving CSP processes which meet this specification | Download (pdf) of Specifying problem one using the failures model for CSP and deriving CSP processes which meet this specification
-
[15]
A CSP solution to the trains problem
A. W. Roscoe
In B.T. Denvir et al, editor, The Analysis of Concurrent Systems. No. 207. Pages 384–388. Springer. 1985.
Details about A CSP solution to the trains problem | BibTeX data for A CSP solution to the trains problem | Download (pdf) of A CSP solution to the trains problem
-
[16]
Local symmetry and triangle laws are sufficient for metrisability
A. W. Roscoe and P.J. Collins
In Colloquia Mathematica Societatis Janos Bolyai 41. Pages 177–181. 1985.
Details about Local symmetry and triangle laws are sufficient for metrisability | BibTeX data for Local symmetry and triangle laws are sufficient for metrisability | Download (pdf) of Local symmetry and triangle laws are sufficient for metrisability
-
[17]
A timed model for communicating sequential processes
A. W. Roscoe and G.M. Reed
In Theoretical Computer Science. Vol. 58. Pages 249–261. 1988.
Details about A timed model for communicating sequential processes | BibTeX data for A timed model for communicating sequential processes | Download (pdf) of A timed model for communicating sequential processes
-
[18]
The pursuit of deadlock freedom
A. W. Roscoe and Naiem Dathi
In Information and Computation. Vol. 75. No. 3. Pages 289–327. December, 1987.
Details about The pursuit of deadlock freedom | BibTeX data for The pursuit of deadlock freedom | Link to The pursuit of deadlock freedom
-
[19]
Metric spaces as models for real−time concurrency
A. W. Roscoe and G.M. Reed
In Main et al, editor, Proceedings of the Third Workshop on the Mathematical Foundations of Programming Language Semantics (New Orleans‚ 1987). No. 298. Pages 331–343. Springer. 1988.
Details about Metric spaces as models for real−time concurrency | BibTeX data for Metric spaces as models for real−time concurrency | Download (pdf) of Metric spaces as models for real−time concurrency
-
[20]
Laws of programming
A. W. Roscoe‚ 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
In Communications of the ACM. Vol. 30. No. 8. Pages 672–686. August, 1987.
Previously appeared as Oxford University Computing Laboratory Technical Report PRG−42.
Details about Laws of programming | BibTeX data for Laws of programming | Download (pdf) of Laws of programming
-
[21]
Routing messages through networks: an exercise in deadlock avoidance
A. W. Roscoe
In Muntean et al., editor, Programming of Transputer Based Machines: Proceedings of 7th occam User Group Technical Meeting. Amsterdam. 1987. IOS B.V..
Details about Routing messages through networks: an exercise in deadlock avoidance | BibTeX data for Routing messages through networks: an exercise in deadlock avoidance | Link to Routing messages through networks: an exercise in deadlock avoidance
-
[22]
Transforming occam programs
A. W. Roscoe and M.H. Goldsmith
In The Design and Application of Parallel Digital Processors. No. 298. 1988.
Details about Transforming occam programs | BibTeX data for Transforming occam programs | Download (pdf) of Transforming occam programs
-
[23]
A timed model for communicating sequential processes
A. W. Roscoe and G.M. Reed
In Proc.ICALP 86. No. 226. Pages 314–323. Springer. 1986.
Details about A timed model for communicating sequential processes | BibTeX data for A timed model for communicating sequential processes | Download (pdf) of A timed model for communicating sequential processes
-
[24]
The laws of occam programming
A. W. Roscoe and C.A.R. Hoare
In Theoretical Computer Science. Vol. 60. Pages 177–229. 1988.
Previously appeared as Oxford University Computing Laboratory Technical Report PRG−53‚ 1986.
Details about The laws of occam programming | BibTeX data for The laws of occam programming | Download (pdf) of The laws of occam programming
-
[25]
The decomposition of a rectangle into rectangles of minimal perimeter
A. W. Roscoe‚ T.Y. Kong and D.M. Mount
No. CAR−TR−169. University of Maryland Center for Automation Research. 1986.
Also SIAM Journal of Computing 17‚ 6 pp1215−1231.
Details about The decomposition of a rectangle into rectangles of minimal perimeter | BibTeX data for The decomposition of a rectangle into rectangles of minimal perimeter | Download (pdf) of The decomposition of a rectangle into rectangles of minimal perimeter
-
[26]
An Operational Semantics for CSP
A. W. Roscoe‚ S. D. Brookes and D. J. Walker
Oxford University Computing Laboratory. 1986.
Details about An Operational Semantics for CSP | BibTeX data for An Operational Semantics for CSP | Link to An Operational Semantics for CSP
-
[27]
An alternative order for the failures model
A. W. Roscoe
No. PRG−67. Oxford University Computing Laboratory. July, 1988.
in Two papers on CSP‚ Also appeared in Journal of Logic and Computation 2‚ 5 pp557−577
Details about An alternative order for the failures model | BibTeX data for An alternative order for the failures model | Link to An alternative order for the failures model
-
[28]
Unbounded nondeterminism in CSP
A. W. Roscoe
No. PRG−67. Oxford University Computing Laboratory. July, 1988.
in Two papers on CSP‚ Also appeared in Journal of Logic and Computation‚ Vol 3‚ No 2 pp131−172 (1993)
Details about Unbounded nondeterminism in CSP | BibTeX data for Unbounded nondeterminism in CSP | Link to Unbounded nondeterminism in CSP
-
[29]
Unbounded nondeterminism in CSP
A. W. Roscoe and G.Barrett
In Proceedings of MFPS89. No. 298. Springer. 1989.
Details about Unbounded nondeterminism in CSP | BibTeX data for Unbounded nondeterminism in CSP | Download (pdf) of Unbounded nondeterminism in CSP
-
[30]
Deadlock analysis in networks of communicating processes
A. W. Roscoe and S.D. Brookes
In Distributed Computing. No. 4. Pages 209–230. 1991.
Details about Deadlock analysis in networks of communicating processes | BibTeX data for Deadlock analysis in networks of communicating processes | Download (pdf) of Deadlock analysis in networks of communicating processes
-
[31]
A lattice of conditions on topological spaces II
A. W. Roscoe‚ P. Moody‚ G.M. Reed and P.J. Collins
In Fundamenta Mathematicae. No. 138. Pages 69–81. 1991.
Details about A lattice of conditions on topological spaces II | BibTeX data for A lattice of conditions on topological spaces II | Download (pdf) of A lattice of conditions on topological spaces II
-
[32]
The point−countable base problem
A. W. Rosoce‚ P.J. Collins and G.M. Reed
In G.M. Reed and J. van Mill, editors, Problems in Topology. Elsevier. 1990.
Details about The point−countable base problem | BibTeX data for The point−countable base problem | Download (pdf) of The point−countable base problem
-
[33]
Maintaining consistency in distributed databases
A. W. Roscoe
No. PRG−87. Oxford University Computing Laboratory. 1990.
Details about Maintaining consistency in distributed databases | BibTeX data for Maintaining consistency in distributed databases | Link to Maintaining consistency in distributed databases
-
[34]
Communication and correctness in Timed CSP
A. W. Roscoe‚ S.A. Schneider‚ J.W. Davies‚ D.M. Jackson and G.M. Reed
Esprit SPEC project. 1990.
Details about Communication and correctness in Timed CSP | BibTeX data for Communication and correctness in Timed CSP
-
[35]
A temporal logic for Timed CSP
D.M. Jackson‚ J.W. Davies‚ G.M. Reed and S.A. Schneider
Esprit SPEC project. 1990.
Details about A temporal logic for Timed CSP | BibTeX data for A temporal logic for Timed CSP
-
[36]
Topology‚ computer science and the mathematics of convergence
A. W. Roscoe
In G.M. Reed‚ A. W. Roscoe and R.F. Wachter, editors, Topology and Category Theory in Computer Science. OUP. 1991.
Details about Topology‚ computer science and the mathematics of convergence | BibTeX data for Topology‚ computer science and the mathematics of convergence | Link to Topology‚ computer science and the mathematics of convergence
-
[37]
Topology and category theory in computer science
A. W. Roscoe‚ G.M. Reed and R.F. Wachter, editors
proceedings of a special session at the 1989 Oxford Topology Conference
Details about Topology and category theory in computer science | BibTeX data for Topology and category theory in computer science
-
[38]
Analysing TM_FS: a study of nondeterminism in real−time concurrency
A. W. Roscoe and G.M. Reed
In Concurrency: Theory Language and Architecture. Vol. 491. 1991.
Details about Analysing TM_FS: a study of nondeterminism in real−time concurrency | BibTeX data for Analysing TM_FS: a study of nondeterminism in real−time concurrency | Link to Analysing TM_FS: a study of nondeterminism in real−time concurrency
-
[39]
CSP and timewise refinement
A. W. Roscoe‚ G. M. Reed and S. A. Schneider
In Proceedings of the BCS−FACS Refinement Workshop. LNCS. 1991.
Details about CSP and timewise refinement | BibTeX data for CSP and timewise refinement
-
[40]
Star covering properties
A. W. Roscoe‚ E.K. van Douwen‚ G.M. Reed and I.J. Tree
In Topology and its Applications. Vol. 39. Pages 71−103. 1991.
Details about Star covering properties | BibTeX data for Star covering properties | Download (pdf) of Star covering properties
-
[41]
Formal methods in the development of the H1 Transputer
A. W. Roscoe‚ A.D.B. Cox‚ M.H. Goldsmith and J.B. Scattergood
In Proceedings of Transputing 91. IOS. 1991.
Details about Formal methods in the development of the H1 Transputer | BibTeX data for Formal methods in the development of the H1 Transputer
-
[42]
Concepts of digital topology
A. W. Roscoe and T.Y. Kong
In Topology and its applications. Vol. 46. Pages 219–262. 1992.
Details about Concepts of digital topology | BibTeX data for Concepts of digital topology | Download (pdf) of Concepts of digital topology
-
[43]
Timed CSP: theory and practice
A. W. Roscoe‚ J.Davies‚ D.Jackson‚ G.M.Reed‚ J.Reed and S.A. Schneider
In Proceedings of REX Workshop. Vol. 600. LNCS. 1992.
Details about Timed CSP: theory and practice | BibTeX data for Timed CSP: theory and practice
-
[44]
Acyclic monotone normality
A. W. Roscoe and P. Moody
In Topology and its Applications. Vol. 47. Pages 53−67. 1992.
Details about Acyclic monotone normality | BibTeX data for Acyclic monotone normality | Download (pdf) of Acyclic monotone normality
-
[45]
Occam in the specification and verification of microprocessors
A. W. Roscoe
In Phil Trans R. Soc. Lond A. Vol. 339. Pages 137−151. 1992.
Also in Mechanised Reasoning and Hardware Design‚ M.J.C. Gordon and C.A.R. Hoare‚ eds (Prentice−Hall‚ 1992)‚ extended version available at http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/45ex.ps
Details about Occam in the specification and verification of microprocessors | BibTeX data for Occam in the specification and verification of microprocessors | Link to Occam in the specification and verification of microprocessors
-
[46]
A semantic model for occam II
A. W. Roscoe‚ M.H. Goldsmith and B.G.O. Scott
In Proceedings of Transputing. Vol. 93. 1991.
Details about A semantic model for occam II | BibTeX data for A semantic model for occam II
-
[47]
Denotational semantics for occam II
A. W. Roscoe‚ M.H. Goldsmith and B.G.O. Scott
No. PRG−108. Oxford University Computing Laboratory. 1993.
Details about Denotational semantics for occam II | BibTeX data for Denotational semantics for occam II | Download (pdf) of Denotational semantics for occam II
-
[48]
Developing and verifying protocols in CSP
A. W. Roscoe
In Proceedings of Mierlo workshop on protocols. TU Eindhoven. 1993.
Details about Developing and verifying protocols in CSP | BibTeX data for Developing and verifying protocols in CSP
-
[49]
Fixed points without completeness
A. W. Roscoe‚ M.W. Mislove and S.A. Schneider
In Theoretical Computer Science. Vol. 138. Chapter 2. Pages 273–314. 1993.
Details about Fixed points without completeness | BibTeX data for Fixed points without completeness
-
[50]
Model−checking CSP
A. W. Roscoe
In A Classical Mind: essays in Honour of C.A.R. Hoare. Chapter 21. Prentice−Hall. 1994.
Details about Model−checking CSP | BibTeX data for Model−checking CSP | Link to Model−checking CSP
-
[51]
A Classical Mind: essays in Honour of C.A.R. Hoare
A. W. Roscoe, editor
Prentice−Hall. 1994.
Details about A Classical Mind: essays in Honour of C.A.R. Hoare | BibTeX data for A Classical Mind: essays in Honour of C.A.R. Hoare
-
[52]
Denotational semantics for occam2‚ Part 1
A. W. Roscoe‚ M.H. Goldsmith and B.G.O. Scott
In Transputer Communications. Vol. 1 of 2. Pages 65–91. 1994.
Details about Denotational semantics for occam2‚ Part 1 | BibTeX data for Denotational semantics for occam2‚ Part 1
-
[53]
Denotational semantics for occam2‚ Part 2
A. W. Roscoe‚ M.H. Goldsmith and B.G.O. Scott
In Transputer Communications. Vol. 2 of 1. Pages 25–67. 1994.
Details about Denotational semantics for occam2‚ Part 2 | BibTeX data for Denotational semantics for occam2‚ Part 2
-
[54]
Non−interference through determinism
A. W. Roscoe‚ J.C.P. Woodcock and L. Wulf
In Proceedings of ESORICS 94. 1994.
Details about Non−interference through determinism | BibTeX data for Non−interference through determinism | Download (pdf) of Non−interference through determinism
-
[55]
Non−interference through determinism
A. W. Roscoe‚ J.C.P. Woodcock and L. Wulf
In Journal of Computer Security. Vol. 4 of 1. Pages 27–54. 1996.
revised version of above
Details about Non−interference through determinism | BibTeX data for Non−interference through determinism | Download (pdf) of Non−interference through determinism
-
[56]
CSP and determinism in security modelling
1996
In Proceedings of 1995 IEEE Symposium on Security and Privacy. IEEE Computer Society Press. 1996.
Details about CSP and determinism in security modelling | BibTeX data for CSP and determinism in security modelling | Link to CSP and determinism in security modelling
-
[57]
Composing and decomposing systems under security properties
A. W. Roscoe and L. Wulf
In Proceedings of 1995 IEEE Computer Security Foundations Workshop. IEEE Computer Society Press. 1995.
Details about Composing and decomposing systems under security properties | BibTeX data for Composing and decomposing systems under security properties | Link to Composing and decomposing systems under security properties
-
[58]
Modelling and verifying key−exchange protocols using CSP and FDR
A. W. Roscoe
In Proceedings of 1995 IEEE Computer Security Foundations Workshop. IEEE Computer Society Press. 1995.
Details about Modelling and verifying key−exchange protocols using CSP and FDR | BibTeX data for Modelling and verifying key−exchange protocols using CSP and FDR | Link to Modelling and verifying key−exchange protocols using CSP and FDR
-
[59]
Hierarchical compression for model−checking CSP‚ or How to check 10^20 dining philosophers for deadlock
A. W. Roscoe‚ D.M.Jackson P.H.B. Gardiner M.H. Goldsmith J.R. Hulance and J.B. Scattergood
In Proceedings of TACAS 1995. BRICS. 1995.
also revised in a version of these proceedings published by LNCS
Details about Hierarchical compression for model−checking CSP‚ or How to check 10^20 dining philosophers for deadlock | BibTeX data for Hierarchical compression for model−checking CSP‚ or How to check 10^20 dining philosophers for deadlock | Download (pdf) of Hierarchical compression for model−checking CSP‚ or How to check 10^20 dining philosophers for deadlock
-
[60]
The timed failures−stability model for Timed CSP
A. W. Roscoe and G.M. Reed
No. PRG−119. Oxford University Computing Laboratory. 1996.
also appeared in Theoretical Computer Science‚ Vol 211 (1999)
Details about The timed failures−stability model for Timed CSP | BibTeX data for The timed failures−stability model for Timed CSP | Download (pdf) of The timed failures−stability model for Timed CSP
-
[61]
Intensional specifications of security protocols
A. W. Roscoe
In Proceedings of 1996 IEEE Computer Security Foundations Workshop. IEEE Computer Society Press. 1996.
Details about Intensional specifications of security protocols | BibTeX data for Intensional specifications of security protocols | Link to Intensional specifications of security protocols
-
[62]
On transition systems and non−well−founded sets
A. W. Roscoe and R.S. Lazic
In Annals of the New York Academiy of Sciences. Vol. 806. 1996.
Details about On transition systems and non−well−founded sets | BibTeX data for On transition systems and non−well−founded sets | Download (pdf) of On transition systems and non−well−founded sets
-
[63]
The perfect spy for model−checking crypto−protocols
A. W. Roscoe and M.H. Goldsmith
In Proceedings of DIMACS workshop on the design and formal verification of crypto−protocols. 1997.
http://dimacs.rutgers.edu/workshops/program2/program.html
Details about The perfect spy for model−checking crypto−protocols | BibTeX data for The perfect spy for model−checking crypto−protocols | Download (pdf) of The perfect spy for model−checking crypto−protocols
-
[64]
A Case Study of the Formal Specification of a Parallel System using CSP
A. W. Roscoe and S. Kiyamura
In S. Noguchi and M. Ota, editors, Correct Models of Parallel Computing. IOS Press. 1997.
Details about A Case Study of the Formal Specification of a Parallel System using CSP | BibTeX data for A Case Study of the Formal Specification of a Parallel System using CSP
-
[65]
Using CSP to detect errors in the TMN protocol
A. W. Roscoe and G. Lowe
University of Leicester. 1996.
and IEEE transactions on Software Engineering Vol 23 (1997)
Details about Using CSP to detect errors in the TMN protocol | BibTeX data for Using CSP to detect errors in the TMN protocol | Link to Using CSP to detect errors in the TMN protocol
-
[66]
Verifying Determinism of Concurrent Systems Which Use Unbounded Arrays
A. W. Roscoe and R. Lazic
In Proceedings of INFINITY'98. July, 1998.
extended version as Oxford University Computing Laboratory TR−2−98.
Details about Verifying Determinism of Concurrent Systems Which Use Unbounded Arrays | BibTeX data for Verifying Determinism of Concurrent Systems Which Use Unbounded Arrays | Link to Verifying Determinism of Concurrent Systems Which Use Unbounded Arrays
-
[67]
Proving security protocols with model checkers by data independence techniques
A. W. Roscoe
In Proceedings of CSFW 1998. IEEE Press. 1998.
Details about Proving security protocols with model checkers by data independence techniques | BibTeX data for Proving security protocols with model checkers by data independence techniques | Download (pdf) of Proving security protocols with model checkers by data independence techniques
-
[68]
The theory and practice of concurrency
A. W. Roscoe
Prentice Hall. 1998.
The text book teaching material can be found at http://www.comlab.ox.ac.uk/publications/books/concurrency/
Details about The theory and practice of concurrency | BibTeX data for The theory and practice of concurrency | Download (pdf) of The theory and practice of concurrency
-
[69]
What is intransitive noninterference?
A. W. Roscoe and M.H. Goldsmith
In Proceedings of CSFW 1999. IEEE Press. 1999.
Details about What is intransitive noninterference? | BibTeX data for What is intransitive noninterference? | Link to What is intransitive noninterference?
-
[70]
Proving security protocols with model checkers by data independence techniques
A. W. Roscoe and P.J. Broadfoot
In Journal of Computer Security. Vol. 7. 1999.
Details about Proving security protocols with model checkers by data independence techniques | BibTeX data for Proving security protocols with model checkers by data independence techniques | Download (pdf) of Proving security protocols with model checkers by data independence techniques
-
[71]
Data independence with predicate symbols
A. W. Roscoe and R.S. Lazic
In Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA'99). Vol. I. CSREA Press. 1999.
Details about Data independence with predicate symbols | BibTeX data for Data independence with predicate symbols | Link to Data independence with predicate symbols
-
[72]
Verifying an infinite family of inductions simultaneously using data independence and FDR
A. W. Roscoe and 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). Kluwer Academic Publishers. 1999.
Details about Verifying an infinite family of inductions simultaneously using data independence and FDR | BibTeX data for Verifying an infinite family of inductions simultaneously using data independence and FDR | Download (pdf) of Verifying an infinite family of inductions simultaneously using data independence and FDR
-
[74]
TTP: A case study in combining induction and data independence
A. W. Roscoe and S.J. Creese
No. PRG−TR−1−99. Oxford University Computing Laboratory. 1999.
Details about TTP: A case study in combining induction and data independence | BibTeX data for TTP: A case study in combining induction and data independence | Link to TTP: A case study in combining induction and data independence
-
[75]
Data independent induction over structured networks
A. W. Roscoe and S.J. Creese
In Proceedings of PDPTA2000. 2000.
Details about Data independent induction over structured networks | BibTeX data for Data independent induction over structured networks | Link to Data independent induction over structured networks
-
[76]
Automating Data Independence
A. W. Roscoe‚ P.J. Broadfoot and G. Lowe
In Proceedings of ESORICS2000. Vol. 1895. LNCS. 2000.
Details about Automating Data Independence | BibTeX data for Automating Data Independence | Download (pdf) of Automating Data Independence
-
[77]
Millennial Perspectives in Computer Science
A. W. Roscoe‚ J. Davies and J. Woodcock, editors
Palgrave. 2000.
Details about Millennial Perspectives in Computer Science | BibTeX data for Millennial Perspectives in Computer Science
-
[78]
The successes and failures of behavioural models
A. W. Roscoe‚ R. Forster and G.M. Reed
In Millennial Perspectives in Computer Science. Palgrave. 2000.
Details about The successes and failures of behavioural models | BibTeX data for The successes and failures of behavioural models | Download (pdf) of The successes and failures of behavioural models
-
[79]
The Modelling and Analysis of Security Protocols
A. W. Roscoe‚ P. Ryan‚ S. Schneider‚ M. Goldsmith and G. Lowe
Addison−Wesley. 2001.
Details about The Modelling and Analysis of Security Protocols | BibTeX data for The Modelling and Analysis of Security Protocols
-
[81]
What can you Decide about Resetable Arrays?
A. W. Roscoe and R. S. Lazic
In Proceedings of VCL 2001. 2001.
Details about What can you Decide about Resetable Arrays? | BibTeX data for What can you Decide about Resetable Arrays? | Link to What can you Decide about Resetable Arrays?
-
[82]
Compiling Shared Variable Programs into CSP
A. W. Roscoe
In Proceedings of PROGRESS workshop 2001. 2001.
Details about Compiling Shared Variable Programs into CSP | BibTeX data for Compiling Shared Variable Programs into CSP | Download (pdf) of Compiling Shared Variable Programs into CSP
-
[83]
Internalising Agents in CSP Protocol Models
A. W. Roscoe and P. J. Broadfoot
In Proceedings of WITS 2002. 2002.
Extended Abstract
Details about Internalising Agents in CSP Protocol Models | BibTeX data for Internalising Agents in CSP Protocol Models | Link to Internalising Agents in CSP Protocol Models
-
[84]
Capturing parallel attacks within the data independence framework
A. W. Roscoe and P. J. Broadfoot
In Proceedings of CSFW 15. IEEE Press. 2002.
Details about Capturing parallel attacks within the data independence framework | BibTeX data for Capturing parallel attacks within the data independence framework | Link to Capturing parallel attacks within the data independence framework
-
[85]
On Model Checking Data−independent Systems with Arrays without Reset
A. W. Roscoe‚ R. S. Lazic and T. C. Newcomb
In Proceedings of VCL 2001. 2001.
Details about On Model Checking Data−independent Systems with Arrays without Reset | BibTeX data for On Model Checking Data−independent Systems with Arrays without Reset | Link to On Model Checking Data−independent Systems with Arrays without Reset
-
[85]
On Model Checking Data−independent Systems with Arrays without Reset
A. W. Roscoe‚ R. S. Lazic and T. C. Newcomb
In Theory and Practice of Logic Programming. Vol. 4. No. 5 & 6. Pages 659−693. 2004.
Details about On Model Checking Data−independent Systems with Arrays without Reset | BibTeX data for On Model Checking Data−independent Systems with Arrays without Reset | Download (pdf) of On Model Checking Data−independent Systems with Arrays without Reset
-
[86]
Embedding agents within the intruder to detect parallel attacks
A. W. Roscoe and P.J. Broadfoot
In Journal of Computer Security. Vol. 12. No. 3−4. Pages 379−408. 2004.
Details about Embedding agents within the intruder to detect parallel attacks | BibTeX data for Embedding agents within the intruder to detect parallel attacks | Download (pdf) of Embedding agents within the intruder to detect parallel attacks
-
[87]
Authentication in pervasive computing
A. W. Roscoe‚ S.J. Creese‚ M.H. Goldsmith and I.Zakiuddin
In Proceedings of the First International Conference on Security in Pervasive Computing. LNCS. March, 2003.
Details about Authentication in pervasive computing | BibTeX data for Authentication in pervasive computing | Link to Authentication in pervasive computing
-
[87]
Formal Verification of Arbitrary Network Topologies
A. W. Roscoe and S.J. Creese
In Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA'99). Vol. II. CSREA Press. June, 1999.
Details about Formal Verification of Arbitrary Network Topologies | BibTeX data for Formal Verification of Arbitrary Network Topologies | Download (pdf) of Formal Verification of Arbitrary Network Topologies
-
[88]
Bisimulation and refinement reconciled
A. W. Roscoe‚ C.A.R. Hoare‚ C. Fournet‚ P.H.B. Gardiner‚ R. Milner‚ S.Rajamani and J. Rehof
Microsoft. 2003.
Details about Bisimulation and refinement reconciled | BibTeX data for Bisimulation and refinement reconciled
-
[89]
On the expressive power of CSP refinement
A. W. Roscoe
In Formal Aspects of Computing. Vol. 17 of 2. Pages 93–112. 2003.
Preliminary version in Proceedings of AVoCS03‚ Southampton University Technical Report‚ April 2003
Details about On the expressive power of CSP refinement | BibTeX data for On the expressive power of CSP refinement | Link to On the expressive power of CSP refinement
-
[90]
Polymorphic systems with arrays: decidability and undecidability
A. W. Roscoe‚ R. S. Lazic and T. C. Newcomb
In Proceedings of South−East Europe Workshop on Formal Methods. August, 2003.
Extended abstract
Details about Polymorphic systems with arrays: decidability and undecidability | BibTeX data for Polymorphic systems with arrays: decidability and undecidability | Download (pdf) of Polymorphic systems with arrays: decidability and undecidability
-
[91]
Watchdog transformations for property−oriented model checking
A. W. Roscoe‚ M.H. Goldsmith‚ N.Moffat‚ T. Whitworth and I. Zakiuddin
In Proceedings of FME 2003. 2003.
Details about Watchdog transformations for property−oriented model checking | BibTeX data for Watchdog transformations for property−oriented model checking | Download (pdf) of Watchdog transformations for property−oriented model checking
-
[92]
The attacker in ubiquitous computing environments: formalising the threat model
A. W. Roscoe‚ S.J. Creese‚ M.H. Goldsmith and I.Zakiuddin
In Proceedings of FAST 2003‚ Pisa. 2003.
Details about The attacker in ubiquitous computing environments: formalising the threat model | BibTeX data for The attacker in ubiquitous computing environments: formalising the threat model | Download (pdf) of The attacker in ubiquitous computing environments: formalising the threat model
-
[93]
Translating CSP trace refinement to UNITY unreachability : a study in data independence
A. W. Roscoe‚ Xu Wang and R.S. Lazic
No. RR−03−08. Oxford University Computing Laboratory. April, 2003.
Details about Translating CSP trace refinement to UNITY unreachability : a study in data independence | BibTeX data for Translating CSP trace refinement to UNITY unreachability : a study in data independence | Download (ps.gz) of Translating CSP trace refinement to UNITY unreachability : a study in data independence | Link to Translating CSP trace refinement to UNITY unreachability : a study in data independence
-
[94]
Compiling Statemate Statecharts into CSP and verifying them using FDR
A. W. Roscoe
January, 2003.
Extended Abstract
Details about Compiling Statemate Statecharts into CSP and verifying them using FDR | BibTeX data for Compiling Statemate Statecharts into CSP and verifying them using FDR | Link to Compiling Statemate Statecharts into CSP and verifying them using FDR
-
[95]
Seeing beyond divergence
A. W. Roscoe
In Communicating Sequential Processes‚ the first 25 years. No. 3525. Springer LNCS. 2005.
Details about Seeing beyond divergence | BibTeX data for Seeing beyond divergence | Download (pdf) of Seeing beyond divergence
-
[96]
Finitary refinement checks for infinitary specifications
A. W. Roscoe
In Proceedings of CPA 2004. June, 2004.
Details about Finitary refinement checks for infinitary specifications | BibTeX data for Finitary refinement checks for infinitary specifications | Download (pdf) of Finitary refinement checks for infinitary specifications
-
[97]
Research directions for trust and security in human−centric computing
A. W. Roscoe‚ Sadie Creese‚ Michael Goldsmith and Irfan Zakiuddin
In Proceedings of SPPC 2004. 2004.
Details about Research directions for trust and security in human−centric computing | BibTeX data for Research directions for trust and security in human−centric computing | Download (pdf) of Research directions for trust and security in human−centric computing
-
[98]
Responsiveness of Interoperating Components
A. W. Roscoe‚ J. N. Reed and J. E. Sinclair
In Formal Aspects of Computing. Vol. 16. Pages 394–411. 2004.
Details about Responsiveness of Interoperating Components | BibTeX data for Responsiveness of Interoperating Components | Download (pdf) of Responsiveness of Interoperating Components
-
[99]
Relating Data Independent Trace Checks in CSP with UNITY Reachability under a Normality Assumption
A. W. Roscoe‚ Xu Wang and R. S. Lazic
In Proceedings of IFM 2004. Vol. 2999. Springer LNCS. 2004.
Details about Relating Data Independent Trace Checks in CSP with UNITY Reachability under a Normality Assumption | BibTeX data for Relating Data Independent Trace Checks in CSP with UNITY Reachability under a Normality Assumption | Download (pdf) of Relating Data Independent Trace Checks in CSP with UNITY Reachability under a Normality Assumption
-
[100]
Web Services Security: a preliminary study using Casper and FDR
A. W. Roscoe and E. Kleiner
In Proceedings of Automated Reasoning for Security Protocol Analysis (ARSPA 04). 2004.
Details about Web Services Security: a preliminary study using Casper and FDR | BibTeX data for Web Services Security: a preliminary study using Casper and FDR | Download (pdf) of Web Services Security: a preliminary study using Casper and FDR
-
[101]
Polymorphic Systems with Arrays‚ 2−Counter Machines and Multiset Rewriting
A. W. Roscoe‚ R. S. Lazic and Tom Newcomb
In Proceedings of INFINITY 2004. 2004.
Details about Polymorphic Systems with Arrays‚ 2−Counter Machines and Multiset Rewriting | BibTeX data for Polymorphic Systems with Arrays‚ 2−Counter Machines and Multiset Rewriting | Download (pdf) of Polymorphic Systems with Arrays‚ 2−Counter Machines and Multiset Rewriting
-
[102]
On Model checking data−independent systems with arrays with whole−array operations
A. W. Roscoe‚ R. S. Lazic and Tom Newcomb
In Communicating Sequential Processes. No. 3525. Springer LNCS. 2005.
Details about On Model checking data−independent systems with arrays with whole−array operations | BibTeX data for On Model checking data−independent systems with arrays with whole−array operations | Download (pdf) of On Model checking data−independent systems with arrays with whole−array operations
-
[103]
Exploiting Empirical Engagement in Authentication Protocol Design
Sadie Creese‚ Michael Goldsmith‚ Richard Harrison‚ Bill Roscoe‚ Paul Whittaker and Irfan Zakiuddin
In Proceedings of SPPC 2005. May, 2005.
Details about Exploiting Empirical Engagement in Authentication Protocol Design | BibTeX data for Exploiting Empirical Engagement in Authentication Protocol Design
-
[104]
On the relationship between Web Services Security and traditional protocols
A. W. Roscoe and Eldar Kleiner
In Proceedings of MFPS 2005. 2005.
To appear.
Details about On the relationship between Web Services Security and traditional protocols | BibTeX data for On the relationship between Web Services Security and traditional protocols | Download (pdf) of On the relationship between Web Services Security and traditional protocols
-
[105]
Revivals‚stuckness and the hierarchy of CSP Models
A. W. Roscoe
December, 2008.
to appear (revision of 2005 and 2007 drafts)
Details about Revivals‚stuckness and the hierarchy of CSP Models | BibTeX data for Revivals‚stuckness and the hierarchy of CSP Models | Download (pdf) of Revivals‚stuckness and the hierarchy of CSP Models
-
[106]
The pursuit of buffer tolerance
A. W. Roscoe
May, 2005.
unpublished draft
Details about The pursuit of buffer tolerance | BibTeX data for The pursuit of buffer tolerance | Download (pdf) of The pursuit of buffer tolerance
-
[107]
Confluence thanks to extensional determinism
A. W. Roscoe
In Proceedings of Bertinoro meeting on Concurrency‚ BRICS 2005. May, 2005.
Revised version‚ publication reference ENTCS 1336‚ 2006
Details about Confluence thanks to extensional determinism | BibTeX data for Confluence thanks to extensional determinism | Download (pdf) of Confluence thanks to extensional determinism
-
[108]
Security and trust for ubiquitous communication
A. W. Roscoe‚ Sadie Creese‚ Mike Reed and Jeff Sanders
In ITU WSIS Thematic Meeting on Cybersecurity‚ Geneva‚ Switzerland. June, 2005.
Details about Security and trust for ubiquitous communication | BibTeX data for Security and trust for ubiquitous communication | Download (pdf) of Security and trust for ubiquitous communication
-
[109]
Machine−Verifiable Responsiveness
A. W. Roscoe‚ J. N Reed and J. E Sinclair
In Proceedings of AVOCS 2005. 2005.
Details about Machine−Verifiable Responsiveness | BibTeX data for Machine−Verifiable Responsiveness | Download (pdf) of Machine−Verifiable Responsiveness
-
[110]
Extending noninterference properties to the timed world
A. W. Roscoe and Jian Huang
In Proceedings of SAC 2006. 2006.
to appear
Details about Extending noninterference properties to the timed world | BibTeX data for Extending noninterference properties to the timed world | Download (pdf) of Extending noninterference properties to the timed world
-
[111]
Bootstrapping Multi−Party Ad−Hoc Security
A. W. Roscoe‚ S. J. Creese‚ M. H. Goldsmith and Ming Xiao
In Proceedings of SAC 2006. 2006.
to appear
Details about Bootstrapping Multi−Party Ad−Hoc Security | BibTeX data for Bootstrapping Multi−Party Ad−Hoc Security | Download (pdf) of Bootstrapping Multi−Party Ad−Hoc Security
-
[112]
A taxonomy of web services in CSP
A. W. Roscoe‚ A. Martin and L. Momtahan
In Proceedings of Web Languages and Formal Methods 2005. 2005.
Details about A taxonomy of web services in CSP | BibTeX data for A taxonomy of web services in CSP | Download (pdf) of A taxonomy of web services in CSP
-
[113]
Human−centred computer security
A. W. Roscoe
2006.
Unpublished draft
Details about Human−centred computer security | BibTeX data for Human−centred computer security | Download (pdf) of Human−centred computer security
-
[114]
Modelling unbounded parallel sessions of security protocols in CSP
A. W. Roscoe and E. Kleiner
2006.
Details about Modelling unbounded parallel sessions of security protocols in CSP | BibTeX data for Modelling unbounded parallel sessions of security protocols in CSP | Download (pdf) of Modelling unbounded parallel sessions of security protocols in CSP
-
[115]
Verifying Statemate Statecharts Using CSP and FDR
A. W. Roscoe and Zhenzhong Wu
In Proceedings of ICFEM 2006. 2006.
Details about Verifying Statemate Statecharts Using CSP and FDR | BibTeX data for Verifying Statemate Statecharts Using CSP and FDR | Download (pdf) of Verifying Statemate Statecharts Using CSP and FDR
-
[116]
Efficient group authentication protocols based on human interaction
A. W. Roscoe and L. H. Nguyen
In Proceedings of ARSPA 2006. 2006.
Details about Efficient group authentication protocols based on human interaction | BibTeX data for Efficient group authentication protocols based on human interaction | Download (pdf) of Efficient group authentication protocols based on human interaction
-
[117]
Responsiveness and stable revivals
A. W. Roscoe‚ J. N. Reed and J. E. Sinclair
In Formal Aspects of Computing. Vol. 19. No. 3. August, 2007.
Details about Responsiveness and stable revivals | BibTeX data for Responsiveness and stable revivals | Download (pdf) of Responsiveness and stable revivals
-
[118]
Nets with Tokens Which Carry Data
A. W. Roscoe‚ Ranko Lazic‚ Tom Newcomb‚ Joel Ouaknine and James Worrell
In Springer LNCS 3349. 2007.
Details about Nets with Tokens Which Carry Data | BibTeX data for Nets with Tokens Which Carry Data | Download of Nets with Tokens Which Carry Data | Download (pdf) of Nets with Tokens Which Carry Data
-
[119]
SVA‚ a tool for analysing shared−variable programms
A. W. Roscoe and David Hopkins
In Proceedings of AVoCS 2007. Pages 177–183. 2007.
to appear
Details about SVA‚ a tool for analysing shared−variable programms | BibTeX data for SVA‚ a tool for analysing shared−variable programms | Download (pdf) of SVA‚ a tool for analysing shared−variable programms
-
[120]
Authenticating ad hoc networks by comparison of short digests
A. W. Roscoe and L. H. Nguyen
In Information and Computation. Vol. 206. Pages 250−271. 2008.
Details about Authenticating ad hoc networks by comparison of short digests | BibTeX data for Authenticating ad hoc networks by comparison of short digests | Download (pdf) of Authenticating ad hoc networks by comparison of short digests
-
[121]
The three Platonic models of divergence−strict CSP
A.W. Roscoe
In Proceedings of ICTAC '08. 2008.
Details about The three Platonic models of divergence−strict CSP | BibTeX data for The three Platonic models of divergence−strict CSP | Download (pdf) of The three Platonic models of divergence−strict CSP
-
[122]
Separating two roles of hashing in one−way message authentication
L.H. Nguyen and A.W. Roscoe
In Proceedings of FCS−ARSPA−WITS. 2008.
(This version is extended by appendices not present in proceedings.)
Details about Separating two roles of hashing in one−way message authentication | BibTeX data for Separating two roles of hashing in one−way message authentication | Download (pdf) of Separating two roles of hashing in one−way message authentication
-
[124]
A representative function approach to symmetry exploitation for CSP refinement checking
N Moffat‚ M.H. Goldsmith and A.W. Roscoe
In Proceedings of IFCEM 2008. 2008.
Details about A representative function approach to symmetry exploitation for CSP refinement checking | BibTeX data for A representative function approach to symmetry exploitation for CSP refinement checking | Download (pdf) of A representative function approach to symmetry exploitation for CSP refinement checking
-
[125]
On the expressiveness of CSP
A.W. Roscoe
2011.
Draft of February 2011‚ which is very different from previous draft (2008).
Details about On the expressiveness of CSP | BibTeX data for On the expressiveness of CSP | Download (pdf) of On the expressiveness of CSP
-
[126]
Authentication protocols based on low−bandwidth unspoofable channels: a comparative survey
L.H. Nguyen and A.W. Roscoe
In Journal of Computer Security. Vol. 19. 2011.
Details about Authentication protocols based on low−bandwidth unspoofable channels: a comparative survey | BibTeX data for Authentication protocols based on low−bandwidth unspoofable channels: a comparative survey | Download (pdf) of Authentication protocols based on low−bandwidth unspoofable channels: a comparative survey
-
[127]
CSP is expressive enough for pi
A.W. Roscoe
2010.
Details about CSP is expressive enough for pi | BibTeX data for CSP is expressive enough for pi | Download (pdf) of CSP is expressive enough for pi
-
[128]
New combinatorial bounds for universal hash functions
L.H. Nguyen and A.W. Roscoe
2009.
Details about New combinatorial bounds for universal hash functions | BibTeX data for New combinatorial bounds for universal hash functions | Download (pdf) of New combinatorial bounds for universal hash functions
-
[129]
Usability and security of out−of−bound channels in secure device pairing protocols
I. Flechais R. Kainda and A.W. Roscoe
2009.
Details about Usability and security of out−of−bound channels in secure device pairing protocols | BibTeX data for Usability and security of out−of−bound channels in secure device pairing protocols | Download (pdf) of Usability and security of out−of−bound channels in secure device pairing protocols
-
[130]
Local search in model checking
P.J. Armstrong A.W. Roscoe and Pragyesh
2009.
Details about Local search in model checking | BibTeX data for Local search in model checking | Download (pdf) of Local search in model checking
-
[131]
Insight‚ innovation and collaboration
C.B. Jones and A.W. Roscoe
2010.
Details about Insight‚ innovation and collaboration | BibTeX data for Insight‚ innovation and collaboration | Download (pdf) of Insight‚ innovation and collaboration
-
[132]
Reflections on the work of C.A.R. Hoare
A.W. Roscoe C.B. Jones and K.R. Wood (editors)
Springer. 2010.
Details about Reflections on the work of C.A.R. Hoare | BibTeX data for Reflections on the work of C.A.R. Hoare
-
[133]
Secure and usable out−of−band channels for ad hoc mobile device interactions
R. Kainda‚ I. Flechais and A.W. Roscoe
2010.
Details about Secure and usable out−of−band channels for ad hoc mobile device interactions | BibTeX data for Secure and usable out−of−band channels for ad hoc mobile device interactions | Download (pdf) of Secure and usable out−of−band channels for ad hoc mobile device interactions
-
[134]
Security and Usability: Analysis and Evaluation
Ronald Kainda‚ Ivan Flechais and A.W. Roscoe
2010.
Details about Security and Usability: Analysis and Evaluation | BibTeX data for Security and Usability: Analysis and Evaluation | Download (pdf) of Security and Usability: Analysis and Evaluation
-
[135]
Understanding Concurrent Systems
A.W. Roscoe
Springer. 2010.
Details about Understanding Concurrent Systems | BibTeX data for Understanding Concurrent Systems | Link to Understanding Concurrent Systems
-
[136]
A new bound for t−wise almost universal hash functions
L.H. Nguyen and A.W. Roscoe
No. RR−10−24. OUCL. November, 2010.
Details about A new bound for t−wise almost universal hash functions | BibTeX data for A new bound for t−wise almost universal hash functions | Download (pdf) of A new bound for t−wise almost universal hash functions
-
[137]
Reverse authentication in financial transactions
Chen Bangdao and A.W. Roscoe
2010.
In Proceedings of IWSSI/SPMU‚ Helsinki
Details about Reverse authentication in financial transactions | BibTeX data for Reverse authentication in financial transactions | Download (pdf) of Reverse authentication in financial transactions
-
[138]
The missing link: Human Interactive Security Protocols in mobile payment
L.H. Nguyen Chen Bangdao and A.W. Roscoe
2010.
In Proceedings of 5th International Workshop on Security‚ Kobe‚ Japan
Details about The missing link: Human Interactive Security Protocols in mobile payment | BibTeX data for The missing link: Human Interactive Security Protocols in mobile payment | Download (pdf) of The missing link: Human Interactive Security Protocols in mobile payment
-
[139]
Mobile Electronic Identity: Securing Payment on Mobile Phones
Chen Bangdao and A.W. Roscoe
2011.
Proceedings of WISTP 2011
Details about Mobile Electronic Identity: Securing Payment on Mobile Phones | BibTeX data for Mobile Electronic Identity: Securing Payment on Mobile Phones | Download (pdf) of Mobile Electronic Identity: Securing Payment on Mobile Phones
-
[140]
Secure mobile ad−hoc interactions: reasoning about out−of−band (oob) channels
R. Kainda‚ I. Flechais and AW Roscoe
In In Second International Workshop on Security and Privacy in Spontaneous Interaction and Mobile Phone Use (IWSSI/SPMU). 2010.
Details about Secure mobile ad−hoc interactions: reasoning about out−of−band (oob) channels | BibTeX data for Secure mobile ad−hoc interactions: reasoning about out−of−band (oob) channels | Link to Secure mobile ad−hoc interactions: reasoning about out−of−band (oob) channels
-
[141]
Two heads are better than one: security and usability of device associations in group scenarios
R. Kainda‚ I. Flechais and A.W. Roscoe
In Proceedings of the Sixth Symposium on Usable Privacy and Security. Pages 5. ACM. 2010.
Details about Two heads are better than one: security and usability of device associations in group scenarios | BibTeX data for Two heads are better than one: security and usability of device associations in group scenarios
-
[142]
Translating Timed Automata to Tock−CSP
M. Khattri‚ A.W. Roscoe and J. Ouaknine
In Parallel and Distributed Computing and Networks/720: Software Engineering. ACTA Press. 2011.
Details about Translating Timed Automata to Tock−CSP | BibTeX data for Translating Timed Automata to Tock−CSP
-
[143]
Model checking cryptographic protocols subject to combinatorial attack
A.W. Roscoe‚ T. Smyth and L. Nguyen
2012.
Details about Model checking cryptographic protocols subject to combinatorial attack | BibTeX data for Model checking cryptographic protocols subject to combinatorial attack
-
[144]
SAT−solving in CSP trace refinement
H. Palikareva‚ J. Ouaknine and A.W. Roscoe
In Science of Computer Programming. 2011.
Details about SAT−solving in CSP trace refinement | BibTeX data for SAT−solving in CSP trace refinement | Link to SAT−solving in CSP trace refinement
-
[145]
Checking noninterference in the timed world
A.W Roscoe and J. Huang
In Formal Aspects of Computing. Vol. 25. 2013.
Details about Checking noninterference in the timed world | BibTeX data for Checking noninterference in the timed world | Download (pdf) of Checking noninterference in the timed world
-
[146]
Reverse Authentication in Financial Transactions and Identity Management
Bangdao Chen‚ Long Nguyen and A.W. Roscoe
In Mobile Networks and Applications. Pages 1−16. 2012.
10.1007/s11036−012−0366−2
Details about Reverse Authentication in Financial Transactions and Identity Management | BibTeX data for Reverse Authentication in Financial Transactions and Identity Management | Link to Reverse Authentication in Financial Transactions and Identity Management
-
[147]
Static livelock analysis in CSP
J. Ouaknine‚ H. Palikareva‚ A. Roscoe and J. Worrell
In CONCUR 2011–Concurrency Theory. Vol. 6901 of Lecture Notes in Computer Science. Pages 389–403. Springer. 2011.
Details about Static livelock analysis in CSP | BibTeX data for Static livelock analysis in CSP | DOI (10.1007/978-3-642-23217-6_26) | Link to Static livelock analysis in CSP
-
[148]
Body sensor network key distribution using human interactive channels
X. Huang‚ Q. Wang‚ B. Chen‚ A. Markham‚ R. Jäntti and A.W. Roscoe
In Proceedings of the 4th International Symposium on Applied Sciences in Biomedical and Communication Technologies. Pages 143. ACM. 2011.
Details about Body sensor network key distribution using human interactive channels | BibTeX data for Body sensor network key distribution using human interactive channels | DOI (http://dx.doi.org/10.1145/2093698.2093841)
-
[148]
When Context Is Better Than Identity: Authentication by Context Using Empirical Channels
B. Chen‚ L. Nguyen and A. Roscoe
In Security Protocols XIX. Pages 115–125. 2011.
Details about When Context Is Better Than Identity: Authentication by Context Using Empirical Channels | BibTeX data for When Context Is Better Than Identity: Authentication by Context Using Empirical Channels | Download (pdf) of When Context Is Better Than Identity: Authentication by Context Using Empirical Channels
-
[149]
Model checking Timed CSP
P. Armstrong‚ G. Lowe‚ J Ouaknine and A.W Roscoe
2012.
Details about Model checking Timed CSP | BibTeX data for Model checking Timed CSP | Download (pdf) of Model checking Timed CSP
-
[150]
Recent developments in FDR
P. Armstrong‚ M.H. Goldsmith‚ G. Lowe‚ J. Ouaknine‚ H. Palikareva‚ A. Roscoe and J. Worrell
In CAV 2012. 2012.
Details about Recent developments in FDR | BibTeX data for Recent developments in FDR | Download fdr-2-94-examples.tar of Recent developments in FDR | Download paper_227.pdf of Recent developments in FDR
-
[151]
Short−output universal hash functions and their use in fast and secure message authentication
L.H. Nguyen and A.W. Roscoe
In FSE 2012. 2012.
Details about Short−output universal hash functions and their use in fast and secure message authentication | BibTeX data for Short−output universal hash functions and their use in fast and secure message authentication | Download PublicationFile of Short−output universal hash functions and their use in fast and secure message authentication | Download fse20120_submission_4.pdf of Short−output universal hash functions and their use in fast and secure message authentication | Download (pdf) of Short−output universal hash functions and their use in fast and secure message authentication
-
[152]
Fairness analysis through priority
P.J. Hopcroft P. Armstrong and A.W. Roscoe
2012.
Details about Fairness analysis through priority | BibTeX data for Fairness analysis through priority | Download (pdf) of Fairness analysis through priority
-
[153]
Social networks for importing and exporting security
Bangdao Chen and A.W. Roscoe
2012.
Details about Social networks for importing and exporting security | BibTeX data for Social networks for importing and exporting security | Download of Social networks for importing and exporting security
-
[154]
Simple construction of epsilon−biased distribution
L.H. Nguyen and A.W. Roscoe
In IACR cryptology e−print archive. 2012.
Details about Simple construction of epsilon−biased distribution | BibTeX data for Simple construction of epsilon−biased distribution | Link to Simple construction of epsilon−biased distribution
-
[155]
Bootstrapping body sensor networks using human controlled LED−camera channels
A.W. Roscoe Xin Huang Shangyuan Guo Bangdao Chen
In ICITST. 2012.
Details about Bootstrapping body sensor networks using human controlled LED−camera channels | BibTeX data for Bootstrapping body sensor networks using human controlled LED−camera channels | Link to Bootstrapping body sensor networks using human controlled LED−camera channels
-
[156]
User interactive Internet of things privacy preserved access control
A.W. Roscoe Xin Huang Rong Fu Bangdao Chen Tingting Zhang
In ICITST. 2012.
Details about User interactive Internet of things privacy preserved access control | BibTeX data for User interactive Internet of things privacy preserved access control | Link to User interactive Internet of things privacy preserved access control
-
[157]
Human Interactive Secure ID Management in Body Sensor Networks
A.W. Roscoe Xin Huang Xiao Ma Bangdao Chen Andrew Markham Quinghua Wang
In Journal of Networks. Vol. 7. 2012.
Details about Human Interactive Secure ID Management in Body Sensor Networks | BibTeX data for Human Interactive Secure ID Management in Body Sensor Networks | Link to Human Interactive Secure ID Management in Body Sensor Networks
-
[158]
Reverse authentication in financial transactions and identity management
L.H. Nguyen Bangdao Chen and A.W. Roscoe
In Mobile Networks and Applications. 2012.
Details about Reverse authentication in financial transactions and identity management | BibTeX data for Reverse authentication in financial transactions and identity management | Link to Reverse authentication in financial transactions and identity management
-
[159]
SAT solving in CSP trace refinement
Hristina Palikareva‚ Joel Ouaknine and A.W. Roscoe
In Science of Computer Programming. Vol. 77. 2012.
Details about SAT solving in CSP trace refinement | BibTeX data for SAT solving in CSP trace refinement | Link to SAT solving in CSP trace refinement
-
[160]
The automated verification of timewise refinement
A.W. Roscoe
In EIT−CPSE. 2013.
Details about The automated verification of timewise refinement | BibTeX data for The automated verification of timewise refinement | Download tring2.csp of The automated verification of timewise refinement | Download tring.csp of The automated verification of timewise refinement | Download twrs.pdf of The automated verification of timewise refinement
-
[161]
Slow abstraction through priority
A.W. Roscoe and P.J. Hopcroft
In Festschrift for He Jifeng‚ to appear in LNCS. 2013.
Details about Slow abstraction through priority | BibTeX data for Slow abstraction through priority | Download (pdf) of Slow abstraction through priority
-
[162]
Human interactive secure key and ID exchange protocols in body sensor networks
A.W. Roscoe Xin Huang Bangdao Chen Andrew Markham Quinghua Wang Zheng Yan
In IET Information Security. Vol. 7. 2013.
Details about Human interactive secure key and ID exchange protocols in body sensor networks | BibTeX data for Human interactive secure key and ID exchange protocols in body sensor networks | Link to Human interactive secure key and ID exchange protocols in body sensor networks
-
[163]
A Static Analysis Framework for Livelock Freedom in CSP
Joël Ouaknine‚ Hristina Palikareva‚ A. W. Roscoe and James Worrell
In Logical Methods in Computer Science. Vol. 9. No. 3. 2013.
Details about A Static Analysis Framework for Livelock Freedom in CSP | BibTeX data for A Static Analysis Framework for Livelock Freedom in CSP | DOI (10.2168/LMCS-9(3:24)2013) | Download (pdf) of A Static Analysis Framework for Livelock Freedom in CSP
-
[164]
FDR3 — A Modern Refinement Checker for CSP
Thomas Gibson−Robinson‚ Philip Armstrong‚ Alexandre Boulgakov and A.W. Roscoe
In Tools and Algorithms for the Construction and Analysis of Systems. Pages 187−201. 2014.
Details about FDR3 — A Modern Refinement Checker for CSP | BibTeX data for FDR3 — A Modern Refinement Checker for CSP | Download Document.pdf of FDR3 — A Modern Refinement Checker for CSP | Download Samples.zip of FDR3 — A Modern Refinement Checker for CSP | DOI (10.1007/978-3-642-54862-8_13)
-
[165]
FDR into The Cloud
Thomas Gibson−Robinson and A.W. Roscoe
In Communicating Process Architectures. 2014.
Details about FDR into The Cloud | BibTeX data for FDR into The Cloud | Download Samples.zip of FDR into The Cloud | Download ClusterFDR.pdf of FDR into The Cloud
-
[166]
Reflections on the need to de−skill CSP
A.W. Roscoe
In Proceedings of CPA 2014. 2014.
Details about Reflections on the need to de−skill CSP | BibTeX data for Reflections on the need to de−skill CSP | Download (pdf) of Reflections on the need to de−skill CSP
-
[167]
Computing Maximal Bisimulations
Alexandre Boulgakov‚ Thomas Gibson−Robinson and A.W. Roscoe
In Formal Methods and Software Engineering − 16th International Conference on Formal Engineering Methods‚ ICFEM 2014‚ Proceedings. 2014.
Details about Computing Maximal Bisimulations | BibTeX data for Computing Maximal Bisimulations | DOI (10.1007/978-3-319-11737-9_2) | Link to Computing Maximal Bisimulations
-
[167]
Computing maximal bisimulations
Alexandre Bougakov‚ Thomas Gibson Robinson and A.W. Roscoe
In Proceedings of ICFEM. 2014.
Details about Computing maximal bisimulations | BibTeX data for Computing maximal bisimulations | Download PublicationFile of Computing maximal bisimulations | Download ICFEM 2014 Version 10.pdf of Computing maximal bisimulations
-
[168]
On the expressive power of CSP extended by priority
A.W. Roscoe
2014.
Details about On the expressive power of CSP extended by priority | BibTeX data for On the expressive power of CSP extended by priority | Download prex.pdf of On the expressive power of CSP extended by priority | Download pricsplike.tar of On the expressive power of CSP extended by priority
-
[169]
Practical partial order reduction for CSP
A.W. Roscoe T. Gibson−Robinson H. Hansen and X Wang
In NASA Formal Methods‚ 2015. 2015.
Details about Practical partial order reduction for CSP | BibTeX data for Practical partial order reduction for CSP
-
[170]
FDR3: a parallel refinement checker for CSP
Thomas Gibson−Robinson‚ Philip Armstrong‚ Alexandre Boulgakov and A.W. Roscoe
In International Journal on Software Tools for Technology Transfer. 2015.
Details about FDR3: a parallel refinement checker for CSP | BibTeX data for FDR3: a parallel refinement checker for CSP | DOI (10.1007/s10009-015-0377-y) | Link to FDR3: a parallel refinement checker for CSP
-
[171]
The expressiveness of CSP with priority
A.W. Roscoe
In Proceedings of MFPS 2015. 2015.
Details about The expressiveness of CSP with priority | BibTeX data for The expressiveness of CSP with priority | Download (pdf) of The expressiveness of CSP with priority
-
[172]
Detecting failed attacks on human−interactive security protocols
A.W. Roscoe
2016.
Details about Detecting failed attacks on human−interactive security protocols | BibTeX data for Detecting failed attacks on human−interactive security protocols | Download (pdf) of Detecting failed attacks on human−interactive security protocols
-
[173]
Computing maximal weak and other bisimulations
Alexandre Boulgakov‚ Thomas Gibson−Robinson and A.W. Roscoe
2016.
Details about Computing maximal weak and other bisimulations | BibTeX data for Computing maximal weak and other bisimulations | Download (pdf) of Computing maximal weak and other bisimulations
-
[174]
Efficient deadlock−freedom checking using local analysis and SAT solving
Pedro Antonino‚ Thomas Gibson−Robinson and A.W. Roscoe
In Proceedings of IFM. 2016.
Details about Efficient deadlock−freedom checking using local analysis and SAT solving | BibTeX data for Efficient deadlock−freedom checking using local analysis and SAT solving | Download (pdf) of Efficient deadlock−freedom checking using local analysis and SAT solving
-
[175]
Reducing complex CSP models to traces via priority
David Mestel and A.W. Roscoe
In Proceedings of MFPS 2016. 2016.
Details about Reducing complex CSP models to traces via priority | BibTeX data for Reducing complex CSP models to traces via priority | Download (pdf) of Reducing complex CSP models to traces via priority
-
[176]
Rigorous development of component−based systems using component metadata and patterns
A. Mota M.V.M. Oliviera P. Antonino R. Ramos A.Sampaio and A.W. Roscoe
In Formal Aspects of Computing. 2016.
Details about Rigorous development of component−based systems using component metadata and patterns | BibTeX data for Rigorous development of component−based systems using component metadata and patterns | Link to Rigorous development of component−based systems using component metadata and patterns
-
[177]
The relationship between CSP‚ FDR and Buchi Automata
A.W. Roscoe and Thomas Gibson−Robinson
2016.
Details about The relationship between CSP‚ FDR and Buchi Automata | BibTeX data for The relationship between CSP‚ FDR and Buchi Automata | Download (pdf) of The relationship between CSP‚ FDR and Buchi Automata
-
[178]
Tighter reachability criteria for deadlock freedom analysis
Pedro Antonino‚ Thomas Gibson−Robinson and A.W. Roscoe
2016.
Details about Tighter reachability criteria for deadlock freedom analysis | BibTeX data for Tighter reachability criteria for deadlock freedom analysis | Download (pdf) of Tighter reachability criteria for deadlock freedom analysis
-
[179]
Card games as pointer structures: case studies in mobile CSP modelling
A.W. Roscoe
2016.
Details about Card games as pointer structures: case studies in mobile CSP modelling | BibTeX data for Card games as pointer structures: case studies in mobile CSP modelling | Download patience.tar of Card games as pointer structures: case studies in mobile CSP modelling | Download cards1.pdf of Card games as pointer structures: case studies in mobile CSP modelling
-
[180]
Auditable PAKEs: approaching fair exchange without a TTP
A.W. Roscoe and P.Y.A. Ryan
2017.
Details about Auditable PAKEs: approaching fair exchange without a TTP | BibTeX data for Auditable PAKEs: approaching fair exchange without a TTP | Download (pdf) of Auditable PAKEs: approaching fair exchange without a TTP
-
[181]
The automatic detection of token structures and invariants using SAT checking
Pedro Antonino‚ Thomas Gibson−Robinson and A.W. Roscoe
2017.
Details about The automatic detection of token structures and invariants using SAT checking | BibTeX data for The automatic detection of token structures and invariants using SAT checking | Download (pdf) of The automatic detection of token structures and invariants using SAT checking | Link to The automatic detection of token structures and invariants using SAT checking
-
[182]
Checking static properties using conservative approximations to reachability
Pedro Antonino‚ Thomas Gibson−Robinson and A.W. Roscoe
2017.
Details about Checking static properties using conservative approximations to reachability | BibTeX data for Checking static properties using conservative approximations to reachability | Download of Checking static properties using conservative approximations to reachability
-
[183]
Temporal signature (Draft)
A.W. Roscoe
2017.
Details about Temporal signature (Draft) | BibTeX data for Temporal signature (Draft) | Download (pdf) of Temporal signature (Draft)
-
[184]
A proof of entropy minimisation for outputs in deletion channels via hidden word statistics
Peter YA Ryan Arash Atashpendar David Mestel A.W. Roscoe
2018.
Details about A proof of entropy minimisation for outputs in deletion channels via hidden word statistics | BibTeX data for A proof of entropy minimisation for outputs in deletion channels via hidden word statistics | Download (pdf) of A proof of entropy minimisation for outputs in deletion channels via hidden word statistics
-
[185]
From clustering super sequences to entropy minimising subsequences for single and double deletions
Peter YA Ryan Arash Atashpendar Marc Beunardeau Aisling Conolly Remi Geraud David Mestel A.W. Roscoe
2018.
Details about From clustering super sequences to entropy minimising subsequences for single and double deletions | BibTeX data for From clustering super sequences to entropy minimising subsequences for single and double deletions | Link to From clustering super sequences to entropy minimising subsequences for single and double deletions
-
[186]
Proceedings of FM 2018
Details about Proceedings of FM 2018 | BibTeX data for Proceedings of FM 2018 | Link to Proceedings of FM 2018
-
[187]
Process algebra and model checking
A.W. Roscoe Rance Cleaveland and Scott Smolka
2018.
Details about Process algebra and model checking | BibTeX data for Process algebra and model checking | Link to Process algebra and model checking
-
[188]
Reguard: finding reentrancy bugs in smart contracts
B. Chen C. Liu H. Liu Z. Cao. Z. Chen and A.W. Roscoe
2018.
Details about Reguard: finding reentrancy bugs in smart contracts | BibTeX data for Reguard: finding reentrancy bugs in smart contracts | Link to Reguard: finding reentrancy bugs in smart contracts
-
[189]
Efficient verification of concurrent systems using local analysis based approximations and SAT solving
T. Gibson−Robinson P Antonino and A.W. Roscoe
Vol. 31. 2019.
Details about Efficient verification of concurrent systems using local analysis based approximations and SAT solving | BibTeX data for Efficient verification of concurrent systems using local analysis based approximations and SAT solving | Link to Efficient verification of concurrent systems using local analysis based approximations and SAT solving
-
[190]
Key agreement via protocols
A.W. Roscoe and Wang Lei
2019.
Details about Key agreement via protocols | BibTeX data for Key agreement via protocols | Link to Key agreement via protocols
-
[191]
Efficient verification of concurrent systems using synchronisation analysis and SAT/SMT solving
T. Gibson−Robinson P Antonino and A.W. Roscoe
In ACM Transactions on Software Engineering Methods. Vol. 18. 2019.
Details about Efficient verification of concurrent systems using synchronisation analysis and SAT/SMT solving | BibTeX data for Efficient verification of concurrent systems using synchronisation analysis and SAT/SMT solving | Link to Efficient verification of concurrent systems using synchronisation analysis and SAT/SMT solving
-
[192]
Formalising and verifying smart contracts with Solidifier: a bounded model checker for Solidity
P Antonino and A.W. Roscoe
2020.
Details about Formalising and verifying smart contracts with Solidifier: a bounded model checker for Solidity | BibTeX data for Formalising and verifying smart contracts with Solidifier: a bounded model checker for Solidity | Link to Formalising and verifying smart contracts with Solidifier: a bounded model checker for Solidity
-
[193]
Translating between models of concurrency
D. Mestel and A.W. Roscoe
In Acta Informatica. 2020.
Details about Translating between models of concurrency | BibTeX data for Translating between models of concurrency | Download modshifcsp.tar of Translating between models of concurrency | Download modshif-ult.pdf of Translating between models of concurrency
-
[194]
Neural Network Security: Hiding CNN Parameters with Guided Grad−CAM
Linda Guiga and A.W. Roscoe
2020.
Details about Neural Network Security: Hiding CNN Parameters with Guided Grad−CAM | BibTeX data for Neural Network Security: Hiding CNN Parameters with Guided Grad−CAM | Download (pdf) of Neural Network Security: Hiding CNN Parameters with Guided Grad−CAM
-
[195]
Solidifer: bounded model checking Solidity using lazy contract deployment and precise memory modelling
Pedro Antonino and A.W. Roscoe
In Symposium on Applied Computing (SAC) 2021. 2021.
Details about Solidifer: bounded model checking Solidity using lazy contract deployment and precise memory modelling | BibTeX data for Solidifer: bounded model checking Solidity using lazy contract deployment and precise memory modelling | Download (pdf) of Solidifer: bounded model checking Solidity using lazy contract deployment and precise memory modelling
-
[196]
Partially fair computation from timed release encryption and oblivious transfer
Geoffroy Couteau‚ PYA Ryan and A.W. Roscoe
2021.
Details about Partially fair computation from timed release encryption and oblivious transfer | BibTeX data for Partially fair computation from timed release encryption and oblivious transfer | Link to Partially fair computation from timed release encryption and oblivious transfer
-
[197]
CSP: a practical process algebra
S.D. Brookes and A.W. Roscoe
2021.
Details about CSP: a practical process algebra | BibTeX data for CSP: a practical process algebra | Download (pdf) of CSP: a practical process algebra