文件名称：Formal Correctness of Security Protocols
文件大小：3.99MB
文件格式：ZIP
更新时间：2015-04-18 18:11:18
formal method protocol correctness
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 (BDDs) and model checkers. Software seems much more resistant to verification; recent celebrated work using SAT solvers can only prove very simple properties. Security protocols are software; to be precise, they are concurrent algorithms based on cryptographic operations. Unusually, these algorithms include a threat model: one process is assumed to be an enemy with wide powers to capture and combine other people’s messages. Given these complicating factors, it is unsurprising that protocol verification became a long-standing open problem in computer security. As late as 1995, the problem appeared to be intractable. Today, however, security protocols can be verified automatically using a number of freely available tools. Though many side issues remain, the core problem must be regarded as solved. Many people can take credit for this remarkable success. In particular, Oxford’s Security Research Group pioneered the use of model checkers to analyse protocols [142]. Their work has been widely copied. However, model checkers do not prove properties: they search a finite space for possible flaws. Being automatic, they are excellent for debugging, but the failure to find a bug does not mean that none exist. The Inductive Method described in the present volume takes some ideas from the Oxford group, such as their message primitives, and applies them in the context of proof. Industrial-grade protocols such as SSL/TLS, Kerberos and even the huge SET protocol suite [37] can then be tackled. Although these proofs are far from automatic, the effort needed to undertake them is considerably less than that required to design the protocol in the first place. Merely to derive an abstract protocol from the standards documents can take weeks, a task that automatic tools cannot escape. Giampaolo Bella is amply qualified to write this book. He has been involved with the Inductive Method almost from its inception. He has worked to extend its scope, for example to smartcards, and to refine the types of properties it can express. These efforts also illustrate why the Inductive Method is still valuable in the era of off-the-shelf protocol verifiers. It can help explain how these verifiers work: some of them are based on formal models similar to those described in this book. Besides, off-the-shelf tools inherently have a limited scope: they are designed to solve problems of a particular sort. Bella has shown that the Inductive Method can easily be extended to new security environments, which can then be studied formally. Such work enables the development of a new generation of automatic tools, and so the field progresses. Cambridge, February 2006 Lawrence C. Paulson
【文件预览】：
11-Verifying a Smartcard Protocol.pdf
2-The Analysis of Security Protocols.pdf
7-Verifying a Deployed Protocol.pdf
14-Conclusions.pdf
13-Verifying Two Accountability Protocols.pdf
10-Modelling Smartcards.pdf
9-139-151 Verifying Another Deployed Protocol.pdf
8-Modelling Agents’ Knowledge of Messages.pdf
4-Verifying the Protocol Goals.pdf
1-Introduction.pdf
12-Modelling Accountability.pdf
back-matter.pdf
3-The Inductive Method.pdf
6-Modelling Timestamping and Verifying a Classical Protocol.pdf
front-matter.pdf
5-The Principle of Goal Availability.pdf