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. 202 - 219.

Available under License : See the attached licence file.

Download (208kB)
PDF (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
Additional Information: © Springer-Verlag Berlin Heidelberg 2007. The original publication is available at
Divisions: Faculty of Engineering and Physical Sciences > Computing Science
Depositing User: Symplectic Elements
Date Deposited: 07 Dec 2012 19:20
Last Modified: 18 Sep 2014 01:59

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