Verifying multi-party authentication using rank functions and PVS

R.H.A. Verhoeven, F. Dechesne

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review


In this paper we present a fully formal correctness proof of a multi-party version of the Needham-Schroeder-Lowe public key authentication protocol. As the protocol allows for an arbitrary number of participants, the model consisting of all possible protocol executions exceeds any bounds imposed by model checking methods. By modelling the protocol in the CSP-framework and using the Rank Theorem we obtain an abstraction level that allows to give a correctness proof in PVS for the protocol with respect to authentication, for the protocol running in parallel in multiple instantiations, possibly with different numbers of agents for each instance.

This specific result shows how, more generally, the formalisation in CSP and application of the theorem prover PVS make full formal verification of multi-party security protocols possible.
Original languageEnglish
Title of host publicationFormal Aspects in Security and Trust
Subtitle of host publication5th International Workshop, FAST 2008, Malaga, Spain, October 9-10, 2008. Revised Selected Papers
EditorsP. Degano, J. Guttman, F. Martinelli
Place of PublicationBerlin
Number of pages16
ISBN (Electronic)978-3-642-01465-9
ISBN (Print)978-3-642-01464-2
Publication statusPublished - 2009

Publication series

NameLecture Notes in Computer Science (LNCS)
ISSN (Print)0302-9743


Dive into the research topics of 'Verifying multi-party authentication using rank functions and PVS'. Together they form a unique fingerprint.

Cite this