文件名称:
Formal Correctness of Security Protocols
开发工具:
文件大小: 3mb
下载次数: 0
上传时间: 2012-03-29
详细说明： 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 s ubscription 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 ...展开收缩
(系统自动生成,下载前可以参看下载内容)
下载文件列表
相关说明
- 本站资源为会员上传分享交流与学习,如有侵犯您的权益,请联系我们删除.
- 本站是交换下载平台，提供交流渠道，下载内容来自于网络，除下载问题外，其它问题请自行百度。
- 本站已设置防盗链，请勿用迅雷、QQ旋风等多线程下载软件下载资源，下载后用WinRAR最新版进行解压.
- 如果您发现内容无法下载，请稍后再次尝试；或者到消费记录里找到下载记录反馈给我们.
- 下载后发现下载的内容跟说明不相乎，请到消费记录里找到下载记录反馈给我们，经确认后退回积分.
- 如下载前有疑问，可以通过点击"提供者"的名字，查看对方的联系方式，联系对方咨询.
