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.
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].
Security-typed languages and distributed computation
Abstract:
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.
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.
Bruno Blanchet (Inria)
Andrew Gordon (Microsoft Research, Cambridge)
References
Andrew Myers (Cornell University)
David Wagner (University of California, Berkeley)