Verifying multi-party authentication using rank functions and PVS

R.H.A. Verhoeven, F. Dechesne

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer 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.
Originele taal-2Engels
TitelFormal Aspects in Security and Trust
Subtitel5th International Workshop, FAST 2008, Malaga, Spain, October 9-10, 2008. Revised Selected Papers
RedacteurenP. Degano, J. Guttman, F. Martinelli
Plaats van productieBerlin
Aantal pagina's16
ISBN van elektronische versie978-3-642-01465-9
ISBN van geprinte versie978-3-642-01464-2
StatusGepubliceerd - 2009

Publicatie series

NaamLecture Notes in Computer Science (LNCS)
ISSN van geprinte versie0302-9743


Duik in de onderzoeksthema's van 'Verifying multi-party authentication using rank functions and PVS'. Samen vormen ze een unieke vingerafdruk.

Citeer dit