EXTENDED DEADLINE *** 25 May 2001 ***
Workshop on Logical Aspects of Cryptographic Protocol Verification
Post-CAV Workshop on Logical Aspects of
Cryptographic Protocol Verification
July 23, 2001
Paris, France
Aims and Scope
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. It is the aim of
this one-day workshop to bring together researchers in the field of
cryptographic protocol verification to share new results in the
field. Specific domains of interest are, among others:
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.
A selection of accepted papers will be published in a volume of
Electronic Notes in Theoretical Computer Science. The workshop will be
held after CAV'01 in the same location (la Mutualit ). CAV'01 follows
FMICS'01 and SAS'01.
Invited Speakers
Roberto Amadio, title to be announced.
Michael Rusinowitch will talk on the CASRUL cryptographic protocol verification system and on the complexity of attack
detection.
Yassine Lakhnech, title to be announced.
Submission Information
Submissions should be in PostScript format. The body of each
submission should start with a short abstract and should be at most 10
pages long. The submission may include in addition an appendix
containing technical details, which reviewers may read or not, at
their discretion. The submission should contain the contact author's
physical and e-mail addresses and phone number.
Submissions should be sent by email to goubault@lsv.ens-cachan.fr
Hubert Comon
LSV, ENS Cachan
Mourad Debbabi
Universit Laval, Qubec
Jon Millen
Computer Science Lab, SRI International
Scott Stoller
State University of New York, Stony Brook