Muutke küpsiste eelistusi

Modelling & Analysis of Security Protocols [Pehme köide]

  • Formaat: Paperback / softback, 320 pages, kõrgus x laius x paksus: 235x186x16 mm, kaal: 600 g
  • Ilmumisaeg: 06-Dec-2000
  • Kirjastus: Addison Wesley
  • ISBN-10: 0201674718
  • ISBN-13: 9780201674712
Teised raamatud teemal:
  • Pehme köide
  • Hind: 103,14 €*
  • * saadame teile pakkumise kasutatud raamatule, mille hind võib erineda kodulehel olevast hinnast
  • See raamat on trükist otsas, kuid me saadame teile pakkumise kasutatud raamatule.
  • Kogus:
  • Lisa ostukorvi
  • Tasuta tarne
  • Lisa soovinimekirja
  • Formaat: Paperback / softback, 320 pages, kõrgus x laius x paksus: 235x186x16 mm, kaal: 600 g
  • Ilmumisaeg: 06-Dec-2000
  • Kirjastus: Addison Wesley
  • ISBN-10: 0201674718
  • ISBN-13: 9780201674712
Teised raamatud teemal:
Security protocols are one of the most critical elements in enabling the secure communication and processing of information, ensuring its confidentiality, integrity, authenticity and availability. These protocols are vulnerable to a host of subtle attacks, so designing protocols to be impervious to such attacks has proved to be extremely challenging and error prone.   This book provides a thorough and detailed understanding of one of the most effective approaches to the design and evaluation of security critical systems, describing the role of security protocols in distributed secure systems and the vulnerabilities to which they are prey.  The authors introduce security protocols, the role they play and the cryptographic mechanisms they employ, and detail their role in security architectures, e-commerce, e-cash etc. Precise characterizations of key concepts in information security, such as confidentiality, authentication and integrity are introduced and a range of tools and techniques are described which will ensure that a protocol guarantees certain security services under appropriate assumptions.   Modeling and Analysis of Security Protocols provides:

An in-depth discussion of the nature and role of security protocols and their vulnerabilities.

A rigorous framework in which security protocols and properties can be defined in detail.

An understanding of the tools and techniques used to design and evaluate security protocols.
Preface xi
Introduction
1(40)
Security protocols
1(5)
Security properties
6(8)
Cryptography
14(7)
Public-key certificates and infrastructures
21(2)
Encryption modes
23(1)
Cryptographic hash functions
23(1)
Digital signatures
24(4)
Security protocol vulnerabilities
28(6)
The CSP approach
34(3)
Casper: the user-friendly interface of FDR
37(1)
Limits of formal analysis
38(1)
Summary
38(3)
An introduction to CSP
41(36)
Basic building blocks
42(7)
Parallel operators
49(6)
Hiding and renaming
55(5)
Further operators
60(2)
Process behaviour
62(12)
Discrete time
74(3)
Modelling security protocols in CSP
77(16)
Trustworthy processes
77(5)
Data types for protocol models
82(2)
Modelling an intruder
84(3)
Putting the network together
87(6)
Expressing protocol goals
93(32)
The Yahalom protocol
95(2)
Secrecy
97(4)
Authentication
101(9)
Non-repudiation
110(6)
Anonymity
116(6)
Summary
122(3)
Overview of FDR
125(16)
Comparing processes
126(3)
Labelled Transition Systems
129(6)
Exploiting compositional structure
135(4)
Counterexamples
139(2)
Casper
141(20)
An example input file
141(8)
The %-notation
149(2)
Case study: the Wide-Mouthed-Frog protocol
151(6)
Protocol specifications
157(2)
Hash functions and Vernam encryption
159(1)
Summary
160(1)
Encoding protocols and intruders for FDR
161(14)
CSP from Casper
161(2)
Modelling the intruder: the perfect spy
163(4)
Wiring the network together
167(2)
Example deduction system
169(2)
Algebraic equivalences
171(1)
Specifying desired properties
172(3)
Theorem proving
175(26)
Rank functions
177(4)
Secrecy of the shared key: a rank function
181(6)
Secrecy on nB
187(4)
Authentication
191(6)
Machine assistance
197(2)
Summary
199(2)
Simplifying transformations
201(20)
Simplifying transformations for protocols
201(4)
Transformations on protocols
205(3)
Examples of safe simplifying transformations
208(3)
Structural transformations
211(2)
Case study: The CyberCash Main Sequence protocol
213(6)
Summary
219(2)
Other approaches
221(16)
Introduction
221(1)
The Dolev-Yao model
222(1)
BAN logic and derivatives
222(5)
FDM and InaJo
227(1)
NRL Analyser
227(1)
The B-method approach
228(1)
The non-interference approach
229(1)
Strand spaces
229(3)
The inductive approach
232(2)
Spi calculus
234(1)
Provable security
235(2)
Prospects and wider issues
237(8)
Introduction
237(1)
Abstraction of cryptographic primitives
237(1)
The refinement problem
238(1)
Combining formal and cryptographic styles of analysis
238(2)
Dependence on infrastructure assumptions
240(1)
Conference and group keying
240(1)
Quantum cryptography
241(1)
Data independence
242(3)
A Background cryptography 245(8)
A.1 The RSA algorithm
247(1)
A.2 The EIGamal public key system
248(2)
A.3 Complexity theory
250(3)
B The Yahalom protocol in Casper 253(16)
B.1 The Casper input file
253(1)
B.2 Casper output
254(15)
C CyberCash rank function analysis 269(16)
C.1 Secrecy
269(4)
C.2 Authentication
273(12)
Bibliography 285(8)
Notation 293(2)
Index 295


Peter Ryan has over 15 years experience in cryptography and mathematical modelling, computer security and formal methods, gained at GCHQ, CESG, DERA and SRI Cambridge. He is a DERA Fellow, an IMA Fellow and Chair of the Steering Committee of ESORICS. In 1999 he was awarded the title of DERA Fellow.  Steve Schneider is a Senior Lecturer in the Department of Computer Science, Royal Holloway, University of London, UK. He has published a large number of journal and conference papers in the areas of concurrency theory and security.  Michael Goldsmith is Managing Director of Formal Systems (Europe) Ltd, the company which developed the FDR tool and devised the techniques described in the book in collaboration with DERA and the University of Oxford. He is a Senior Research Fellow of Worcester College, Oxford.  Gavin Lowe is a Lecturer in Computer Science at the University of Oxford. He was responsible for discovering the attack on the Needham-Schroeder Public-Key protocol, which established the power of the current approach.   Bill Roscoe is Professor of Computing Science at the University of Oxford. He is one of the principal developers of CSP and of its application to cryptoprotocols and other aspects of computer security.