SAS'01 Invited Session on Security on Wednesday July 18th, 2001

B. Blanchet     A. Gordon     A. Myers     D. Wagner

Bruno Blanchet (Inria)

Abstracting Cryptographic Protocols by Prolog Rules

Abstract: Most current cryptographic protocol verifiers meet the state space explosion problem, and have to limit the number of executions of the considered protocol for the verification process. In this talk, we will introduce a representation of cryptographic protocols, based on Prolog rules, that solves these problems by performing well-chosen approximations that preserve attacks. We use our representation to verify secrecy properties of protocols, that is, determine whether an adversary can obtain a given message or not. The usual Prolog algorithm does not terminate on the rules representing a protocol, so we have designed, proved correct, and implemented an efficient algorithm to handle this particular situation. The experimental results show that many examples of protocols of the literature, including Skeme, can be analyzed by our tool with very small resources: the analysis takes from less than 0.1 s for simple protocols to 23 s for the main mode of Skeme.

Andrew Gordon (Microsoft Research, Cambridge)

A Type and Effect Analysis of Security Protocols

Joint work with Alan Jeffrey (DePaul University)

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

My talk will describe our method and give some simple examples. Papers describing the method in detail appear elsewhere [1,2].


A.D. Gordon and A. Jeffrey. Authenticity by typing for security protocols. In 14th IEEE Computer Security Foundations Workshop. IEEE Computer Society Press, 2001. To appear.

A.D. Gordon and A. Jeffrey. Typing correspondence assertions for communication protocols. In Mathematical Foundations of Programming Semantics 17, Electronic Notes in Theoretical Computer Science. Elsevier, 2001. To appear.

Andrew Myers (Cornell University)

Security-typed languages and distributed computation


Recently there has been considerable interest in programming languages that encode security policies in type declarations. Type-checking is used to determine whether a program enforces these policies. This approach enjoys many of the benefits of static type-checking, but is particularly of interest because it can enforce information flow properties such as noninterference, for which purely dynamic mechanisms are ineffective.

Enforcing information flow properties for distributed systems adds a new challenges: mutual distrust among the principals, and untrusted hosts. Our new approach, secure program partitioning, automatically rewrites a program into communicating subprograms that run securely on the set of available hosts yet collectively implement the original program. This fine-grained rewriting is based on the security types in the original program and the trust relationships among principals and hosts in the system. Computation in the original program is written in a single-host style, yet the resulting distributed system can satisfy the strong confidentiality and integrity properties specified by the program.

David Wagner (University of California, Berkeley)

Static Analysis and Software Assurance.

Abstract: In the past decade, explosive growth in computer networks has brought security issues to the forefront. One of the greatest challenges in computer security today is the software assurance problem: How do we deal with the fact that our most trusted software, even our security software itself, is often buggy?

In this talk, I will discuss how static analysis can help with the software assurance problem. I will describe some recent experience with static analysis tools for vulnerability detection. I will also survey a number of open problems in the field and suggest a few promising directions for future research.