Verifying multi-party authentication protocols

For my MSc thesis at Eindhoven University of Technology, I did some work on the verification of multi-party authentication protocols, using rank functions and the theorem prover PVS. This eventually resulted in a published paper .


Accompanying PVS code

theory PVS version description
csp_rules 4.1/4.2
Neil Evans’ framework for modelling CSP and Schneider’s Rank Theorem, updated from PVS version 3.1 and slightly extended
nsl* 4.1/4.2
Analysis of the Needham-Schroeder-Lowe public key protocol using rank functions
gnsl* 4.1/4.2
Analysis of Cremers and Mauw’s Generalised Needham-Schroeder-Lowe public key protocol, using rank functions

*Requires the csp_rules theory as a library, for which the appropriate path must be set in the file dynetwork.pvs.

Running the gnsl theory

  • Initial set up
    1. Install PVS
    2. Download and uncompress the appropriate versions of the gnsl and csp_rules theories (making sure to adjust the path to the latter in the file dynetwork.pvs)
  • Opening the theory
    1. Start PVS (this opens Emacs)
    2. Change the current context to the folder containing the gnsl with the command M‑x change‑context
    3. Open the file gnsl.pvs
  • Working with the theory
    1. Perform any command on opened file (get PVS help with the command C‑x h)
      • for proving the theory and its importchain, use the command M‑x pri
      • for stepping through a proof, move the cursor onto a lemma and use the command M‑x step-proof (stepping through it with TAB 1 or ESC n TAB 1 for n steps)