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.
| PDF (licence) 32Kb | |
| 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
Tools
Tools