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.

[img]
Preview
PDF
fairness_pvs.pdf
Available under License : See the attached licence file.

Download (208kB)
[img]
Preview
PDF (licence)
SRI_deposit_agreement.pdf

Download (33kB)

Abstract

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 http://www.springerlink.com
Divisions: Faculty of Engineering and Physical Sciences > Computing Science
Depositing User: Symplectic Elements
Date Deposited: 07 Dec 2012 19:20
Last Modified: 09 Jun 2014 13:14
URI: http://epubs.surrey.ac.uk/id/eprint/738611

Actions (login required)

View Item View Item

Downloads

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