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.
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.
References
Abadi, M., Blanchet, B.: Computer-Assisted Verification of a Protocol for Certified Email. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 316–335. Springer, Heidelberg (2003)
Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Transactions on Information Theory 29(2) (1983)
Dutertre, B., Schneider, S.A.: Embedding CSP in PVS: an application to authentication protocols. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol. 1275, Springer, Heidelberg (1997)
Evans, N.: Investigating Security through Proof. PhD thesis, Royal Holloway, University of London (2003)
Gürgens, S., Rudolph, C.: Security analysis of (un-) fair non-repudiation protocols. In: Abdallah, A.E., Ryan, P.Y A., Schneider, S. (eds.) FASec 2002. LNCS, vol. 2629, pp. 97–114. Springer, Heidelberg (2003)
Kremer, S., Markowitch, O., Zhou, J.: An intensive survey of non-repudiation protocols. Technical Report 473 (2002)
Kremer, S., Raskin, J.-F.: A game-based verification of non-repudiation and fair exchange protocols. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, Springer, Heidelberg (2001)
Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 147–166. Springer, Heidelberg (1996)
Markowitch, O., Roggeman, Y.: Probabilistic non-repudiation without trusted third party. In: Second Workshop on Security in Communication Network 99 (1999)
Roscoe, A.W.: Modelling and verifying key-exchange protocols using CSP and FDR. In: Proceedings of 8th IEEE Computer Security Foundations Workshop (1995)
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall International, Englewood Cliffs (1998)
Ryan, P., Schneider, S., Goldsmith, M., Lowe, G., Roscoe, B.: The Modelling And Analysis Of Security Protocols. Addison Wesley, London (2000)
Schneider, S.A.: Formal analysis of a non-repudiation protocol. In: Proceedings of the 11th IEEE Computer Security Foundations Workshop (1998)
Schneider, S.A.: Verifying authentication protocols in CSP. IEEE TSE, 24(9) (September 1998)
Schneider, S.A.: Concurrent and real-time systems: the CSP approach. John Wiley & Sons, West Sussex, England (1999)
Shmatikov, V., Mitchell, J.C.: Analysis of abuse-free contract signing. In: Frankel, Y. (ed.) FC 2000. LNCS, vol. 1962, pp. 174–191. Springer, Heidelberg (2001)
Tedrick, T.: How to exchange half a bit. In: CRYPTO, pp. 147–151 (1983)
Wei, K., Heather, J.: Embedding the stable failures model of CSP in PVS. In: accepted by Fifth International Conference on Integrated Formal Methods, Eindhoven, The Netherlands (2005)
Wei, K., Heather, J.: Towards verification of timed non-repudiation protocols. In: Dimitrakos, T., Martinelli, F., Ryan, P.Y A., Schneider, S. (eds.) FAST 2005. LNCS, vol. 3866, Springer, Heidelberg (2006)
Zhou, J., Gollmann, D.: A fair non-repudiation protocol. In: Proceedings of the IEEE Symposium on Research in Security and Privacy, Oakland, CA, pp. 55–61. IEEE Computer Society Press, Los Alamitos (1996)
Zhou, J., Gollmann, D.: Towards verification of non-repudiation protocols. In: Proceedings of 1998 International Refinement Workshop and Formal Methods Pacific, pp. 370–380, Canberra, Australia (September 1998)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wei, K., Heather, J. (2007). A Theorem-Proving Approach to Verification of Fair Non-repudiation Protocols. In: Dimitrakos, T., Martinelli, F., Ryan, P.Y.A., Schneider, S. (eds) Formal Aspects in Security and Trust. FAST 2006. Lecture Notes in Computer Science, vol 4691. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-75227-1_14
Download citation
DOI: https://doi.org/10.1007/978-3-540-75227-1_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-75226-4
Online ISBN: 978-3-540-75227-1
eBook Packages: Computer ScienceComputer Science (R0)