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)