Review report on EPSRC Grant GR/N24872
(01/10/2000 -- 30/09/2003)


Wide-area programming: Language, Semantics and Infrastructure Design

Peter Sewell, Robin Milner
http://www.cl.cam.ac.uk/users/{pes20,rm135}

1  Summary

This project draws together two major lines of research: the study of distributed system design and the semantic theory of concurrent processes and programming languages. Wide area distributed systems are becoming ubiquitous and critical. System designers require a clear understanding of their behaviour in the presence of partial failure, malicious attack, and, increasingly, mobility of hardware and software components. To support this, we are designing levels of abstraction for distributed programming with clear, rigorous semantics. During the period of this grant, we have focussed on the following aspects of distributed computation:

2  Programme of Work

The main items of work are described in turn below. The project structure is largely as originally envisaged; changes are discussed in §3.

Network Semantics: The TCP/UDP Semantics
The protocols UDP and TCP are ubiquitous, forming the basis of almost all communication on the Internet, above the IP internet protocol. UDP provides unreliable asynchronous messaging; TCP provides bidirectional streams, with retransmission and flow- and congestion-control. Both are normally used by application programs via the sockets API.

These protocols, and the API, involve many complexities, both contingent and intrinsic. They have been developed over the last 25 years, with some substantial incremental changes. There is no single definitive version; instead, there are many implementations which differ in subtle ways, but have been tuned to -- in the common cases -- interoperate successfully. Further, their behaviour is not well documented, even in informal prose. Some aspects are described in standards (e.g.POSIX), RFCs, and well-known texts (e.g.those of Stevens). However, while collectively these describe most common behaviour, they are not complete, nor completely correct -- for the whole, there is nothing better than reading the source code of the implementations that one is dealing with. This source is not always available. Where it is, it is emphatically not arranged for clarity -- instead, it is more-or-less optimised for performance, and embodies many historical artifacts arising from incremental change. Analysing the source to determine what the external behaviour is requires considerable expertise.

To support the production of reliable software using TCP and UDP sockets we must address these issues, understanding --with mathematical rigour-- both continuous and discrete properties: not only statistical properties of traffic, but also the precise interactions of API and network events within protocol implementations, the treatment of different kinds of failure, generation of errors, and so on. We need models of these that are precise (covering all important details, including implementation differences), accurate (faithful to the current deployed implementations), and also usable (as informal documentation by a wide audience, and as a basis for formal verification by specialists).

In this task we are developing such a formal model for UDP, TCP, and sockets. The model is based upon the available documentation in conjunction with the source code of the BSD reference implementation. Crucially, however, it is being experimentally validated against the most common implementations, checking that the specification accurately describes their behaviour. A key part of our work is the experimental discovery of differences in behaviour between these implementations.

Our formal semantics of UDP has been published [1, 2, 3, 4, 5]. The associated software library has been used by Leifer, at INRIA, in an implementation of failure detectors.

The UDP work, while of independent use, was essentially an initial trial, to develop tools and techniques. We then moved onto the much larger task of TCP, which is still in progress. The first draft of the TCP model is complete (some 14000 lines of HOL source, or 150 typeset pages). Much work has gone into untangling the historical accumulation of modification and extension, yielding a semantics that is (relatively) intelligible and clear as well as precise.

The models are expressed using operational semantics within the HOL theorem prover. This has allowed us to verify internal consistency, checking type-correctness of the model and doing machine-checked proof of various sanity properties. It is also key for our experimental validation: we have extended HOL with a special-purpose symbolic model-checker which we apply to our model in order to validate it against experimentally-captured traces.

These traces are generated on a test network with machines running three of the common implementations (Linux, FreeBSD, Windows XP). We have written a test harness that allows remote execution of system calls, remote white-box inspection of protocol state where possible, network packet injection, and network packet sniffing, all under the control of a test script; it also logs all events and generates a trace suitable for input to HOL.

At present we generate some 2625 traces, chosen to get good coverage of the model. A good fraction can already be processed by the HOL symbolic evaluator, but further work is required, both on the evaluator itself and on correcting the model in the light of its results, to ensure that it does include all the real-world behaviour. The large size of our model has also necessitated our making various improvements to the HOL system.

Once our formal model is complete and validated, we intend to prepare an annotated version for publication and dissemination. We expect this to be of use in several ways:
Expressing Infrastructure Layers: Module systems and Versioning
In this task we turn to programming language issues, looking at what is communicated, complementing the previous task's focus on how communication takes place.

High-level programming languages for distributed computation should allow arbitrary language values to be communicated; most flexibly, they should provide type-safe marshalling of arbitrary values to and from byte strings. There are many important issues, which have received little attention in the literature. In particular: (1) unmarshalling can involve rebinding to local resources; (2) values of abstract types can be communicated, and a globally-coherent notion of type equality is needed to ensure that unmarshalling respects abstraction; and (3) interoperation between separately-built programs with different versions of shared modules must be supported, with fine-grain version control.

In our early work here [6] (supported partly by this grant and partly by the overlapping GRL62290), we focussed on abstract types in the setting of an ML-like module system. We modelled separate compilation/linking and execution of programs that interact along typed channels. Interaction may involve communication of values of abstract types; we proposed some simple fine-grain versioning control of these types to support interoperation of old and new code. The system made use of a second-class module system, with singleton kinds to express type sharing, and a novel operational semantics for separate compilation/linking and execution. An implementation was produced as a student project.

Most programming languages adopt static binding, but for distributed programming an exclusive reliance on static binding is too restrictive: dynamic binding is required in various guises, eg when a marshalled value is received from the network, containing identifiers that must be rebound to local resources. Typically it is provided only by ad-hoc mechanisms that lack clean semantics. In [7] we developed core dynamic rebinding mechanisms as extensions to simply-typed call-by-value (CBV) lambda-calculus. To do so we first explored refinements of the CBV reduction strategy that delay instantiation, to ensure computations make use of the most recent versions of rebound definitions. We introduced redex-time and destruct-time strategies. The latter formed the basis for a lambda-mark calculus that supports dynamic rebinding of marshalled values, while remaining as far as possible statically-typed. We extended lambda-mark with concurrency and communication, giving examples showing how wrappers for encapsulating untrusted code can be expressed. Finally, we showed that a high-level semantics for dynamic updating can also be based on the destruct-time strategy, defining a lambda-update calculus with simple primitives to provide type-safe, dynamic updating of code. We have a direct implementation of the destruct-time lambda semantics, and are working on realistic compilation strategies. We thereby established primitives and a common semantic foundation for a variety of real-world dynamic rebinding requirements.

In [8, 9] we returned to the question of abstraction-preserving marshalling, addressing some pragmatic difficulties in the earlier proposal of [6]. Here we obtained a namespace for abstract types that is global, i.e.meaningful between programs, by hashing module definitions. We examined the scenarios in which values of abstract types are communicated from one program to another, and ensured, by constructing hashes appropriately, that the dynamic and static notions of type equality mirror one another. In many common cases this ensures marshalling/unmarshalling `just works' as one would wish, without the earlier need to propagate new-generated type names. Again we used singleton kinds to express abstraction in the static semantics; now abstraction is tracked in the dynamic semantics by coloured brackets. These allowed us to prove preservation, erasure, and coincidence results. We argued that our proposal is a good basis for extensions to existing ML-like languages, pragmatically straightforward for language users and for implementors.

In [10] we looked in more detail at dynamic update of running systems, e.g.telecomms switches that cannot afford lengthy restarts. One would like this to be possible in a semantically well-founded way, rather than by issuing binary patches. To this end, we defined a small update calculus with precise mathematical semantics, based on the redex-time lambda-calculus. It supports updating technology similar to that of the programming language Erlang. Here new versions of a module can be added to a running system, and there is fine-grain control for how execution changes over from old to new code. Work on a second update calculus, with updating of the implementations of abstract data types, reminiscent of the language Dynamic ML, is in progress, forming part of the thesis work of PhD student Gareth Stoyle.

In ongoing work we are considering the integration of marshalling constructs in the presence of both dynamic rebinding and abstract types, and also with rich languages of versions and version constraints. In a paper submitted for publication we discuss the (large!) design space and also describe an experimental language, Acute, which we are designing and implementing to carry out some more substantial experiments. As a further, internal, experiment, we are developing Acute above the FreshML of Pitts et al. It is itself an extension of a fragment of OCaml; a medium-to-long term goal is to integrate these constructs with the OCaml distribution; our close contacts with members of INRIA Rocquencourt (including Leifer, Peskine, and the OCaml development team) may make this feasible.

We have also considered the integration of lightweight XML support into a high-level concurrent language, with a simple type system that guarantees well-formedness but does not involve the complexity of systems for validity [11]. An implementation was produced as a student project.

Reasoning
As listed in the Network Semantics section above, semantic models of distributed systems have several applications, one of which is to support formal proof about higher-level abstractions. Such proofs, about executable code rather than idealisations, are still technically very challenging, so case studies are required to establish techniques and idioms.

Our initial work on UDP involved hand proof of properties of a simple heart-beat algorithm, expressed in an OCaml fragment for which we gave a pen-and-paper operational semantics. It is obviously desirable to be able to carry out such proofs within a mechanical proof assistant, to assure that none of the many cases are overlooked. To do so requires the programming language also to be embedded in the proof assistant, integrated with the network semantics. This is being worked on by Michael Compton, a PhD student in the Automated Reasoning Group. The UDP and language semantics have been set up, here using the Isabelle proof assistant (the UDP semantics being semi-automatically ported from HOL), and some properties established; work is ongoing.

For a larger example, we are working on coding the Chord P2P algorithm above the TCP semantics, adding the necessary concurrency primitives to Acute (which already has modules and a TCP library matching our specification).

Earlier work, proving the correctness of a communication infrastructure for mobile computation (providing high-level location-independent messaging between mobile computations, was completed in the first 18 months of this grant [12, 13]; supported partly by this grant and partly by the overlapping GRL62290.

Security Policy
Moving to a higher level of abstraction, flexible control of security policy is needed in large distributed systems. A number of rule- and role-based systems have been proposed, but there is an unresolved tension between expressiveness and tractability, and to our knowledge few large-scale realistic examples have been developed. Building on earlier work at Cambridge (the OASIS system) and elsewhere we have developed Cassandra, a language and system for expressing policy, and a substantial case study. We have developed a security policy for a national Electronic Health Record system, based on the requirements for the ongoing UK National Health Service procurement exercise. This is part of the thesis work of PhD student Moritz Becker.

Cassandrapolicies are expressed in a language based on Datalog with constraints. The expressiveness of the language (and its computational complexity) can be tuned by choosing an appropriate constraint domain. Cassandrais role-based; it supports credential-based access control (e.g.between administrative domains); and rules can refer to remote policies (for automatic credential retrieval and trust negotiation). Moreover, the policy language is small, and it has a formal semantics for query evaluation and for the access control engine.

For the case study we choose a constraint domain C0 that is sufficiently expressive to encode many policy idioms. The case study turns out to require many subtle variants of these; it is important to express this variety smoothly, rather than add them as ad hoc features. By ensuring only a constraint compact fragment of C0 is used, we guarantee a finite and computable fixed-point model. We use a top-down evaluation algorithm, for efficiency and to guarantee termination.

The case study (with some 310 rules and 58 roles) demonstrates that this language is expressive enough for a real-world application; preliminary implementation results suggest that the performance should be acceptable. A paper has been submitted for publication.

A journal version of earlier work on Securing Mobility was also completed during the project [14]; we are currently studying how to integrate such primitives, allowing encapsulation of untrusted code, with the Acute constructs for marshalling.

Anonymity and Privacy
In the last few years new desirable properties of distrubuted systems have been identified. One of these is massive scalability in the presence of failures; this has lead to the development of peer-to-peer systems. Others are anonymity and privacy against a variety of network adversaries. Indeed, anonymity systems which enable users to send anonymous email and do anonymous web browsing have been designed and implemented, many using mix networks. We have made substantial progress in identifying just how much anonymity these systems provide. This is the subject of Andrei Serjantov's PhD thesis work.

We developed a new metric for measuring anonymity, showed that our new metric is practical (can be calculated for real anonymity systems) and useful for comparing anonymity properties of various schemes [15]. This line of work was continued by looking at various known mixes and identifying some of their anonymity properties against active and passive attackers [16]. This work is directly relevant to deployed systems providing strongly anonymous email. This lead us to a design of a new mix with stronger properties which also adapts to the traffic load [17]. Finally, we devised a method for analysing anonymity properties of timed mixes [18]. More work along this general line of research is in progress; we have developed a model which enables us to assess the anonymity of an entire mix network (a complete system) rather than just its building blocks.

We have also examined the anonymity of real-time connection-based systems which enable anonymous web browsing. We showed in [19] that such systems currently provide no anonymity against some realistic threat models, but can be improved. Furthermore, we noted that contrary to popular opinion, peer-to-peer anonymity systems generally provide less anonymity against our threat mdoel than "classic" designs.

One further line of work is looking at how padding and rerouting improves the anonymity of systems [20]. Here we took a slightly different model, showing how to calculate anonymity and the extent to which padding and rerouting helps on simple examples. Finally, we noted that anonymity systems can be used as a building block to provide stronger censorship resistance [21].

Operational Theory
This task is a continuation of a preceding EPSRC project in Cambridge (investigators Robin Milner, Philippa Gardner and Peter Sewell) on theoretical models for distributed systems. Journal versions of earlier Operational Theory work were completed during the project: work on indexed models for interleaving and causal semantics of name-passing calculi [22]; and work on deriving bisimulation congruences from rewrite systems, without name-binding but with rewriting up to a monoidal parallel operator and with parametric rewrite rules [23].

Groundwork laid in these journal papers, and by a conference paper by Leifer and Milner in 2000, took the form of an original theory that allows a labelled transition system (LTS), and thereby also a variety of behavioural relations such as the failures preorder or bisimilarity, to be derived and analysed uniformly over a wide range of models. Moreover, the uniform method guarantees that these relations are congruential, i.e. they faithfully characterise the behaviour of agents in all possible contexts.

In the present project the emphasis has been to apply this work to models that express the /emphmobility of distributed systems in the widest possible sense of the word. This includes movement of physical interactive devices (mobile phones or hand-held computers), of software among mobile and fixed devices, of links (e.g. URLs) between hardware and software, and even reconfiguration and data-movement within a software system. The intention is that within the same frame one can model computing and communication, both microscopically and macroscopically.

In a series of papers [24, 25, 26, 27, 28, 29, 30, 31] the groundwork has been both refined abstractly and applied to a specific model, bigraphical reactive systems. Bigraphs are so called because they combine two different structures in a system: its placing (locality) and its linking connectivity. Mobility consists of reconfiguration of both structures. In the cited work, especially in the two long Technical Reports, it is shown that various previous concurrency models are representable, including both the Pi Calculus and the Ambient Calculus. The papers further show that significant parts of the Pi behavioural theory of the Pi Calculus are exactly recovered. Subsequent work (not published) will further investigate the representation of Ambients and of Petri Nets within the bigraph model. Thus the model aspires to cover as wide a range of distributed-system concepts as possible, while retaining a sharp and tractable theory.

Three PhD students have been involved in this work. The PhD dissertation of Leifer [29] was mostly done earlier, but completed within the project period. Ole-Hoegh Jensen is writing a dissertation on bigraphs for the Pi and Ambient Calculi, while Alistair Turnbull is working on a linear graphical calculus called Min, intended as a intemediate language/model for compilation of interactive languages such as Java.

Other
During the course of the project the PhD thesis of Keith Wansbrough, on Simple Polymorphic Usage Analysis was completed [32], as was a tutorial on the p-calculus and its applications [33].

3  Development

The project has developed much as in the original proposal. The main changes were: (1) emphasis shifted towards the Network Semantics task, as the value and scale of this work became apparent, and (2) the work on Anonymity and Privacy was added. In more detail:

The Network Semantics task has expanded substantially from the work envisaged in the initial proposal, where we considered only rather idealised process calculi, only loosely based on UDP and TCP and ignoring the sockets API. Shortly after beginning that work, it became clear that to really understand communication semantics in the presence of failure and attack it is necessary to examine more of the real-world detail, and indeed that a fully-validated model would be of much wider applicability.

Work on Module Systems and Versioning has also progressed further than originally envisaged, moving to an experimental implementation, integrating several of the required features.

In the original proposal more work on reasoning was envisaged. Our shift of goal in the Network Semantics section, from an idealised calculus to a real-world accurate and detailed model, has inevitably delayed the treatment of larger-scale reasoning examples; we hope to carry them out in the near future.

In the future we hope also to link the work on Security Policy to the lower-level Network Semantics models, reasoning about the behaviour of the distributed policy engine in the presence of failure. This link was envisaged in the original proposal, under Case Study: OASIS; as it has turned out we have looked at both Network Semantics and Policy in greater depth, but so far independently.

The task on Anonymity and Privacy was not part of the the original proposal; it arose as the thesis work of the project student (Andrei Serjantov) developed in this direction, from his early contributions to Network Semantics.

Finally, the original proposal contained a task Interworking and Implementation. Various implementation work has already been described; for the Module Systems and Versioning work it has been more fruitful --for the time being-- to study the problems in a clean setting rather that commit to interoperation with an existing language, with all the complexities of an existing (and limited) type system that that entails. We are, however, aiming to develop primitives that can eventually be smoothly integrated with existing ML/OCaml implementations.

4  Personnel

The original proposal was coauthored by Peter Sewell (PI), James Leifer, and Robin Milner (CI); it was intended to employ Leifer as a Research Associate. In the event, Leifer took up a position at INRIA Rocquencourt; as the publications indicate, there has been an active collaboration with him and with Gilles Peskine, a PhD student there.

Keith Wansbrough has been employed as an RA for the duration of the project, working on many aspects. Alistair Turnbull was also employed part-time for 6 months, working on operational theory. Andrei Serjantov was supported by the project studentship, initially working on Network Semantics but then turning to the foundations of Anonymity and Privacy. PhD students Gareth Stoyle and Moritz Becker have also contributed substantially to this work, looking respectively at programming language design for dynamic update and at security policy, and Michael Compton, a PhD student in the automated reasoning group, has begun work on reasoning above the UDP model. Two undergraduate interns, Vilhelm Sjöberg and Christian Steinrücken, were supported during the summer of 2003 to work on the early stages of the Acute implementation.

Other collaborators include Gavin Bierman (University of Cambridge), Michael Norrish (National ICT Australia (NICTA), Canberra research lab), Michael Hicks (University of Maryland, College Park), Ole Jensen (Aalborg University), George Danezis (University of Cambridge), Claudia Diaz (K.U.Leuven ESAT-COSIC, Leuven-Heverlee, Belgium), Richard Newman (CISE Department, University of Florida, Gainesville, FL), Ira Moskowitz (Naval Research Laboratory Washington, DC), Paul Syverson (Naval Research Laboratory Washington, DC), and Gian Luca Cattani (University of Cambridge and DS Data Systems).

5  Wider contribution

Sewell was an invited speaker at a joint EPSRC/DTI Outreach seminar, and has served on the programme committees for the FWAN workshop (Foundations of Wide-Area Languages), EXPRESS 02, EXPRESS 03, POPL 04, and ICFP 04. Milner gave invited talks at POPL01, ICATPN01 (Petri Nets), ICGT02 (Graph Rewriting), and a short course on Bigraphs at the Advanced Course on Petri Nets, Eichstätt, September 03.


Review report on EPSRC Grant GR/N24872
(01/10/2000 -- 30/09/2003)


Wide-area programming: Language, Semantics and Infrastructure Design

List of Publications

The five publications identified as particularly significant are [4, 7, 8, 14, 28], indicated by a below.

References

[1]
Andrei Serjantov, Peter Sewell, and Keith Wansbrough. The UDP calculus: Rigorous semantics for real networking. Technical Report 515, Computer Laboratory, University of Cambridge, July 2001. iv+70pp. Technical Report.

[2]
Andrei Serjantov, Peter Sewell, and Keith Wansbrough. The UDP calculus: Rigorous semantics for real networking. In Proceedings of TACS 2001: Theoretical Aspects of Computer Software (Sendai), LNCS 2215, pages 535--559, October 2001. Conference; Refereed.

[3]
Peter Sewell, Keith Wansbrough, and Michael Norrish. Timing UDP: The HOL model. Available from http://www.cl.cam.ac.uk/users/pes20/Netsem/index.html, July 2001. Software.

[4]
Keith Wansbrough, Michael Norrish, Peter Sewell, and Andrei Serjantov. Timing UDP: mechanized semantics for sockets, threads and failures. In Proceedings of ESOP 2002: European Symposium on Programming (Grenoble) LNCS 2305, pages 278--294, April 2002. Conference; Refereed; .

[5]
Michael Norrish, Peter Sewell, and Keith Wansbrough. Rigour is good for you, and feasible: reflections on formal treatments of C and UDP sockets. In Proceedings of 10th ACM SIGOPS European Workshop (Saint-Emilion), pages 49--53, September 2002. Conference; Refereed.

[6]
Peter Sewell. Modules, abstract types, and distributed versioning. In Proceedings of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (London), pages 236--247, January 2001. Conference; Refereed.

[7]
Gavin Bierman, Michael Hicks, Peter Sewell, Gareth Stoyle, and Keith Wansbrough. Dynamic rebinding for marshalling and update, with destruct-time lambda. In Proc. ICFP 2003: the 8th International Conference on Functional Programming, August 2003. Conference; Refereed; Int. Co-author; .

[8]
James Leifer, Gilles Peskine, Peter Sewell, and Keith Wansbrough. Global abstraction-safe marshalling with hash types. In Proc. ICFP 2003: the 8th International Conference on Functional Programming, August 2003. Conference; Refereed; Int. Co-author; .

[9]
James Leifer, Gilles Peskine, Peter Sewell, and Keith Wansbrough. Global abstraction-safe marshalling with hash types. Technical Report UCAM-CL-TR-569, University of Cambridge Computer Laboratory, June 2003. Also published as INRIA Rocquencourt report RR-4851. Technical Report; Int. Co-author.

[10]
Gavin Bierman, Michael Hicks, Peter Sewell, and Gareth Stoyle. Formalizing dynamic software updating. In Proceedings of USE 2003: the Second International Workshop on Unanticipated Software Evolution, April 2003. Conference; Refereed; Int. Co-author.

[11]
G. M. Bierman and P. Sewell. Iota: A concurrent XML scripting language with applications to home area networking. Technical Report 557, Computer Laboratory, University of Cambridge, January 2003. 32pp. Technical Report.

[12]
Asis Unyapoth and Peter Sewell. Nomadic Pict: Correct communication infrastructure for mobile computation. In Proceedings of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (London), pages 116--127, January 2001. Conference, Refereed.

[13]
Asis Unyapoth. Nomadic Pi Calculi: Expressing and Verifying Infrastructure for Mobile Computation. PhD thesis, Computer Laboratory, University of Cambridge, June 2001. Published as Technical Report 514. PhD Dissertation.

[14]
Peter Sewell and Jan Vitek. Secure composition of untrusted code: Box-p, wrappers and causality types. Journal of Computer Security, 11(2):135--188, 2003. Journal; Refereed; Int. Co-author; .

[15]
Andrei Serjantov and George Danezis. Towards an information theoretic metric for anonymity. In Paul Syverson and Roger Dingledine, editors, Privacy Enhancing Technologies, volume 2482 of LNCS, San Francisco, CA, April 2002. Conference; Refereed.

[16]
Andrei Serjantov, Roger Dingledine, and Paul Syverson. From a trickle to a flood: Active attacks on several mix types. In Fabien Petitcolas, editor, 5th Workshop on Information Hiding, volume 2578 of LNCS, pages 36--52. Springer-Verlag, October 2002. Conference; Refereed; Int. Co-author.

[17]
Claudia Diaz and Andrei Serjantov. Generalising mixes. In Roger Dingledine, editor, Proc. PET 2003: the 3rd Privacy Enhancing Technologies workshop. Springer-Verlag, LNCS 2760, March 2003. Conference; Refereed; Int. Co-author.

[18]
Andrei Serjantov and Richard E. Newman. On the anonymity of timed pool mixes. In Security and Privacy in the Age of Uncertainty, pages 427--434, Athens, Greece, May 2003. Kluwer. (Workshop on Privacy and Anonymity Issues in Networked and Distributed Systems) Conference; Refereed; Int. Co-author.

[19]
Andrei Serjantov and Peter Sewell. Passive attack analysis for connection-based anonymity systems. In Proc. ESORICS 2003: the 8th European Symposium on Research in Computer Security, LNCS 2808, October 2003. Conference; Refereed.

[20]
Richard E. Newman, Ira S. Moskowitz, Paul Syverson, and Andrei Serjantov. Metrics for traffic analysis prevention. In Roger Dingledine, editor, Proc. PET 2003: the 3rd Privacy Enhancing Technologies workshop. Springer-Verlag, LNCS 2760, March 2003. Conference; Refereed; Int. Co-author.

[21]
Andrei Serjantov. Anonymizing censorship resistant systems. In Proc. IPTPS: the 1st International Peer To Peer Systems Workshop, March 2002. Conference; Refereed.

[22]
Gian Luca Cattani and Peter Sewell. Models for name-passing processes: Interleaving and causal. Information and Computation, page 55pp. Accepted for publication. Journal; Refereed.

[23]
Peter Sewell. From rewrite rules to bisimulation congruences. Theoretical Computer Science, 274(1--2):183--230, March 2002. Journal; Refereed.

[24]
R. Milner. Computational flux. In Proc. 28th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pages 220--221, 2001. Conference, Invited Paper.

[25]
R. Milner. The flux of interaction. In Proc. 22nd International Conference on Application and Theory of Petri Nets, pages 19--22, 2001. Conference, Invited Paper.

[26]
R. Milner. Bigraphical reactive systems. In CONCUR 2001 -- Concurrency Theory, Proc. 12th International Conference, LNCS2154, pages 16--35, 2001. Conference, Invited Paper.

[27]
R. Milner. Bigraphs as a model for mobile interaction. In ICGT 2002, First International Conference on Graph Transformation, LNCS2505, pages 8--13, 2002. Conference, Invited Paper.

[28]
O.-H. Jensen and R. Milner. Bigraphs and transitions. In Proc 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), page 16pp, 2003. Conference; Refereed; .

[29]
J. Leifer. Operational congruences for reactive systems. Technical Report 521, University of Cambridge Computer Laboratory, 2001. PhD Dissertation.

[30]
R. Milner. Bigraphical reactive systems: basic theory. Technical Report 523, University of Cambridge Computer Laboratory, September 2001. 87pp, Technical Report.

[31]
O.-H. Jensen and R. Milner. Bigraphs and mobile processes. Technical Report 570, University of Cambridge Computer Laboratory, July 2003. 121pp, Technical Report.

[32]
Keith Wansbrough. Simple Polymorphic Usage Analysis. PhD thesis, Computer Laboratory, University of Cambridge, 2002. PhD Dissertation.

[33]
Peter Sewell. Chapter 9, Pi Calculus, in the book Formal Methods for Distributed Processing, A Survey of Object Oriented Approaches, edited by Howard Bowman and John Derrick, December 2001. Book Chapter.

This document was translated from LATEX by HEVEA.