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:
All submissions will be peer-reviewed. Authors of accepted papers must
guarantee that their paper will be presented at the workshop.
Tool-supported proofs of security protocols typically rely on
abstractions from real cryptography by term algebras, so-called
Dolev-Yao models. However, there was traditionally no cryptographic
justification, i.e., no theorem that said what a proof with a Dolev-Yao
abstraction implied for the real implementation, even if provably secure
cryptographic primitives are used.
There are several kinds of automated reasoning methods for security
protocol analysis, including model checking, theorem proving, and
symbolic search methods. Our group has carried out recent case studies
using finite-state checking and a formal protocol logic, including
studies of wireless networking protocols and some approaches to network
mobility. These case studies provide interesting insight into specific
protocols and motivate improvements in the methods that are useful for
analyzing other protocols. This talk will describe the methods, recent
progress, and case studies.
The workshop dinner will take place, starting from 20:30, at the Restaurante Charcutaria, Rua do
Alecrim 47-A. A map showing the location can be found here and a more detailed map here.
We are also planning a formal post-workshop publication as a special
Journal issue, with an additional reviewing process.
The workshop will be held on July 16 as part of ICALP 2005,
the 32nd International Colloquium on Automata, Languages and Programming,
July 11-15, 2005, Lisbon, Portugal.
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.
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.Audience
The workshop will be open to all interested persons.Program Committee
Accepted papers
Carlos
Caleiro, Luca Viganò, and David Basin
Cas Cremers, Sjouke Mauw, and Erik de
Vink
Deepak D'Souza, K.R. Raghavendra, and Barbara
Sprick
Alexey
Gotsman, Fabio Massacci, and Marco Pistore
Kenji Imamoto and Kouichi Sakurai
Monica Nesi and
Giuseppina Rucci
Christoffer Rosenkilde
Nielsen, Esben Heltoft Andersen, and Hanne Riis NielsonInvited Talks
Justifying Formal
Methods and Cryptography under Active Attacks, and Limitations
Thereof
We show how to justify a Dolev-Yao style model under active attacks and
in arbitrary protocol environments. The justification is done by
defining an ideal system handling Dolev-Yao style terms and a
cryptographic realization with the same user interface, and by showing
that the realization is as secure as the ideal system in the sense of
reactive simulatability. The Dolev-Yao style system contains asymmetric
and symmetric encryptions, digital signatures, and MACs, and the
definition of reactive simulatability encompasses arbitrary active
attacks and enjoys general composition and property-preservation
properties. Security holds in the standard model of cryptography and
under standard assumptions of adaptively secure primitives.
Furthermore, we show that hashes in their usual generality in Dolev-Yao
models cannot be proven sound with respect to their cryptographic
counterparts in the sense of reactive simulatability. For XOR we even
show that no Dolev-Yao model can be proven sound with respect to any at
least moderately natural realization of the XOR function. On the
positive side, we show that XOR can be proven sound under passive
attacks and that hash functions can be proven sound if we restrict their
usage in specific and easily checkable way.
Protocol Analysis:
Wireless Networking and MobilitySchedule
09:00 - 09:15
Welcome by Pierpaolo Degano and Luca Viganò
09:15 - 10:05
Invited talk by John C. Mitchell
Protocol
Analysis: Wireless Networking and Mobility
10:05 - 10:45
Cas Cremers, Sjouke Mauw, Erik de Vink
A Syntactic Criterion for
Injectivity of Authentication Protocols
10:45 - 11:15
Coffee break
11:15 - 11:55
Alexey Gotsman, Fabio Massacci, Marco Pistore
Towards an
Independent Semantics and Verification Technology for the HLPSL
Specification Language
11:55 - 12:35
Kenji Imamoto and Kouichi Sakurai
Design and Analysis of
Diffie-Hellman-Based Key Exchange Using One-time ID by SVO Logic
12:45 - 14:15
Lunch
14:15 - 15:05
Invited talk by Michael Backes
Justifying
Formal Methods and Cryptography under Active Attacks, and Limitations
Thereof
15:05 - 15:45
Carlos Caleiro, Luca Viganò, David Basin
Deconstructing
Alice and Bob
15:45 - 16:15
Coffee break
16:15 - 16:55
Christoffer Rosenkilde Nielsen, Esben Heltoft Andersen, Hanne Riis
Nielson
Static Validation of a Voting Protocol
16:55 - 17:35
Monica Nesi and Giuseppina Rucci
Formalizing and Analyzing the
Needham-Schroeder Symmetric-Key Protocol by Rewriting
17:35 - 18:15
Deepak D'Souza, K.R. Raghavendra, Barbara Sprick
An Automata Based
Approach for Verifying Information Flow Properties
18:15 - 18:45
Final discussion
20:30 -
Workshop dinner
Publication
Accepted contributions have been published as volume 135(1) of the Electonic Notes in Theoretical
Computer Science ENTCS.
Last modified: Tue Aug 9 11:05:05 CEST 2005