University College Cork
Cork, Ireland
Sunday, July 04, 2004

The proceedings have been published: ENTCS volume 125 issue 1

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. Moreover, 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.
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. Thus, this progress can be seen as one of the recent success stories of the automated reasoning community.

The workshop will bring together researchers and practitioners from both the security and the automated reasoning 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.


The program will consist of the following talks (click on the presentation titles to download the slides) Here is a preliminary schedule:

09:00 - 09:10 Welcome
09:10 - 10:00 Foley
10:00 - 10:30 Bond, Clulow
10:30 - 11:00 Coffee break
11:00 - 11:30 Chen, Clark, Jacob
11:30 - 12:00 Lynch, Meadows
12:00 - 12:30 Chevalier, Küsters, Rusinowitch, Turuani
12:30 - 14:00 Lunch
14:00 - 14:30 Caleiro, Viganò, Basin
14:30 - 15:00 Armando, Compagna
15:00 - 15:30 Mazaré
15:30 - 16:00 Coffee break
16:00 - 16:30 Steel, Bundy
16:30 - 17:00 Hankes Drielsma, Mödersheim
17:00 - 17:15 Kleiner, Roscoe
17:15 - 17:30 Sadri, Toni


The informal proceedings contain all accepted contributions will be will be distributed at the workshop.
Click here to download the
pdf file.

Moreover, workshop participants will be invited to submit full versions of their papers to a special issue of the Journal of Automated Reasoning, which will be open also to non-participants, in all cases with fresh reviewing.

Organization and Program Committee


The workshop is open to all interested persons.

Workshop Venue

The workshop will be held on July 04 as part of IJCAR 2004 (2nd International Joint Conference on Automated Reasoning), University College Cork, Cork, Ireland, July 04 - July 08, 2004.


For further information on the workshop, please send an email to arspa at avispa-project dot org

Last modified: Fri Mar 18 14:50:16 CET 2005