Abstract
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.
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 language | English |
---|---|
Title of host publication | Formal Aspects in Security and Trust |
Subtitle of host publication | 5th International Workshop, FAST 2008, Malaga, Spain, October 9-10, 2008. Revised Selected Papers |
Editors | P. Degano, J. Guttman, F. Martinelli |
Place of Publication | Berlin |
Publisher | Springer |
Chapter | 15 |
Pages | 226-241 |
Number of pages | 16 |
ISBN (Electronic) | 978-3-642-01465-9 |
ISBN (Print) | 978-3-642-01464-2 |
DOIs | |
Publication status | Published - 2009 |
Publication series
Name | Lecture Notes in Computer Science (LNCS) |
---|---|
Volume | 5491 |
ISSN (Print) | 0302-9743 |