Embedding CSP in PVS: An Application to Authentication Protocols
Bruno Dutertre, Steve A. Schneider · 2013
In [28], Schneider applies CSP to the modelling and analysis of authentication protocols and develops a general proof strategy for verifying authentication properties. This paper shows how the PVS theorem prover can provide effective mechanical support to the approach. Contents 1 Introduction 1 2 Authentication Protocols in CSP 3 2.1 CSP notation : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 3 2.2 A general model for authentication protocols : : : : : : : : : : : : : 4 2.3 Checking authentication properties : : : : : : : : : : : : : : : : : : : 7 3 An Embedding of CSP in PVS 9 3.1 Lists : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 10 3.2 Basic CSP : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 14 3.3 Parametric processes : : : : : : : : : : : : : : : : : : : : : : : : : : : 18 3.4 Properties of processes : : : : : : : : : : : : : : : : : : : : : : : : : : 21 3.5 Fixed points and induction : : : : : : : : : : : : : : : ...