Program & Workshop Co-ChairsS. Autexier (U. Saarbrücken)H. Mantel (DFKI Saarbrücken)
Program CommitteeD. Basin (U. Freiburg)I. Cervesato (ITT Industries) R. Focardi (U. Venezia) R. Hähnle (Chalmers U.) N. Heintze (Agere Systems) A. Ireland (Heriot-Watt, Edinburgh) D. Kapur (U. New Mexico, Albuquerque) C. Kreitz (Cornell, Ithaca) F. Martinelli (CNR Pisa) F. Massacci (U. di Trento) C. Meadows (NRL) S. Schneider (Royal Holloway, U. London)
Call for papers
Online Proceedings
|
| Submission Deadline: | April 22, 2002 |
| Notification of acceptance: | May 31, 2002 |
| Final version due: | June 25, 2002 |
| Early registration: | June 15, 2002 |
| Workshop date: | July 25-26, 2002 |
Contact
If you need further information do not hesitateto contact us by sending an e-mail to verification-ws@ags.uni-sb.de (Subject: `Information').
Preliminary Workshop Program
| Thursday, July 25th, 2002 | |
| Session 1: Applications of ATP in Verification | |
| 8:45 - 9:00 | Welcoming and Opening Remarks |
| 9:00 - 9:30 | D. Kröning: Application Specific Higher Order Logic Theorem Proving |
| 9:30 - 10:00 | V. Vanackère: The TRUST protocol analyser, Automatic and efficient verification of cryptographic protocols |
| 10:00 - 10:30 | C. Benzmüller, C. Giromini, A. Nonnengart, J. Zimmer: Reasoning Services in MathWeb-SB for symbolic verification of Hybrid Systems |
| 10:30 - 11:00 | Coffee Break |
| Session 2: Logical Approaches (Joint with FCS) | |
| 11:00 - 11:30 | A. W. Appel, N. G. Michael, A. Stump, R. Virga: A Trustworthy Proof Checker |
| 11:30 - 12:00 | E. Cohen: Proving Protocols Safe from Guessing |
| 12:00 - 12:30 | A. Armando, L. Compagna: Automatic SAT-Compilation of Protocol Insecurity via Reduction to Planning |
| 12:30 - 14:00 | Lunch |
| Session 3: (Joint with FCS) | |
| 14:00 - 15:30 | VERIFY Invited Talk: F. Massacci: Formal Verification of SET by Visa and Mastercard: Lessons for Formal Methods in Security |
| 15:30 - 16:00 | Coffee Break |
| Session 4: Security Protocols (Joint with FCS) | |
| 16:00 - 16:30 | C. Meadows: Identifying Potential Type Confusion in Authenticated Messages |
| 16:30 - 17:00 | G. Steel, A. Bundy, E. Denney: Finding Counterexamples to Inductive Conjectures and Discovering Security Protocol Attacks |
| Friday, July 26th, 2002 | |
| Session 5: (Joint with FCS) | |
| 9:00 - 10:30 | FCS Invited Talk: D. Gollmann: Defining Security is Difficult and Error Prone |
| 10:30 - 11:00 | Coffee Break |
| Session 6: Specification and Verification | |
| 11:00 - 11:30 | A. L. Herzog, J. Guttman: Eager Formal Methods for Security Management |
| 11:30 - 12:00 | A. Armando, M.-P. Bonacina, S. Ranise, M. Rusinowitch, A. K. Sehgal: High-performance deduction for verification: a case study in the theory of arrays |
| 12:00 - 12:30 | B. Beckert, U. Keller, P.H. Schmidt: Translating the Object Constraint Language into First-order Predicate Logic |
| 12:30 - 14:00 | Lunch |
| Session 7: (Joint with FCS) | |
| 14:00 - 15:30 |
Panel: The Future of Protocol Verification Panelists: Ernie Cohen, Microsoft Research, UKL; Alan Jeffrey, DePaul University, USA; Fabio Martinelli, CNR, Italy; Fabio Massacci, University of Trento, Italy; Catherine Meadows, Naval Research Laboratory, USA; David Basin (tentative), Albert-Ludwigs-Universität, Germany |
| 15:30 - 15:40 | Closing Remarks |
Topic
Traditionally, verification has been one of the main areas of application for automated theorem proving. On the one hand side, the formal development of safety or security critical systems creates numerous deduction problems that are not only interesting and challenging but also of practical relevance. On the other hand, automated theorem proving offers the means to reduce the development burden in such formal developments, thus making them feasible.
The aim of this verification workshop is to bring together people who are interested in the development of safety and security critical systems, in formal methods in general, in automated theorem proving, and in tool support for formal developments. The overall objective of VERIFY is on the identification of open problems and the discussion of possible solutions under the theme
The emphasis of this years workshop will be on the application of formal methods to issues in computer security. Computer security is of fast-growing importance as computer systems more and more affect various aspects of everyday life. Examples are electronic commerce, computer assisted business processes, air traffic control, and multi-functional chipcards as well as databases containing personal data like, e.g., social security information, health records, or bank accounts. To ensure the security of those systems is a primordial task because security violations may endanger financial assets or even human lives. The application of formal methods during the development process results in a high confidence that the resulting systems operate correctly. Major research topics in this area are the modelling of security requirements and the development of powerful theorem proving support. Therefore, submissions in this area are especially encouraged.
Topics of interest include (but are not limited to)
| + Access control | + Protocol verification |
| + ATP techniques in verification | + Refinement and decomposition |
| + Case studies (specification and verification) | + Reuse of specifications and proofs |
| + Combination of verification systems | + Safety critical systems |
| + Compositional and modular reasoning | + Security for mobile computing |
| + Fault tolerance | + Security models |
| + Gaps between problems and techniques | + Verification systems |
| + Information flow control |
Due to the focus on security of this years workshop, there are common interests with the LICS workshop on foundations of computer security, FCS. Joint submissions to both workshops were possible which are presented in VERIFY/FCS joint sessions at the workshop.