Verifying multi-party authentication using rank functions and PVS

R.H.A. Verhoeven; F. Dechesne

doi:10.1007/978-3-642-01465-9_15

Verifying multi-party authentication using rank functions and PVS

R.H.A. Verhoeven, F. Dechesne

Formal System Analysis

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

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.

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	https://doi.org/10.1007/978-3-642-01465-9_15
Publication status	Published - 2009

Publication series

Name	Lecture Notes in Computer Science (LNCS)
Volume	5491
ISSN (Print)	0302-9743

Access to Document

10.1007/978-3-642-01465-9_15

Cite this

Verhoeven, R. H. A., & Dechesne, F. (2009). Verifying multi-party authentication using rank functions and PVS. In P. Degano, J. Guttman, & F. Martinelli (Eds.), Formal Aspects in Security and Trust: 5th International Workshop, FAST 2008, Malaga, Spain, October 9-10, 2008. Revised Selected Papers (pp. 226-241). (Lecture Notes in Computer Science (LNCS); Vol. 5491). Springer. https://doi.org/10.1007/978-3-642-01465-9_15

@inproceedings{b22ab20e2be2430e846247e59d55b039,

title = "Verifying multi-party authentication using rank functions and PVS",

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.",

author = "R.H.A. Verhoeven and F. Dechesne",

year = "2009",

doi = "10.1007/978-3-642-01465-9_15",

language = "English",

isbn = "978-3-642-01464-2",

series = "Lecture Notes in Computer Science (LNCS)",

publisher = "Springer",

pages = "226--241",

editor = "P. Degano and J. Guttman and F. Martinelli",

booktitle = "Formal Aspects in Security and Trust",

address = "Germany",

}

Verhoeven, RHA & Dechesne, F 2009, Verifying multi-party authentication using rank functions and PVS. in P Degano, J Guttman & F Martinelli (eds), Formal Aspects in Security and Trust: 5th International Workshop, FAST 2008, Malaga, Spain, October 9-10, 2008. Revised Selected Papers. Lecture Notes in Computer Science (LNCS), vol. 5491, Springer, Berlin, pp. 226-241. https://doi.org/10.1007/978-3-642-01465-9_15

Verifying multi-party authentication using rank functions and PVS. / Verhoeven, R.H.A.; Dechesne, F.

Formal Aspects in Security and Trust: 5th International Workshop, FAST 2008, Malaga, Spain, October 9-10, 2008. Revised Selected Papers. ed. / P. Degano; J. Guttman; F. Martinelli. Berlin : Springer, 2009. p. 226-241 (Lecture Notes in Computer Science (LNCS); Vol. 5491).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Verifying multi-party authentication using rank functions and PVS

AU - Verhoeven, R.H.A.

AU - Dechesne, F.

PY - 2009

Y1 - 2009

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-642-01465-9_15

DO - 10.1007/978-3-642-01465-9_15

M3 - Conference contribution

SN - 978-3-642-01464-2

T3 - Lecture Notes in Computer Science (LNCS)

SP - 226

EP - 241

BT - Formal Aspects in Security and Trust

A2 - Degano, P.

A2 - Guttman, J.

A2 - Martinelli, F.

PB - Springer

CY - Berlin

ER -

Verhoeven RHA, Dechesne F. Verifying multi-party authentication using rank functions and PVS. In Degano P, Guttman J, Martinelli F, editors, Formal Aspects in Security and Trust: 5th International Workshop, FAST 2008, Malaga, Spain, October 9-10, 2008. Revised Selected Papers. Berlin: Springer. 2009. p. 226-241. (Lecture Notes in Computer Science (LNCS)). https://doi.org/10.1007/978-3-642-01465-9_15

Verifying multi-party authentication using rank functions and PVS

Abstract

Publication series

Access to Document

Fingerprint

Cite this