Dynamic Typing for Security Protocols
Matteo Maffei · ARCA (Università Ca' Foscari Venezia) · 2006
Estabilishing a safe communication over an untrusted network, where malicious intruders try to trick honest principals, has long been a challenge and is still a delicate issue. Even when data in transit on the network are protected by cryptographic techniques and these are assumed to be a fully reliable building-block, an intruder can engage a number of potentially dangerous actions, notably, intercepting/replaying/forging messages, to break the intended protocol goals. As a matter of fact, the presence of hostile entities makes protocol design complex and often error prone, as shown by many attacks to long standing protocols reported in the literature. The goal of the research in this field is to provide programmers with effective and easy-to-use tools for verifying the safety of applications communicating over untrusted networks. This thesis goes towards this direction. We target authentication protocols, whose purpose is enabling two entities to achieve mutual and reliable agreement on some pieces of information, typically the identity of the other party, its presence, the origin of a message, its intended destination. We focus on these protocols for two main reasons. Authentication is the building block of several modern and widely used applications, like e-commerce and e-banking, and is difficult to verify as typically achieved by different message components, each one providing a part of the intended authentication guarantee. For instance, the secrecy of a key proves the identity of the owner, the freshness of some piece of code guarantees the recentness of the authentication request and so on. The approach here presented may be summarized as follows. Security protocols are modelled through ρ-spi calculus, a process calculus derived from Abadi and Gordon’s spi calculus. The next step is the development of a type-based static analysis reasoning about security at the language level, thus not involving any protocol execution. Types do not only check safety but also clarify the underlying protocol logic, formalize the role of message components and explain in which extent these contribute to achieve authentication. Thanks to type inference, the analysis is fully automated and does not require any expertise on the part of programmers. Furthermore, the static and compositional nature of the analysis makes it suitable to verify network systems composed of an unbounded number of components. From a technical point of view, the type system is dynamic as it relies on some additional information attached to ciphertexts, specifying the role of message components. The last part of this thesis compares dynamic versus static typing for authentication, pointing out relative merits and drawbacks and discussing some differences in terms of compositionality.