Skip to main content
University of Oxford Department of Computer Science
  Contact Us     Search  
  1. Home
  2. About Us
  3. People
  4. Emeritus Faculty
  5. Bill Roscoe

Bill Roscoe

Personal photo - Bill Roscoe

Professor Bill Roscoe FREng

Emeritus Professor

Senior Research Fellow, University College

Themes:

Completed Projects:

Interests

Research areas

  1. Concurrency: this is the study of how systems interact by communication when operating in parallel. Most of my work is done on the process algebra CSP (or Communicating Sequential Processes) originally introduced by Tony Hoare. This is a relatively mature area (I have worked on it since beginning my own doctoral work in 1978) but it still throws up new surprises and insights: for example relatively recently I discovered ways to prove that some of the models that have been studied for many years are in some sense Platonic: they underly every possible model. The work I do under this category is largely theoretical, but it underpins many of the more practical topics below. My work on CSP divides into two parts: the original untimed CSP where we worry about the order of events but not about exactly when they each happen, and timed versions such as Timed CSP, which I developed with Mike Reed and has a continuous time model, and various discrete models.
  2. Verification: this is the study of how to prove that systems meet their specification, and these days is almost always done or much assisted by verification tools: programs that analyse other programs, usually comparing them against some specification. Most of my own work in this area is based on, or related to, CSP and its refinement checker FDR (see below). My work on verification breaks down into actually doing practical verification and developing methods that make it easier or more powerful. I've enjoyed working with industry over the years to help them with specific verifications, especially inmos (in former times) and QinetiQ. I'm interested in induction, data independence, their combination, and similar ideas to help generalise verification (and in particular model checking) from something that can only be done for a very specific system to something that can prove results about classes of them.   
  3. FDR  (standing for Failures Divergence Refinement) is a verification tool for CSP. What it primarily does is discover if one CSP program refines another, namely has less possible observations that can be made of it. Thus refinement essentially coincides with reduction of nondeterminism. FDR is a model checker, but an unusual one because it concentrates on refinement. It has a wide user base in academia, government and industry, both as a tool in itself and also as the "back end" to others. I have led its design since it was first written in 1991. We recently had funding from EPSRC to look, amongst other things, at how we can include modern model checking ideas such as SAT checking into it: for results see paper 150. I am interested in improving how FDR works, in developing ways of using it effectively (for example on real-time systems), and in finding ways of verifying non-CSP notations such as Statecharts with it.  A current interest is investigating what types of language can, in principle, be translated into CSP (see paper 125)    We have relatively recently added Timed CSP into FDR, giving its role in modelling real-time systems a new impetus: see papers 145, 149, 150. More recently,  improved versions of this called FDR3 and FDR4  were released, developed mainly by Tom Gibson-Robinson.  Our group is actively exploring how to make FDR more efficient, giving it new capabilities and finding new ways of applying it.
  4. SVA  is a front end for FDR that analyses shared variable programs, developed by me and David Hopkins.  It is described in Chapters 18 and 19 of Understanding Concurrent Systems.
  5. Computer Security: I became interested in this in the mid 1990's when I saw the successes other people were having applying the ideas of CSP. I work on three different topics in security. Noninterference is the study of how information might either leak, or be shown not to leak, from one user to another across a computer system. Understanding this is a real challenge and is perhaps the most convincing application of the finer theoretical details of concurrency theory: it is very easy to come up with convincing looking specifications of noninterference that are wrong. I concentrate on the idea that a system S is free of information leakage from A to B if, after suitably abstracting A's behaviour in S, the resulting view (B's) is either deterministic or perhaps maximally refined. I have two big goals in this area: finding a way of expressing noninterference elegantly for stochastic systems (the main desideratum being a model that mixes nondeterminism and probability at the right level of abstraction) and finding real practical applications for our noninterference work - it can readily be checked on FDR. Cryptographic protocol analysis is the study of how to analyse protocols that use cryptography to achieve results like key exchange, authentication and secure e-commerce. We do not study the mathematical details of the underlying cryptography, which is modelled symbolically. Gavin Lowe realised in 1994 that these protocols could be modelled and analysed on FDR and, ever since then, he, I and our co-workers have developed and refined these techniques to the point where they are now robust and widely applicable. A spin-off of this work my development of protocols and related cryptography for bootstrapping ad hoc networks. Here we develop methods for securely building secure networks between pairs or larger groups of systems based not on traditional methods such as PKIs, but on a minimum of non-fakable human interaction (either just human-machine, or a mixture of human-machine and human-human).  Applications of this include medical data exchange, secure telephony and improved credit card security: see below.  Principles derived from this work have recently enabled us to develop more efficient forms of cryptographic signature.  This novel view of how to do authentication leads to a new cryptographic primitive: the keyed digest function.  I am interested in discovering more about these and developing them so they can be computed efficiently and confidently.  I have recently shown how to make this and another style of protocol (PAKEs) auditable in the sense that participants in a failed run can discover whether they were being attacked or not.  This in turn has led me to study fair exchange.  These and other recent work of mine on security has been based on applying variations on delay, or time-lock, encryption, in which information is not accessible until some measure of time has passed.  
    A theme running through much of me security work over the past two decades has been how to replace and supplement authentication technology based on names (i.e. PKIs) by more flexible authentication ideas based on context. 

 

In the past I've also worked on general topology, digital topology and hardware verification, but these are not current areas.

I enjoy collaborating with industry, particularly users of my own research. 

External Interests and entrepreneurship

In January 2017 I took partial retirement from Oxford, and as of 1 August 2020 am a 40% employee of Oxford. I set up Chieftin Lab in Shenzhen, China and latterly the University College Oxford Blockchain Research Centre.    These are associated with the UK company The Blockhouse Technology zLtd (TBTL.) I work on areas such as blockchain, fintech, regtech (the automation of laws and regulations) and post-quantum security at these.   I am dedicated to creating distributed trust without the disaster that is Proof of Work or anything else that wastes resources.

i lead the Digital Civilisation initiative in collaboration with colleagues in Hainan, China and elsewhere, seeking to create a sciety with minimal boundaries and universal standards.  

Cocotec was spun out of Oxford by Philippa Hopcroft, Tom Gibson-Robinson, Guy Broadfoot and me in 2018.  The four of us had ideas about technology for developing verified event-based software using a new model based technology.  We obtained funding for these ideasas hrough EPSRC and the Aerospace Technology Institute  in partnership with Innovate UK.  The verification engine  behind  the  resulting  Coco  System  is  based  on  ideas  and  theory related  to  CSP  and  FDR.  It  is  based  on  a remarkably effective compositional verification technique that allows it to create and verify event-based software systems with hundreds of thousands of lines of code.  Cocotec is now led full time by Tom and Philippa in Guildford.

Inspired by my ideas on contextual and multi-channel authentication, Chris Autry set up Iothic, a company with a radical new architecture fot IoT security.

 

Prospective Research Students

In principle I'm interested in taking on research students interested in any of these areas, but obviously I am likely to have some more specific projects in mind at any given moment. Please email me if you are interested in becoming my research student.

 

Understanding Concurrent Systems  

Published in October 2010 by Springer, this book provides an up-to-date introduction to CSP, its theory and applications, including the use of CSP to give semantics for, and generate tools for, other models of concurrent systems.

Biography

Bill Roscoe (Andrew William, hence A.W. Roscoe on papers) was born and brought up in Dundee, Scotland. He read Mathematics at University College, Oxford (Univ) 1975-78, obtaining the top mark for his year in the university. Together with another Univ student, Steve Brookes (now at CMU), he joined the Computing Laboratory (PRG) as a research student in 1978, and their DPhil work with Tony Hoare was on the mathematical foundations and models of his Communicating Sequential Processes (CSP) process algebra. Almost all Bill's subsequent research has either been based on CSP or has been a spin-off from it (examples of the latter being Hardware Verification and Computer Security). He was a Junior Research Fellow of St Edmund Hall 1980-3 and a Royal Society Research Fellow 1982-3. He became a College Lecturer at Univ in 1979 and a Tutorial Fellow there in 1983, when he was also appointed a University Lecturer in Computer Science at Oxford. He was given the title of Professor in 1997. In 2007 his job title was changed to "Research Professor" and he became a Senior Research Fellow at Univ. In 1993-7 he was Senior Tutor of Univ, in 1998-2000 he was the last ever Chairman of the Mathematical Sciences Faculty Board, and was Head of the Department of Computer Science (formerly called Director of the Computing Labratory) 2003-8 and 2009-14.

In January 2017 I took partial retirement from Oxford and now work part time there, and part time in other roles.

Selected Publications

View AllManage publications

Activities

Completed Projects

Past Students

Pedro Antonino
Sasha Boulgakov
Xin Huang
Jonathan Lawrence
Ivo Maffei
David Mestel
Hristina Palikareva
Jantje Silomon

About Us

Back to Top