Verifying multi-party authentication protocols

• Publications
• Accompanying PVS Code
• Running the gnsl theory

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 resulted in a published paper .

Publications

• Master’s thesis Proving correctness of a multi-party authentication protocol with rank functions (2007)
  

  @MASTERSTHESIS{verhoeven2007multiparty,
    author  = {R.H.A. Verhoeven},
    title   = {Proving correctness of a multi-party authentication protocol with rank functions},
    school  = {Eindhoven University of Technology},
    year    = {2007},
    url     = {http://repository.tue.nl/631698}
  }

• Article Verifying Multi-party Authentication Using Rank Functions and PVS, with Francien Dechesne (2008)

Accompanying PVS code

The PVS code is available for multiple versions of PVS. There are three theories.

Theory	Description
csp_rules	Neil Evans’ framework for modelling Communicating Sequential Processes (CSP) and Schneider’s Rank Theorem, updated from PVS version 3.1 and slightly extended
nsl*	Analysis of the Needham-Schroeder-Lowe public key protocol using rank functions
gnsl*	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.

The code is accompanied by the proof summaries generated by PVS, showing the status of each proof. In the proof summaries of theories nsl and gnsl, some proofs of theorems and lemmas are labelled as "incomplete". This is only because those theories depend on the library csp_rules (invoked in dynetwork.pvs). If all the files in csp_rules are imported directly and present within the same directory, instead of being imported as a library, then all theorems and lemmas are proved and labelled "complete".

For PVS version 7.1, also the complete runs of the most important proofs in the theory gnsl are included.

Running the gnsl theory

• Initial set up
  1. Install PVS
  2. Obtain a local copy of the appropriate versions of the gnsl and csp_rules theories (making sure to adjust the path to the latter in the former's file dynetwork.pvs)
• Opening the theory
  1. Start PVS (this opens Emacs)
  2. Change the current context to the folder containing the gnsl theory with the command M‑x change‑workspace (for versions prior to PVS 7.1 use M‑x change‑context instead)
  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)