From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Delivered-To: caml-list@yquem.inria.fr Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id 1B069BC28 for ; Wed, 3 Nov 2004 11:21:03 +0100 (CET) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id iA3AL2C5029278 for ; Wed, 3 Nov 2004 11:21:02 +0100 Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id LAA23434 for ; Wed, 3 Nov 2004 11:21:02 +0100 (MET) From: lvigano@inf.ethz.ch Received: from medoc.inf.ethz.ch (medoc.inf.ethz.ch [129.132.178.200]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id iA3AL2ha029274 for ; Wed, 3 Nov 2004 11:21:02 +0100 Received: from localhost (localhost [127.0.0.1]) by medoc.inf.ethz.ch (Postfix) with ESMTP id D02EA16880 for ; Wed, 3 Nov 2004 11:20:50 +0100 (MET) Received: from medoc.inf.ethz.ch ([127.0.0.1]) by localhost (medoc [127.0.0.1]) (amavisd-new, port 10024) with LMTP id 09256-01-10 for ; Wed, 3 Nov 2004 11:20:50 +0100 (MET) Received: from localhost.localdomain (lennox.inf.ethz.ch [129.132.178.21]) by medoc.inf.ethz.ch (Postfix) with ESMTP id 82857168EC for ; Wed, 3 Nov 2004 11:20:38 +0100 (MET) Received: (from lvigano@localhost) by localhost.localdomain (8.11.6/8.9.3) id iA3AKmI18338 for caml-list@pauillac.inria.fr; Wed, 3 Nov 2004 11:20:48 +0100 Date: Wed, 3 Nov 2004 11:20:48 +0100 Message-Id: <200411031020.iA3AKmI18338@localhost.localdomain> To: caml-list@pauillac.inria.fr Subject: CFP: JAR special issue on Automated Reasoning for Security Protocol Analysis X-Virus-Scanned: by amavisd-new at inf.ethz.ch X-Miltered: at concorde with ID 4188B10E.001 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at concorde with ID 4188B10E.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; cfp:01 error-prone:01 model:01 logics:01 logics:01 decidability:01 synthesis:01 genova:01 rusinowitch:01 2004.:98 universita:98 basin:98 26,:98 abstract:01 postscript:01 X-Spam-Checker-Version: SpamAssassin 3.0.0 (2004-09-13) on yquem.inria.fr X-Spam-Status: No, score=0.2 required=5.0 tests=FORGED_RCVD_HELO,NO_REAL_NAME autolearn=disabled version=3.0.0 X-Spam-Level: Special Issue of The Journal of Automated Reasoning on Automated Reasoning for Security Protocol Analysis http://www.avispa-project.org/arspa *********************** *** 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 security protocols. 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 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. EDITORS ======= 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) SUBMISSION ========== 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 arspa@avispa-project.org 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 http://www.wkap.nl/authors/jrnlstylefiles/ Submitted papers must be original and not submitted for publication elsewhere. The submitted papers will be subject to the standard journal refereeing process. DEADLINE FOR SUBMISSION ======================= NOVEMBER 26, 2004 WEB-SITE ======== http://www.avispa-project.org/arspa