Soft Constraint Programming for Analyzing Security Protocols

Title: Soft Constraint Programming for Analyzing Security Protocols

Abstract: This research proposes a uniform formalism for security protocols' two crucial goals: confidentiality and authentication. Unlike previous work, these goals are no longer viewed as yes/no properties but are given an extra parameter, the security level. This approach allows for different levels of confidentiality and authentication for different messages or principals.

The research framework is designed for protocol analysis and is amenable to mechanization through model checking. The authors apply their framework to the asymmetric Needham-Schroeder protocol and, subsequently, to a larger, three-phase protocol known as Kerberos. They discovered a new attack on the Needham-Schroeder protocol as a form of retaliation by principals who have been attacked previously. They also demonstrate the framework's application on Kerberos, a widely deployed protocol.

Implications: The research suggests that real-world security is based on security levels rather than categorical, definitive security assurances. This approach allows for a more nuanced understanding of security protocols and their vulnerabilities, enabling the development of more effective security measures.

Link to Article: https://arxiv.org/abs/0312025v1 Authors: arXiv ID: 0312025v1