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 .

## 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

theory | PVS version | description |
---|---|---|

`csp_rules` |
4.1/4.2 6 |
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 6 |
Analysis of the Needham-Schroeder-Lowe public key protocol using rank functions |

`gnsl` * |
4.1/4.2 6 |
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
- Install PVS
- 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
- Start PVS (this opens Emacs)
- Change the current context to the folder containing the
`gnsl`

with the command`M‑x change‑context`

- Open the file
`gnsl.pvs`

- Working with the theory
- 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`

for*n*TAB 1*n*steps)

- for proving the theory and its importchain, use the command

- Perform any command on opened file (get PVS help with the command