The Coinductive Approach to Verifying Cryptographic Protocols

  • Jesse Hughes
  • Martijn Warnier
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2755)


We look at a new way of specifying and verifying cryptographic protocols using the Coalgebraic Class Specification Language. Protocols are specified into CCSL (with temporal operators for ”free”) and translated by the CCSL compiler into theories for the theorem prover PVS. Within PVS, the desired security conditions can then be (dis)proved.

In addition, we are interested in using assumptions which are reflected in real-life networks. However, as a result, we present only a partial solution here. We have not proved full correctness of a protocol under such loose restrictions. This prompts discussion of what assumptions are acceptable in protocol verification, and when practical concerns may outweigh theoretical motivations.


Message Passing Security Protocol Practical Concern Cryptographic Protocol Protocol Message 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: The spi calculus. In: Proceedings of the Fourth ACM Conference on Computer and Communications Security, April 1997, pp. 36–47. ACM Press, New York (1997)Google Scholar
  2. 2.
    Burrows, M., Abadi, M., Needham, R.: A logic of authentication. Proc. Royal Soc., Series A 426, 233–271 (1989)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Clark, J., Jacob, J.: A Survey of Authentication Protocol Literature, version 1.0 (1997), available at
  4. 4.
    Dolev, D., Yao, A.: On the security of public key protocols. IEEE Transactions on Information Theory 29(6) (1983)Google Scholar
  5. 5.
    Lowe, G.: An attack on the Needham-Schroeder public-key authentication protocol. Information Processing Letters 56, 131–133 (1995)CrossRefzbMATHGoogle Scholar
  6. 6.
    Lowe, G.: Casper: A compiler for the analysis of security protocols. In: PCSFW: Proceedings of The 10th Computer Security Foundations Workshop. IEEE Computer Society Press, Los Alamitos (1997)Google Scholar
  7. 7.
    Millen, J., Shmatikov, V.: Constraint solving for bounded-process cryptographic protocol analysis. In: 8th ACM Conference on Computer and Communication Security, ACM SIGSAC, November 2001, pp. 166–175 (2001)Google Scholar
  8. 8.
    Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Communications of the ACM 21(12), 993–999 (1978)CrossRefzbMATHGoogle Scholar
  9. 9.
    Owre, S., Rushby, J.M., Shankar, N., von Henke, F.: Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Trans. on Softw. Eng. 21(2), 107–125 (1995)CrossRefGoogle Scholar
  10. 10.
    Paulson, L.C.: Isabelle. LNCS, vol. 828. Springer, Heidelberg (1994)CrossRefzbMATHGoogle Scholar
  11. 11.
    Paulson, L.C.: The inductive approach to verifying cryptographic protocols. Journ. of Computer Security 6, 85–128 (1998)CrossRefGoogle Scholar
  12. 12.
    Rothe, J., Tews, H., Jacobs, B.: The coalgebraic class specification language CCSL. Journal of Universal Comp. Sci. 7(2) (2001)Google Scholar
  13. 13.
    Shanker, N., Owre, S., Rushby, J.M., Stringer-Calvert, D.: PVS prover guide, Version 2.3 (1999)Google Scholar
  14. 14.
    Tews, H.: Coalgebraic Methods for Object Oriented Specification. PhD thesis, Technical University of Dresden (October 2002)Google Scholar
  15. 15.
    Thayer, F.J., Herzog, J.C., Guttman, J.D.: Strand spaces: Proving security protocols correct. Journal of Computer Security 7(1) (1999)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Jesse Hughes
    • 1
  • Martijn Warnier
    • 1
  1. 1.Computing Science InstituteUniversity of NijmegenNijmegenThe Netherlands

Personalised recommendations