PVS code

file	PVS version	description
pvs42_csp-rules.tar.gz	4.1/4.2	Neil Evans' framework for modelling CSP and Schneider's Rank Theorem, updated from PVS version 3.1 and slightly extended
pvs42_nsl.tar.gz	4.1/4.2	Analysis of the Needham-Schroeder-Lowe public key protocol using rank functions
pvs42_gnsl.tar.gz	4.1/4.2	Analysis of Cremers and Mauw's Generalised Needham-Schroeder-Lowe public key protocol, using rank functions

Master's Thesis

Proving correctness of a multi-party authentication protocol with rank functions

@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}
}

Site last updated: 11-11-2008 (new PVS version)
Site will not be maintained after 15-11-2008. The PVS code will be transferred to Francien Dechesne's site.