Formal Correctness of Security Protocols With 62 Figures and 4 Table
Computer network security is critical to fraud prevention and accountability. Network participants are required to observe predefined steps called security protocols, whose proof of correctness is evidence that each protocol step preserves some desired pr
- PDF / 3,317,360 Bytes
- 281 Pages / 439.37 x 666.142 pts Page_size
- 11 Downloads / 215 Views
Giampaolo Bella
Formal Correctness of Security Protocols With 62 Figures and 4 Tables
Author
Series Editor
Giampaolo Bella Università di Catania Dipartimento di Matematica e Informatica Viale Andrea Doria 6 95125 Catania, Italy
Ueli Maurer ¨ Theoretische Informatik Inst. fur ¨ ¨ ETH Zurich, 8092 Zurich Switzerland
[email protected]
Library of Congress Control Number: 2007921678 ACM Computing Classification: C.2.2, D.2.4, D.3.1, F.3.1, F.4.1, I.2.3 ISSN 1619-7100 ISBN-13 978-3-540-68134-2 Springer Berlin Heidelberg New York This work is subject to copyright. All rights are reserved, whether the whole or part of the material is concerned, specifically the rights of translation, reprinting, reuse of illustrations, recitation, broadcasting, reproduction on microfilm or in any other way, and storage in data banks. Duplication of this publication or parts thereof is permitted only under the provisions of the German Copyright Law of September 9, 1965, in its current version, and permission for use must always be obtained from Springer. Violations are liable for prosecution under the German Copyright Law. Springer is a part of Springer Science+Business Media springer.com © Springer-Verlag Berlin Heidelberg 2007 The use of general descriptive names, registered names, trademarks, etc. in this publication does not imply, even in the absence of a specific statement, that such names are exempt from the relevant protective laws and regulations and therefore free for general use. Typesetting: Integra, India Cover design: KünkelLopka, Heidelberg Printed on acid-free paper
SPIN: 11818311
45/3100/Integra
543210
To the loving memory of my father, Carmelo, whose death helped me broaden my views of life. To my mother, Agata, whose loss of eyesight helped me bring those views to a focus.
Foreword
This book describes a key technique, the Inductive Method, for proving the correctness of security protocols. It is clearly written, starting with the basic concepts of cryptography and leading to advanced matters such as smartcards and non-repudiation. The book is also comprehensive and timely, with some of the cited papers still in their journal’s publishing queues. Security protocols are short message exchanges designed to protect sensitive information from being stolen or altered. Mobile phones, Internet shopping sites and subscription television boxes all rely on them. Even with good cryptography, security protocols are subject to many types of attack. Perhaps a hacker can combine pieces of old messages to create what appears to be a valid response to a challenge. The danger is greater if the participants in the transaction can be expected to cheat, as with many Internet purchases. Because the number of possible attacks is infinite, the only way we can be sure that a protocol is correct is by mathematical proof. Researchers have been attempting to prove the correctness of various computer system components since the 1970s. Hardware can be verified to a great extent using logic-based tools such as binary decision diagrams
Data Loading...
