Lisbon, Portugal
Saturday, July 16, 2005

Background, aim and scope

Experience over the last twenty years has shown that, even assuming perfect cryptography, the design of security protocols (or cryptographic protocols, as they are sometimes called) 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.

Work in this direction initially started in the security community but recently there has been a tremendous progress thanks to contributions from different automated reasoning communities, such as model checking, resolution, planning, rewriting/narrowing, and higher-order theorem proving. There has been another wave of progress due to research in applying non-classical logics, such as epistemic and belief logics, to analyze protocols and their properties. Moreover, a third stream includes static methods, among which those based on abstract interpretation, data and control flow analysis, and type systems proved to be particularly successful. Finally, bisimulations and related techniques have also been applied successfully.

Based on this progress, a large number of formal methods and tools have been developed that have been quite successful in determining strengths and weaknesses of many protocols, i.e. in proving the correctness of the protocols or in identifying attacks on them.

The ARSPA workshop aims to bring together researchers and practitioners from both the security and the formal methods communities, from academia and industry, who are working on developing and applying automated reasoning techniques and tools for the formal specification and analysis of security protocols.

Contributions are welcomed on the following topics or related ones:

The workshop will provide a forum for all researchers and practitioners who are interested in this area to share their ideas and report their results. We thus solicit submissions of papers both on mature work and on work in progress.

All submissions will be peer-reviewed. Authors of accepted papers must guarantee that their paper will be presented at the workshop.


The workshop will be open to all interested persons.

Program Committee

Accepted papers

Invited Talks


09:00 - 09:15 Welcome by Pierpaolo Degano and Luca Viganò
09:15 - 10:05 Invited talk by John C. Mitchell
Protocol Analysis: Wireless Networking and Mobility
10:05 - 10:45 Cas Cremers, Sjouke Mauw, Erik de Vink
A Syntactic Criterion for Injectivity of Authentication Protocols
10:45 - 11:15 Coffee break
11:15 - 11:55 Alexey Gotsman, Fabio Massacci, Marco Pistore
Towards an Independent Semantics and Verification Technology for the HLPSL Specification Language
11:55 - 12:35 Kenji Imamoto and Kouichi Sakurai
Design and Analysis of Diffie-Hellman-Based Key Exchange Using One-time ID by SVO Logic
12:45 - 14:15 Lunch
14:15 - 15:05 Invited talk by Michael Backes
Justifying Formal Methods and Cryptography under Active Attacks, and Limitations Thereof
15:05 - 15:45 Carlos Caleiro, Luca Viganò, David Basin
Deconstructing Alice and Bob
15:45 - 16:15 Coffee break
16:15 - 16:55 Christoffer Rosenkilde Nielsen, Esben Heltoft Andersen, Hanne Riis Nielson
Static Validation of a Voting Protocol
16:55 - 17:35 Monica Nesi and Giuseppina Rucci
Formalizing and Analyzing the Needham-Schroeder Symmetric-Key Protocol by Rewriting
17:35 - 18:15 Deepak D'Souza, K.R. Raghavendra, Barbara Sprick
An Automata Based Approach for Verifying Information Flow Properties
18:15 - 18:45 Final discussion
20:30 - Workshop dinner

The workshop dinner will take place, starting from 20:30, at the Restaurante Charcutaria, Rua do Alecrim 47-A.

A map showing the location can be found here and a more detailed map here.


Accepted contributions have been published as volume 135(1) of the Electonic Notes in Theoretical Computer Science ENTCS.

We are also planning a formal post-workshop publication as a special Journal issue, with an additional reviewing process.

Workshop Venue

The workshop will be held on July 16 as part of ICALP 2005, the 32nd International Colloquium on Automata, Languages and Programming, July 11-15, 2005, Lisbon, Portugal.

For problems, questions, or requests of further information on the workshop, please send an email to

Last modified: Tue Aug 9 11:05:05 CEST 2005