·
Cryptographic Verification by
Typing for a Sample Protocol Implementation. C. Fournet and K.
Bhargavan. In **Foundations of Security
Analysis and Design VI (FOSAD),** Bertinoro,
2010. Springer LNCS, 2011.

Type systems are effective tools for verifying the security of cryptographic
protocols and implementations. They provide automation, modularity and
scalability, and have been applied to large protocols. In this tutorial, we illustrate the use of
types for verifying authenticity properties, first using a symbolic model of
cryptography, then relying on a concrete computational assumption. We introduce
refinement types (that is, types carrying formulas to record invariants) for
programs written in F# and verified by F7, an SMT-based type checker. We
describe a sample authenticated RPC protocol, we implement it in F#, and we
specify its security against active adversaries. We develop a sample symbolic
library, we present its main cryptographic invariants, and we show that our RPC
implementation is perfectly secure when linked to this symbolic library. We
implement the same library using concrete cryptographic primitives, we make a
standard computational assumption, and we show that our RPC implementation is
also secure with overwhelming probability when linked to this concrete library.

- Extracting
and Verifying Cryptographic Models from C Protocol Code by Symbolic
Execution. With M.
Aizatulin and J. Jürjens. To appear at CCS 2011. Available on arXiv, July 2011.

Consider the problem of verifying security properties of a cryptographic protocol coded in C. We propose an automatic solution that needs neither a pre-existing protocol description nor manual inspection of source code. First, symbolically execute the C program to obtain symbolic expressions for the network message sent by the protocol. Second, apply algebraic rewriting to obtain a process calculus description. Third, run an existing protocol analyzer (ProVerif) to prove security properties or find attacks. We formalize our algorithm and appeal to existing results for ProVerif to establish computational soundness. We analyze only a single execution path, so our results are limited to protocols with no significant branching. The results in this paper provide the first computationally sound verification of weak secrecy and authentication for (single execution paths of) C code.

- Guiding
a General-Purpose C Verifier to Prove Cryptographic Protocols. With F. Dupressoir, J. Jürjens, and D.
Naumann. In
**24th IEEE Computer Security Foundations Symposium (CSF 2011)**, pages 1-17, Cernay-la-Ville, June 27-29, 2011. IEEE Computer Society. An extended version appears as Technical Report MSR-TR-2010-50, Microsoft Research, May 2011.

We describe, for the first time, how to verify security properties of C code for cryptographic protocols by using a general-purpose verifier. We prove security theorems in the symbolic model of cryptography. Our techniques include: use of ghost state to attach formal algebraic terms to concrete byte arrays and to detect collisions when two distinct terms map to the same byte array; decoration of a crypto API with contracts based on symbolic terms; and expression of the attacker model in terms of C programs. We rely on the general-purpose verifier VCC; we guide VCC to prove security simply by writing suitable header files and annotations in implementation files, rather than by changing VCC itself. We formalize the symbolic model in Coq in order to justify the addition of axioms to VCC.

- Maintaining
Database Integrity with Refinement Types. With I. Baltopoulos and J. Borgström. To
appear in ECOOP 2011.

Given recent advances in automated theorem proving, we present a new method for determining whether database transactions preserve integrity constraints. The constraints we consider are check constraints and referential-integrity constraints---extracted from SQL table declarations---and application-level invariants expressed as formulas of first-order logic. Our motivation is to use static analysis of database transactions as an alternative to costly runtime integrity checks. We work in the setting of a functional multi-tier language, where functional code is compiled to SQL in order to query and update a relational database. We use refinement types (types qualified by logical formulas) to track constraints on data and the underlying state of the database; our static analysis of transactional code uses a refinement-type checker, which relies on recent highly efficient SMT algorithms to check proof obligations. Our method is based on a list-processing semantics for an SQL fragment within the functional language, and is illustrated by a series of programming examples. Our analysis could be applied either at the time of code development, to catch bugs early, or later at the time of deployment on the database server, to allow only integrity-preserving stored procedures to be accepted.

- Measure Transformer Semantics for Bayesian Machine
Learning. With J. Borgström, M. Greenberg, J. Margetson, and J.
Van Gael. In
**European Symposium on Programming (ESOP 2011)**, Saarbruecken, March 30-April 1, 2011. Springer LNCS 6602:77-96, 2011. An extended version appears as Technical Report MSR-TR-2011-18, Microsoft Research, July 2011.

The Bayesian
approach to machine learning amounts to inferring posterior distributions of
random variables from a probabilistic model of how the variables are related
(that is, a prior distribution) and a set of observations of variables. There is a trend in machine learning towards
expressing Bayesian models as probabilistic programs. As a foundation for this kind of programming,
we propose a core functional calculus with primitives for sampling prior
distributions and observing variables.
We define combinators for distribution
transformers, based on theorems in measure theory, and use these to give a
rigorous semantics to our core calculus. The original features of our semantics
include its support for discrete, continuous, and hybrid distributions, and
observations of zero-probability events.
We compile our core language to a small imperative language that in
addition to the distribution transformer semantics also has a straightforward semantics
via factor graphs, data structures that enable many efficient inference
algorithms. We then use an existing
inference engine for efficient approximate inference of posterior marginal
distributions, treating thousands of observations per second for large
instances of realistic models.

- Robin Milner 1934 -
2010: Verification, Languages, and Concurrency With R. Harper, J. Harrison,
A. Jeffrey, and P. Sewell. In
**Principles of Programming Languages (POPL 2011)**, p473.

A special session
of the symposium pays tribute to Robin Milner; the session features talks by
Robert Harper (Carnegie Mellon University), John Harrison (Intel), and Alan
Jeffrey (Bell Labs), and is organised by Andrew D. Gordon (Microsoft Research)
and Peter Sewell (University of Cambridge).

- Semantic
subtyping with an SMT solver. With G. M. Bierman, C.
Hriţcu, and D. Langworthy. In
**ACM SIGPLAN International Conference on Functional Programming**, Baltimore, September 27-29, 2010. Pages 105-116. ACM Press. An extended version appears as Technical Report MSR-TR-2010-99, Microsoft Research, December 2010. The Dminor project has a binary release and a readme (including some sample code).

We study a first-order functional language with the novel combination of the ideas of refinement type (the subset of a type to satisfy a Boolean expression) and type-test (a Boolean expression testing whether a value belongs to a type). Our core calculus can express a rich variety of typing idioms; for example, intersection, union, negation, singleton, nullable, variant, and algebraic types are all derivable. We formulate a semantics in which expressions denote terms, and types are interpreted as first-order logic formulas. Subtyping is defined as valid implication between the semantics of types. The formulas are interpreted in a specific model that we axiomatize using standard first-order theories. On this basis, we present a novel type-checking algorithm able to eliminate many dynamic tests and to detect many errors statically. The key idea is to rely on an SMT solver to compute subtyping efficiently. Moreover, using an SMT solver allows us to show the uniqueness of normal forms for non-deterministic expressions, to provide precise counterexamples when type-checking fails, to detect empty types, and to compute instances of types statically and at run-time.

- Programming Languages and Systems: 19th European
Symposium on Programming, ESOP 2010. Held as Part of the Joint European Conferences
on Theory and Practice of Software, ETAPS 2010, Paphos,
Cyprus, March 20-28, 2010.
Editor. Springer LNCS 6012. ISBN 978-3-642-11956-9.

- Modular
Verification of Security Protocol Code by Typing. With K. Bhargavan and
C. Fournet. In
**ACM SIGPLAN Principles of Programming Languages**, Madrid, January 17-23, 2010. Pages 445-456. ACM Press. A draft technical report is available, December 2010.

We propose a method for verifying the security of protocol implementations. Our method is based on declaring and enforcing invariants on the usage of cryptography. To this end, we develop cryptographic libraries that embed a logic model of their cryptographic structures, and specify pre- and post-conditions on their functions so as to maintain their invariants. We present a theory to justify the soundness of modular code verification via our method. We implement the method for protocols coded in F# and verified using F7, our SMT-based typechecker for refinement types, that is, types including formulas to record invariants. As illustrated by a series of programming examples, our method can flexibly deal with a range of different cryptographic constructions and protocols. We evaluate the method on a series of larger case studies of protocol code, previously checked using a whole-program analysis based on ProVerif, a leading verifier for cryptographic protocols. Our results indicate that compositional verification by typechecking with refinement types is more scalable than the best domain-specific analysis currently available for cryptographic code.

- Principles and
Applications of Refinement Types. With C. Fournet. In
**International Summer School Logics and Languages for Reliability and Security**, Marktoberdorf, August, 2009. Technical Report MSR-TR-2009-147, Microsoft Research, October 2009. Updated December 2010.

A refinement type {x:T|C} is the subset of the type T consisting of the values x to satisfy the formula C. In these tutorial notes we explain the principles of refinement types by developing from first principles a concurrent lambda-calculus whose type system supports refinement types. Moreover, we describe a series of applications of our refined type theory and of related systems.

- A Compositional Theory
for STM Haskell.
With J. Borgstroem and K. Bhargavan. In
**ACM SIGPLAN Haskell Symposium**, Edinburgh, September 3, 2009. Pages 69-80. ACM Press.

We address the problem of reasoning about Haskell programs that use Software Transactional Memory (STM). As a motivating example, we consider Haskell code for a concurrent non-deterministic tree rewriting algorithm implementing the operational semantics of the ambient calculus. The core of our theory is a uniform model, in the spirit of process calculi, of the run-time state of multi-threaded STM Haskell programs. The model was designed to simplify both local and compositional reasoning about STM programs. A single reduction relation captures both pure functional computations and also effectful computations in the STM and I/O monads. We state and prove liveness, soundness, completeness, safety, and termination properties relating source processes and their Haskell implementation. Our proof exploits various ideas from concurrency theory, such as the bisimulation technique, but in the setting of a widely used programming language rather than an abstract process calculus. Additionally, we develop an equational theory for reasoning about STM Haskell programs, and establish for the first time equations conjectured by the designers of STM Haskell. We conclude that using a pure functional language extended with STM facilitates reasoning about concurrent implementation code.

- Roles, Stacks,
Histories: A Triple for Hoare. With J. Borgstroem and R. Pucella. In C.B. Jones,
A.W. Roscoe, K.R. Wood (Eds),
**Reflections on the Work of C.A.R. Hoare**, pages 71-100. Springer, 2010. An extended version of this paper appears as Technical Report MSR-TR-2009-97, Microsoft Research, November 2009. A journal version of this paper appears in**Journal of Functional Programming**21(2):159—207, 2011.

Behavioural type and effect systems regulate properties such as adherence to object and communication protocols, dynamic security policies, avoidance of race conditions, and many others. Typically, each system is based on some specific syntax of constraints, and is checked with an ad hoc solver. Instead, we advocate types refined with first-order logic formulas as a basis for behavioural type systems, and general purpose automated theorem provers as an effective means of checking programs. In particular, we describe a triple of security-related type systems: for stack inspection, for history-based access control, and for role-based access control. The three are all instances of a refined state monad. Our semantics allows a precise comparison of the similarities and differences of these mechanisms. Moreover, the benefit of behavioural type-checking is to rule out the possibility of unexpected security exceptions, a common problem with code-based access control.

- Towards a Verified Reference Implementation of a
Trusted Platform Module.
With Aybek Mukhamedov
and Mark Ryan. In
**Seventeenth International Workshop on Security Protocols**, Cambridge, April 1-3, 2009. Springer LNCS, to appear.

We develop a reference implementation for a fragment of the API for a Trusted Platform Module. Our code is written in a functional language, suitable for verification with various tools, but is automatically translated to a subset of C, suitable for interoperability testing with production code, and for inclusion in a specification or standard for the API. One version of our code corresponds to the widely deployed TPM 1.2 specification, and is vulnerable to a recently discovered dictionary attack; verification of secrecy properties of this version fails producing an attack trace and highlights an ambiguity in the specification that has security implications. Another version of our code corresponds to a suggested amendment to the TPM 1.2 specification; verification of this version succeeds. From this case study we conclude that recent advances in tools for verifying implementation code for cryptographic APIs are reaching the point where it is viable to develop verified reference implementations. Moreover, the published code can be in a widely understood language like C, rather than one of the specialist formalisms aimed at modelling cryptographic protocols.

- Secure Compilation of a
Multi-Tier Web Language. With I. Baltopoulos. In
**ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI 2009)**, Savannah, Georgia, January 24, 2009. ACM Press. Pages 27-38.

Storing state in the client tier (in forms or cookies, for example) improves the efficiency of a web application, but it also renders the secrecy and integrity of stored data vulnerable to untrustworthy clients. We study this general problem in the context of the Links multi-tier programming language. Like other systems, Links stores unencrypted application data, including web continuations, on the client tier; hence, Links is open to attacks that expose secrets, and modify control flow and application data. We characterise these attacks as failures of the general principle that ecurity properties of multi-tier applications should follow from review of the source code (as opposed to the detailed study of the files compiled for each tier, for example). We eliminate these threats by augmenting the Links compiler to encrypt and authenticate any data stored on the client. We model this compilation strategy as a translation from a core fragment of the language to a concurrent lambda-calculus equipped with a formal representation of cryptography. To formalize source-level reasoning about Links programs, we define a type-and-effect system for our core language; our implementation can machine-check various integrity properties of the source code. By appeal to a recent system of refinement types for secure implementations, we show that our compilation strategy guarantees all the properties provable by our type-and-effect system.

- Code-carrying
authorization.
With S. Maffeis, M. Abadi, and C. Fournet. In
**13th European Symposium on Research in Computer Security (ESORICS 2008)**, Malaga, October 6-8, 2008. Springer LNCS 5283:563-579 (DOI).

In authorization, there is often a wish to shift the burden of proof to those making requests, since they may have more resources and more specific knowledge to construct the required proofs. We introduce an extreme instance of this approach, which we call Code-Carrying Authorization (CCA). With CCA, access-control decisions can partly be delegated to untrusted code obtained at run-time. The dynamic verification of this code ensures the safety of authorization decisions. We define and study this approach in the setting of a higher-order spi calculus. The type system of this calculus provides the needed support for static and dynamic verification.

- Type inference for
correspondence types. With H. Huettel and R.
Rydhof Hansen. In
**6th International Workshop on Security Issues in Concurrency (SecCo 2008)**, Toronto, August 23, 2008.

We present a type and effect system for proving correspondence assertions in a pi-calculus with polarized channels, dependent pair types and effect terms. Given a process P and a type environment E, we describe how to generate constraints that are formulae in the Alternating Least Fixed-Point (ALFP) logic. A reasonable model of the generated constraints yields a type and effect assignment such that P becomes well-typed with respect to E if and only if this is possible. The formulae generated satisfy a finite model property; a system of constraints is satisfiable if and only if it has a finite model. As a consequence, we obtain the result that type and effect inference in our system is polynomial-time decidable.

- Refinement
types for secure implementations. With J. Bengtson, K.
Bhargavan, C. Fournet, and S. Maffeis. In
**20th IEEE Computer Security Foundations Symposium (CSF 2008)**, pages 17-32, Pittsburgh, Pennsylvania, June 23-25, 2008. IEEE Computer Society. An extended version of this paper appears as Technical Report MSR-TR-2008-118, Microsoft Research, September 2008. Updated February 2010 and November 2010. A journal version appears ACM TOPLAS 33(2):8 (2011).

We present the design and implementation of a typechecker for verifying security properties of the source code of cryptographic protocols and access control mechanisms. The underlying type theory is a lambda-calculus equipped with refinement types for expressing pre- and post-conditions within first-order logic. We derive formal cryptographic primitives and represent active adversaries within the type theory. Well-typed programs enjoy assertion-based security properties, with respect to a realistic threat model including key compromise. The implementation amounts to an enhanced typechecker for the general purpose functional language F#; typechecking generates verification conditions that are passed to an SMT solver. We describe a series of checked examples. This is the first tool to verify authentication properties of cryptographic protocols by typechecking their source code.

- Service combinators for farming virtual
machines.
With K. Bhargavan and I. Narasamdya. In
**COORDINATION 2008**, Oslo, June 4-6, 2008. Springer LNCS 5052:33-49. An extended version of this paper appears as Technical Report MSR-TR-2007-165, Microsoft Research, December 2007.

Management is one of the main expenses of running the server farms that implement enterprise services, and operator errors can be costly. Our goal is to develop type-safe programming mechanisms for combining and managing enterprise services, and we achieve this goal in the particular setting of farms of virtual machines. We assume each server is service-oriented, in the sense that the services it provides, and the external services it depends upon, are explicitly described in metadata. We describe the design, implementation, and formal semantics of a library of combinators whose types record and respect server metadata. We describe a series of programming examples run on our implementation, based on existing server code for order processing, a typical data centre workload.

- Getting operations logic right: types,
service-orientation, and static analysis. With K. Bhargavan.
Position paper for the Workshop on The Rise and Rise of the
Declarative Datacentre, MSR Cambridge, May 12-13, 2008.

The human operators of datacentres work from a manual, sometimes known as the run book, that lists how to perform operating procedures such as the provisioning, deployment, monitoring, and upgrading of servers. To improve failure and recovery rates, it is attractive to replace human intervention by software, known as operations logic, that automates such operating procedures. We advocate a declarative programming model for operations logic, and the use of static analysis to detect programming errors, such as the potential for misconfiguration.

- The Rise and Rise of the
Declarative Datacentre. Co-editor with K. Bhargavan, T. Harris, and P. Toft.
Appears as Technical
Report TR-2008-61, Microsoft Research, May
2008. Position Papers from the Workshop on The
Rise and Rise of the Declarative Datacentre, MSR Cambridge, May 12-13,
2008.
- Verified implementations
of the Information Card federated identity-management protocol.
In
**ACM Symposium on Information, Computer and Communication Security (ASIACCS '08)**, Tokyo, March 18-20, 2008. With K. Bhargavan, C. Fournet, and N. Swamy.

We describe reference implementations for
selected configurations of the user authentication protocol defined by the *Information
Card Profile V1.0*. Our code can interoperate with existing implementations
of the client, identity provider, and relying party roles of the protocol. We
derive formal proofs of security properties for our code using an automated
theorem prover. Hence, we obtain the most substantial examples of verified
implementations of cryptographic protocols to date, and the first for any federated
identity-management protocols. Moreover, we present a tool that downloads
security policies from services and token servers and compiles them to a
verifiably secure client proxy.

- A
chart semantics for the
pi-calculus. With J. Borgstroem and A. Phillips. In
**14th International Workshop on Expressiveness in Concurrency (EXPRESS 2007)**, Electronic Notes in Theoretical Computer Science 194(2):3-29 (January 2008).

We present a graphical semantics for the pi-calculus, that is easier to visualize and better suited to expressing causality and temporal properties than conventional relational semantics. A pi-chart is a finite directed acyclic graph recording a computation in the pi-calculus. Each node represents a process, and each edge either represents a computation step, or a message-passing interaction. Pi-charts enjoy a natural pictorial representation, akin to message sequence charts, in which vertical edges represent control flow and horizontal edges represent data flow based on message passing. A pi-chart represents a single computation starting from its top (the nodes with no ancestors) to its bottom (the nodes with no descendants). Unlike conventional reductions or transitions, the edges in a pi-chart induce ancestry and other causal relations on processes. We give both compositional and operational definitions of pi-charts, and illustrate the additional expressivity afforded by the chart semantics via a series of examples, including secrecy properties and usage bounds guaranteed by a type system.

- A
type discipline for authorization in distributed systems. With C. Fournet and S.
Maffeis. In
**20th IEEE Computer Security Foundations Symposium (CSF 2007)**, pages 31-48, Venice, July 6-8, 2007. IEEE Computer Society.

We consider the problem of statically verifying
the conformance of the code of a system to an explicit authorization policy. In
a distributed setting, some part of the system may be compromised, that is,
some nodes of the system and their security credentials may be under the
control of an attacker. To help predict and bound the impact of such partial
compromise, we advocate logic-based policies that explicitly record
dependencies between principals. We propose a conformance criterion, *safety
despite compromised principals*, such that an invalid authorization decision
at an uncompromised node can arise only when nodes on which the decision
logically depends are compromised. We formalize this criterion in the setting
of a process calculus, and present a verification technique based on a type
system. Hence, we can verify policy conformance of code that uses a wide range
of the security mechanisms found in distributed systems, ranging from secure
channels down to cryptographic primitives, including secure hashes, encryption,
and public-key signatures.

- Design
and Semantics of a Decentralised Authorization Language. With M. Becker and C.
Fournet. In
**20th IEEE Computer Security Foundations Symposium (CSF 2007)**, pages 3-15, Venice, July 6-8, 2007. IEEE Computer Society. An extended version of this paper appears as Technical Report MSR-TR-2006-120, Microsoft Research, September 2006. A journal version appears in**Journal of Computer Security**18(4):597-643 (2010).

We present a declarative authorization language that strikes a careful balance between syntactic and semantic simplicity, policy expressiveness, and execution efficiency. The syntax is close to natural language, and the semantics consists of just three deduction rules. The language can express many common policy idioms using constraints, controlled delegation, recursive predicates, and negated queries. We describe an execution strategy based on translation to Datalog with Constraints, and table-based resolution. We show that this execution strategy is sound, complete, and always terminates, despite recursion and negation, as long as simple syntactic conditions are met.

- Verified
reference implementations of WS-Security protocols.
With K. Bhargavan and C. Fournet. In
**3rd International Workshop on Web Services and Formal Methods (WS-FM 2006)**, Vienna, September 8-9, 2006.

We describe a new reference implementation of the web services security specifications. The implementation is structured as a library in the functional programming language F#. Applications written using this library can interoperate with other compliant web services, such as those written using Microsoft WSE and WCF frameworks. Moreover, the security of such applications can be automatically verified by translating them to the applied pi calculus and using an automated theorem prover. We illustrate the use of our reference implementation through examples drawn from the sample applications included with WSE and WCF. We formally verify their security properties. We also experimentally evaluate their interoperability and performance.

- Provable implementations
of security protocols. In
**Twenty First Annual IEEE Symposium on Logic in Computer Science (LICS 2006)**, pages 345-346, Seattle, August 12-15, 2006. Invited paper.

Proving cryptographic security protocols has been a challenge ever since Needham and Schroeder threw down the gauntlet in their pioneering 1978 paper on authentication protocols: "The need for techniques to verify the correctness of such protocols is great, and we encourage those interested in such problems to consider this area." By now, there is a wide range of informal and formal methods that can catch most design errors. Still, as in other areas of software, the trouble is that while practitioners are typically happy for researchers to write formal models of their natural language specifications and to apply design principles, they are reluctant to do so themselves. In practice, specifications tend to be partial and ambiguous, and the implementation code is the closest we get to a formal description of most protocols. This motivates the subject of my talk: the relatively new enterprise of adapting formal methods for security protocols to work on code instead of abstract models. The goal is to lower the practical cost of security protocol verification by eliminating the need to write a separate formal model. I will describe current tools that partially address the problem, and discuss what remains to be done.

- Verified interoperable
implementations of security protocols. With K. Bhargavan, C.
Fournet, and S. Tse. In
**19th IEEE Computer Security Foundations Workshop (CSFW 2006)**, pages 139-152, Venice, July 5-7, 2006. IEEE Computer Society.

We present an architecture and tools for verifying implementations of security protocols. Our implementations can run with both concrete and symbolic cryptographic libraries. The concrete implementation is for production and interoperability testing. The symbolic implementation is for debugging and formal verification. We develop our approach for protocols written in F#, a dialect of ML, and verify them by compilation to ProVerif, a resolution-based theorem prover for cryptographic protocols. We establish the correctness of this compilation scheme, and we illustrate our approach with protocols for Web Services security.

- Policy Advisor for WSE
3.0.
With K. Bhargavan and C. Fournet. In
**Web Service Security: Scenarios, patterns, and implementation guidance for Web Services Enhancements (WSE) 3.0**. Pages 324-330. Microsoft Press, 2006. [Amazon] [MSDN] - An advisor for web
services security policies. With K. Bhargavan, C. Fournet, and G. O'Shea. In
**2005 ACM Workshop on Secure Web Services (SWS 2005)**, Fairfax, VA, USA. Pages 1-9. ACM Press, 2005.

We identify common security vulnerabilities found during security reviews of web services with policy-driven security. We describe the design of an advisor for web services security configurations, the first tool both to identify such vulnerabilities automatically and to offer remedial advice. We report on its implementation as a plugin for Microsoft Web Services Enhancements (WSE).

- Algebraic
Process Calculi: The First Twenty Five Years and Beyond. Co-editor with L. Aceto. Short Contributions from the Workshop on Algebraic Process Calculi:
The First Twenty Five Years and Beyond (PA-05), Bertinoro,
Forlì, Italy, August 1-5, 2005. BRICS Note
NS-05-03. Also appears as Volume
162, pages 1-340 of Electronic
Notes in Theoretical Computer Science.
- Secrecy despite
compromise: types, cryptography, and the pi-calculus. With A. Jeffrey. In
**CONCUR'05**, Springer LNCS, 3653:186-201, 2005.

A realistic threat model for cryptographic protocols or for language-based security should include a dynamically growing population of principals (or security levels), some of which may be compromised, that is, come under the control of the adversary. We explore such a threat model within a pi-calculus. A new process construct records the ordering between security levels, including the possibility of compromise. Another expresses the expectation of conditional secrecy of a message - that a particular message is unknown to the adversary unless particular levels are compromised. Our main technical contribution is the first system of secrecy types for a process calculus to support multiple, dynamically-generated security levels, together with the controlled compromise or downgrading of security levels. A series of examples illustrates the effectiveness of the type system in proving secrecy of messages, including dynamically-generated messages. It also demonstrates the improvement over prior work obtained by including a security ordering in the type system. Perhaps surprisingly, the soundness proof for our type system for symbolic cryptography is via a simple translation into a core typed pi-calculus, with no need to take symbolic cryptography as primitive.

- Foundations of Software
Science and Computation Structures. Editor.
**Theoretical Computer Science**333:1-2, March 2005.

- A
type discipline for authorization policies. With C. Fournet and S.
Maffeis. In
**European Symposium on Programming (ESOP 2005),**Springer LNCS 3444:141-156, 2005. An extended version of this paper appears as Technical Report MSR-TR-2003-83, Microsoft Research, September 2005. A journal version appears in**ACM Transactions on Programming Languages and Systems**29(5) (August 2007).

Distributed systems and applications are often expected to enforce high-level authorization policies. To this end, the code for these systems relies on lower-level security mechanisms such as, for instance, digital signatures, local ACLs, and encrypted communications. In principle, authorization specifications can be separated from code and carefully audited. Logic programs, in particular, can express policies in a simple, abstract manner. For a given authorization policy, we consider the problem of checking whether a cryptographic implementation complies with the policy. We formalize authorization policies by embedding logical predicates and queries within a spi-calculus. This embedding is new, simple, and general; it allows us to treat logic programs as specifications of code using secure channels, cryptography, or a combination. Moreover, we propose a new dependent type system for verifying such implementations against their policies. Using Datalog as an authorization logic, we show how to type several examples using policies and present a general schema for compiling policies.

- Secure sessions for web
services. With K. Bhargavan, R. Corin, and C. Fournet. In
**2004 ACM Workshop on Secure Web Services (SWS 2004)**, Washington DC. ACM Press, 2004.

WS-Security provides basic means to secure SOAP
traffic, one envelope at a time. For typical web services, however, using WS-Security
independently for each message is rather inefficient; besides, it is often
important to secure the integrity of a whole session, as well as each
message. To these ends, recent specifications provide further SOAP-level
mechanisms. WS-SecureConversation introduces *security
contexts*, which can be used to secure sessions between two parties.
WS-Trust specifies how security contexts are issued and obtained. We
develop a semantics for the main mechanisms of
WS-Trust and WS-SecureConversation, expressed as a
library for TulaFale, a formal scripting language for
security protocols. We model typical protocols relying on these
mechanisms, and automatically prove their main security properties. We
also informally discuss some limitations of these specifications.

- Verifying policy-based security for web services. With K. Bhargavan and
C. Fournet. In
**2004 ACM Conference on Computer and Communication Security (CCS 2004),**pages 268-277, Washington DC. ACM Press, 2004. An extended version of this paper appears as Technical Report MSR-TR-2004-84, Microsoft Research, November 2005.

WS-SecurityPolicy is a declarative configuration language for driving web services security mechanisms. We describe a formal semantics for WS-SecurityPolicy, and propose a more abstract link language for specifying the security goals of web services and their clients. Hence, we present the architecture and implementation of fully automatic tools that (1) compile policy files from link specifications, and (2) verify by invoking a theorem prover whether a set of policy files run by any number of senders and receivers correctly implements the goals of a link specification, in spite of active attackers. Policy-driven web services implementations are prone to the usual subtle vulnerabilities associated with cryptographic protocols; our tools help prevent such vulnerabilities, as we can verify policies when first compiled from link specifications, and also re-verify policies against their original goals after any modifications during deployment.

- TulaFale:
A security tool for web services. With K. Bhargavan, C.
Fournet, and R. Pucella. In
**Formal Methods for Components and Objects (FMCO 2003),**Springer LNCS 3188:197-222, 2004.

Web services security specifications are typically expressed as a mixture of XML schemas, example messages, and narrative explanations. We propose a new specification language for writing complementary machine-checkable descriptions of SOAP-based security protocols and their properties. Our TulaFale language is based on the pi calculus (for writing collections of SOAP processors running in parallel), plus XML syntax (to express SOAP messaging), logical predicates (to construct and filter SOAP messages), and correspondence assertions (to specify authentication goals of protocols). Our implementation compiles TulaFale into the applied pi calculus, and then runs Blanchet's resolution-based protocol verifier. Hence, we can automatically verify authentication properties of SOAP protocols.

- From Stack Inspection to Access Control: A Security
Analysis for Libraries. With F. Besson, T. Blanc, and C. Fournet. In
**17th IEEE Computer Security Foundations Workshop (CSFW 2004)**, pages 61-75, Pacific Grove, June 28-30, 2004. IEEE Computer Society.

We present a new static analysis to help identify security defects in class libraries for runtimes, such as JVMs or the CLR, that rely on stack inspection for access control. Our tool inputs a set of class libraries plus a description of the permissions granted to unknown, potentially hostile code. It constructs a permission-sensitive call graph, which can be queried to identify potential defects. We describe the tool architecture, various examples of security queries, and a practical implementation that analyses large pre-existing libraries for the CLR. We also develop a new formal model of the essentials of access control in the CLR (types, classes and inheritance, access modifiers, permissions, and stack inspection). In this model, we state and prove the correctness of the analysis.

- A semantics for web
services authentication. With K. Bhargavan and
C. Fournet. In
**Conference Record of POPL 2004 The 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages**, pages 198-209, ACM Press, 2004. An extended version of this paper appears as Technical Report MSR-TR-2003-83, Microsoft Research, February 2004. A journal version appears in**Theoretical Computer Science**340(1):102-153 (June 2005).

We consider the problem of specifying and verifying cryptographic security protocols for XML web services. The security specification WS-Security describes a range of XML security tokens, such as username tokens, public-key certificates, and digital signature blocks, amounting to a flexible vocabulary for expressing protocols. To describe the syntax of these tokens, we extend the usual XML data model with symbolic representations of cryptographic values. We use predicates on this data model to describe the semantics of security tokens and of sample protocols distributed with the WSE implementation of WS-Security. By embedding our data model within Abadi and Fournet's applied pi calculus, we formulate and prove security properties with respect to the standard Dolev-Yao threat model. Moreover, we informally discuss issues not addressed by the formal model. To the best of our knowledge, this is the first approach to the specification and verification of security protocols based on a faithful account of the XML wire format.

- Foundations
of Software Science and Computational Structures, 6th International
Conference, FOSSACS 2003. Held as Part of the Joint European Conferences
on Theory and Practice of Software, ETAPS 2003. Warsaw, Poland,
April 2003. Editor. Springer LNCS 2620. ISBN 3-540-00897-7.

- Deciding validity in a
spatial logic for trees With C. Calcagno and L. Cardelli. In the
proceedings of the
**ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI)**, pages 62-73, January 18, 2003, New Orleans, USA. An extended version of this paper appears as Technical Report MSR-TR-2002-113, Microsoft Research, December 2002. A journal version appears in**Journal of Functional Programming**15:543-572 (2005).

We consider a propositional spatial logic for finite trees. The logic includes A|B (spatial composition), and A|>B (the implication induced by composition), and 0 (the unit of composition). We show that the satisfaction and validity problems are equivalent, and decidable. The crux of the argument is devising a finite enumeration of trees to consider when deciding whether a spatial implication is satisfied. We introduce a sequent calculus for the logic, and show it to be sound and complete with respect to an interpretation in terms of satisfaction. Finally, we describe a complete proof procedure for the sequent calculus. We envisage applications in the area of logic-based type systems for semistructured data. We describe a small programming language based on this idea.

- Validating a web service
security abstraction by typing With R.
Pucella. In the proceedings of the
**2002 ACM Workshop on XML Security**, pages 18-29, November 22, 2002, Fairfax VA, USA. An extended version of this paper appears as Technical Report MSR-TR-2002-108, Microsoft Research, December 2002. A journal version appears in**Formal Aspects of Computing**17:277-318, 2005.

An XML web service is, to a first approximation, an RPC service in which requests and responses are encoded in XML as SOAP envelopes, and transported over HTTP. We consider the problem of authenticating requests and responses at the SOAP-level, rather than relying on transport-level security. We propose a security abstraction, inspired by earlier work on secure RPC, in which the methods exported by a web service are annotated with one of three security levels: none, authenticated, or both authenticated and encrypted. We model our abstraction as an object calculus with primitives for defining and calling web services. We describe the semantics of our object calculus by translating to a lower-level language with primitives for message passing and cryptography. To validate our semantics, we embed correspondence assertions that specify the correct authentication of requests and responses. By appeal to the type theory for cryptographic protocols of Gordon and Jeffrey's Cryptyc, we verify the correspondence assertions simply by typing. Finally, we describe an implementation of our semantics via custom SOAP headers.

- Typing One-to-One and
One-to-Many Correspondences in Security Protocols With A. Jeffrey. In
**Software Security - Theories and Systems (ISSS 2002),**Springer LNCS 2609:263-282, 2002.

Both one-to-one and one-to-many correspondences between events, sometimes known as injective and non-injective agreements, respectively, are widely used to specify correctness properties of cryptographic protocols. In earlier work, we showed how to typecheck one-to-one correspondences for protocols expressed in the spi-calculus. We present a new type and effect system able to verify both one-to-one and one-to-many correspondences.

- Automating type
soundness proofs via decision procedures and guided reductions With D.
Syme. In the
**9th International Conference on Logic for Programming Artificial Intelligence and Reasoning**, Springer LNCS 2514:418-434.

Operational models of fragments of the Java Virtual Machine and the .NET Common Language Runtime have been the focus of considerable study in recent years, and of particular interest have been specifications and machine-checked proofs of type soundness. In this paper we aim to increase the level of automation used when checking type soundness for these formalizations. We present a semi-automated technique for reducing a range of type soundness problems to a form that can be automatically checked using a decidable first-order theory. Deciding problems within this fragment is exponential in theory but is often efficient in practice, and the time required for proof checking can be controlled by further hints from the user. We have applied this technique to two case studies, both of which are type soundness properties for subsets of the .NET Common Language Runtime. These case studies have in turn aided us in our informal analysis of that system.

- Types and effects for
asymmetric cryptographic protocols With A.
Jeffrey. In
**15th IEEE Computer Security Foundations Workshop (CSFW 2002)**, pages 77-91, Cape Breton, June 24-26, 2002. IEEE Computer Society. An extended version of this paper appears as Technical Report MSR-TR-2002-31, Microsoft Research, August 2002.

We present the first type and effect system for
proving authenticity properties of security protocols based on asymmetric cryptography.
The most significant new features of our type system are: (1) a separation of *public
types* (for data possibly sent to the opponent) from *tainted types*
(for data possibly received from the opponent) via a subtype relation; (2) *trust
effects*, to guarantee that tainted data does not, in fact, originate from
the opponent; and (3) *challenge/response types* to support a variety of
idioms used to guarantee message freshness. We illustrate the applicability of
our system via protocol examples.

- Finite-control mobile ambients With W. Charatonik and J.-M. Talbot. In
**European Symposium on Programming (ESOP 2002),**Springer LNCS 2305:295-313, 2002.

We define a finite-control fragment of the ambient calculus, a formalism for describing distributed and mobile computations. A series of examples demonstrates the expressiveness of our fragment. In particular, we encode the choice-free, finite-control, synchronous p-calculus. We present an algorithm for model checking this fragment against the ambient logic (without composition adjunct). This is the first proposal of a model checking algorithm for ambients to deal with recursively-defined, possibly nonterminating, processes. Moreover, we show that the problem is PSPACE-complete, like other fragments considered in the literature. Finite-control versions of other process calculi are obtained via various syntactic restrictions. Instead, we rely on a novel type system that bounds the number of active ambients and outputs in a process; any typable process has only a finite number of derivatives.

- Stack Inspection:
Theory and Variants. With C. Fournet. In
**Conference Record of POPL 2002 The 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages**, pages 307-318, ACM Press, 2002. An extended version of this paper appears as Technical Report MSR-TR-2001-103, Microsoft Research, December 2001. A journal version appears in**ACM Transactions on Programming Languages and Systems**25(3):360-399 (May 2003).

Stack inspection is a security mechanism implemented in runtimes such as the JVM and the CLR to accommodate components with diverse levels of trust. Although stack inspection enables the fine-grained expression of access control policies, it has rather a complex and subtle semantics. We present a formal semantics and an equational theory to explain how stack inspection affects program behaviour and code optimisations. We discuss the security properties enforced by stack inspection, and also consider variants with stronger, simpler properties.

- Types for the Ambient
Calculus With L. Cardelli and G. Ghelli. In
**Information and Computation**177:160-194 (2002). Collects material from papers presented at POPL99, ICALP'99, and TCS 2000.

The ambient calculus is a concurrent calculus
where the unifying notion of `ambient' is used to model many different
constructs for distributed and mobile computation. We study a type system
that describes several properties of ambient behavior.
The type system allows ambients to be partitioned in
disjoint sets (*groups*), according to the intended design of a system, in
order to specify both the communication and the mobility behavior
of ambients.

- Notes on nominal calculi
for security and mobility In R. Focardi, R. Gorrieri (eds.),
**Foundations of Security Analysis and Design**, pages 262-330, Springer LNCS 2171, 2002. Slides for the lectures at the Bertinoro summer school, September 18-30, 2000, are available here.

There is great interest in applying nominal calculi---computational formalisms that include dynamic name generation---to the problems of programming, specifying, and verifying secure and mobile computations. These notes introduce three nominal calculi---the pi calculus, the spi calculus, and the ambient calculus. We describe some typical techniques, and survey related work.

- Authenticity by typing
for security protocols With A. Jeffrey. In
**14th IEEE Computer Security Foundations Workshop (CSFW 2001)**, pages 145-159, Cape Breton, June 11-13, 2001. IEEE Computer Society.**Journal of Computer Security**11(4):451-521, 2003.

We propose a new method to check authenticity properties of cryptographic protocols. First, code up the protocol in the spi-calculus of Abadi and Gordon. Second, specify authenticity properties by annotating the code with correspondence assertions in the style of Woo and Lam. Third, figure out types for the keys, nonces, and messages of the protocol. Fourth, check that the spi-calculus code is well-typed according to a novel type and effect system presented in this paper. Our main theorem guarantees that any well-typed protocol is robustly safe, that is, its correspondence assertions are true in the presence of any opponent expressible in spi. It is feasible to apply this method by hand to several well-known cryptographic protocols. It requires little human effort per protocol, puts no bound on the size of the opponent, and requires no state space enumeration. Moreover, the types for protocol data provide some intuitive explanation of how the protocol works. This paper describes our method and gives some simple examples. Our method has led us to the independent rediscovery of flaws in existing protocols and to the design of improved protocols.

- Typing correspondence
assertions for communication protocols With A.
Jeffrey. In
**Seventeenth Conference on the Mathematical Foundations of Programming Semantics (MFPS 2001)**,**Preliminary Proceedings of the 17th Conference on the Mathematical Foundations of Programming Semantics (MFPS 17)**, Aarhus, May 24-27, 2001. BRICS Notes Series NS-01-2, May 2001, pages 99-120.**Theoretical Computer Science**300(2003):379-409.

Woo and Lam propose correspondence assertions for specifying authenticity properties of security protocols. The only prior work on checking correspondence assertions depends on model-checking and is limited to finite-state systems. We propose a dependent type and effect system for checking correspondence assertions. Since it is based on type-checking, our method is not limited to finite-state systems. This paper presents our system in the simple and general setting of the p-calculus. We show how to type-check correctness properties of example communication protocols based on secure channels.

- Logical properties of name restriction With L.
Cardelli. In
**Typed Lambda Calculi and Applications (TLCA'01),**Springer LNCS 2044:46-60, 2001*.*

We extend the modal logic of ambients to the full ambient calculus, including name restriction. We introduce logical operators that can be used to make assertions about restricted names, and we study their properties.

- The complexity of model
checking mobile ambients With W. Charatonik, S. Dal Zilio, S.
Mukhopadhyay, and J.-M. Talbot. In
**Foundations of Software Science and Computation Structures (FoSSaCS 2001),**Springer LNCS 2030:152-167, 2001*.***Theoretical Computer Science**308(2003):277-331.

We settle the complexity bounds of the model checking problem for the replication-free ambient calculus with public names against the ambient logic without parallel adjunct. We show that the problem is PSPACE-complete. For the complexity upper-bound, we devise a new representation of processes that remains of polynomial size during process execution; this allows us to keep the model checking procedure in polynomial space. Moreover, we prove PSPACE-hardness of the problem for several quite simple fragments of the calculus and the logic; this suggests that there are no interesting fragments with polynomial-time model checking algorithms.

- Typing a multilanguage
intermediate code. With D. Syme. In
**Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages**, ACM Press, pages 248-260, 2001. An extended version of this paper appears as Technical Report MSR-TR-2000-106, Microsoft Research, December 2000.

The Microsoft .NET Framework is a new computing architecture designed to support a variety of distributed applications and web-based services. .NET software components are typically distributed in an object-oriented intermediate language, Microsoft IL, executed by the Microsoft Common Language Runtime. To allow convenient multi-language working, IL supports a wide variety of high-level language constructs, including class-based objects, inheritance, garbage collection, and a security mechanism based on type safe execution. This paper precisely describes the type system for a substantial fragment of IL that includes several novel features: certain objects may be allocated either on the heap or on the stack; those on the stack may be boxed onto the heap, and those on the heap may be unboxed onto the stack; methods may receive arguments and return results via typed pointers, which can reference both the stack and the heap, including the interiors of objects on the heap. We present a formal semantics for the fragment. Our typing rules determine well-typed IL instruction sequences that can be assembled and executed. Of particular interest are rules to ensure no pointer into the stack outlives its target. Our main theorem asserts type safety, that well-typed programs in our IL fragment do not lead to untrapped execution errors. Our main theorem does not directly apply to the product. Still, the formal system of this paper is an abstraction of informal and executable specifications we wrote for the full product during its development. Our informal specification became the basis of the product team's working specification of type-checking. The process of writing this specification, deploying the executable specification as a test oracle, and applying theorem proving techniques, helped us identify several security critical bugs during development.

- A
commitment relation for the ambient calculus
With L. Cardelli. Note, 2000.

We present a commitment relation, a kind of labeled transition system, for the ambient calculus. This note is an extract from an unpublished annex to our original article on the ambient calculus.

- Region analysis and a p-calculus with groups With S. Dal Zilio. In
**Proceedings of MFCS 2000: the 25th International Symposium on Mathematical Foundations of Computer Science, August 28-September 1, 2000, Bratislava, Slovak Republic**, Springer LNCS 1893:1-20, 2000.**Journal of Functional Programming**12(3):229-292 (May 2002).

We show that the typed region calculus of Tofte and Talpin can be encoded in a typed p-calculus equipped with name groups and a novel effect analysis. In the region calculus, each boxed value has a statically determined region in which it is stored. Regions are allocated and de-allocated according to a stack discipline, thus improving memory management. The idea of name groups arose in the typed ambient calculus of Cardelli, Ghelli, and Gordon. There, and in our p-calculus, each name has a statically determined group to which it belongs. Groups allow for type-checking of certain mobility properties, as well as effect analyses. Our encoding makes precise the intuitive correspondence between regions and groups. We propose a new formulation of the type preservation property of the region calculus, which avoids Tofte and Talpin's rather elaborate co-inductive formulation. We prove the encoding preserves the static and dynamic semantics of the region calculus. Our proof of the correctness of region de-allocation shows it to be a specific instance of a general garbage collection principle for the p-calculus with effects.

- Secrecy and group
creation With L. Cardelli and G. Ghelli.
In
**Proceedings CONCUR 2000**, Springer LNCS 1877:365-379, 2000. A journal version appears in**Information and Computation**196(2):127-155 (2005).

We add an operation of group creation to the typed p-calculus, where a group is a type for channels. Creation of fresh groups has the effect of statically preventing certain communications, and can block the accidental or malicious leakage of secrets. Intuitively, no channel belonging to a fresh group can be received by processes outside the initial scope of the group. We formalize this intuition by adapting a notion of secrecy introduced by Abadi, and proving a preservation of secrecy property.

- Ambient groups and
mobility types With L. Cardelli and G. Ghelli.
In
**Proceedings TCS 2000**, Springer LNCS 1872:333-347, 2000.

We add name groups and group creation to the typed ambient calculus. Group creation is surprisingly interesting: it has the effect of statically preventing certain communications, and can thus block the accidental or malicious escape of capabilities that is a major concern in practical systems. Moreover, ambient groups allow us to refine our earlier work on type systems for ambient mobility. We present type systems in which groups identify the set of ambients that a process may cross or open.

- Anytime, anywhere: Modal
logics for mobile ambients With L. Cardelli.
In
**Proceedings POPL'00**, ACM Press, pages 365--377, 2000.

The Ambient Calculus is a process calculus where processes my reside within a hierarchy of locations and modify it. The purpose of the the calculus is to study mobility, which is seen as the change of spatial configurations over time. In order to describe properties of mobile computations we devise a modal logic that can talk about space as well as time, and that has the Ambient Calculus as a model.

- Mobility types for mobile
ambients With L. Cardelli
and G. Ghelli. In
**Proceedings ICALP'99**, Springer LNCS 1644:230--239, 1999. An extended version of this paper appears as Technical Report MSR-TR-99-32, Microsoft Research, June 1999.

An ambient is a named cluster of processes and subambients, which moves as a group. The untyped ambient calculus is a process calculus in which ambients model a variety of concepts such as network nodes, packets, channels, and software agents. In these models, some ambients are intended to be mobile, some immobile; and some are intended to be ephemeral, some persistent. We describe type systems able to formalize these intentions: they can guarantee that an ambient will remain immobile, and that an ambient will not be dissolved by its environment. These guarantees could help establish security properties of models, for instance. A novel feature of our type systems is their distinction between mobile and immobile processes.

- Equational properties of mobile ambients With L. Cardelli.
In
**Proceedings FoSSaCS'99**, Springer LNCS, 1999. An extended version of this paper appears as Technical Report MSR-TR-99-11, Microsoft Research, April 1999. A journal version appears in**Mathematical Structures in Computer Science**13(2003):371-408.

The ambient calculus is a process calculus for describing mobile computation. We develop a theory of Morris-style contextual equivalence for proving properties of mobile ambients. We prove a context lemma that allows derivation of contextual equivalences by considering contexts of a particular limited form, rather than all arbitrary contexts. We give an activity lemma that characterizes the possible interactions between a process and a context. We prove several examples of contextual equivalence. The proofs depend on characterizing reductions in the ambient calculus in terms of a labelled transition system.

- Types for mobile ambients With L. Cardelli. In
**Proceedings POPL'99**, ACM Press, pages 79--92, 1999.

Java has demonstrated the utility of type systems for mobile code, and in particular their use and implications for security. Security properties rest on the fact that a well-typed Java program (or the corresponding verified bytecode) cannot cause certain kinds of damage. In this paper we provide a type system for mobile computation, that is, for computation that is continuously active before and after movement. We show that a well-typed mobile computation cannot cause certain kinds of run-time fault: it cannot cause the exchange of values of the wrong kind, anywhere in a mobile system.

- A concurrent object
calculus: reduction and typing With P. D. Hankin. In
**3rd International Workshop on High-Level Concurrent Languages (HLCL'98)**, Elsevier ENTCS 16(3), 1998. An extended version of this paper appears as Technical Report 457, University of Cambridge Computer Laboratory, February 1999.

We obtain a new formalism for concurrent object-oriented languages by extending Abadi and Cardelli's imperative object calculus with operators for concurrency from the pi-calculus and with operators for synchronisation based on mutexes. Our syntax of terms is extremely expressive; in a precise sense it unifies notions of expression, process, store, thread, and configuration. We present a chemical-style reduction semantics, and prove it equivalent to a structural operational semantics. We identify a deterministic fragment that is closed under reduction and show that it includes the imperative object calculus. A collection of type systems for object-oriented constructs is at the heart of Abadi and Cardelli's work. We recast one of Abadi and Cardelli's first-order type systems with object types and subtyping in the setting of our calculus and prove subject reduction. Since our syntax of terms includes both stores and running expressions, we avoid the need to separate store typing from typing of expressions. We translate communication channels and the choice-free asynchronous pi-calculus into our calculus to illustrate its expressiveness; the types of read-only and write-only channels are supertypes of read-write channels.

- A bisimulation method for
cryptographic protocols With M. Abadi. In
**Proceedings ESOP'98**, Springer LNCS, 1998. Full version in**Nordic Journal of Computing**5(1998): 267-303.

We introduce a definition of bisimulation for cryptographic protocols. The definition includes a simple and precise model of the knowledge of the environment with which a protocol interacts. Bisimulation is the basis of an effective proof technique, which yields proofs of classical security properties of protocols and also justifies certain protocol optimisations. The setting for our work is the spi calculus, an extension of the pi calculus with cryptographic primitives. We prove the soundness of the bisimulation proof technique within the spi calculus.

- Mobile ambients. With L. Cardelli.
**Theoretical Computer Science**240 (2000):177-213. A conference version appears in**Proceedings FoSSaCS'98**, Springer LNCS, 1998. An extended abstract of this paper appears in the proceedings of the workshop on**Higher Order Operational Techniques in Semantics**, held at Stanford University, December 8-11, 1997.

We introduce a calculus describing the movement of processes and devices, including movement through administrative domains.

- A Calculus for cryptographic protocols: the spi calculus. With M. Abadi.
**Information and Computation**148(1999):1-70. An extended version of this paper appears as Research Report 149, Digital Equipment Corporation Systems Research Center, January 1998, and, in preliminary form, as Technical Report 414, University of Cambridge Computer Laboratory, January 1997.

We introduce the spi calculus, an extension of the pi calculus designed for the description and analysis of cryptographic protocols. We show how to use the spi calculus, particularly for studying authentication protocols. The pi calculus (without extension) suffices for some abstract protocols; the spi calculus enables us to consider cryptographic issues in more detail. We represent protocols as processes in the spi calculus and state their security properties in terms of coarse-grained notions of protocol equivalence.

- Operational equivalences for untyped and polymorphic object calculi. In
**Higher Order Operational Techniques in Semantics**, pages 9-54, Cambridge University Press, 1998.

We survey several definitions of operational equivalence from studies of the lambda-calculus in the setting of the sigma-calculus, Abadi and Cardelli's untyped object calculus. In particular, we study the relationship between the following: the equational theory induced by the primitive semantics; Morris-style contextual equivalence; experimental equivalence (the equivalence implicit in a Milner-style context lemma); and the form of Abramsky's applicative bisimilarity induced by Howe's format.

We repeat this study in the setting of Abadi and Cardelli's polymorphic object calculus obtained by
enriching system **Fsub**** **with primitive
covariant self types for objects. In particular, we
obtain for the first time a co-inductive characterisation of contextual equivalence
for an object calculus with subtyping, parametric polymorphism, variance
annotations and structural typing rules. Soundness of the equational
theory induced by the primitive semantics of the calculus has not been proved denotationally, because structural typing rules invalidate
conventional denotational models. Instead, we show
soundness of the equational theory using operational
techniques.

**Higher Order Operational Techniques in Semantics****.**Edited with Andrew M. Pitts. Cambridge University Press, 1998.**Compilation and Equivalence of Imperative Objects****.**With Paul D. Hankin and S. B. Lassen. In**Proceedings FST+TCS'97**, Springer Lecture Notes in Computer Science, December 1997. An extended version appears in the**Journal of Functional Programming**9(4):373-426, July 1999. The full version appeared in preliminary form as Technical Report 429, University of Cambridge Computer Laboratory, June 1997, and as BRICS Report RS-97-19, June 1997.

We adopt the untyped imperative object calculus of Abadi and Cardelli as a minimal setting in which to study problems of compilation and program equivalence that arise when compiling object-oriented languages. We present both a big-step and a small-step substitution-based operational semantics for the calculus and prove them equivalent to the closure-based operational semantics given by Abadi and Cardelli. Our first result is a direct proof of the correctness of compilation to a stack-based abstract machine via a small-step decompilation algorithm. Our second result is that contextual equivalence of objects coincides with a form of Mason and Talcott's CIU equivalence; the latter provides a tractable means of establishing operational equivalences. Finally, we prove correct an algorithm, used in our prototype compiler, for statically resolving method offsets. This is the first study of correctness of an object-oriented abstract machine, and of operational equivalence for the imperative object calculus.

- Reasoning about
Cryptographic Protocols in the Spi Calculus. With M. Abadi. In
**CONCUR'97: Concurrency Theory**, Springer Lecture Notes in Computer Science, volume 1243, pages 59--73, July 1997.

The spi calculus is an extension of the pi calculus with constructs for encryption and decryption. This paper develops the theory of the spi calculus, focusing on techniques for establishing testing equivalence, and applying these techniques to the proof of authenticity and secrecy properties of cryptographic protocols.

- A Calculus for Cryptographic Protocols: The Spi Calculus. With M. Abadi. In
**Proceedings of the Fourth ACM Conference on Computer and Communications Security**, ACM Press, pages 36--47, April 1997.

We introduce the spi calculus, an extension of the pi calculus designed for the description and analysis of cryptographic protocols. We show how to use the spi calculus, particularly for studying authentication protocols. The pi calculus (without extension) suffices for some abstract protocols; the spi calculus enables us to consider cryptographic issues in more detail. We represent protocols as processes in the spi calculus and state their security properties in terms of coarse-grained notions of protocol equivalence.

- Nominal Calculi for
Security and Mobility. In
**Proceedings of the DARPA Workshop on Foundations for Secure Mobile Code**, US Naval Postgraduate School, Monterey, pages 10--14, March 1997.

Needham defines a pure name to be ``nothing but a bit pattern that is an identifier, and is only useful for comparing for identity with other bit patterns---which includes looking up in tables in order to find other information''. In this paper, we argue that pure names are relevant to both security and mobility. Nominal calculi are computational formalisms that include pure names and the dynamic generation of fresh, unguessable names. We survey recent work on nominal calculi with primitives representing location failure, process migration and cryptography, and suggest areas for further work.

- Five Axioms of Alpha-Conversion. With T. F.
Melham. In
**Theorem Proving in Higher Order Logics: 9th Interational Conference, TPHOLs'96**, Springer Lecture Notes in Computer Science, volume 1125, pages 173--191, August 1996.

We present five axioms of name-carrying
lambda-terms identified up to alpha-conversion---that is, up to renaming of bound
variables. We assume constructors for constants, variables, application and
lambda-abstraction. Other constants represent a function `Fv`

that returns the set of free
variables in a term and a function that substitutes a term for a variable free
in another term. Our axioms are (1) equations relating `Fv`

and each constructor, (2)
equations relating substitution and each constructor, (3) alpha-conversion
itself, (4) unique existence of functions on lambda-terms defined by structural
iteration, and (5) construction of lambda-abstractions given certain functions
from variables to terms. By building a model from de Bruijn's
nameless lambda-terms, we show that our five axioms are a conservative
extension of HOL. Theorems provable from the axioms include distinctness, injectivity and an exhaustion principle for the
constructors, principles of structural induction and primitive recursion on
lambda-terms, Hindley and Seldin's substitution
lemmas and the existence of their length function. These theorems and the model
have been mechanically checked in the Cambridge HOL system.

**The Haskell Language Report, Version 1.3**. With J. Peterson [editor], K. Hammond [editor], L. Augustsson, B. Boutel, W. Burton, J. Fasel, J. Hughes, P. Hudak, T. Johnsson, M. Jones, S. Peyton Jones, A. Reid and P. Wadler. Yale University Research Report YALEU/DCS/RR-1106, May 1996.**The Haskell Library Report, Version 1.3**. With J. Peterson [editor], K. Hammond [editor], L. Augustsson, J. Fasel, M. Jones, S. Peyton Jones and A. Reid. Yale University Research Report YALEU/DCS/RR-1105, May 1996.- Book Review. Review of B. Potter,
J. Sinclair and D. Till,
*An Introduction to Formal Specification and Z*and A. Diller,*Z: An Introduction to Formal Methods*.**Journal of Functional Programming**, 6(2):375--377, March 1996. - Concurrent Haskell.
With S. L. Peyton Jones and S. Finne. In
**Conference Record of the 23rd ACM Symposium on Principles of Programming Languages, St Petersburg Beach, Florida**, pages 295--308, January 1996.

Some applications are most easily expressed in a programming language that supports concurrency, notably interactive and distributed systems. We propose extensions to the purely-functional language Haskell that allows it to express explicitly concurrent applications; we call the resulting language Concurrent Haskell. The resulting system appears to be both expressive and efficient, and we give a number of examples of useful abstractions that can be built from our primitives. We have developed a freely-available implementation of Concurrent Haskell, and are now using it as a substrate for a graphical user interface toolkit.

- Bisimilarity for a First-Order
Calculus of Objects with Subtyping. With G. D. Rees. In
**Conference Record of the 23rd ACM Symposium on Principles of Programming Languages, St Petersburg Beach, Florida**, pages 386--395, January 1996. Full version available as Technical Report 386, Computer Laboratory, University of Cambridge, January 1996.

Bisimilarity (also known as `applicative bisimulation') has attracted a good deal of attention as an operational equivalence for lambda-calculi. It approximates or even equals Morris-style contextual equivalence and admits proofs of program equivalence via co-induction. It has an elementary construction from the operational definition of a language. We consider bisimilarity for one of the typed object calculi of Abadi and Cardelli. By defining a labelled transition system for the calculus in the style of Crole and Gordon and using a variation of Howe's method we establish two central results: that bisimilarity is a congruence, and that it equals contextual equivalence. So two objects are bisimilar iff no amount of programming can tell them apart. Our third contribution is to show that bisimilarity soundly models the equational theory of Abadi and Cardelli. This is the first study of contextual equivalence for an object calculus and the first application of Howe's method to subtyping. By these results, we intend to demonstrate that operational methods are a promising new direction for the foundations of object-oriented programming.

- Monadic I/O in Haskell
1.3. With K. Hammond. In
**Proceedings of the Haskell Workshop, June 25, 1995, La Jolla, California**, pages 50-68, Yale University Research Report YALEU/DCS/RR-1075, 1995.

We describe the design and use of monadic I/O in Haskell 1.3, the latest revision of the lazy functional programming language Haskell. Haskell 1.3 standardises the monadic I/O mechanisms now available in many Haskell systems. The new facilities allow more sophisticated text-based application programs to be written portably in Haskell. Apart from the use of monads, the main advances over standard Haskell 1.2 are: character I/O based on handles (analogous to ANSI C file pointers), an error handling mechanism, terminal interrupt handling and a POSIX interface. The standard also provides implementors with a flexible framework for extending Haskell to incorporate new language features. In addition to a tutorial description of the new facilities this paper includes a worked example: a monad for combinator parsing which is based on the standard I/O monad.

- Bisimilarity
as a Theory of Functional Programming. Mini-Course. Notes to accompany
graduate lectures at BRICS in the
Computer Science Department of Aarhus University, March 1995. Earlier
versions of part of this material appeared in the proceedings of the
Glasgow FP'94 and MFPS'95 conferences. BRICS Notes Series NS-95-3, Aarhus
University. Errata in the printing
of July 1995.

Operational intuition is central to computer science. These notes introduce functional programmers to operational semantics and operational equivalence. We show how the idea of bisimilarity from CCS may be applied to deterministic functional languages. On elementary operational grounds it justifies equational reasoning and proofs about infinite streams.

- Bisimilarity
as a Theory of Functional Programming. In proceedings of the
**Eleventh Conference on the Mathematical Foundations of Programming Semantics, New Orleans, March 29 to April 1, 1995**, Elsevier Electronic Notes in Theoretical Computer Science, volume 1. 1995. (The full text of the proceedings is only accessible from institutes that have a regular subscription to the journal Theoretical Computer Science.) Full version in**Theoretical Computer Science**228 (1999):5-47.

Morris-style contextual equivalence---invariance of termination under any context of ground type---is the usual notion of operational equivalence for deterministic functional languages such as FPC (PCF plus sums, products and recursive types). Contextual equivalence is hard to establish directly. Instead we define a labelled transition system for call-by-name FPC (and variants) and prove that CCS-style bisimilarity equals contextual equivalence---a form of operational extensionality. Using co-induction we establish equational laws for FPC. By considering variations of Milner's `bisimulations up to ~' we obtain a second co-inductive characterisation of contextual equivalence in terms of reduction behaviour and production of values. Hence we use co-inductive proofs to establish contextual equivalence in a series of stream-processing examples. Finally, by proving a context lemma we show how Milner's original term-model can be extended to FPC, but in fact our form of bisimilarity supports simpler co-inductive proofs.

- A Sound Metalogical Semantics
for Input/Output Effects. With R. L. Crole. In
**CSL'94 Computer Science Logic, Kazimierz, Poland, September 1994**. Springer Lecture Notes in Computer Science, volume 933, pages 339--353, 1995. Full version in**Mathematical Structures in Computer Science**9(1999): 125--188.

We study the longstanding problem of semantics for input/output (I/O) expressed using side-effects. Our vehicle is a small higher-order imperative language, with operations for interactive character I/O and based on ML syntax. Unlike previous theories, we present both operational and denotational semantics for I/O effects. We use a novel labelled transition system that uniformly expresses both applicative and imperative computation. We make a standard definition of bisimilarity and prove it is a congruence using Howe's method.

Next, we define a metalogical type theory M which we may give a denotational semantics to O. M generalises Crole and Pitts' FIX-logic by adding in a parameterised recursive datatype, which is used to model I/O. M comes equipped both with judgements of equality of expressions, and an operational semantics; M itself is given a domain-theoretic semantics in the category CPPO of cppos (bottom-pointed posets with joins of omega chains) and Scott continuous functions. We use the CPPO semantics to prove that the equational theory is computationally adequate for the operational semantics using formal approximation relations. The existence of such relations uses key ideas from Pitts' recent work.

A monadic-style textual translation into M induces a denotational semantics on O. Our final result justifies metalogical reasoning: if the denotations of two O programs are equal in M then the O programs are in fact operationally equivalent.

- A Tutorial on Co-induction and Functional Programming To appear in
**Proceedings of the 1994 Glasgow Workshop on Functional Programming**, pages 78--95. Springer Workshops in Computing, 1995.

Co-induction is an important tool for reasoning about unbounded structures. This tutorial explains the foundations of co-induction, and shows how it justifies intuitive arguments about lazy streams, of central importance to lazy functional programmers. We explain from first principles a theory based on a new formulation of bisimilarity for functional programs, which coincides exactly with Morris-style contextual equivalence. We show how to prove properties of lazy streams by co-induction and derive Bird and Wadler's Take Lemma, a well-known proof technique for lazy streams.

- A Mechanisation of Name-Carrying Syntax up to Alpha-Conversion. In
**Higher-order logic theorem proving and its applications. Proceedings, 1993**. Springer Lecture Notes in Computer Science, volume 780, pages 414--426. 1994.

We present a new strategy for representing syntax in a mechanised logic. We define an underlying type of de Bruijn terms, define an operation of named lambda-abstraction, and hence inductively define a set of conventional name-carrying terms. The result is a mechanisation of the practice of most authors studying formal calculi: to work with conventional name-carrying notation and substitution, but to identify terms up to alpha-conversion. This strategy falls between most previous works, which either treat bound variable names literally or dispense with them altogether. The theory has been implemented in the Cambridge HOL system and used in an experimental application.

- Factoring an Adequacy Proof (Preliminary Report). With R. L. Crole. In
**Proceedings of the 1993 Glasgow Workshop on Functional Programming**, pages 9--25. Springer Workshops in Computing. 1994.

This paper contributes to the methodology of using metalogics for reasoning about programming languages. As a concrete example we consider a fragment of ML corresponding to call-by-value PCF and translate it into a metalogic which contains (amongst other types) computation types and a fixpoint type. The main result is a soundness property (*): if the denotations of two programs are provably equal in the metalogic, they have the same operationally observable behaviour. As usual, this follows from a computational adequacy result. In early notes, Plotkin showed how such proofs could be factored into two stages, the first non-trivial and the second (essentially) routine; our contribution is to rework his suggestion within a new framework. We define a metalogic, which incorporates computation and fixpoint types, and specify a modular translation of the ML fragment. Our proof of (*) factors into two parts. First, the term language of the metalogic is equipped with an operational semantics and a (generic) computational adequacy result obtained. Second, a simple syntactic argument establishes a correspondence between the operational behaviour of an object program and of its denotation. The first part is not routine but is proved once and for all. The second is a detailed but essentially trivial calculation that is easily adaptable to other object languages. Such a factored proof is important because it promises to scale up more easily than a monolithic one. We show that it may be adapted to an object language with call-by-name functions and one with a simple exception mechanism.

- An Operational Semantics for I/O in a Lazy Functional
Language. In
**FPCA'93: Conference on Functional Programming Languages and Computer Architecture, Copenhagen**, pages 136--145. ACM Press, 1993.

I/O mechanisms are needed if functional languages are to be suitable for general purpose programming and several implementations exist. But little is known about semantic methods for specifying and proving properties of lazy functional programs engaged in I/O. As a step towards formal methods of reasoning about realistic I/O we investigate three widely implemented mechanisms in the setting of teletype I/O: synchronised-stream (primitive in Haskell), continuation-passing (derived in Haskell) and Landin-stream I/O (where programs map an input stream to an output stream of characters). Using methods from Milner's CCS we give a labelled transition semantics for the three mechanisms. We adopt bisimulation equivalence as equality on programs engaged in I/O and give functions to map between the three kinds of I/O. The main result is the first formal proof of semantic equivalence of the three mechanisms, generalising an informal argument of the Haskell committee.

- The Binomial Theorem
Proven in HOL. In M. J. C. Gordon and T. F. Melham (editors),
**Introduction to HOL: A theorem proving environment for higher order logic**, Chapter 7, pages 77-92. Cambridge University Press, 1993.

The Binomial Theorem in HOL is a medium sized worked example whose subject matter is more widely known than any specific piece of hardware or software. This article introduces the small amount of algebra and mathematical notation needed to state and prove the Binomial Theorem, shows how this is rendered in HOL, and outlines the structure of the proof.

- A Mechanised Definition
of SILAGE in HOL. Technical Report 287, Computer Laboratory, University
of Cambridge, February 1993.

If formal methods of hardware verification are to have any impact on the practices of working engineers, connections must be made between the languages used in practice to design circuits, and those used for research into hardware verification. Silage is a simple dataflow language marketed for specifying digital signal processing circuits. Higher Order Logic (HOL) is extensively used for research into hardware verification. This paper presents a formal definition of a substantial subset of Silage, by mapping Silage declarations into HOL predicates. The definition has been mechanised in the HOL theorem prover to support the transformational design of Silage circuits as theorem proving in HOL.

- Experience with
Embedding Hardware Description Languages in HOL. With R. Boulton, M. Gordon, J. Harrison, J. Herbert and J. Van
Tassel. In
**Theorem Provers in Circuit Design: Theory, Practice and Experience: Proceedings of the IFIP TC10/WG 10.2 International Conference, Nijmegen, June 1992**. IFIP Transactions A-10, pages 129--156. North-Holland, 1992.

The semantics of hardware description languages can be represented in higher order logic. This provides a formal definition that is suitable for machine processing. Experiments are in progress at Cambridge to see whether this method can be the basis of practical tools based on the HOL theorem-proving assistant. Three languages are being investigated: ELLA, Silage and VHDL. The approaches taken for these languages are compared and current progress on building semantically-based theorem-proving tools is discussed.

- The Formal Definition of
a Synchronous Hardware-Description Language in Higher Order Logic. In
**1992 IEEE International Conference on Computer Design: VLSI in Computers & Processors**, pages 531--534. IEEE Computer Society Press, 1992.

If formal methods of hardware verification are to have any impact on the practices of working designers, connections must be made between the languages used in practice to design circuits, and those used for research into hardware verification. Silage is a simple dataflow language used for specifying digital signal processing circuits. Higher Order Logic (HOL) is extensively used for research into hardware verification. We have used a novel combination of operational and predicative semantics to define formally a substantial subset of Silage by mapping Silage definitions into HOL predicates. Here we sketch the method used, discuss what is gained by a formal definition, and explain an immediate practical application---secure transformational design of Silage circuits as theorem proving in HOL.

- Functional Programming and Input/Output. PhD dissertation,
University of Cambridge, 1992. Published in the series Distinguished
Dissertations in Computer Science, Cambridge University Press, 1994.
Paperback edition 2008.

A common attraction to functional programming is the ease with which proofs can be given of program properties. A common disappointment with functional programming is the difficulty of expressing input/output (I/O) while at the same time being able to verify programs. In this dissertation we show how a theory of functional programming can be smoothly extended to admit both an operational semantics for functional I/O and verification of programs engaged in I/O.

The first half develops the operational theory of
a semantic metalanguage used in the second half. The metalanguage **M** is a simply-typed lambda-calculus
with product, sum, function, lifted and recursive types. We study two
definitions of operational equivalence: Morris-style contextual equivalence,
and a typed form of Abramsky's applicative bisimulation. We prove operational extensionality for **M**---that
these two definitions give rise to the same operational equivalence. We prove equational laws that are analogous to the axiomatic domain
theory of LCF and derive a co-induction principle.

The second half defines a small functional
language, **H**, and shows how the semantics of **H** can be extended to
accommodate I/O. **H** is essentially a fragment of
Haskell. We give both operational and denotational
semantics for **H**. The denotational semantics
uses **M** in a case study of Moggi's proposal to
use monads to parameterise semantic descriptions. We define operational and denotational equivalences on **H** and show that denotational implies operational equivalence. We develop a
theory of **H** based on equational laws and a
co-induction principle.

We study simplified forms of four
widely-implemented I/O mechanisms: side-effecting, Landin-stream,
synchronised-stream and continuation-passing I/O. We give reasons why
side-effecting I/O is unsuitable for lazy languages. We extend the semantics of
**H** to include the other three mechanisms and prove that the three are
equivalent to each other in expressive power.

We investigate monadic I/O, a high-level model for functional I/O based on Wadler's suggestion that monads can express interaction with state in a functional language. We describe a simple monadic programming model, and give its semantics as a particular form of state transformer. Using the semantics we verify a simple programming example.