Elsevier

Computers & Security

Volume 24, Issue 4, June 2005, Pages 322-333
Computers & Security

Information Assurance for security protocols

https://doi.org/10.1016/j.cose.2004.10.004Get rights and content

Abstract

Security protocols are used pervasively to protect distributed communications in the third Millennium. This motivates the need for a definition of Information Assurance for security protocols, which, to the best of our knowledge, is still missing. Such a definition is advanced in terms of the requirements that security protocols be analysed at the same time realistically, accurately and formally, notions that the existing literature only favours in separate contexts. The precise meanings of these terms are described by means of general considerations and concrete examples. The main goal of this paper is to draw attention to and raise concern on this novel but significant niche of computer security.

Section snippets

Overview

Computer Security began its course with the implementation of some rudimentary access-control features in Multics (Corbatò and Vyssotsky, 1965), that is in the late 1960s. At that time, security merely meant to regulate access to the sensitive resources of a single computer. Technology progressed fast, bringing a number of new problems forward. With the development of large-scale computer networks, the figure of a new expert became necessary, the security architect. We are not going to survey

Realism

During the last two decades, Dolev and Yao's (1983) famous paper has substantially influenced security protocol analyses, regardless of whether they were informal or formal. Dolev and Yao's contribution is essential evidence that collusion of a number of principals to subvert a protocol is equivalent to the hostility of a single, powerful attacker. “Powerful” means the ability to monitor the entire network traffic, to break down messages by the conventional operations of splitting and

Accuracy

We concentrate on the goals of confidentiality and authentication. Confidentiality of a message means that the message remains undisclosed to those not intended to learn it (Dolev and Yao, 1983, Neuman and Ts'o, 1996). Authentication of a principal means that we truly are communicating with that principal (Gollmann, 2000b, Gollmann, 2001). We observe that neither of these two properties is boolean in the real world: only certain levels of confidentiality or authentication are achieved in

Formalism

Formal analyses of security protocols facilitate a deep understanding of the protocols. A variety of approaches have been taken, ranging from state enumeration (Ryan and Schneider, 2000), to provable security (Bellare and Rogaway, 1995), to induction (Paulson, 1998). These efforts have led to the discovery of a number of protocol attacks (and of the corresponding patches), or to the formal establishment that certain goals are achieved.

However, we observe that the exhibition of an attack raises

Conclusions

We have laid the ground towards the development of a definition of Information Assurance for security protocols. We require that security protocols be analysed realistically, accurately and formally.

“Realistically” means that the model underlying the analysis should exceed the limits of the classical Dolev and Yao's model. We showed how this highlights another consequence of Lowe's attack on the popular asymmetric Needham–Schroeder protocol.

“Accurately” means that the protocol goals should not

Acknowledgements

We are grateful to Simon Foley, Michael Leuschel and Fabio Massacci for useful discussions on the topic of this paper.

Giampaolo Bella is an Assistant Professor at the University of Catania (Italy), teaching the Computer Security course and classes in Computer Architectures. His main research interests are in the use of formal methods for the verification of crucial security properties, but he is also interested in hardware verification and in constraint programming. He was a Research Associate at the Technical University of Munich (Germany) in the year 2000, after he received his Ph.D. from the Cambridge

References (39)

  • G. Lowe

    An attack on the Needham–Schroeder public-key authentication protocol

    Information Processing Letters

    (1995)
  • M. Abadi

    Secrecy by typing in security protocols

    Journal of the ACM

    (1999)
  • M. Abadi et al.

    Mobile values, new names, and secure communication

  • M. Abadi et al.

    Prudent engineering practice for cryptographic protocols

    IEEE Transactions on Software Engineering

    (January 1996)
  • R. Anderson

    Why cryptosystems fail

    Proceedings of the 1st ACM conference on communications and computer security (CCS'93)

    (1993)
  • R. Anderson et al.

    Robustness principles for public key protocols

  • G. Bella et al.

    Confidentiality levels and deliberate/indeliberate protocol attacks

  • G. Bella et al.

    Soft constraint programming to analysing security protocols

    Theory and Practice of Logic Programming

    (2004)
  • G. Bella et al.

    Kerberos version IV: inductive analysis of the secrecy goals

  • G. Bella et al.

    Verifying the SET registration protocols

    IEEE Journal of Selected Areas in Communications

    (2003)
  • Bella G, Bistarelli S, Massacci F. A protocol's life after attacks. In: Proceedings of the 11th international workshop...
  • M. Bellare et al.

    Provably secure session key distribution—the three party case

  • S.M. Bellovin et al.

    Augmented encrypted key exchange: a password-based protocol secure against dictionary attacks and password file compromise

  • S. Bistarelli

    Semirings for soft constraint solving and programming

    (2004)
  • S. Bistarelli et al.

    Semiring-based constraint solving and optimization

    Journal of the ACM

    (1997)
  • S. Bistarelli et al.

    Soft concurrent constraint programming

  • M. Burrows et al.

    A logic of authentication

    Proceedings of the Royal Society of London

    (1989)
  • W. Cheswick et al.

    Firewalls and Internet security: repelling the wily hacker

    Addison-Wesley

    (2004)
  • L. Cholvy et al.

    Analyzing consistency of security policies

    Proceedings of the 16th IEEE symposium on security and privacy

    (1997)
  • Cited by (5)

    • Secure multiparty payment with an intermediary entity

      2009, Computers and Security
      Citation Excerpt :

      Extension.Hashes[i]. In this section, we analyze our protocol using the approach of realistic and accurate analyses proposed in Bella and Bistarelli (2004). Solution: Pi could compare H(SubPd′i,j), where SubPd′i,j is the received purchase, with the appropriate ST_X509.

    • Critical factors of information security implementation

      2009, 2009 1st International Conference on Networked Digital Technologies, NDT 2009
    • Semiring-based soft constraints

      2008, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

    Giampaolo Bella is an Assistant Professor at the University of Catania (Italy), teaching the Computer Security course and classes in Computer Architectures. His main research interests are in the use of formal methods for the verification of crucial security properties, but he is also interested in hardware verification and in constraint programming. He was a Research Associate at the Technical University of Munich (Germany) in the year 2000, after he received his Ph.D. from the Cambridge University Computer Laboratory. His Ph.D. dissertation, entitled “Inductive Verification of Cryptographic Protocols” (CUCL Technical Report 493), focuses on how to use inductive techniques with a mechanized proof assistant to verify real-world security protocols.

    Stefano Bistarelli is an Assistant Professor of Computer Science at the Department of Science of the University of Chieti-Pescara and External Researcher of the Institute of Informatics and Telematics of C.N.R. Pisa. He obtained his Ph.D. in Computer Science in 2001 at the Computer Science Department of the University of Pisa. His thesis was awarded by the Italian Association of Artificial Intelligence and by the Italian Chapter of the European Association of Theoretical Computer Science. His research interests range from Artificial Intelligence to Programming Languages, with particular attention to constraint programming, constraint solution algorithms, and soft constraints. He is also interested in Security. Recently, he published his work as book LNCS 2962 by Springer.

    View full text