V. Cortier - Formal Models and Techniques for Analyzing Security Protocols

FORMAL MODELS AND TECHNIQUES FOR ANALYZING SECURITY PROTOCOLS Cryptology and Information Security Series The Cryptology & Information Security Series (CISS) presents the latest research results in the theory and practice, analysis and design, implementation, application and experience of cryptology and information security techniques. It covers all aspects of cryptology and information security for an audience of information security researchers with specialized

technical backgrounds.

Coordinating Series Editors: Raphael C.-W. Phan and Jianying Zhou Series editors

Feng Bao, Institute for Infocomm Research, Singapore Nasir Memon, Polytech University, USA Kefei Chen, Shanghai Jiaotong University, China Chris Mitchell, RHUL, United Kingdom Robert Deng, SMU, Singapore David Naccache, cole Normale Sup rieure, France Yevgeniy Dodis, New York University, USA Gregory Neven, IBM Research, Switzerland Dieter Gollmann, TU Hamburg-Harburg, Germany Phong Nguyen, CNRS / cole Normale Suprieure, France Markus Jakobsson, Indiana University, USA Andrew Odlyzko, University of Minnesota, USA Marc Joye, Thomson R&D, France Adam Young, MITRE Corporation, USA Javier Lopez, University of Malaga, Spain Moti Yung, Columbia University, USA

Volume 5

Recently published in this series

Vol. 4. Y. Li and J. Zhou (Eds.), Radio Frequency Identification System Security RFIDsec10 Asia Workshop Proceedings

Vol. 3. C. Czosseck and K. Geers (Eds.), The Virtual Battlefield: Perspectives on Cyber Warfare

Vol. 2. M. Joye and G. Neven (Eds.), Identity-Based Cryptography Vol. 1. J. Lopez and J. Zhou (Eds.), Wireless Sensor Network Security

ISSN 1871-6431 (print)

ISSN 1879-8101 (online)

Formal Models and Techniques for Analyzing Security Protocols

Edited by

Vronique Cortier

CNRS

and

Steve Kremer

INRIA

Amsterdam Berlin Tokyo Washington, DC

2011 The authors and IOS Press.

All rights reserved. No part of this book may be reproduced, stored in a retrieval system, or transmitted, in any form or by any means, without prior written permission from the publisher. ISBN 978-1-60750-713-0 (print)

ISBN 978-1-60750-714-7 (online)

Library of Congress Control Number: 2011923591

Publisher

IOS Press BV

Nieuwe Hemweg 6B

1013 BG Amsterdam

The Netherlands

fax: +31 20 687 0019

e-mail: order@iospress.nl

Distributor in the USA and Canada

IOS Press, Inc.

4502 Rachael Manor Drive

Fairfax, VA 22032

USA

fax: +1 703 323 3668

e-mail: iosbooks@iospress.com

LEGAL NOTICE

The publisher is not responsible for the use which might be made of the following information. PRINTED IN THE NETHERLANDS

Formal Models and Techniques for Analyzing Security Protocols v

V. Cortier and S. Kremer (Eds.)

IOS Press, 2011

2011 The authors and IOS Press. All rights reserved.

Preface

Security protocols are small distributed programs which aim to achieve security proper-ties such as confidentiality, authentication, anonymity, etc. Nowadays, security proto-cols are omnipresent in our daily lives: home-banking, electronic commerce, mobile phones, etc. However, because these protocols are generally implemented on poten-tially insecure networks (e.g. the Internet) they are extremely difficult to devise. Using Roger Needhams words Security protocols are three line programs that people still manage to get wrong. Based on the seminal work of Dolev and Yao, symbolic meth-ods for analyzing such protocols have been in development for about 25 years. The main components of these models are the perfect cryptography assumption and an un-bounded non-deterministic adversary that has complete control of the network.

The field of symbolic analysis of security protocols has seen significant advances during the last few years. We now have a better understanding of decidability and com-plexity questions and models with solid theoretical foundations have been developed together with proof techniques. Automated tools have also been designed and success-fully applied to numerous protocols, including industrial protocols, for the provision of security or the discovery of attacks, and models have been extended with algebraic properties in order to weaken the perfect cryptography assumption. Recently, even computational soundness results towards cryptographic models have been achieved.

However, the field was still missing a book which summarized the state-of-the-art of these advances. While we certainly do not pretend to give a complete overview of the field, which would be impossible in a single book, nevertheless, we believe that we have covered a representative sample of the ongoing work in this field, which is still very active. This book contains an introduction and 10 tutorial-like chapters on selected

topics, each written by a leading expert in the field of formal analysis of security proto-cols. We are extremely grateful to all the authors for their hard work and effort in pre-paring these chapters.

January 2011

Vronique Cortier and Steve Kremer

This page intentionally left blank

Contents

Preface v Vronique Cortier and Steve Kremer

Introduction 1 Vronique Cortier and Steve Kremer

Verifying a Bounded Number of Sessions and Its Complexity 13 Michael Rusinowitch and Mathieu Turuani

Constraint Solving Techniques and Enriching the Model with Equational Theories 35

Hubert Comon-Lundh, Stphanie Delaune and Jonathan K. Millen Analysing Security Protocols Using CSP 62

Gavin Lowe

Using Horn Clauses for Analyzing Security Protocols 86

Bruno Blanchet

Applied pi Calculus 112

Mark D. Ryan and Ben Smyth

Types for Security Protocols 143

Riccardo Focardi and Matteo Maffei

Protocol Composition Logic 182

Anupam Datta, John C. Mitchell, Arnab Roy and Stephan Hyeonjun Stiller Shapes: Surveying Crypto Protocol Runs 222

Joshua D. Guttman

Security Analysis Using Rank Functions in CSP 258

Steve Schneider

Computational Soundness The Case of Diffie-Hellman Keys 277 Emmanuel Bresson, Yassine Lakhnech, Laurent Mazar and Bogdan Warinschi

Author Index 303

This page intentionally left blank

Formal Models and Techn i ques for Analyz i ng Secur i ty Protocols

V . Cort i er and S . Kremer (Eds . )

IOS Press, 2011

2011 The authors and IOS Press . All r i ghts reserved .

do i :10 . 3233/978-1-60750-714-7-1

Introduction

Vronique CORTIER a and Steve KREMER b

a LORIA, CNRS

b LSV, ENS Cachan & CNRS & INRIA

Formal methods have shown their interest when developing critical systems, where safety or security is important. This is particularly true in the eld of security protocols. Such protocols aim at securing communications over a public network. Small aws in the development of such systems may cause important economical damages. Examples of security protocols include the Transport Layer Security (TLS) protocol and its prede-cessor, the Secure Sockets Layer (SSL). These protocols are typically used for guaran-teeing a secure connection to a web site in particular for secure payment over the Inter-net. Most web browsers display a small lock to indicate that you are executing a secure session using one of these protocols. Another emergent application of security protocol is electronic voting. For instance, in the 2007 national elections in Estonia the govern-ment offered the possibility to vote via the Internet. The development of such proto-cols is error-prone and aws are regularly discovered. For example, the SAML 2.0 Web Browser Single Sign-On authentication system developed by Google has recently been attacked. The Single Sign-On protocol allows a user to identify himself only once and then access to various applications (such as Gmail or Google calendar). While designing a formal model of this protocol, Armando et al [ACC + 08] discovered that a dishonest service provider could actually impersonate any of its users at another service provider. This aw has been corrected since. Those examples show the need of precise security guarantees when designing protocols. Moreover, the relatively small size of security pro-tocols makes the use of formal verication reasonable.