VERIFY on Thursday

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

All sessions take place in auditorium 6.

Session 1: Applications of ATP in Verification

08:45-09:00  Welcoming and Opening Remarks

09:00-09:30  Daniel Kröning, Carnegie Mellon U, USA
Application specific higher order logic theorem proving
Theorem proving allows the formal verification of the correctness of very large systems. In order to increase the acceptance of theorem proving systems during the design process, we implemented higher order logic proof systems for ANSI-C and Verilog within a framework for application specific proof systems. Furthermore, we implement the language of the PVS theorem prover as well-established higher order specification language. The tool allows the verification of the design languages using a PVS specification and the verification of hardware designs using a C program as specification. We implement powerful decision procedures using Model Checkers and satisfiability checkers. We provide experimental results that compare the performance of our tool with PVS on large industrial scale hardware examples.

09:30-10:00  Vincent Vanackère, Provence U, Marseille, France
The TRUST protocol analyser, automatic and efficient verification of cryptographic protocols
The paper presents TRUST, a verifier for cryptographic protocols. In our framework, a protocol is modeled as a finite number of processes interacting with an hostile environment; the security properties expected from the protocol are specified by inserting logical assertions on the environment knowledge in the process.
Our analyser relies on an exact symbolic reduction method combined with several techniques aiming to alleviate the number of interleavings that have to be considered. We argue that our verifier is able to perform a full analysis on up to 3 parallel (interleaved) sessions of most protocols. Moreover, authentication and secrecy properties are specified in a very natural way, and whenever an error is found an attack against the protocol is given by our tool.

10:00-10:30  Christoph Benzmüller, Saarland U, Germany
Corrado Giromini, Saarland U, Germany
Andreas Nonnengart, DFKI Saarbrücken, Germany
Jürgen Zimmer, Saarland U, Germany
Reasoning services in MathWeb-SB for symbolic verification of hybrid systems
We propose to apply mathematical service systems developed in the context of the Calculemus initiative to support the verification of hybrid systems. For this we want to identify and analyse different kinds of mathematical subtasks occurring in industrial-strength examples of hybrid system verification. These kinds of subtasks, suitable for being tackled with reasoning specialists, can be modeled as mathematical service requests to a network of service systems like the Mathweb Software Bus. For the deductive model checking approach we have identified the following candidates of mathematical service requests: The solution of differential equations, subsumption of sets of constraints, and their solution. A further candidate can be the elimination of second

Session 2: Logical Approaches

Joint with FCS
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 FCS
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 FCS
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.