 | |
All
sessions take place in auditorium 6.| 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 |
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. |
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. |
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. |
| |
![[previous]](../img/prev.gif){kind=small}
![[up]](../img/up.gif){kind=small}
![[next]](../img/next.gif){kind=small}
