University of Surrey

Test tubes in the lab Research in the ATI Dance Research

A theorem-proving approach to verification of fair non-repudiation protocols

Wei, K and Heather, J (2007) A theorem-proving approach to verification of fair non-repudiation protocols Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 4691 L. pp. 202-219.

Available under License : See the attached licence file.

Download (208kB)
Text (licence)

Download (33kB)


We use a PVS embedding of the stable failures model of CSP to verify non-repudiation protocols, allowing us to prove the correctness of properties that are difficult to analyze in full generality with a model checker. The PVS formalization comprises a semantic embedding of CSP and a collection of theorems and proof rules for reasoning about non-repudiation properties. The well-known Zhou-Gollmann protocol is analyzed within this framework. © Springer-Verlag Berlin Heidelberg 2007.

Item Type: Article
Divisions : Faculty of Engineering and Physical Sciences > Computing Science
Authors :
Wei, K
Heather, J
Date : 2007
Contributors :
Additional Information : © Springer-Verlag Berlin Heidelberg 2007. The original publication is available at
Depositing User : Symplectic Elements
Date Deposited : 07 Dec 2012 19:20
Last Modified : 31 Oct 2017 14:52

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