Abstract
We model any network configuration arising from the execution of a security protocol as a soft constraint satisfaction problem (SCSP). We formalise the protocol goal of confidentiality as a property of the solution for an SCSP, hence confidentiality always holds with a certain security level. The policySCSP models the network configuration where all admissible protocol sessions have terminated successfully, and an imputable SCSP models a given network configuration. Comparing the solutions of these two problems elicits whether the given configuration hides a confidentiality attack. We can also compare attacks and decide which is the most significant. The approach is demonstrated on the asymmetric Needham-Schroeder protocol.
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
M. Abadi and R. M. Needham. Prudent Engineering Practice for Cryptographic Protocols. IEEE Transactions on Software Engineering, 22(1):6–15, 1996.
G. Bella. Modelling Security Protocols Based on Smart Cards. In Proc. of the International Workshop on Cryptographic Techniques & E-Commerce (CrypTEC’99), pages 139–146. City University of Hong Kong, 1999.
S. Bistarelli, H. Fargier, U. Montanari, F. Rossi, T. Schiex, and G. Verfaillie. Semiring-based CSPs and Valued CSPs: Basic Properties and Comparison. In Over-Constrained Systems. Springer-Verlag, 1996.
S. Bistarelli, H. Fargier, U. Montanari, F. Rossi, T. Schiex, and G. Verfaillie. Semiring-based csps and valued csps: Frameworks, properties, and comparison. CONSTRAINTS: An international journal. Kluwer, 4(3), 1999.
S. Bistarelli. Soft Constraint Solving and programming: a general framework. PhD thesis, Dipartimento di Informatica, 2001.
G. Bella, F. Massacci, L. C. Paulson, and P. Tramontano. Formal Verification of Cardholder Registration in SET. In Proc. of European Symposium on Research in Computer Security (ESORICS 2000), LNCS. Springer-Verlag, 2000. In press.
S. Bistarelli, U. Montanari, and F. Rossi. Constraint Solving over Semirings. In Proc. of the 14th International Joint Conference on Artificial Intelligence (IJCAI’95). Morgan Kaufman, 1995.
S. Bistarelli, U. Montanari, and F. Rossi. Semiring-based Constraint Solving and Optimization. Journal of the ACM, pages 201–236, 1997.
G. Bella and L. C. Paulson. Kerberos Version IV: Inductive Analysis of the Secrecy Goals. In Proc. of European Symposium on Research in Computer Security (ESORICS’98), volume 1485 of LNCS, pages 361–375. Springer-Verlag, 1998.
G. Bella and E. Riccobene. Formal Analysis of the Kerberos Authentication System. Journal of Universal Computer Science, 3(12):1337–1381, 1997.
D. Dubois, H. Fargier, and H. Prade. The Calculus of Fuzzy Restrictions as a Basis for Flexible Constraint Satisfaction. In Proc. of IEEE International Conference on Fuzzy Systems, pages 1131–1136. IEEE Press, 1993.
H. Fargier and J. Lang. Uncertainty in Constraint Satisfaction Problems: a Probabilistic Approach. In Proc. of European Conference on Symbolic and Qualitative Approaches to Reasoning and Uncertainty (ECSQARU), pages 97–104. Springer-Verlag, 1993.
E. C. Freuder and R. J. Wallace. Partial constraint satisfaction. AI Journal, 1992.
G. Lowe. An Attack on the Needham-Schroeder Public-Key Authentication Protocol. Information Processing Letters, 56(3):131–133, 1995.
G. Lowe. Some New Attacks upon Security Protocols. In In Proc. of Computer Security Foundations Workshop (CSFW96), pages 139–146. IEEE Press, 1996.
G. Lowe and B. Roscoe. Using CSP to Detect Errors in the TMN Protocol. IEEE Transactions on Software Engineering, 3(10), 1997.
A. K. Mackworth. Constraint Satisfaction. In Encyclopedia of AI (second edition), pages 285–293. John Wiley & Sons, 1992.
R. M. Needham and M. D. Schroeder. Using Encryption for Authentication in Large Networks of Computers. Communications of the ACM, 21(12):993–999, 1978.
L. C. Paulson. The Inductive Approach to Verifying Cryptographic Protocols. Journal of Computer Security, 6:85–128, 1998.
CHE AUTORE METTIAMO QUI? Data Encryption Standard. National Bureau of Standards, Jan 1977. Federal Information Processing Standards Publications, FIPS Pub. 46.
R. Rivest, A. Shamir, and L. Adleman. A Method for Obtaining Digital Signatures and Public-Key Cryptosystems. Communications of the ACM, 21(2):120–126, 1976.
Zs. Ruttkay. Fuzzy Constraint Satisfaction. In Proc. of 3rd IEEE International Conference on Fuzzy Systems, pages 1263–1268, 1994.
V.A. Saraswat. Concurrent constraint programming language. PhDthesis, Carnegie-Mellon University, 1989.
T. Schiex. Possibilistic Constraint Satisfaction Problems, or “How to Handle Soft Constraints?”. In Proc. of 8th Conference on Uncertainty in AI, pages 269–275, 1992.
D. S. Scott. Domains for denotational semantics. In Proc. ICALP. Springer-Verlag, 1982.
T. Schiex, H. Fargier, and G. Verfaille. Valued Constraint Satisfaction Problems: Hard and Easy Problems. In Proc. of the 14th International Joint Conference on Artificial Intelligence (IJCAI’95), pages 631–637. Morgan Kaufmann, 1995.
M. Wallace. Practical Applications of Constraint Programming. Constraints: An International Journal, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bella, G., Bistarelli, S. (2001). Soft Constraints for Security Protocol Analysis: Confidentiality. In: Ramakrishnan, I.V. (eds) Practical Aspects of Declarative Languages. PADL 2001. Lecture Notes in Computer Science, vol 1990. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45241-9_8
Download citation
DOI: https://doi.org/10.1007/3-540-45241-9_8
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41768-2
Online ISBN: 978-3-540-45241-6
eBook Packages: Springer Book Archive