| |
| |
| 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 | |