• Joshua Guttman, MITRE
  What is Cryptographic Protocol Analysis?

  Abstract
  Instead of formalizing the behavior of cryptographic protocol participants at runtime, like much of the literature, we formalize the actions of the protocol analyst.
  We view protocol analysis as a labeled transition system. A node represents a partial description of a set of executions. Transitions represent ways to add information to a description. This transition relation is complete for a simple, Dolev-Yao-style analysis.
  The modal mu-calculus associated with this transition system expresses results of protocol analysis, such as confidentiality and authentication properties. Moreover, two different protocols that differ inessentially, e.g. only in the forms of messages, will satisfy exactly the same formulas. Thus, elementary equivalence in this logic appears to represent "having the same analysis" as a relation between protocols. Moreover, a portion of this logic -- the set of formulas of a particular form -- is preserved by the steps of a protocol design process.

• Virgil Gligor, ECE Department and CyLab, CMU Pittsburgh
  On the Evolution of Adversary Models in Cryptographic Protocols (Part II: the Fragility of Adversary Definitions)

  (based on joint work with B. Parno, T. Kwon and J. S. Shin)

  Abstract
  In a previous presentation with a similar title, I argued that new computing technologies introduce new security vulnerabilities, which sometimes require the re-definition of the adversary assumed by security designs [1]. An example of such technologies is provided by networks whose nodes operate in an unattended manner, such as sensor and mesh networks. The question of how to (re)define an adversary, and how to prove that a cryptographic protocol (e.g., an encryption scheme, an entity authentication protocols) counters that adversary, has been answered rather successfully in modern cryptography. Some of these proofs are even carried out with the benefit of automated protocol-analysis tools.
  In this talk, I argue that adversary definitions that have been successfully used in cryptography theory are fragile; i.e., restrictions placed on the adversary behavior can be circumvented in practice. Fragility is caused by mismatches between the computational models assumed by adversary definitions and the practical realities of large-scale networks, such as the Internet. For example, a large number of encryption/decryption oracles may be available to an adversary in practice when only single-oracle access is assumed in theory; or bounds on the number of attack queries that can be issued by an adversary in theory cannot be enforced in practice. I illustrate these mismatches in two examples. In the first, a PPT adversary is defined as a RAM with access to an oracle for encryption and one for decryption. However, if the computational model is changed and a large, but bounded, number of different oracles operating concurrently becomes available to a network adversary, which is otherwise weaker that Dolev and Yao.s, then encryption schemes that offer a very strong sense of security (i.e., schemes proved to be IND-CCA2 secure) can be broken with non-negligible probability. (This example is based on joint work with Bryan Parno.) In the second example, bounds placed on the number of attack queries launched by an adversary against password-based authenticated key exchange (PAKE) protocols whose security is proven in either the standard or the random oracle models, can be circumvented by multi-threaded client-server models of computation in Internet. (This is based on joint work with Taekyoung Kwon and Ji Sun Shin.)
  I conclude that adversary definitions used in cryptographic-protocol analyses must come with .warning labels. regarding the models of computation assumed and the security vulnerabilities that might arise in practice when model mismatches arise. Good theory owes this to good practice.
  [1] V. D. Gligor. On the Evolution of Adversary Models in Cryptographic Protocols (or Know your Friend and Foe Alike), Proc. of the 13th International Workshop on Security Protocols, Cambridge University, UK, April 2005, Springer Verlag, LNCS vol. 4631, pp. 276-283
  

• A Note on First-order Logic and Security Protocols
  Reynald Affeldt and Hubert Comon-Lundh
• Active Intruders with Caps
  Siva Anantharaman, Hai Lin, Christopher Lynch, Paliath Narendran and Michael Rusinowitch
• Type-checking Zero-knowledge
  Michael Backes, Catalin Hritcu and Matteo Maffei
• Testing Decision Procedures for Security-by-Contract
  Nataliia Bielova, Fabio Massacci and Ida Sri Rejeki Siahaan
• Statically Detecting Message Confusions in a Multi-Protocol Setting
  Chiara Bodei, Linda Brodo, Pierpaolo Degano and Han Gao
• On Secure Distributed Implementations of Dynamic Access Control
  Avik Chaudhuri
• Chaining Secure Channels
  Christopher Dilloway
• A Logic for Reasoning about Networked Secure Systems
  Deepak Garg, Jason Franklin, Dilsun Kaynar and Anupam Datta
• Computationally Sound Symbolic Anonymity of a Ring Signature
  Yusuke Kawamoto, Hideki Sakurada and Masami Hagiya
• Automated Proofs for Asymmetric Encryption
  Pascal Lafourcade, Cristian Ene, Yassine Lakhnech, Judicaël Courant and Marion Daubignard
• Analysing Object-Capability Security
  Toby Murray
• Separating two roles of hashing in one-way message authentication
  Long Nguyen and Bill Roscoe
• Using Elyjah to Analyse Java Implementations of Cryptographic Protocols
  Nicholas O'Shea
• MultiTrust: An Authorization Framework with Customizable Distributed Proof Construction
  Charles Zhang and Marianne Winslett
• Certificates for Tree Automata Completion
  Roberto Zunino

Program

The only mechanism for paper submissions is via the

Important dates

• Alessandro Aldini (Università di Urbino, Italy)
• Alessandro Armando (Università di Genova, Italy)
• Michael Backes (Universität des Saarlandes, Germany)
• Lujo Bauer (CMU, USA; co-chair)
• Veronique Cortier (LORIA INRIA-Lorraine, France)
• Cas Cremers (ETH Zurich, Switzerland)
• Pierpaolo Degano (Universita` di Pisa, Italy)
• Sandro Etalle (Technical University of Eindhoven, The Netherlands; co-chair)
• Riccardo Focardi (Universita` di Venezia, Italy)
• Dieter Gollman (Technische Universität Hamburg-Harburg, Germany)
• Jerry den Hartog (Technical University of Eindhoven, The Netherlands; co-chair)
• Jan Jürjens (The Open University, UK)
• Ralf Küsters (Universität Trier, Germany)
• Gavin Lowe (Oxford University, UK)
• Catherine Meadows (Naval Research Laboratory, USA)
• Sebastian Mödersheim (IBM Zurich Research Lab, Switzerland)
• Mark Ryan (University of Birmingham, UK)
• Luca Viganò (Università di Verona, Italy; co-chair)
• Steve Zdancewic (University of Pennsylvania, USA)