Information Assurance for security protocols
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)
An attack on the Needham–Schroeder public-key authentication protocol
Information Processing Letters
(1995)Secrecy by typing in security protocols
Journal of the ACM
(1999)- et al.
Mobile values, new names, and secure communication
- et al.
Prudent engineering practice for cryptographic protocols
IEEE Transactions on Software Engineering
(January 1996) Why cryptosystems fail
Proceedings of the 1st ACM conference on communications and computer security (CCS'93)
(1993)- et al.
Robustness principles for public key protocols
- et al.
Confidentiality levels and deliberate/indeliberate protocol attacks
- et al.
Soft constraint programming to analysing security protocols
Theory and Practice of Logic Programming
(2004) - et al.
Kerberos version IV: inductive analysis of the secrecy goals
- et al.
Verifying the SET registration protocols
IEEE Journal of Selected Areas in Communications
(2003)
Provably secure session key distribution—the three party case
Augmented encrypted key exchange: a password-based protocol secure against dictionary attacks and password file compromise
Semirings for soft constraint solving and programming
Semiring-based constraint solving and optimization
Journal of the ACM
Soft concurrent constraint programming
A logic of authentication
Proceedings of the Royal Society of London
Firewalls and Internet security: repelling the wily hacker
Addison-Wesley
Analyzing consistency of security policies
Proceedings of the 16th IEEE symposium on security and privacy
Cited by (5)
Secure multiparty payment with an intermediary entity
2009, Computers and SecurityCitation 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.
A secure vehicle-to-roadside communication payment protocol in vehicular ad hoc networks
2008, Computer CommunicationsImplementation and performance evaluation of a payment protocol for vehicular ad hoc networks
2010, Electronic Commerce ResearchCritical factors of information security implementation
2009, 2009 1st International Conference on Networked Digital Technologies, NDT 2009Semiring-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.