Automatic Verification of Security Protocols

Internet is becoming everyday a more widely used medium for electronic commerce. This development is hampered by the natural insecurity of communications, as it is not possible to guarantee that some data exchanged is not listened by someone else, or even that it really originated from the claimed sender. This lack of security leads to the development of security protocols, that is small messages sequences, after which the author provides some properties to the user, such as the correct identification of the users (called agents) and the privacy of some data pieces. There has been a significant amount of work toward the specification of security protocols and the search for attacks, but much less toward the positive verification of protocol properties. After a quick overview of the main techniques developped for considering these three levels, we will focus on some recent ones that are based on constraint solving and unification. They combine several different problems, such as unification and matching in some theories, reachability problems, deduction, and all this in the context of the properties of cryptographic primitives.