FCS on Thursday

Detailed program
Thursday July 25th, 2002
See also the unified by-slot program


Sessions take place in auditorium 5 unless otherwise indicated.

08:45-09:00  Opening Remarks

Session 1: Foundations of Security

Chair: Véronique Cortier

09:00-09:30  Ralf Küsters, U Kiel, Germany
On the decidability of cryptographic protocols with open-ended data structures
Formal analysis of cryptographic protocols has mainly concentrated on protocols with closed-ended data structures, where closed-ended data structure means that the messages exchanged between principals have fixed and finite format. However, in many protocols the data structures used are open-ended, i.e., messages have an unbounded number of data fields. Formal analysis of protocols with open-ended data structures is one of the challenges pointed out by Meadows. This work studies decidability issues for such protocols. We propose a protocol model in which principals are described by transducers, i.e., finite automata with output, and show that in this model security is decidable and PSPACE-hard in presence of the standard Dolev-Yao intruder.

09:30-10:00  Kong-wei Lye, Carnegie Mellon U, USA
Jeannette M. Wing, Carnegie Mellon U, USA
Game strategies in network security
This paper presents a game-theoretic method for analyzing the security of computer networks. We view the interactions between an attacker and the administrator as a two-player stochastic game and construct a model for the game. Using a non-linear program, we compute the Nash equilibrium or best-response strategies for the players (attacker and administrator). We then explain why the strategies are realistic and how administrators can use these results to enhance the security of their network.

10:00-10:30  Sylvain Conchon, Oregon Health and Science U, USA
Modular information flow analysis for process calculi
We present a framework to extend, in a modular way, the type systems of process calculi with information-flow annotations that ensure a noninterference property based on bisimulation. Our method of adding security annotations readily supports modern typing features, such as polymorphism and type reconstruction, together with a non-interference proof. Furthermore, the new systems thus obtained can detect, for instance, information flow caused by contentions on distributed resources, which are not detected in a satisfactory way by using testing equivalences.

Session 2: Logical Approaches

Joint with VERIFY
Room: auditorium 6
Chair: Catherine Meadows

11:00-11:30  Andrew W. Appel, Princeton U, USA
Neophytos G. Michael, Princeton U, USA
Aaron Stump, Stanford U, USA
Roberto Virga, Princeton U, USA
A trustworthy proof checker
Proof-Carrying Code (PCC) and other applications in computer security require machine-checkable proofs of properties of machine-language programs. The main advantage of the PCC approach is that the amount of code that must be explicitly trusted is very small: it consists of the logic in which predicates and proofs are expressed, the safety predicate, and the proof checker. We have built a minimal-TCB checker, and we explain its design principles, and the representation issues of the logic, safety predicate, and safety proofs. We show that the trusted code in such a system can indeed be very small. In our current system the TCB is less than 2,700 lines of code (an order of magnitude smaller even than other PCC systems) which adds to our confidence of its correctness.

11:30-12:00  Ernie Cohen, Microsoft Research Cambridge, UK
Proving protocols safe from guessing
We describe how to prove cryptographic protocols secure against a Dolev-Yao attacker that can also engage in idealized offline guessing attacks. Our method is based on constructing a first-order invariant that bounds, in every reachable state, both the information available to an an attacker and the steps of guessing attacks starting from this information. We have implemented the method as an extension to the protocol verifier TAPS, making it the first mechanical verifier to prove protocols secure against guessing attacks in an unbounded model.

12:00-12:30  Alessandro Armando, U Genova, Italy
Luca Compagna, U Genova, Italy
Automatic SAT-compilation of security problems
We provide a fully automatic translation from security protocol specifications into propositional logic which can be effectively used to find attacks to protocols. Our approach results from the combination of a reduction of security problems to planning problems and well-known SAT-reduction techniques developed for planning. We also propose and discuss a set of transformations on security problems whose application has a dramatic effect on the size of the propositional encoding obtained with our SAT-compilation technique. We describe a model-checker for security protocols based on our ideas and show that attacks to a set of well-known authentication protocols are found in few seconds by state-of-the-art SAT solvers.

Session 3: VERIFY Invited talk

Joint with VERIFY
Room: auditorium 6
Chair: Heiko Mantel

14:00-15:30  Fabio Massacci, U Trento, Italy
Invited talk: Formal verification of SET by Visa and Mastercard: Lessons for formal methods in security
The Secure Electronic Transaction (SET) protocol has been proposed by a consortium of credit card companies and software corporations to secure e-commerce transactions. When the customer makes a purchase, the SET dual signature guarantees authenticity while keeping the customer's account details secret from the merchant and his choice of goods secret from the bank.
SET verification has always been a holy grail for security verification and many papers do conclude with "and this technique can be applied to SET" and yet the forthcoming application is not so forthcoming...
In this talk, I report the results of the verification efforts on the SET protocol, a joint work with G. Bella and L. Paulson from the University of Cambridge. In a nutshell, we proved that the protocol is reasonably secure. by using Isabelle and the inductive method we showed that the credit card details do remain confidential and customer, merchant and bank can confirm most details of a transaction even when some of those details are kept from them.
And now, the question come: you verified SET, so what?
What can we learn for this verification effort? Are there lessons for security design? Which security designs are easier to verify? What kind of techniques and tricks are necessary? What do we need to scale so that security verification can become an easier task? I will give a personal perspective on the problem.

Session 4: Verification of Security Protocols

Joint with VERIFY
Room: auditorium 6
Chair: Dieter Gollmann

16:00-16:30  Catherine Meadows, Naval Research Laboratory, USA
Identifying potential type confusion in authenticated messages
A type confusion attack is one in which a principal accepts data of one type as data of another. Although it has been shown by Heather et al. that there are simple formatting conventions that will guarantee that protocols are free from simple type confusions in which fields of one type are substituted for fields of another, it is not clear how well they defend against more complex attacks, or against attacks arising from interaction with protocols that are formatted according to different conventions. In this paper we show how type confusion attacks can arise in realistic situations even when the types are explicitly defined in at least some of the messages, using examples from our recent analysis of the Group Domain of Interpretation Protocol. We then develop a formal model of types that can capture potential ambiguity of type notation, and outline a procedure for determining whether or not the types of two messages can be confused. We also discuss some open issues.

16:30-17:00  Graham Steel, U Edinburgh, UK
Alan Bundy, U Edinburgh, UK
Ewen Denney, U Edinburgh, UK
Finding counterexamples to inductive conjectures and discovering security protocol attacks
We present an implementation of a method for finding counterexamples to universally quantified conjectures in first-order logic. Our method uses the proof by consistency strategy to guide a search for a counterexample and a standard first-order theorem prover to perform a concurrent check for inconsistency. We explain briefly the theory behind the method, describe our implementation, and evaluate results achieved on a variety of incorrect conjectures from various sources. Some work in progress is also presented: we are applying the method to the verification of cryptographic security protocols. In this context, a counterexample to a security property can indicate an attack on the protocol, and our method extracts the trace of messages exchanged in order to effect this attack. This application demonstrates the advantages of the method, in that quite complex side conditions decide whether a particular sequence of messages is possible. Using a theorem prover provides a natural way of dealing with this. Some early results are presented and we discuss future work. Keywords: Counterexamples, Security Protocols, Non-theorems, Proof by Consistency.