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.
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.
|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:||23 Sep 2013 19:52|
Actions (login required)
Downloads per month over past year