********************************
*** NEW: PROCEEDINGS TO BE   ***
***      PUBLISHED IN ENTCS  ***
********************************


				ARSPA'05

			 The Second Workshop on
			Automated Reasoning for
		      Security Protocol Analysis

			co-located with ICALP'05
			    Lisboa, Portugal
		             July 16, 2005

		  http://www.avispa-project.org/arspa


			***********************
			*** CALL FOR PAPERS ***
			***********************


		  Submission deadline: April 15, 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:

- Automated analysis and verification of security protocols.
- Languages, logics and calculi for the design and specification of
    security protocols.
- Verification methods: accuracy, efficiency.
- Decidability and complexity of cryptographic verification problems.
- Synthesis and composition of security protocols.
- Integration of formal security specification, refinement and
    validation techniques in development methods and tools.

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.



AUDIENCE
========

The workshop will be held on Saturday, July 16, 2005, and will be open to
all interested persons.



INVITED TALKS
=============

The technical program will include presentations of the accepted papers,
and one or two invited talks.



PROGRAM COMMITTEE
=================

- Alessandro Armando  (Universita` di Genova, Italy)
- David Basin  (ETH Zurich, Switzerland)
- Jorge Cuellar  (SIEMENS AG, Munich, Germany)
- Pierpaolo Degano (Universita` di Pisa, Italy; co-chair)
- Joshua Guttman  (The MITRE Corporation, USA)
- Roberto Gorrieri  (Universita` di Bologna, Italy)
- Sjouke Mauw  (University of Eindhoven, The Netherlands)
- Hanne Riis Nielson  (Technical University of Denmark)
- Michael Rusinowitch  (INRIA-LORRAINE, Nancy, France)
- Luca Vigano` (ETH Zurich, Switzerland; co-chair)



SUBMISSION
==========

Submissions should be at most 15 pages (a4paper, 11pt) and the cover
page should include title, names of authors, and the co-ordinates of the
corresponding author.
Authors are invited to submit their papers electronically, as portable
document format (pdf) or postscript (ps), by the deadline of April 15,
2005.
The only mechanism for paper submissions is via the electronic
submission web-site, accessible via the workshop web-site.
Notification of acceptance or rejection will be sent to the authors no
later than May 14, 2005.
Final versions of accepted papers must be received by June 06, 2005.



PUBLICATION
===========

Accepted contributions will be be published in a special volume of the
Electonic Notes in Theoretical Computer Science ENTCS. 
Informal proceedings will be available at the workshop and be
published on-line on the workshop's web page at
		  http://www.avispa-project.org/arspa
We are also planning a formal post-workshop publication as a special
Journal issue, with an additional reviewing process.



IMPORTANT DATES
===============

- Submission deadline:        April 15, 2005
- Notification of acceptance: May   15, 2005
- Final versions due:         June  06, 2005
- Workshop:                   July  16, 2005



WORKSHOP WEB-SITE
=================

http://www.avispa-project.org/arspa

The workshop is supported by the IST Project AVISPA
(http://www.avispa-project.org)


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