Preface Volume 55, Issue 1

AbstractThis volume contains the Proceedings of the First Workshop on Logical Aspects of Cryptographic Protocol Verification (LACPV'2001), held in Paris, France, July 23, 2001 as a satellite workshop of CAV'01.Security of computer systems is a growing field of concerns. While security in the large is quite a large and daunting field, the study of cryptographic protocols has received renewed interest in recent years, mostly because of the emergence of electronic commerce. The focus in cryptographic protocols, as opposed to mere cryptography, is the interaction of cryptographic primitives with message exchanges and possible malevolent actions from intruders. Most of the discovered bugs in cryptographic protocols are not so much tied to subtleties in cryptography, rather to logical aspects of interactions between principals.From a protocol-oriented point of view, cryptographic protocols pose new challenges: there may be an unbounded number of principals (processes in parallel), state spaces are infinite even with bounded numbers of principals, and so on. Several models exist that handle the complexity of cryptographic protocol verification, based on process calculi, first-order logic, automata theory, complexity theory among others.As such, cryptographic protocol verification is emerging as a research field in its own right, strongly linked to logic. The purpose of the LACPV workshop is to bring together researchers in the field of cryptographic protocol verification to share new results in the field. Domains of interest include formal relationships between models of cryptographic protocols, translations, expressive power; comparison between verification methods, accuracy, efficiency; fragments of first-order logic or extensions corresponding to various problems of interest in cryptographic protocol verification; decidability and complexity of cryptographic verification problems, reachability, decidable subcases; new logics and calculi for verifying cryptographic protocols; new approaches to reduce state spaces from infinite to finite; logical characterizations of confidentiality/secrecy, authentication/integrity, non-duplication, non-repudiation, etc.Three invited talks, by Y. Lakhnech, M. Rusinowitch, and R. Amadio, plus five submitted papers out of ten were selected for presentation at LACPV'2001. They were reviewed by the program committee consisting, besides editor, of Hubert ComonLSV, ENS CachanMourad DebbabiUniversité Laval, QuébecJon MillenComputer Science Lab, SRI InternationalScott StollerState University of New York, Stony BrookThis volume will be published as volume 55, issue 1, in the series Electronic Notes in Theoretical Computer Science (ENTCS). This series is published electronically through the facilities of Elsevier Science B.V. and its auspices. The volumes in the ENTCS series can be accessed at the URL http://www.elsevier.nl/locate/entcsA printed version of the current volume is distributed to the participants at the workshop in Paris.We are very grateful to the following persons, whose help has been crucial for the success of LACPV'2001: Alain Finkel for his help in managing CAV satellite workshops; Mike Mislove, one of the Managing Editors of the ENTCS series, for his assistance with the use of the ENTCS style files.July 05, 2001Jean Goubault-Larrec