Next: Introduction

CSP, PVS and a Recursive Authentication Protocol

Jeremy Bryans and Steve Schneider
Department of Computer Science
Royal Holloway and Bedford New College
Egham, Surrey, TW20 0EX

Introduction
CSP
- Traces
The protocol
- CSP Description
Authentication
- A key theorem
Translating to PVS notation
- The authentication property
Incorrect Implementation
- PVS analysis
- Corrected Implementation
Dealing with failed proofs
References