• Peter Ryan (University of Luxembourg)
  How Many Officials Does it Take to Change an Election?

  Abstract
  It is essential that a voting system provide a high degree of confidence in the accuracy of the outcome. The importance of this as a foundation of democracy has come to prominence in recent years with the 2000 and 2004 US presidential elections, doubts about electronic voting systems in the Netherlands etc. Such assurance is difficult to achieve while at the same time guaranteeing ballot secrecy unless one is prepared to vest a high degree of trust in the process and officials. Recently, considerable progress has been made in developing schemes that do provide strong guarantees of accuracy and privacy with minimal trust assumptions. Such schemes typically make significant use of cryptographic mechanisms. More recent schemes, such a Pret a Voter or Scantegrity II also provide a fairly simple and familiar voter experience. Such schemes provide a high degree of trustworthiness, but the challenge remains to instill trust in such systems, i.e. convince the stakeholders that they should trust the system.
  In this talk I discuss the challenges presented by the design and evaluation of such systems. I will present the notions of voter-verifiability, along with various requirements of voting systems: accuracy, coercion-resistance etc. and outline a number of recent proposals to achieve these properties in a way that is sufficiently usable and understandable to inspire widespread trust.

• David Sands (Chalmers University of Technology)
  Perfecting the Semantics of Imperfect Security

  Abstract
  Declassification is essential in practically useful information flow control systems. However, many semantic models for dynamic information flow mechanisms proposed to date suffer from a common shortcoming: they build on semantic models of security which are inherently flow insensitive, which means that many simple intuitively secure programs will be considered insecure. In this talk we address this problem and propose a solution in the context of a particular rather general dynamic policy mechanism called flow locks.
  [Describing joint work with Niklas Broberg]

• A Policy Model for Secure Information Flow
  Adedayo Adetoye and Atta Badii.
• A General Framework for Nondeterministic, Probabilistic, and Stochastic Noninterference
  Alessandro Aldini and Marco Bernardo.
• Validating Security Protocols under the General Attacker
  Wihem Arsac, Giampaolo Bella, Xavier Chantry and Luca Compagna.
• Achieving Security Despite Compromise Using Zero-Knowledge
  Michael Backes, Martin Peter Grochulla, Catalin Hritcu and Matteo Maffei.
• Usage automata
  Massimo Bartoletti
• Static Detection of Logic Flaws in Service Applications
  Chiara Bodei, Linda Brodo and Roberto Bruni.
• A Compilation Method for the Verification of Temporal-Epistemic Properties of Cryptographic Protocols
  Ioana Boureanu, Mika Cohen and Alessio Lomuscio.
• Type-based Analysis of Financial APIs (extended abstract)
  Matteo Centenaro, Riccardo Focardi, Flaminia Luccio and Graham Steel.
• Analysing PKCS#11 Key Management APIs with Unbounded Fresh Data
  Sibylle Fröschle and Graham Steel.
• Transformations between Cryptographic Protocols
  Joshua Guttman.
• Formal Validation of OFEPSP+ with AVISPA
  Jorge L. Hernandez-Ardieta, Ana I. Gonzalez-Tablas and Benjamin Ramos.
• On the Automated Correction of Protocols with Improper Message Encoding
  Dieter Hutter and Raul Monroy.
• Finite Models in Crypto-Protocol Verification
  Jan Jürjens and Tjark Weber.
• Towards a Type System for Security APIs
  Gavin Keighren, David Aspinall and Graham Steel.
• Separating Trace Mapping and Reactive Simulatability Soundness: The Case of Adaptive Corruption
  Laurent Mazare and Bogdan Warinschi.

Program

Computer security is an established field of computer science of both theoretical and practical significance. In recent years, there has been increasing interest in logic-based foundations for various methods in computer security, including the formal specification, analysis and design of security protocols and their applications, the formal definition of various aspects of security such as access control mechanisms, mobile code security and denial-of-service attacks, and the modeling of information flow and its application to confidentiality policies, system composition, and covert channel analysis.

• Lujo Bauer (CMU, USA)
• Luca Compagna (SAP Research, France)
• Veronique Cortier (LORIA INRIA-Lorraine, France)
• Pierpaolo Degano (Università di Pisa, Italy; co-chair)
• Sandro Etalle (Technical University of Eindhoven, The Netherlands)
• Riccardo Focardi (Università di Venezia, Italy)
• Dieter Gollman (Technische Universität Hamburg-Harburg, Germany)
• Roberto Gorrieri (Università di Bologna, Italy)
• Joshua Guttman (MITRE, USA)
• Jerry den Hartog (Technical University of Eindhoven, The Netherlands)
• Jan Jürjens (The Open University, UK)
• Gavin Lowe (Oxford University, UK)
• Catherine Meadows (Naval Research Laboratory, USA)
• Jonathan Millen (MITRE, USA)
• Sebastian Mödersheim (IBM Zurich Research Lab, Switzerland)
• Mark Ryan (University of Birmingham, UK)
• Luca Viganò (Università di Verona, Italy; co-chair)

Additional Information