FLoC 2006 - VERIFY

Verification Workshop
Seattle, August 15 - 16, 2006

VERIFY on Wednesday, August 16th

Session 5 (09:30‑10:30)

09:30‑10:30 Christoph Walther (TU Darmstadt)
Verification in the Classroom
Education is the key to transfer technology and methods into practical use. Concerning program verification, students of computer science often become acquainted with the subject in beginners' lectures when they learn to prove a statement about a while-loop computing the factorial function or similar things. Usually these are time-consuming (and error-prone) pencil-and-paper exercises involving a lot of tedious proof steps to learn some principles of verification. However, because of the complexity of nontrivial algorithms, one can hardly go beyond the simple while-loops investigated for verification in a beginners' lecture. But the motivation of the students largely increases when they can gather practical experiences with the principles and methods taught. Students of computer science expect to see the computer solve some problem instead of working on their own on small problems using pencil and paper only, thus treating the whole subject as a purely theoretical exercise. To improve the situation, verification tools are needed which ease the access to practical verification for beginners and non-expert users. The development of the VeriFun system aims to support such an access. In the talk, we identify design objectives underlying the development of VeriFun to achieve this goal, illustrate their realization in the system, and report about experiences obtained when VeriFun was used in several courses of different degree.

Break (10:30‑11:00)

Session 6: Security Protocols (11:00‑12:30)

11:00‑12:00 Luca Vigano (ETH Zürich)
Automated Reasoning for Security Protocol Analysis [pdf]
Experience over the last twenty years has shown that the design of protocols for Internet security is highly error-prone and that conventional validation techniques based on informal arguments and/or testing are not up to the task. It is now widely recognized that only formal analysis can provide the level of assurance required by both the developers and the users of the protocols. This is especially true not only when one considers the simple academic protocols that have been proposed as example applications for automated reasoning techniques and tools (such as the Needham-Schroeder Public Key Protocol and the like), but also when one tries to scale up these techniques and tools to industrial-strength Internet security protocols (like Kerberos and IKE).

After an introduction to Internet security protocols and a survey of some prominent techniques and tools for security protocol analysis, I will discuss the techniques that underlie the AVISPA Tool, which is a state-of-the-art tool for push-button protocol validation. The AVISPA Tool provides a modular and expressive formal language for specifying protocols and their security properties, and integrates different back-ends that implement a variety of automatic protocol analysis techniques. I will in particular focus on one back-end, the symbolic on-the-fly model-checker OFMC, which colleagues and I have been developing at the ETH Zurich. I will also discuss the integration of a framework that allows OFMC to handle algebraic properties of cryptographic operators in a uniform and modular way, and show how this provides a basis also for reasoning about off-line guessing attacks. Finally, I will discuss a first application of OFMC and the AVISPA Tool for reasoning about Web Services.

12:00‑12:30 Siraj Shaikh (University of Gloucestershire)
Vicky Bush (University of Gloucestershire)
Steve Schneider (University of Surrey)
A heuristic for constructing rank functions to verify authentication protocols
Schneider introduced a rank function approach to analysing authentication protocols. The approach specifies protocols in CSP and uses a general-purpose rank function theorem to verify their authentication properties. A crucial element of this verification is the construction of a suitable rank function, the existence of which is not always certain. Constructing a rank function is non-trivial and often deceptive, and requires an insight into the working of the protocol. In this paper, we investigate the use of rank functions in Schneider’s analysis and propose a heuristic for constructing a candidate rank function for authentication protocols. Our strategy makes use of Schneider’s original proof strategy for authentication [7] and involves step-by-step manipulation of CSP traces to put forward a clear and relatively uncomplicated approach to constructing a candidate rank function. Finally, we use the Woo-Lam protocol as an example to demonstrate our approach.

Lunch break (12:30‑14:00)

Session 7: Compositional & Modular Reasoning (14:30‑15:30)

14:30‑15:00 Viorica Sofronie-Stokkermans (Max Planck Institute for Computer Science)
Local reasoning in verification
The goal of this paper is to show, concretely, the wide applicability of results on hierarchical reasoning in local theory extensions in verification. We start with an up-to-date survey of our results on reasoning in local theory extensions, ranging from characterizations of locality to interpolation. We then provide several examples, emphasizing theories occurring in a natural way in verification. Finally, we present several applications - some already existing in the literature, others obtained during the work in the AVACS project - where such theories occur in a natural way.

15:00‑15:30 Andreas Schlosser (Technische Universität Darmstadt)
Christoph Walther (Technische Universität Darmstadt)
Markus Aderhold (TU Darmstadt)
Axiomatic Specifications in VeriFun
Axiomatic specifications stipulate properties of operations axiomatically and are used to reason about mathematical structures like groups, rings, fields, etc. on an abstract layer. Axiomatic specifications allow the organization of the mathematical structures under investigation in a modularized and hierarchical manner, thus supporting wellstructured presentations. A further advantage is that concrete implementations inherit all instances of the proven properties of a specification after it has been proved that the implementation satisfies the axioms of the specification. To utilize these benefits, the interactive verification tool VeriFun has been extended to support axiomatic specifications. We illustrate the expressiveness of our approach by several examples and compare the features provided with those known from other proposals.