Publications

The papers given here are not necessarily identical to any previously published paper. Copyright and all rights therein are maintained by the authors or by other copyright holders. Additional bibliographic details appear in this bibtex file. Please contact me if you don't find the paper you are looking for.

Secure Implementations of Typed Session Abstractions (.pdf), with Ricardo Corin, Pierre-Malo Dénielou, Karthikeyan Bhargavan, and James J. Leifer, in 20th IEEE Computer Security Foundations Symposium (CSF20), pages 170--186. July 2007.

Distributed applications can be structured as parties that exchange messages according to some pre-arranged communication patterns. These sessions (or contracts, or protocols) simplify distributed programming: when coding a role for a given session, each party just has to follow the intended message flow, under the assumption that the other parties are also compliant. In an adversarial setting, remote parties may not be trusted to play their role. Hence, defensive implementations also have to monitor one another, in order to detect any deviation from the assigned roles of a session. This task involves low-level coding below session abstractions, thus giving up most of their benefits. We explore language-based support for sessions. We extend the ML language with session types that express flows of messages between roles, such that well-typed programs always play their roles. We compile session type declarations to cryptographic communication protocols that can shield programs from any low-level attempt by coalitions of remote peers to deviate from their roles. Our main result is that, when reasoning about programs that use our session implementation, one can safely assume that all session peers comply with their roles---without trusting their remote implementations.

Design and Semantics of a Decentralized Authorization Language (.pdf), with Moritz Y. Becker and Andrew D. Gordon, in 20th IEEE Computer Security Foundations Symposium (CSF20), pages 3--15. July 2007.

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.

A Type Discipline for Authorization in Distributed Systems (.pdf), with Andrew D. Gordon and Sergio Maffeis, in 20th IEEE Computer Security Foundations Symposium (CSF20), pages 31--45. July 2007.

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 encryption and public-key signatures.

Computational Secrecy by Typing for the Pi Calculus (.pdf), with Martín Abadi and Ricardo Corin, in Programming Languages and Systems 4th Asian Symposium (APLAS 2006), LNCS 4279, pages 253--269, Springer-Verlag. November 2006.

We define and study a distributed cryptographic implementation for an asynchronous pi calculus. At the source level, we adapt simple type systems designed for establishing formal secrecy properties. We show that those secrecy properties have counterparts in the implementation, not formally but at the level of bitstrings, and with respect to probabilistic polynomial-time active adversaries. We rely on compilation to a typed intermediate language with a fixed scheduling strategy. While we exploit interesting, previous theorems for that intermediate language, our result appears to be the first computational soundness theorem for a standard process calculus with mobile channels.

Verified Reference Implementations of WS-Security Protocols (.pdf), with Karthikeyan Bhargavan and Andrew D. Gordon, in Web Services and Formal Methods, Third International Workshop (WS-FM 2006), LNCS 4184, pages 88--106, Springer-Verlag. September 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.

Cryptographically Sound Implementations for Communicating Processes (Extended Abstract) (.pdf), with Pedro Adao, in 33rd International Colloquium on Automata, Languages and Programming (ICALP 2006), LNCS 4052, pages 83--94, Springer-Verlag. July 9--16 2006.

We design a core language of principals running distributed programs over a public network. Our language is a variant of the pi calculus, with secure communications, mobile names, and high-level certificates, but without any explicit cryptography. Within this language, security properties can be conveniently studied using trace properties and observational equivalences, even in the presence of an arbitrary (abstract) adversary. With some care, these security properties can be achieved in a concrete setting, relying instead on standard cryptographic primitives and computational assumptions, even in the presence of an adversary modeled as an arbitrary probabilistic polynomial-time algorithm. To this end, we develop a cryptographic implementation that preserves all properties for all safe programs. We give a series of soundness and completeness results that precisely relate the language to its implementation. We also illustrate our approach using a series of protocols and properties expressible in our language, and motivate some unusual design choices.

Verified Interoperable Implementations of Security Protocols (.pdf), with Karthikeyan Bhargavan, Andrew D. Gordon, and Stephen Tse, in 19th IEEE Computer Security Foundations Workshop (CSFW'06), pages 139--152, IEEE Computer Society. June 2006.

We present an architecture and tools for verifying implementations of security protocols. Our implementations can run with both concrete and symbolic implementations of cryptographic algorithms. 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.

An Advisor for Web Services Security Policies (.pdf), with Karthikeyan Bhargavan, Andrew D. Gordon, and Greg O'Shea, in SWS'05: Proceedings of the 2005 ACM Workshop on Secure Web Service, pages 1--9, ACM Press. October 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).

Automated Verification of Selected Equivalences for Security Protocols (.pdf), with Bruno Blanchet and Martín Abadi, in 20th IEEE Symposium on Logic in Computer Science (LICS 2005), pages 331--340, IEEE Computer Society. June 2005. The full version now appears in Journal of Logic and Algebraic Programming.

In the analysis of security protocols, methods and tools for reasoning about protocol behaviors have been quite effective. We aim to expand the scope of those methods and tools. We focus on proving equivalences P   Q in which P and Q are two processes that differ only in the choice of some terms. These equivalences arise often in applications. We show how to treat them as predicates on the behaviors of a process that represents P and Q at the same time. We develop our techniques in the context of the applied pi calculus and implement them in the tool ProVerif.

A Type Discipline for Authorization Policies (.pdf), with Andrew D. Gordon and Sergio Maffeis, in Programming Languages and Systems, 14th European Symposium on Programming, ESOP 2005, LNCS 3444, pages 141--156, Springer-Verlag. April 2005.

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 (.pdf), with Karthikeyan Bhargavan, Ricardo Corin, and Andrew D. Gordon, in SWS'04: Proceedings of the 2004 workshop on Secure web service, pages 56--66, ACM Press. October 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-Trusts 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 (.pdf), with K. Bhargavan and A. D. Gordon, in 11th ACM Conference on Computer and Communications Security (CCS'04), pages 268-277. October 2004.

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.

Ethernet Topology Discovery without Network Assistance (.pdf), with Richard Black and Austin Donnelly, in Proceedings of the 12th IEEE International Conference on Network Protocols (ICNP 2004), pages 328--339, IEEE Computer Society. October 2004.

This work addresses the problem of Layer 2 topology discovery. Current techniques concentrate on using SNMP to query information from Ethernet switches. In contrast, we present a technique that infers the Ethernet (Layer 2) topology without assistance from the network elements by injecting suitable probe packets from the end-systems and observing where they are delivered. We describe the algorithm, formally characterize its correctness and completeness, and present our implementation and experimental results. Performance results show that although originally aimed at the home and small office the techniques scale to much larger networks.

Stuck-Free Conformance (.ps), with C. A. R. Hoare, Sriram K. Rajamani, and Jakob Rehof, in Proceedings of the 16th International Conference on Computer Aided Verification (CAV'04), LNCS 3114, pages 242--254, Springer-Verlag. July 2004.

We present a novel refinement relation (stuck-free conformance) for CCS processes, which satisfies the substitutability property: If I conforms to S, and P is any environment such that P | S is stuck-free, then P | I is stuck-free. Stuck-freedom is related to the CSP notion of deadlock, but it is more discriminative by taking orphan messages in asynchronous systems into account. We prove that conformance is a precongruence on CCS processes, thereby supporting modular refinement. We distinguish conformance from the related preorders, stable failures refinement in CSP and refusal preorder in CCS. We have implemented conformance checking in a new software model checker, ZING, and we report on how we used it to find errors in distributed programs.

TulaFale: A Security Tool for Web Services (.pdf), with K. Bhargavan, A. D. Gordon, and R. Pucella, in International Symposium on Formal Methods for Components and Objects (FMCO'03), LNCS 3188, pages 197--222, Springer-Verlag. 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 (.ps), with Frédéric Besson, Tomasz Blanc, and Andrew D. Gordon, in 17th IEEE Computer Security Foundations Workshop (CSFW'04), pages 61--75, IEEE. June 2004.

We present a new static analysis for reviewing the security of libraries for systems, such as JVMs or the CLR, that rely on stack inspection for access control. We describe its implementation for the CLR. Our tool inputs a set of 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 security defects. It has been applied to large pre-existing libraries. 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.

Just Fast Keying in the Pi Calculus (.pdf), with Martín Abadi and Bruno Blanchet, in Programming Languages and Systems, 13th European Symposium on Programming, ESOP 2004, LNCS 2986, pages 340--354, Springer-Verlag. March 2004.

JFK is a recent, attractive protocol for fast key establishment as part of securing IP communication. In this paper, we analyze it formally in the applied pi calculus (partly in terms of observational equivalences, partly with the assistance of an automatic protocol verifier). We treat JFK's core security properties, and also other properties that are rarely articulated and studied rigorously, such as resistance to denial-of-service attacks. In the course of this analysis we found some ambiguities and minor problems, but we mostly obtain positive results about JFK. For this purpose, we develop ideas and techniques that should be useful more generally in the specification and verification of security protocols.

A Semantics for Web Services Authentication (.pdf), with K. Bhargavan and A. D. Gordon, in 31st ACM Symposium on Principles of Programming Languages (POPL'04), pages 198--209, ACM. January 2004. An extended version appears as Microsoft Research Technical Report MSR-TR-2003-83.

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 Microsoft 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.

Access Control based on Execution History (.pdf) (.ps), with Martín Abadi, in Network and Distributed System Security Symposium (NDSS'03), pages 107--121, Internet Society. February 2003.

Security is a major, frequent concern in extensible software systems such as Java Virtual Machines and the Common Language Runtime. These systems aim to enable simple, classic applets and also, for example, distributed applications, Web services, and programmable networks, with appropriate security expectations. Accordingly, they feature elaborate constructs and mechanisms for associating rights with code, including a technique for determining the run-time rights of a piece of code as a function of the state of the execution stack. These mechanisms prevent many security holes, but they are inherently partial and they have proved difficult to use reliably. We motivate and describe a new model for assigning rights to code: in short, the run-time rights of a piece of code are determined by examining the attributes of any pieces of code that have run (including their origins) and any explicit requests to augment rights. This history-based model addresses security concerns while avoiding pitfalls. We analyze the model in detail; in particular, we discuss its relation to the stack-based model and to the policies and mechanisms of underlying operating systems, and we consider implementation techniques. In support of the model, we also introduce and implement high-level constructs for security, which should be incorporated in libraries or (even better) in programming languages.

Hiding Names: Private Authentication in the Applied Pi Calculus (.pdf) (.ps), with Martín Abadi, in Software Security -- Theories and Systems. Mext-NSF-JSPS International Symposium, Tokyo, November 2002 (ISSS'02), LNCS 2609, pages 317--338, Springer-Verlag. 2003.

We present the analysis of a protocol for private authentication in the applied pi calculus. We treat authenticity and secrecy properties of the protocol. Although such properties are fairly standard, their formulation in the applied pi calculus makes an original use of process equivalences. In addition, we treat identity-protection properties, which are a delicate concern in several recent protocol designs.

Stack Inspection: Theory and Variants (.pdf) (.ps), with Andrew D. Gordon, in Conference record of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'02), pages 307--318, ACM. January 2002.

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.

Modern Concurrency Abstractions for C# (.pdf) (.ps), with Nick Benton and Luca Cardelli, in ECOOP 2002 -- Object Oriented Programming, LNCS 2374, pages 415--440, Springer-Verlag. June 2002.

Polyphonic C# is an extension of the C# language with new asynchronous concurrency constructs, based on the join calculus. We describe the design and implementation of the language and give examples of its use in addressing a range of concurrent programming problems.

Mobile values, new names, and secure communication (.pdf) (.ps), with Martín Abadi, in 28th ACM Symposium on Principles of Programming Languages (POPL'01), pages 104--115. 2001.

We study the interaction of the ``new'' construct with a rich but common form of (first-order) communication. This interaction is crucial in security protocols, which are the main motivating examples for our work; it also appears in other programming-language contexts. Specifically, we introduce a simple, general extension of the pi calculus with value passing, primitive functions, and equations among terms. We develop semantics and proof techniques for this extended language and apply them in reasoning about some security protocols.

Authentication Primitives and their Compilation (.pdf) (.ps), with Martín Abadi and Georges Gonthier, in Conference record of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'00), pages 302--315, ACM. January 2000.

Adopting a programming-language perspective, we study the problem of implementing authentication in a distributed system. We define a process calculus with constructs for authentication and show how this calculus can be translated to a lower-level language using marshaling, multiplexing, and cryptographic protocols. Authentication serves for identity-based security in the source language and enables simplifications in the translation. We reason about correctness relying on the concepts of observational equivalence and full abstraction.

An Asynchronous, Distributed Implementation of Mobile Ambients (.pdf) (.ps), with Jean-Jacques Lévy and Alan Schmitt, in Proceedings of IFIP TCS 2000, LNCS 1872, pages 348--364, IFIP TC1, Springer-Verlag. 17--19 August 2000.

We present a first distributed implementation of the Cardelli-Gordon's ambient calculus. We use Jocaml as an implementation language and we present a formal translation of Ambients into the distributed join calculus, the process calculus associated with Jocaml. We prove the correctness of the translation.

Inheritance in the join-calculus (Extended Abstract) (.pdf) (.ps), with Cosimo Laneve, Luc Maranget, and Didier Rémy, in FST TCS 2000: Foundations of Software Technology and Theoretical Computer Science, LNCS 1974, pages 397--408, Springer-Verlag. December 2000. The full version now appears in Journal of Logic and Algebraic Programming.

We propose an object-oriented calculus with internal concurrency and class-based inheritance that is built upon the join calculus. Method calls, locks, and states are handled in a uniform manner, using asynchronous messages. Classes are partial message definitions that can be combined and transformed. We design operators for behavioral and synchronization inheritance.

A Top-Down Look at a Secure Message (.ps), with Martín Abadi and Georges Gonthier, in Proceedings of the Nineteenth Conference on the Foundations of Software Technology and Theoretical Computer Science (FST&TCS '99), pages 122--141. December 1999.

In ongoing work, we are investigating the design of secure distributed implementations of high-level process calculi (in particular, of the join-calculus). We formulate implementations as translations to lower-level languages with cryptographic primitives. Cryptographic protocols are essential components of those translations. In this paper we discuss basic cryptographic protocols for transmitting a single datum from one site to another. We explain some sufficient correctness conditions for these protocols. As an example, we present a simple protocol and a proof of its correctness.

Secure Communications Processing for Distributed Languages (.pdf) (.ps), with Martín Abadi and Georges Gonthier, in Proceedings of the 1999 IEEE Symposium on Security and Privacy, pages 74--88. May 1999.

Communications processing is an important part of distributed language systems with facilities such as RPC (remote procedure call) and RMI (remote method invocation). For security, messages may require cryptographic operations in addition to ordinary marshaling. We investigate a method for wrapping communications processing around an entity with secure local communication, such as a single machine or a protected network. The wrapping extends security properties of local communication to distributed communication. We formulate and analyze the method within a process calculus.

An Implementation of Ambients in JoCaml, with Alan Schmitt, in 5th Mobile Object Systems Workshop: Programming Languages for Wide-Area Networks. June 1999.

Secure Implementation of Channel Abstractions (.ps), with Martín Abadi and Georges Gonthier, in Proceedings of LICS '98, pages 105--116, IEEE. June 1998.

Communication in distributed systems often relies on useful abstractions such as channels, remote procedure calls, and remote method invocations. The implementations of these abstractions sometimes provide security properties, in particular through encryption. In this paper we study those security properties, focusing on channel abstractions. We introduce a simple high-level language that includes constructs for creating and using secure channels. The language is a variant of the join-calculus and belongs to the same family as the pi calculus. We show how to translate the high-level language into a lower-level language that includes cryptographic primitives. In this translation, we map communication on secure channels to encrypted communication on public channels. We obtain a correctness theorem for our translation; this theorem implies that one can reason about programs in the high-level language without mentioning the subtle cryptographic protocols used in their lower-level implementation.

Bisimulations in the Join-Calculus (.ps), with Michele Boreale and Cosimo Laneve, in Programming Concepts and Methods, IFIP TC2/WG2.2,2.3 International Conference on Programming Concepts and Methods (PROCOMET '98), IFIP, Chapman and Hall. June 1998.

We develop a theory of bisimulation in the join calculus. We introduce a refined operational model that makes interactions with the environment explicit, and discuss the impact of the lexical scope discipline of the join calculus on its extensional semantics. We propose several formulations of bisimulation and establish that all formulations yield the same equivalence. We prove that this equivalence is finer than barbed congruence, but that both relations coincide in the presence of name matching.

A Hierarchy of Equivalences for Asynchronous Calculi (extended abstract) (.ps), with Georges Gonthier, in Proceedings of the 25th International Colloquium on Automata, Languages and Programming (ICALP '98), LNCS 1443, pages 844-855, Springer-Verlag. July 1998.

We generate a natural hierarchy of equivalences for asynchronous name-passing process calculi from simple variations on Milner and Sangiorgi's definition of weak barbed bisimulation. The pi calculus, used here, and the join calculus are examples of such calculi. We prove that barbed bisimulation coincides with Honda and Yoshida's reduction equivalence, and with asynchronous labeled bisimulation when the calculus includes name matching, thus closing both conjectures. We also show that barbed bisimulation is coarser when only one barb is tested. For the pi calculus it becomes an odd limit bisimulation, but for the join-calculus it coincides with both fair testing equivalence and with the weak barbed version of Sjodin and Parrow's coupled simulation.

Implicit Typing à la ML for the join-calculus (.ps), with Cosimo Laneve, Luc Maranget, and Didier Rémy, in Proceedings of the 8th International Conference on Concurrency Theory (CONCUR'97), LNCS 1243, pages 196--212, Springer-Verlag. 1--4 July 1997.

We adapt the Damas-Milner typing discipline to the join calculus. The main result is a new generalization criterion that extends the polymorphism of ML to join definitions. We prove the correctness of our typing rules with regards to a chemical semantics. We also relate typed extensions of the core join calculus to functional languages.

A Calculus of Mobile Agents (.ps), with Georges Gonthier, Jean-Jacques Lévy, Luc Maranget, and Didier Rémy, in Proceedings of the 7th International Conference on Concurrency Theory (CONCUR '96), LNCS 1119, pages 406--421, Springer-Verlag. 26--29 August 1996.

We introduce a calculus for mobile agents and give its chemical semantics, with a precise definition for migration, failure, and failure detection. Various examples written in our calculus illustrate how to express remote executions, dynamic loading of remote resources and protocols with mobile agents. We give the encoding of our distributed calculus into the join-calculus.

The Reflexive Chemical Abstract Machine and the Join-Calculus (.ps), with Georges Gonthier, in Conference record of the 23th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'96), pages 372--385, ACM. January 1996.

By adding reflexion to the chemical machine of Berry and Boudol, we obtain a formal model of concurrency that is consistent with mobility and distribution. Our model provides the foundations of a programming language with functional and object-oriented features. It can also be seen as a process calculus, the join calculus, which we prove equivalent to the pi calculus of Milner, Parrow, and Walker.

JoCaml: a Language for Concurrent Distributed and Mobile Programming (.pdf), with Fabrice Le Fessant, Luc Maranget, and Alan Schmitt, in Advanced Functional Programming, 4th International School, Oxford, August 2002, LNCS 2638, pages 129--158, Springer-Verlag. 2003.

In these lecture notes, we give an overview of concurrent, distributed, and mobile programming using JoCaml. JoCaml is an extension of the Objective Caml language. It extends Objective Caml with support for concurrency and synchronization, the distributed execution of programs, and the dynamic relocation of active program fragments during execution. The programming model of JoCaml is based on the join calculus. This model is characterized by an explicit notion of locality, a strict adherence to local synchronization, and a natural embedding of functional programming a la ML. Local synchronization means that messages always travel to a set destination, and can interact only after they reach that destination; this is required for an efficient asynchronous implementation. Specifically, the join calculus uses ML's function bindings and pattern-matching on messages to express local synchronizations. The lectures and lab sessions illustrate how to use JoCaml to program concurrent and distributed applications in a much higher-level fashion than the traditional threads-and-locks approach.

The Join Calculus: a Language for Distributed Mobile Programming (.pdf) (.ps), with Georges Gonthier, in Applied Semantics. International Summer School, APPSEM 2000, Caminha, Portugal, September 2000, LNCS 2395, pages 268--332, Springer-Verlag. August 2002.

In these notes, we give an overview of the join calculus, its semantics, and its equational theory. The join calculus is a language that models distributed and mobile programming. It is characterized by an explicit notion of locality, a strict adherence to local synchronization, and a direct embedding of the ML programming language. The join calculus is used as the basis for several distributed languages and implementations, such as JoCaml and functional nets. Local synchronization means that messages always travel to a set destination, and can interact only after they reach that destination; this is required for an efficient implementation. Specifically, the join calculus uses ML's function bindings and pattern-matching on messages to program these synchronizations in a declarative manner. Formally, the language owes much to concurrency theory, which provides a strong basis for stating and proving the properties of asynchronous programs. Because of several remarkable identities, the theory of process equivalences admits simplifications when applied to the join calculus. We prove several of these identities, and argue that equivalences for the join calculus can be rationally organized into a five-tiered hierarchy, with some trade-off between expressiveness and proof techniques. We describe the mobility extensions of the core calculus, which allow the programming of agent creation and migration. We briefly present how the calculus has been extended to model distributed failures on the one hand, and cryptographic protocols on the other.

Automated Verification of Selected Equivalences for Security Protocols (.pdf), with Bruno Blanchet and Martín Abadi, Journal of Logic and Algebraic Programming. 2007. To appear. A short version appears in LICS'05.

In the analysis of security protocols, methods and tools for reasoning about protocol behaviors have been quite effective. We aim to expand the scope of those methods and tools. We focus on proving equivalences P   Q in which P and Q are two processes that differ only in the choice of some terms. These equivalences arise often in applications. We show how to treat them as predicates on the behaviors of a process that represents P and Q at the same time. We develop our techniques in the context of the applied pi calculus and implement them in the tool ProVerif.

A Type Discipline for Authorization Policies, with A. D. Gordon and S. Maffeis, ACM Transactions on Programming Languages and Systems, ACM Press. 2007. To appear.

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. We consider the problem of checking whether a distributed implementation based on communication channels and cryptography complies with a logical authorization policy. We formalize authorization policies and their connection to code by embedding logical predicates and claims within a process calculus. We formulate policy compliance operationally by composing a process model of the distributed system with an arbitrary opponent process. Moreover, we propose a dependent type system for verifying policy compliance of implementation code. Using Datalog as an authorization logic, we show how to type several examples using policies and present a general schema for compiling policies.

Just Fast Keying in the Pi Calculus, with Martín Abadi and Bruno Blanchet, ACM Transactions on Information and System Security (TISSEC). 2006. To appear. An extended abstract appears in Programming Languages and Systems, 13th European Symposium on Programming, ESOP 2004.

JFK is a recent, attractive protocol for fast key establishment as part of securing IP communication. In this paper, we analyze it formally in the applied pi calculus (partly in terms of observational equivalences, partly with the assistance of an automatic protocol verifier). We treat JFK's core security properties, and also other properties that are rarely articulated and studied rigorously, such as plausible deniability and resistance to denial-of-service attacks. In the course of this analysis we found some ambiguities and minor problems, such as limitations in identity protection, but we mostly obtain positive results about JFK. For this purpose, we develop ideas and techniques that should be useful more generally in the specification and verification of security protocols.

Secure Sessions for Web Services (.pdf), with Karthikeyan Bhargavan, Ricardo Corin, and Andrew D. Gordon, ACM Transactions on Information and System Security (TISSEC), ACM Press. 2006. To appear.

We address the problem of securing sequences of SOAP messages exchanged between web services and their clients. The WS-Security standard defines basic mechanisms to secure SOAP traffic, one message at a time. For typical web services, however, using WS-Security independently for each message is rather inefficient; moreover, 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 defines 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 pitfalls and limitations of these specifications.

A Semantics for Web Services Authentication, with Karthikeyan Bhargavan and Andrew D. Gordon, Theoretical Computer Science 340(1):102--153, Elsevier. June 2005. See also Microsoft Research Technical Report MSR-TR-2003-83.

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 elements, such as username tokens, public-key certificates, and digital signatures, amounting to a flexible vocabulary for expressing protocols. To describe the syntax of these elements, 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 elements and of sample protocols distributed with the Microsoft 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.

A Hierarchy of Equivalences for Asynchronous Calculi (.pdf) (.ps), with Georges Gonthier, Journal of Logic and Algebraic Programming, Elsevier. 2004. To appear. An extended abstract appears in ICALP'98.

We generate a natural hierarchy of equivalences for asynchronous name-passing process calculi from simple variations on Milner and Sangiorgi's definition of weak barbed bisimulation. The pi calculus, used here, and the join calculus are examples of such calculi. We prove that barbed congruence coincides with Honda and Yoshida's reduction equivalence, and with asynchronous labeled bisimulation when the calculus includes name matching, thus closing those two conjectures. We also show that barbed congruence is coarser when only one barb is tested. For the pi calculus, it becomes a limit bisimulation, whereas for the join calculus, it coincides with both fair testing equivalence and with the weak barbed version of Sjödin and Parrow's coupled simulation.

Private Authentication (.pdf), with Martín Abadi, Theoretical Computer Science 322(3):427--476, Elsevier. September 2004. Special issue on Foundations of Wide Area Network Computing. Parts of this work were presented at PET'02 (LNCS 2482) and ISSS'02 (LNCS 2602)..

Frequently, communication between two principals reveals their identities and presence to third parties. These privacy breaches can occur even if security protocols are in use; indeed, they may even be caused by security protocols. However, with some care, security protocols can provide authentication for principals that wish to communicate while protecting them from monitoring by third parties. We discuss the problem of private authentication and present two protocols for private authentication of mobile principals. Our protocols allow two mobile principals to communicate when they meet at a location if they wish to do so, without the danger of tracking by third parties. We also present the analysis of one of the protocols in the applied pi calculus. We establish authenticity and secrecy properties. Although such properties are fairly standard, their formulation in the applied pi calculus makes an original use of process equivalences. In addition, we treat identity-protection properties, thus exploring a formal model of privacy.

Modern Concurrency Abstractions for C# (.pdf), with Nick Benton and Luca Cardelli, ACM Transactions on Programming Languages and Systems 26(5):769--804, ACM Press. September 2004. An extended abstract appears in ECOOP'02 (LNCS 2374).

Polyphonic C# is an extension of the C# language with new asynchronous concurrency constructs, based on the join calculus. We describe the design and implementation of the language and give examples of its use in addressing a range of concurrent programming problems.

Stack Inspection: Theory and Variants (.pdf), with Andrew D. Gordon, ACM Transactions on Programming Languages and Systems 25(3):360--399, ACM Press. 2003. An extended abstract appears in POPL'02.

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.

Inheritance in the join calculus, with Cosimo Laneve, Luc Maranget, and Didier Rémy, Journal of Logic and Algebraic Programming 57(1--2):23--69, Elsevier. September 2003.

We propose an object-oriented calculus with internal concurrency and class-based inheritance that is built upon the join calculus. Method calls, locks, and states are handled in a uniform manner, using asynchronous messages. Classes are partial message definitions that can be combined and transformed. We design operators for behavioral and synchronization inheritance. We also give a type system that statically enforces basic safety properties. Our model is compatible with the JoCaml implementation of the join calculus.

Secure Implementation of Channel Abstractions, with Martín Abadi and Georges Gonthier, Information and Computation 174(1):37--83, Elsevier. April 2002.

Communication in distributed systems often relies on useful abstractions such as channels, remote procedure calls, and remote method invocations. The implementations of these abstractions sometimes provide security properties, in particular through encryption. In this paper we study those security properties, focusing on channel abstractions. We introduce a simple high-level language that includes constructs for creating and using secure channels. The language is a variant of the join-calculus and belongs to the same family as the pi calculus. We show how to translate the high-level language into a lower-level language that includes cryptographic primitives. In this translation, we map communication on secure channels to encrypted communication on public channels. We obtain a correctness theorem for our translation; this theorem implies that one can reason about programs in the high-level language without mentioning the subtle cryptographic protocols used in their lower-level implementation.

Bisimulations in the Join-Calculus (.pdf) (.ps), with Cosimo Laneve, Theoretical Computer Science 266(1-2):569--603, Elsevier. September 2001.

We develop a theory of bisimulation in the join calculus. We introduce a refined operational model that makes interactions with the environment explicit, and discuss the impact of the lexical scope discipline of the join calculus on its extensional semantics. We propose several formulations of bisimulation and establish that all formulations yield the same equivalence. We prove that this equivalence is finer than barbed congruence, but that both relations coincide in the presence of name matching.

SecPAL: Design and Semantics of a Decentralized Authorization Language (.pdf), with Moritz Y. Becker and Andrew D. Gordon, Microsoft Research Technical Report (MSR-TR-2006-120). September 2006.

We present a declarative authorization language. Policies and credentials are expressed using predicates defined by logical clauses, in the style of constraint logic programming. Access requests are mapped to logical authorization queries, consisting of predicates and constraints combined by conjunctions, disjunctions, and negations. Access is granted if the query succeeds against the current database of clauses. Predicates ascribe rights to particular principals, with flexible support for delegation and revocation. At the discretion of the delegator, delegated rights can be further delegated, either to a fixed depth, or arbitrarily deeply. Our language 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.

A Type Discipline for Authorization Policies, with A. D. Gordon and S. Maffeis, Microsoft Research (MSR-TR-2005-01). 2005.

Stuck-Free Conformance (.ps), with C. A. R. Hoare, Sriram K. Rajamani, and Jakob Rehof, Microsoft Research Technical Report (MSR-TR-2004-69). July 2004.

We present a novel refinement relation (stuck-free conformance) for CCS processes, which satisfies the substitutability property: If I conforms to S, and P is any environment such that P | S is stuck-free, then P | I is stuck-free. Stuck-freedom is related to the CSP notion of deadlock, but it is more discriminative by taking orphan messages in asynchronous systems into account. We prove that conformance is a precongruence on CCS processes, thereby supporting modular refinement. We distinguish conformance from the related preorders, stable failures refinement in CSP and refusal preorder in CCS. We have implemented conformance checking in a new software model checker, ZING, and we report on how we used it to find errors in distributed programs.

A Semantics for Web Services Authentication (.pdf), with Karthikeyan Bhargavan and Andrew D. Gordon, Microsoft Research Technical Report (MSR-TR-2003-83). February 2004.

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 elements, 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 elements, 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 elements and of sample protocols distributed with the Microsoft 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.

Secure Sessions for Web Services, with Karthikeyan Bhargavan, Ricardo Corin, and Andrew D. Gordon, Microsoft Research Technical Report (MSR-TR-2004-114). 2004.

A Distributed Implementation of Ambients (.ps), with Jean-Jacques Lévy and Alan Schmitt. 2000. Manuscript, subsumes papers presented at MOS'99 and FST-TCS 2000.

Secure implementation of channel abstractions (.ps), with Martín Abadi and Georges Gonthier. September 2000. Manuscript, subsumes papers presented at LICS'98 and S&P'99.

Communication in distributed systems often relies on useful abstractions such as channels, remote procedure calls, and remote method invocations. The implementations of these abstractions sometimes provide security properties, in particular through encryption. In this paper we study those security properties, focusing on channel abstractions. We introduce a simple high-level language that includes constructs for creating and using secure channels. The language is a variant of the join-calculus and belongs to the same family as the pi calculus. We show how to translate the high-level language into a lower-level language that includes cryptographic primitives. In this translation, we map communication on secure channels to encrypted communication on public channels. We obtain a correctness theorem for our translation; this theorem implies that one can reason about programs in the high-level language without mentioning the subtle cryptographic protocols used in their lower-level implementation.

Weak Bisimulations by Decreasing Diagrams, with Georges Gonthier. March 1999. Draft.

An Implementation of Ambients in JoCAML, with Alan Schmitt. 1999. Software available from http://join.inria.fr/ambients.html.

The Join-Calculus language (version 1.03), with Luc Maranget. June 1997. Source distribution and documentation available from http://join.inria.fr/.

The Join-Calculus: a Calculus for Distributed Mobile Programming (.ps.gz) (.pdf). November 1998. Ecole Polytechnique, Palaiseau. Also published by INRIA, TU-0556.

This dissertation presents an elementary model of distributed programming, studies this model as a process calculus, and uses this model as the core of a programming language. The join calculus is a small calculus in which computation consists only of asynchronous message-passing communication. It can also be interpreted as the concurrent extension of a small functional language. Its operational semantics is given in terms of chemical abstract machines, with enough details to suggest an actual implementation. By construction, every reduction step can be implemented in at most one low-level network message, independently of the distribution of processes at run-time. We explore several refinements of the join calculus that give a more explicit account of distribution, including primitives for agent-based migration, partial failure, and failure detection. These refinements preserve global scopes and network transparency in the absence of failures. We use numerous notions of observational equivalences adapted to asynchronous systems. These equivalences are organized in a hierarchy where each tier corresponds to a trade-off between suitable discriminating power and efficient proof techniques. These equivalences and used to establish the correctness of encodings internal to the join-calculus and cross-encodings with the pi-calculus.