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

[img]
Preview
PDF (licence)
32Kb
[img]
Preview
PDF
Available under License : See the attached licence file.

203Kb

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.

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
ID Code:738611
Deposited By:Symplectic Elements
Deposited On:07 Dec 2012 19:20
Last Modified:27 Mar 2013 02:33

Document Downloads

Repository Staff Only: item control page


Information about this web site

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