A Logical Approach for Automated Reasoning about Privacy in Security Protocols

Security protocols are distributed systems that rely on cryptographic operations to provide security features. Formal verification of security protocols is important to guarantee that a protocol achieves its goals: the verification is done by reasoning about various properties such as secrecy, authentication and privacy. There are several approaches and techniques to obtain formal proofs of security. In many cases, these proofs are manually written, however this may lead to invalid results due to oversights by the prover or implicit assumptions. Automated verification has shown to be effective in preventing such errors, and there are nowadays a number of tools available that can check security properties of protocols with a very high degree of confidence. While secrecy and authentication goals are typically expressed as reachability properties, privacy is more subtle. A standard way to define privacy is to give a pair of systems that differ in some detail (e.g., two actions are performed by the same agent or by different agents) and check whether an attacker can distinguish the two systems (different notions of distinguishability can be used depending on the privacy property). An alternative approach is (α, β)-privacy, where the protocol specification declares the information that is allowed to be learned and a violation of privacy happens if the attacker manages to learn more than allowed, e.g., if they can deduce that in two instances of the protocol, some actions were performed by the same user (linkability attack). The formalism of (α, β)-privacy enables reasoning about privacy as a reachability property, which makes some proofs easier. Moreover, we do not have to think about possible attacks and prove equivalence between different systems, but we rather model the logical deductions that the attacker can make based on their observations of the real system. There are still several challenges when it comes to automation, which is the main topic of this thesis. We identify a decidable fragment of (α, β)-privacy and design a decision procedure that can check privacy goals, given a bound on the number of transitions in the protocol execution.

One kind of attacks on security protocols relies on the attacker reusing messages in a way that confuses the other participants. This issue arises when the protocol specification does not sufficiently distinguish the meaning of different messages. Considering a typed model where the protocol specifies for every message a type expressing its meaning, these attacks are called type-flaws and occur when a participant accepts a message of a different type than expected. For instance, someone may receive an encrypted message with an expected specific format, but the protocol does not check that the content under encryption is indeed of the right format. When working in such a typed model, it is very useful to establish typing results of the form: “if there exists an attack, then there exists a well-typed one.” Effectively, this rules out all type-flaws. Moreover, the assumption that every message is well-typed significantly helps to establish other results on security protocols. Ideally, we want to verify whether protocols are resistant to type-flaws using purely syntactic requirements, since these can be checked statically without considering the semantics of the protocol execution.

One area that benefits from typing results is protocol composition. In the literature, the security goals of a protocol are typically studied with the protocol running in isolation. However, oftentimes several protocols are running in parallel on the same device or are otherwise interacting with each other. For instance, one protocol could be used to establish a secure connection between two endpoints, while another protocol relies on this secure connection to exchange sensitive information. Another example is several applications sharing a common infrastructure such as an identity server. Protocol composition poses significant challenges to formal verification. Composed systems are much larger and complex than individual components and thus verification is more difficult. Moreover, components can be added or updated and we do not want to verify the entire composed system from scratch as soon as there is a slight change. It is thus desirable to obtain results for composing protocols securely in a modular way, i.e., we wish to derive the security of a composed protocol from the security of its components. While there are a number of results supporting protocol composition for goals like secrecy and authentication, it is harder to achieve compositionality for privacy properties.

In this thesis, we are concerned with the automation of verifying privacy properties of security protocols and with the proofs of typing and compositionality results. We use (α, β)-privacy, which is a symbolic approach that aims to provide a logical and intuitive way of specifying privacy goals. Our results support large classes of security protocols, with standard cryptographic operators, non-determinism, branching and statefulness. Our main contributions are as follows:
• Design of a decision procedure for a fragment of (α, β)-privacy.
• Implementation of the procedure in a prototype tool.
• Application of the procedure and the tool to case studies.
• A typing result for the class of type-flaw resistant protocols.
• A compositionality result for the class of composable protocols.