Static Analysis of Authentication
Riccardo Focardi

Authentication protocols are simple distributed algorithms whose purpose is to enable two entities to achieve mutual and reliable agreement on some piece of information, typically the identity of the other party, its presence, the origin of a message, its intended destination. Achieving the intended agreement guarantees is subtle as shown by many attacks to long standing protocols reported in the literature. In most cases, such attacks dwell on flaws in the protocols' logic, rather than on breaches in the underlying cryptosystem. In this talk, we briefly discuss the state-of-art of formal methods applied to security protocol analysis, and we illustrate a static analysis technique that allows us to validate protocols in the presence of both malicious outsiders and compromised insiders, with no limitation on the number of parallel sessions. The analysis is fully automated being it based on a security type-system which only inspects the protocol code, with no need of generating and exploring all the possible execution sequences.