University of Surrey

Test tubes in the lab Research in the ATI Dance Research

Verifying authentication protocol implementations

Schneider, Steve A (2002) Verifying authentication protocol implementations In: 5th International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS 2002), 20 - 22 March 2002, Enschede, The Netherlands.

This is the latest version of this item.

Available under License : See the attached licence file.

Download (242kB)
[img] Text (licence)

Download (1kB)


Formal methods for verifying authentication protocols tend to assume an idealised, perfect form of encryption. This approach has been spectacularly successful in finding flaws, but when we aim for proofs of correctness then we need to consider this assumption more carefully, and perhaps to weaken it to reflect properties of real cryptographic mechanisms. This paper reviews the existing CSP approach to verifying protocols, and considers how algebraic properties of real cryptographic mechanisms can be incorporated within a rank function verification. The approach is illustrated with an authentication protocol which makes use of exclusive-or.

Item Type: Conference or Workshop Item (Conference Paper)
Divisions : Faculty of Engineering and Physical Sciences > Computer Science
Authors :
Schneider, Steve
Editors :
Jacobs, B
Rensink, A
Date : 20 March 2002
Copyright Disclaimer : Copyright 2002 Springer
Additional Information : This is the author's version of the paper presented at FMoods 2002.
Depositing User : Mr Adam Field
Date Deposited : 05 Sep 2017 11:09
Last Modified : 06 Jul 2019 05:08

Available Versions of this Item

Actions (login required)

View Item View Item


Downloads per month over past year

Information about this web site

© The University of Surrey, Guildford, Surrey, GU2 7XH, United Kingdom.
+44 (0)1483 300800