Abstract
A non-repudiation protocol of Zhou and Gollmann [18] has been mechanically verified. A non-repudiation protocol gives each party evidence that the other party indeed participated, evidence sufficient to present to a judge in the event of a dispute. We use the theorem-prover Isabelle [10] and model the security protocol by an inductive definition, as described elsewhere [1,12]. We prove the protocol goals of validity of evidence and of fairness using simple strategies. A typical theorem states that a given piece of evidence can only exist if a specific event took place involving the other party.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
G. Bella. Message Reception in the Inductive Approach. Research Report 460, University of Cambridge — Computer Laboratory, 1999.
G. Bella. Modelling Agents’ Knowledge Inductively. In Proc. of the 7th International Workshop on Security Protocols, LNCS 1796. Springer-Verlag, 1999.
G. Bella. Mechanising a protocol for smart cards. In Proc. of International Conference on Research in Smart Cards (e-Smart’01), LNCS. Springer-Verlag, 2001. In Press.
G. Bella, F. Massacci, L.C. Paulson, and P. Tramontano. Formal Verification of Cardholder Registration in SET. In F. Cuppens, Y. Deswarte, D. Gollmann, and M. Waidner, editors, Proc. of the 6th European Symposium on Research in Computer Security (ESORICS 2000), LNCS 1895, pages 159–174. Springer-Verlag, 2000.
G. Bella and L.C. Paulson. Kerberos Version IV: Inductive Analysis of the Secrecy Goals. In J.-J. Quisquater, Y. Deswarte, C. Meadows, and D. Gollmann, editors, Proc. of the 5th European Symposium on Research in Computer Security (ESORICS’98), LNCS 1485, pages 361–375. Springer-Verlag, 1998.
G. Bella and L.C. Paulson. Mechanising BAN Kerberos by the Inductive Method. In A. J. Hu and M. Y. Vardi, editors, Proc. of the International Conference on Computer-Aided Verification (CAV’98), LNCS 1427, pages 416–427. Springer-Verlag, 1998.
M. Ben-Or, O. Goldreich, S. Micali, and R. Rivest. A Fair Protocol for Signing Contracts. IEEE Transactions on Information Theory, 36(1):40–46, 1990.
C.A. Meadows. The NRL Protocol Analyzer: An Overview. Journal of Logic Programming, 26(2):113–131, 1996.
T. Okamoto and K. Ohta. How to Simultaneously Exchange Secrets by General Assumptions. In Proc. of the 2nd ACM Conference on Computer and Communication Security (CCS’94), pages 184–192, 1994.
L.C. Paulson. Isabelle: A Generic Theorem Prover. LNCS 828. Springer-Verlag, 1994.
L.C. Paulson. Theory for public-key protocols, 1996. http://www4.informatik.tu-muenchen.de/~isabelle/library/HOL/Auth/Public.html.
L.C. Paulson. The Inductive Approach to Verifying Cryptographic Protocols. Journal of Computer Security, 6:85–128, 1998.
L.C. Paulson. Inductive Analysis of the Internet protocol TLS. ACM Transactions on Computer and System Security, 1999. In press.
P.Y.A. Ryan and S.A. Schneider. The Modelling and Analysis of Security Protocols: the CSP Approach. Addison-Wesley, 2000.
S. Schneider. Verifying Authentication Protocols with CSP. In Proc. of the 10th IEEE Computer Security Foundations Workshop, pages 3–17. IEEE Computer Society Press, 1997.
S. Schneider. Formal Analysis of a Non-Repudiation Protocol. In Proc. of the 11th IEEE Computer Security Foundations Workshop. IEEE Computer Society Press, 1998.
G. Zhou and D. Gollmann. Towards Verification of Non-Repudiation Protocols. In Proc. of the 1998 International Refinement Workshop and Formal Methods Pacific, pages 370–380. Springer-Verlag, 1998.
J. Zhou and D. Gollmann. A Fair Non-Repudiation Protocol. In Proc. of the 15th IEEE Symposium on Security and Privacy, pages 55–61. IEEE Computer Society Press, 1996.
J. Zhou and D. Gollmann. An Efficient Non-Repudiation Protocol. In Proc. of the 10th IEEE Computer Security Foundations Workshop, pages 126–132. IEEE Computer Society Press, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bella, G., Paulson, L.C. (2001). Mechanical Proofs about a Non-repudiation Protocol. In: Boulton, R.J., Jackson, P.B. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2001. Lecture Notes in Computer Science, vol 2152. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44755-5_8
Download citation
DOI: https://doi.org/10.1007/3-540-44755-5_8
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42525-0
Online ISBN: 978-3-540-44755-9
eBook Packages: Springer Book Archive