The Journal of Automated Reasoning
Automated Reasoning for
Security Protocol Analysis
*** CALL FOR PAPERS ***
BACKGROUND 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 automated
deduction, model checking, and artificial intelligence. 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 analyzing 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.
In July 2004, the first
Workshop on Automated Reasoning for Security Protocol Analysis (ARSPA)
took place as part of IJCAR 2004. Motivated by the success of the
workshop, the members of the program committee of ARSPA will guest-edit
a Special Issue of the Journal of Automated Reasoning collecting
original papers on developing and applying automated reasoning
techniques and tools for the formal specification and analysis of
Contributions are welcomed on the following topics and related ones:
- Automated analysis and verification of security protocols.
- Languages, logics, and calculi for the design and specification of
- 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.
Alessandro Armando (Universita` di Genova, Italy)
David Basin (ETH Zurich, Switzerland)
Jorge Cuellar (Siemens AG, Munich, Germany)
Michael Rusinowitch (LORIA-INRIA-Lorraine, France)
Luca Vigano` (ETH Zurich, Switzerland)
Authors should submit their papers electronically, in portable
document format (pdf) or postscript (ps), by sending an email with
subject "JAR submission" to the address
with the file of the paper as an attachment, and the following
information in the body of the email, in plain text:
- paper title
- author names
- coordinates of the corresponding author
- abstract of the paper
The cover page of the submission should also include this information.
Authors are strongly encouraged to use Kluwer's LaTeX stylefiles for
journal submissions available at
Submitted papers must be original and not submitted for publication
elsewhere. The submitted papers will be subject to the standard journal
DEADLINE FOR SUBMISSION
NOVEMBER 26, 2004