| |
| |
Preface | |
| |
| |
| |
Introduction | |
| |
| |
| |
Security protocols | |
| |
| |
| |
Security properties | |
| |
| |
| |
Cryptography | |
| |
| |
| |
Public-key certificates and infrastructures | |
| |
| |
| |
Encryption modes | |
| |
| |
| |
Cryptographic hash functions | |
| |
| |
| |
Digital signatures | |
| |
| |
| |
Security protocol vulnerabilities | |
| |
| |
| |
The CSP approach | |
| |
| |
| |
Casper: the user-friendly interface of FDR | |
| |
| |
| |
Limits of formal analysis | |
| |
| |
| |
Summary | |
| |
| |
| |
An introduction to CSP | |
| |
| |
| |
Basic building blocks | |
| |
| |
| |
Parallel operators | |
| |
| |
| |
Hiding and renaming | |
| |
| |
| |
Further operators | |
| |
| |
| |
Process behaviour | |
| |
| |
| |
Discrete time | |
| |
| |
| |
Modelling security protocols in CSP | |
| |
| |
| |
Trustworthy processes | |
| |
| |
| |
Data types for protocol models | |
| |
| |
| |
Modelling an intruder | |
| |
| |
| |
Putting the network together | |
| |
| |
| |
Expressing protocol goals | |
| |
| |
| |
The Yahalom protocol | |
| |
| |
| |
Secrecy | |
| |
| |
| |
Authentication | |
| |
| |
| |
Non-repudiation | |
| |
| |
| |
Anonymity | |
| |
| |
| |
Summary | |
| |
| |
| |
Overview of FDR | |
| |
| |
| |
Comparing processes | |
| |
| |
| |
Labelled Transition Systems | |
| |
| |
| |
Exploiting compositional structure | |
| |
| |
| |
Counterexamples | |
| |
| |
| |
Casper | |
| |
| |
| |
An example input file | |
| |
| |
| |
The %-notation | |
| |
| |
| |
Case study: the Wide-Mouthed-Frog protocol | |
| |
| |
| |
Protocol specifications | |
| |
| |
| |
Hash functions and Vernam encryption | |
| |
| |
| |
Summary | |
| |
| |
| |
Encoding protocols and intruders for FDR | |
| |
| |
| |
CSP from Casper | |
| |
| |
| |
Modelling the intruder: the perfect spy | |
| |
| |
| |
Wiring the network together | |
| |
| |
| |
Example deduction system | |
| |
| |
| |
Algebraic equivalences | |
| |
| |
| |
Specifying desired properties | |
| |
| |
| |
Theorem proving | |
| |
| |
| |
Rank functions | |
| |
| |
| |
Secrecy of the shared key: a rank function | |
| |
| |
| |
Secrecy on n[subscript B] | |
| |
| |
| |
Authentication | |
| |
| |
| |
Machine assistance | |
| |
| |
| |
Summary | |
| |
| |
| |
Simplifying transformations | |
| |
| |
| |
Simplifying transformations for protocols | |
| |
| |
| |
Transformations on protocols | |
| |
| |
| |
Examples of safe simplifying transformations | |
| |
| |
| |
Structural transformations | |
| |
| |
| |
Case study: The CyberCash Main Sequence protocol | |
| |
| |
| |
Summary | |
| |
| |
| |
Other approaches | |
| |
| |
| |
Introduction | |
| |
| |
| |
The Dolev-Yao model | |
| |
| |
| |
BAN logic and derivatives | |
| |
| |
| |
FDM and InaJo | |
| |
| |
| |
NRL Analyser | |
| |
| |
| |
The B-method approach | |
| |
| |
| |
The non-interference approach | |
| |
| |
| |
Strand spaces | |
| |
| |
| |
The inductive approach | |
| |
| |
| |
Spi calculus | |
| |
| |
| |
Provable security | |
| |
| |
| |
Prospects and wider issues | |
| |
| |
| |
Introduction | |
| |
| |
| |
Abstraction of cryptographic primitives | |
| |
| |
| |
The refinement problem | |
| |
| |
| |
Combining formal and cryptographic styles of analysis | |
| |
| |
| |
Dependence on infrastructure assumptions | |
| |
| |
| |
Conference and group keying | |
| |
| |
| |
Quantum cryptography | |
| |
| |
| |
Data independence | |
| |
| |
| |
Background cryptography | |
| |
| |
| |
The RSA algorithm | |
| |
| |
| |
The ElGamal public key system | |
| |
| |
| |
Complexity theory | |
| |
| |
| |
The Yahalom protocol in Casper | |
| |
| |
| |
The Casper input file | |
| |
| |
| |
Casper output | |
| |
| |
| |
CyberCash rank function analysis | |
| |
| |
| |
Secrecy | |
| |
| |
| |
Authentication | |
| |
| |
Bibliography | |
| |
| |
Notation | |
| |
| |
Index | |