Formal analysis of a non-repudiation protocol
- 1 January 1998
- proceedings article
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
The paper applies the theory of communicating sequential processes (CSP) to the modelling and analysis of a non-repudiation protocol. Non-repudiation protocols differ from authentication and key-exchange protocols in that the participants require protection from each other, rather than from an external hostile agent. This means that the kinds of properties that are required of such a protocol, and the way it needs to be modelled to enable analysis, are different to the standard approaches taken to the more widely studied class of protocols and properties. A non-repudiation protocol proposed by Zhou and Gollmann (1996) is analysed within this framework, and this highlights some novel considerations that are required for this kind of protocoKeywords
This publication has 9 references indexed in Scilit:
- A semantic model for authentication protocolsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Towards a completeness result for model checking of security protocolsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Proving properties of security protocols by inductionPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- The Interrogator modelPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- A Calculus for Cryptographic Protocols: The Spi CalculusInformation and Computation, 1999
- Verifying authentication protocols with CSPPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1997
- Security properties and CSPPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1996
- A formal language for cryptographic protocol requirementsDesigns, Codes and Cryptography, 1996
- Three systems for cryptographic protocol analysisJournal of Cryptology, 1994