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 these bibtex and pdf files. Please contact me if you don't find the paper you are looking for.

Conference papers

Self-Certification: Bootstrapping Certified Typecheckers in F* with Coq (.pdf), with Pierre-Yves Strub, Nikhil Swamy, and Juan Chen, in ACM Symposium on Principles of Programming Languages (POPL'12), pages 571--583. January 2012. © ACM.

Well-established dependently-typed languages like Agda and Coq provide reliable ways to build and check formal proofs. Several other dependently-typed languages such as Aura, ATS, Cayenne, Epigram, F*, F7, Fine, Guru, PCML5, and Ur also explore reliable ways to develop and verify programs. All these languages shine in their own regard, but their implementations do not themselves enjoy the degree of safety provided by machine-checked verification. We propose a general technique called self-certification that allows a typechecker for a suitably expressive language to be certified for correctness. We have implemented this technique for F*, a dependently typed language on the .NET platform. Self-certification involves implementing a typechecker for F* in F*, while using all the conveniences F* provides for the compiler-writer (e.g., partiality, effects, implicit conversions, proof automation, libraries). This typechecker is given a specification (in F*) strong enough to ensure that it computes valid typing derivations.We obtain a typing derivation for the core typechecker by running it on itself, and we export it to Coq as a type-derivation certificate. By typechecking this derivation (in Coq) and applying the F* metatheory (also mechanized in Coq), we conclude that our type checker is correct. Once certified in this manner, the F* typechecker is emancipated from Coq. Self-certification leads to an efficient certification scheme---we no longer depend on verifying certificates in Coq---as well as a more broadly applicable one. For instance, the self-certified F* checker is suitable for use in adversarial settings where Coq is not intended for use, such as run-time certification of mobile code.

Information-Flow Types for Homomorphic Encryptions (.pdf), with Jérémy Planul and Tamara Rezk, in 18th ACM Conference on Computer and Communications Security (CCS'11), pages 351--360. October 2011. © ACM.

We develop a flexible information-flow type system for a range of encryption primitives, precisely reflecting their diverse functional and security features. Our rules enable encryption, blinding, homomorphic computation, and decryption, with selective key re-use for different types of payloads. We show that, under standard cryptographic assumptions, any well-typed probabilistic program using encryptions is secure (that is, computationally non-interferent) against active adversaries, both for confidentiality and integrity. We illustrate our approach using ElGamal and Paillier encryption. We present two applications of cryptographic verification by typing: (1) private search on data streams; and (2) the bootstrapping part of Gentry's fully homomorphic encryption. We provide a prototype typechecker for our system.

Modular Code-Based Cryptographic Verification (.pdf), with Markulf Kohlweiss and Pierre-Yves Strub, in 18th ACM Conference on Computer and Communications Security (CCS'11), pages 341--350. October 2011. © ACM.

Type systems are effective tools for verifying the security of cryptographic programs. They provide automation, modularity and scalability, and have been applied to large security protocols. However, they traditionally rely on abstract assumptions on the underlying cryptographic primitives, expressed in symbolic models. Cryptographers usually reason on security assumptions using lower level, computational models that precisely account for the complexity and success probability of attacks. These models are more realistic, but they are harder to formalize and automate. We present the first modular automated program verification method based on standard cryptographic assumptions. We show how to verify ideal functionalities and protocols written in ML by typing them against new cryptographic interfaces using F7, a refinement type checker coupled with an SMT-solver. We develop a probabilistic core calculus for F7 and formalize its type safety in Coq We build typed module and interfaces for MACs, signatures, and encryptions, and establish their authenticity and secrecy properties. We relate their ideal functionalities and concrete implementations, using game-based program transformations behind typed interfaces. We illustrate our method on a series of protocol implementations.

Secure Distributed Programming with Value-Dependent Types (.pdf), with Nikhil Swamy, Juan Chen, Pierre-Yves Strub, Karthikeyan Bhargavan, and Jean Yang, in ICFP. September 2011. See also the full paper at MSR-TR-2011-37.

Distributed applications are difficult to program reliably and securely. Dependently typed functional languages promise to prevent broad classes of errors and vulnerabilities, and to enable program verification to proceed side-by-side with development. However, as recursion, effects, and rich libraries are added, using types to reason about programs, specifications, and proofs becomes challenging. We present F*, a full-fledged design and implementation of a new dependently typed language for secure distributed programming. Unlike prior languages, F* provides arbitrary recursion while maintaining a logically consistent core; it enables modular reasoning about state and other effects using affine types; and it supports proofs of refinement properties using a mixture of cryptographic evidence and logical proof terms. The key mechanism is a new kind system that tracks several sub-languages within F* and controls their interaction. F* subsumes two previous languages, F7 and Fine. We prove type soundness (with proofs mechanized in Coq) and logical consistency for F*. We have implemented a compiler that translates F* to .NET bytecode, based on a prototype for Fine. F* provides access to libraries for concurrency, networking, cryptography, and interoperability with C#, F#, and the other .NET languages. The compiler produces verifiable binaries with 60\% code size overhead for proofs and types, as much as a 45x improvement over the Fine compiler, while still enabling efficient bytecode verification. To date, we have programmed and verified more than 20,000 lines of F* including (1) new schemes for multi-party sessions; (2) a zero-knowledge privacy-preserving payment protocol; (3) a provenance-aware curated database; (4) a suite of 17 web-browser extensions verified for authorization properties; and (5) a cloud-hosted multi-tier web application with a verified reference monitor.

Compiling Information-Flow Security to Minimal Trusted Computing Bases (.pdf), with Jérémy Planul, in Programming Languages and Systems (ESOP'11), LNCS 6602, pages 216--235. March 2011. © Springer-Verlag.

Information-flow policies can express strong security requirements for programs run by distributed parties with different levels of trust. However, this security is hard to preserve as programs get compiled to distributed systems with (potentially) compromised machines. For instance, many programs involve computations too sensitive to be trusted to any of those machines. Also, many programs are not perfectly secure (non-interferent); as they selectively endorse and declassify information, their relative security becomes harder to preserve. We develop a secure compiler for distributed information flows. To minimize trust assumptions, we rely on cryptographic protection, and we exploit hardware and software mechanisms available on modern architectures, such as secure boots, trusted platform modules, and remote attestation. We present a security model for these mechanisms in an imperative language with dynamic code loading. We define program transformations to generate trusted virtual hosts and to run them on untrusted machines. We obtain confidentiality and integrity theorems under realistic assumptions, showing that the compiled distributed system is at least as secure as the source program.

Typechecking Higher-Order Security Libraries, with Karthikeyan Bhargavan and Nataliya Guts, in APLAS, pages 47--62. 2010.

Modular Verification of Security Protocol Code by Typing (.pdf), with K. Bhargavan and A. D. Gordon, in ACM Symposium on Principles of Programming Languages (POPL'10), pages 445--456. January 2010. © ACM.

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. We develop cryptographic libraries that embed a logic model of their cryptographic structures and that specify preconditions and postconditions 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 carrying 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 whole-program analyses 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.

A Security-Preserving Compiler for Distributed Programs: From Information-Flow Policies to Cryptographic Mechanisms (.pdf), with Gurvan le Guernic and Tamara Rezk, in ACM Conference on Computer and Communications Security (CCS'09), pages 432--441. November 2009. © ACM.

We enforce information flow policies in programs that run at multiple locations, with diverse levels of security. We build a compiler from a small imperative language with locality and security annotations down to distributed code linked to concrete cryptographic libraries. Our compiler splits source programs into local threads; inserts checks on auxiliary variables to enforce the source control flow; implements shared distributed variables using instead a series of local replicas with explicit updates; and finally selects cryptographic mechanisms for securing the communication of updates between locations. We establish computational soundness for our compiler: under standard assumptions on cryptographic primitives, all confidentiality and integrity properties of the source program also hold with its distributed code, despite the presence of active adversaries that control all communications and some of the program locations. We also present performance results for the code obtained by compiling sample programs.

Reliable Evidence: Auditability by Typing (.pdf), with Nataliya Guts and Francesco Zappa Nardelli, in 14th European Symposium on Research in Computer Security (ESORICS 2009), LNCS 5789, pages 168--183. September 2009. © Springer-Verlag.

Many protocols rely on audit trails to allow an impartial judge to verify a posteriori some property of a protocol run. However, in current practice the choice of what data to log is left to the programmer's intuition, and there is no guarantee that it constitutes enough evidence. We give a precise definition of auditability and we show how typechecking can be used to statically verify that a protocol always logs enough evidence. We apply our approach to several examples, including a full-scale auction-like protocol programmed in ML.

Secure Enforcement for Global Process Specifications (.pdf), with Jérémy Planul and Ricardo Corin, in 20th International Conference on Concurrency Theory (CONCUR'09), LNCS 5710, pages 511--526. September 2009. © Springer-Verlag.

Distributed applications may be specified as parallel compositions of processes that summarize their global interactions and hide local implementation details. These processes define a fixed protocol (also known as a contract, or a session) which may be used for instance to compile or verify code for these applications. Security is a concern when the runtime environment for these applications is not fully trusted. Then, parts of their implementation may run on remote, corrupted machines, which do not comply with the global process specification. To mitigate this concern, one may write defensive implementations that monitor the application run and perform cryptographic checks. However, hand crafting such implementations is ad hoc and error-prone. We develop a theory of secure implementations for process specifications. We propose a generic defensive implementation scheme, relying on history-tracking mechanisms, and we identify sufficient conditions on processes, expressed as a new type system, that ensure that our implementation is secure for all integrity properties. We illustrate our approach on a series of examples and special cases, including an existing implementation for sequential multiparty sessions.

Cryptographic Protocol Synthesis and Verification for Multiparty Sessions (.pdf), with Karthikeyan Bhargavan, Ricardo Corin, Pierre-Malo Deniélou, and James J. Leifer, in 22nd IEEE Computer Security Foundations Symposium (CSF'09), pages 124--140. July 2009. © IEEE.

We present the design and implementation of a compiler that, given high-level multiparty session descriptions, generates custom cryptographic protocols. Our sessions specify pre-arranged patterns of message exchanges and data accesses between distributed participants. They provide each participant with strong security guarantees for all their messages. Our compiler generates code for sending and receiving these messages, with cryptographic operations and checks, in order to enforce these guarantees against any adversary that may control both the network and some session participants. We verify that the generated code is secure by relying on a recent type system for cryptography. Most of the proof is performed by mechanized type checking and does not rely on the correctness of our compiler. We obtain the strongest session security guarantees to date in a model that captures the executable details of protocol code. We illustrate and evaluate our approach on a series of protocols inspired by web services.

High-Level Programming for E-Cash (Extended Abstract), with Nataliya Guts and Francesco Zappa Nardelli, in 1st Computational and Symbolic Proofs of Security Workshop. 2009.

Cryptographically Verified Implementations for TLS (.pdf), with Karthikeyan Bhargavan, Ricardo Corin, and Eugen Zalinescu, in ACM Conference on Computer and Communications Security (CCS'08), pages 459--468. October 2008. © ACM.

We intend to narrow the gap between concrete implementations of cryptographic protocols and their verified models. We develop and verify a small functional implementation of the Transport Layer Security protocol (TLS). We make use of the same executable code for interoperability testing against mainstream implementations, for automated symbolic cryptographic verification, and for automated computational cryptographic verification. We rely on a combination of recent tools, and we also develop a new tool for extracting computational models from executable code. We obtain strong security guarantees for TLS as used in typical deployments.

Code-Carrying Authorization (.pdf), with Sergio Maffeis, Martín Abadi, and Andrew D. Gordon, in 13th European Symposium on Research in Computer Security (ESORICS'08), LNCS 5283, pages 563-579. October 2008. © Springer-Verlag.

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.

Refinement Types for Secure Implementations (.pdf), with Jesper Bengtson, Karthikeyan Bhargavan, Andrew D. Gordon, and Sergio Maffeis, in 21st IEEE Computer Security Foundations Symposium (CSF'08), pages 17--32. June 2008. © IEEE.

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.

A Formal Implementation of Value Commitment (.pdf), with Nataliya Guts and Francesco Zappa Nardelli, in Programming Languages and Systems (ESOP'08), LNCS 4960, pages 383--397. March 2008. © Springer-Verlag.

In an optimistic approach to security, one can often simplify protocol design by relying on audit logs, which can be analyzed a posteriori. Such auditing is widely used in practice, but no formal studies guarantee that the log information suffices to reconstruct past runs of the protocol, in order to reliably detect (and provide evidence of) any cheating. We formalize audit logs for a sample optimistic scheme, the value commitment. It is specified in a pi calculus extended with committable locations, and compiled using standard cryptography to implement secure logs. We show that our distributed implementation either respects the abstract semantics of commitments or, using information stored in the logs, detects cheating by a hostile environment.

Verified Implementations of the Information Card Federated Identity-Management Protocol (.pdf), with Karthikeyan Bhargavan, Andrew D. Gordon, and Nikhil Swamy, in Proceedings of the ACM Symposium on Information, Computer and Communications Security (ASIACCS'08), pages 123--135. March 2008. © ACM.

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 roles of the protocol (client, identity provider, and relying party). 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 identity providers and compiles them to a verifiably secure client proxy.

Cryptographically Sound Implementations for Typed Information-Flow Security (.pdf), with Tamara Rezk, in 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'08), pages 323--335. January 2008. © ACM.

In language-based security, confidentiality and integrity policies conveniently specify the permitted flows of information between different parts of a program with diverse levels of trust. These policies enable a simple treatment of security, and they can often be verified by typing. However, their enforcement in concrete systems involves delicate compilation issues. We consider cryptographic enforcement mechanisms for imperative programs with untrusted components. Such programs may represent, for instance, distributed systems connected by some untrusted network. In source programs, security depends on an abstract access-control policy for reading and writing the shared memory. In their implementations, shared memory is unprotected and security depends instead on encryption and signing. We build a translation from well-typed source programs and policies to cryptographic implementations. To establish its correctness, we develop a type system for the target language. Our typing rules enforce a correct usage of cryptographic primitives against active adversaries; from an information-flow viewpoint, they capture controlled forms of robust declassification and endorsement. We show type soundness for a variant of the non-interference property, then show that our translation preserves typability. We rely on concrete primitives and hypotheses for cryptography, stated in terms of probabilistic polynomial-time algorithms and games. We model these primitives as commands in our target language. Thus, we develop a uniform language-based model of security, ranging from computational non-interference for probabilistic programs down to standard cryptographic hypotheses.

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

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. © IEEE.

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. © IEEE.

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. November 2006. © Springer-Verlag.

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. September 2006. © Springer-Verlag.

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. July 9--16 2006. © Springer-Verlag.

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. June 2006. © IEEE.

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. October 2005. © ACM.

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. June 2005. The full version now appears in Journal of Logic and Algebraic Programming. © IEEE.

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. April 2005. © Springer-Verlag.

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 Services, pages 56--66. October 2004. © ACM.

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. © ACM.

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. October 2004. © IEEE.

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. July 2004. © Springer-Verlag.

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. 2004. © Springer-Verlag.

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. June 2004. © IEEE.

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. March 2004. © Springer-Verlag.

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. January 2004. An extended version appears as Microsoft Research Technical Report MSR-TR-2003-83. © ACM.

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. February 2003. © Internet Society.

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. 2003. © Springer-Verlag.

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. January 2002. © ACM.

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. June 2002. © Springer-Verlag.

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. © ACM.

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. January 2000. © ACM.

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. 17--19 August 2000. © Springer-Verlag.

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. December 2000. The full version now appears in Journal of Logic and Algebraic Programming. © Springer-Verlag.

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), LNCS 1738, pages 122--141. December 1999. © Springer-Verlag.

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. © IEEE.

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. June 1998. © IEEE.

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). June 1998. © Chapman and Hall.

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. July 1998. © Springer-Verlag.

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. 1--4 July 1997. © Springer-Verlag.

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. 26--29 August 1996. © Springer-Verlag.

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. January 1996. © ACM.

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.

Lecture notes

Cryptographic Verification by Typing for a Sample Protocol Implementation (.pdf), with Karthik Bhargavan and Andrew D. Gordon, in Proceedings of the Foundations of Seccurity and Design VI Summer School (FOSAD 2010), LNCS. September 2011. © IOS Press. © Springer-Verlag.

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. (1) 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. (2) We describe a sample authenticated RPC protocol, we implement it in F#, and we specify its security against active adversaries. (3) 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. (4) 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.

Principles and Applications of Refinement Types, with Andrew D. Gordon, in International Summer School Logics and Languages for Reliability and Security, Marktoberdorf, August 2009. October 2010. Also Technical Report MSR-TR-2009-147. © IOS Press.

A refinement type is the subset of a type consisting of the values that satisfy a formula. 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.

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. 2003. © Springer-Verlag.

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. August 2002. © Springer-Verlag.

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.

Articles in Journals

Refinement Types for Secure Implementations, with Jesper Bengtson, Karthikeyan Bhargavan, Andrew D. Gordon, and Sergio Maffeis, ACM Transactions on Programming Languages and Systems. 2010. To appear. An short version appears in CSF'08. See also Microsoft Research Technical Report MSR-TR-2008-118 SP1. © ACM.

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.

SecPAL: Design and Semantics of a Decentralized Authorization Language, with Moritz Y. Becker and Andrew D. Gordon, Journal of Computer Security (Special issue for CSF'07). 2009. To appear. © IOS Press.

A Secure Compiler for Session Abstractions, with Ricardo Corin, Pierre-Malo Deniélou, Karthikeyan Bhargavan, and James J. Leifer, Journal of Computer Security (Special issue for CSF'07) 16(5):573--636. 2008. © IOS Press.

Automated Verification of Selected Equivalences for Security Protocols (.pdf), with Bruno Blanchet and Martín Abadi, Journal of Logic and Algebraic Programming 75(1):3--51. 2008. A short version appears in LICS'05. © Elsevier.

Verified Interoperable Implementations of Security Protocols, with Karthikeyan Bhargavan, Andrew D. Gordon, and Stephen Tse, ACM Transactions on Programming Languages and Systems 31(1):1--61. December 2008. © ACM.

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.

Verifying Policy-Based Web Services Security, with Karthikeyan Bhargavan and Andrew D. Gordon, ACM Transactions on Programming Languages and Systems 30(6). October 2008. © ACM.

WS-SecurityPolicy is a declarative language for configuring web services security mechanisms. We describe a formal semantics for WS-SecurityPolicy and propose a more abstract language for specifying secure links between web services and their clients. We present the architecture and implementation of 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. We can verify policies when first compiled from link specifications, and also re-verify policies against their original goals after any modifications during deployment. Moreover, we present general security theorems for all configurations that rely on compiled policies.

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

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.

A Type Discipline for Authorization Policies, with A. D. Gordon and S. Maffeis, ACM Transactions on Programming Languages and Systems 29(5). August 2007. © ACM.

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.

Secure Sessions for Web Services (.pdf), with Karthikeyan Bhargavan, Ricardo Corin, and Andrew D. Gordon, ACM Transactions on Information and System Security (TISSEC) 10(2). May 2007. © ACM.

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 Hierarchy of Equivalences for Asynchronous Calculi (.pdf) (.ps), with Georges Gonthier, Journal of Logic and Algebraic Programming 63(1):131--173. April 2005. An extended abstract appears in ICALP'98. © Elsevier.

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.

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

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.

Private Authentication (.pdf), with Martín Abadi, Theoretical Computer Science 322(3):427--476. 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). © Elsevier.

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. September 2004. An extended abstract appears in ECOOP'02 (LNCS 2374). © ACM.

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

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. September 2003. © Elsevier.

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

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

Others

Pre- and Post-Conditions for Security Typechecking (.pdf), with Karthikeyan Bhargavan and Nataliya Guts, in Workshop on Foundations of Security and Privacy (FCS-PrivMod 2010). July 2010.

We verify implementations of cryptographic protocols that manipulate recursive data structures, such as lists. Our main applications are X.509 certificate chains and XML digital signatures. These applica- tions are beyond the reach of automated provers such as ProVerif, since they require some form of induction. They can be verified using the F7 refinement typechecker, at the cost of annotating each data-processing function with logical formulas embedded in its type. However, this en- tails the duplication of many library functions, so that each instance can be given its own type. We propose a more flexible method for verifying ML programs that use cryptography and recursion. We annotate standard library func- tions (such as list processing functions) with precise, yet reusable types that refer to the pre- and post-conditions of their functional arguments, using generic logical predicates. We use these predicates both to spec- ify higher-order functions and to track security events in programs and cryptographic libraries. We implement our method by extending the F7 typechecker with automated support for these predicates. We evaluate our approach experimentally by verifying a series of security libraries and protocols.

Refinement Types for Secure Implementations (.pdf), with Jesper Bengtson, Karthikeyan Bhargavan, Andrew D. Gordon, and Sergio Maffeis, Microsoft Research Technical Report (MSR-TR-2008-118). 2008. Revised: 2010.

Trustworthy Global Computing, Third Symposium, TGC 2007, Sophia-Antipolis, France, November 5-6, 2007, Revised Selected Papers, with Gilles Barthe, LNCS 4912. 2008. © Springer-Verlag.

A Secure Compiler for Session Abstractions, with Ricardo Corin, Pierre-Malo Deniélou, Karthikeyan Bhargavan, and James Leifer, MSR-INRIA Joint Centre . 2008. Prototype implementation available at \urlhttp://msr-inria.inria.fr/projects/sec/sessions.

A Computational Verifier for Protocol Code (fs2cv), with Karthikeyan Bhargavan, Ricardo Corin, and Eugen Zalinescu, MSR-INRIA Joint Centre . 2008. Prototype implementation available at \urlhttp://msr-inria.inria.fr/projects/sec/fs2cv.

Crypto-Verifying Protocol Implementations in ML, with Karthikeyan Bhargavan and Ricardo Corin, in Proceedings of the 3rd Workshop on Formal and Computational Cryptography (FCC'07). July 2007.

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.

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.

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

Dissertation

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.

Revised: 06-03-2012.