Reference from ESORICS proceedings

6th European Symposium on Research in Computer Security (ESORICS 2000)

Analysing Time Dependent Security Properties in CSP Using PVS

Neil Evans, Steve Schneider

Keywords : authentication protocol verification, automated theorem proving, timed behaviour, CSP, PVS

Abstract : This paper details an approach to verifying time dependent authentication properties of security protocols. We discuss the introduction of time into the Communicating Sequential Processes (CSP) protocol verification framework of [Schneider97]. The embedding of CSP in the theorem prover PVS (Prototype Verification System) is extended to incorporate event-based time, retaining the use of the existing rank function approach to verify such properties. An example analysis is demonstrated using the Wide-Mouthed Frog protocol.

(Pages 222-237)

Proceedings table of contents