Formal Verification of a Type Flaw Attack on a Security Protocol Using Object-Z

  • Benjamin W. Long
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3455)


We have identified a type flaw attack on the Amended Needham Schroeder Protocol with Conventional Keys due to a potential oversight at the presentation layer of the network architecture. Using Object-Z, a formal specification of the protocol is presented allowing us to state the assumed properties of the presentation layer explicitly. Object-Z’s schema calculus is used to verify the attack we have found and the weaknesses upon which the attack depends, thus enabling us to minimise the effort required to prevent the attack and to specify this as part of the model accordingly.


IEEE Computer Society Application Layer Security Protocol Incoming Message 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.
    Boyd, C.: Hidden assumptions in cryptographic protocols. IEE Proceedings, Part E, 433–436 (November 1990)Google Scholar
  2. 2.
    Bozzano, M.: A Logic-Based Approach to Model Checking of Parameterized and Infinite-State Systems. PhD thesis, DISI, University of Genova (June 2002),
  3. 3.
    Bozzano, M., Delzanno, G.: Automated protocol verification in linear logic. In: Proceedings of the Fourth ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, pp. 38–49. ACM Press, New York (2002)CrossRefGoogle Scholar
  4. 4.
    Brackin, S.H.: Evaluating and improving protocol analysis by automatic proof. In: Proceedings of 11th IEEE Computer Security Foundations Workshop (CSFW 1998), pp. 138–152. IEEE Computer Society Press, Los Alamitos (1998)Google Scholar
  5. 5.
    Carlsen, U.: Generating formal cryptographic protocol specifications. In: Proceedings of the 1994 IEEE Computer Society Symposium on Research in Security and Privacy, pp. 137–146. IEEE Computer Society Press, Los Alamitos (1994)CrossRefGoogle Scholar
  6. 6.
    1999 Common Criteria for Information Technology Security Evaluation. Version 2.1. CCIMB-99-031 (August 1999),
  7. 7.
    Clark, J., Jacob, J.: A survey of authentication protocol literature: Version 1.0 (1997), (accessed May 2003)
  8. 8.
    Denning, D.E., Sacco, G.M.: Timestamps in key distribution protocols. Communications of the ACM 24(8), 533–536 (1981)CrossRefGoogle Scholar
  9. 9.
    Donovan, B., Norris, P., Lowe, G.: Analyzing a library of security protocols using Casper and FDR. In: Proceedings of the Workshop on Formal Methods and Security Protocols, Trento, Italy (1999)Google Scholar
  10. 10.
    Duke, R., Rose, G.: Formal Object-Oriented Specification Using Object-Z. Cornerstones of Computing. Macmillan Press Limited, UK (2000)Google Scholar
  11. 11.
    Heather, J., Lowe, G., Schneider, S.: How to prevent type flaw attacks on security protocols. In: Proceedings of 13th IEEE Computer Security Foundations Workshop (CSFW 2000), pp. 32–43. IEEE Computer Society Press, Los Alamitos (2000)Google Scholar
  12. 12.
    Long, B.W.: Formal verification of type flaw attacks in security protocols. In: Proceedings of the 10th Asia-Pacific Software Engineering Conference (APSEC) 2003, pp. 415–424. IEEE Computer Society, Los Alamitos (2003)CrossRefGoogle Scholar
  13. 13.
    Meadows, C.: Identifying potential type confusion in authenticated messages. In: Proceedings of Workshop on Foundation of Computer Security (FCS 2002), pp. 75–84 (2002) (Published as a joint DIKU technical report),
  14. 14.
    Needham, R., Schroeder, M.: Using encryption for authentication in large networks of computers. Communications of the ACM 21(12), 993–999 (1978)zbMATHCrossRefGoogle Scholar
  15. 15.
    Needham, R., Schroeder, M.: Authentication revisited. Operating Systems Review 21(1), 7 (1987)CrossRefGoogle Scholar
  16. 16.
    Potlapally, N.R., Ravi, S., Raghunathan, A., Jha, N.K.: Analyzing the energy consumption of security protocols. In: Proceedings of the 2003 international symposium on Low power electronics and design, pp. 30–35. ACM Press, New York (2003)CrossRefGoogle Scholar
  17. 17.
    Ryan, P., Schneider, S., Goldsmith, M., Lowe, G., Roscoe, B.: The Modelling and Analysis of Security Protocols: The CSP Approach. Addison-Wesley, Reading (2000)Google Scholar
  18. 18.
    Syverson, P., Meadows, C.: Formal requirements for key distribution protocols. In: De Santis, A. (ed.) EUROCRYPT 1994. LNCS, vol. 950, pp. 320–331. Springer, Heidelberg (1995)CrossRefGoogle Scholar
  19. 19.
    Tanenbaum, A.S.: Computer Networks, 4th edn. Prentice Hall PTR, USA (2003)Google Scholar
  20. 20.
    Thayer, F.J., Herzog, J.C., Guttman, J.D.: Strand spaces: Why is a security protocol correct? In: Proceedings of the 1998 IEEE Symposium on Security and Privacy, pp. 160–171. IEEE Computer Society Press, Los Alamitos (1998)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Benjamin W. Long
    • 1
  1. 1.School of Information Technology and Electrical EngineeringThe University of QueenslandBrisbaneAustralia

Personalised recommendations