Vertical Composition of Distributed Systems

Sébastien Pierre Christophe Gondron

Research output: Book/ReportPh.D. thesis

48 Downloads (Pure)

Abstract

Ensuring security is a fundamental problem in modern distributed systems. For that purpose, system designers use security protocols, e.g., to transfer confidential data or to authenticate a user. It has become the norm to use simultaneously everal of these security protocols. For example, to look up the balance on her bank account, a user Alice has to open a web browser session, and in order to access the application of her bank, she must first login through a webpage. All these components make use of security protocols to ensure that the data are exchanged out of reach from potential eavesdroppers and that the bank is authenticated to the client. These security protocols are widely formally verified in the literature, but are only considered in isolation for the most part, and interactions between protocols that run simultaneously are ignored. This is because so called composed protocols can be rather difficult to verify since they are often too big for automated methods. To address these problems, we are interested in compositionality results of this form: given a number of protocols that are secure in isolation and that satisfy a number of simple syntactic conditions, then their composition is also secure. Existing compositionality results focus on parallel composition, where protocols run independently on the same network, only sharing an infrastructure on fixed long-term keys, and on sequential composition where, for instance, one protocol can establish keys that a subsequent protocol then uses. However, vertical composition where protocols that keep a global state interact with each other, such as when a protocol uses another one to transmit messages in a confidential and authenticated manner, have been only scarcely studied. The main objective of this thesis is to formalize a paradigm for vertical composition of stateful protocols. We can notably model trace-based properties, such as confidentiality or authentication; we are however limited when it comes to equivalence-based properties, such as privacy-type properties, which are of uttermost importance on the Internet. This is the reason why we extended in this thesis (α, β)-privacy. This approach allows to express privacy goals as reachability properties and opens the way for vertical compositionality results that also encompass privacy-type properties. Our main contributions include:
• the formalization of vertical compositionality results for stateful protocols,
based on previous results for parallel compositionality and on a sound
abstraction for payloads,
• formalization of voting privacy properties, including receipt-freeness, in
(α, β)-privacy,
• formalization of privacy as reachability properties, and
• a conservative extension of (α, β)-privacy with probabilities
Original languageEnglish
PublisherTechnical University of Denmark
Number of pages180
Publication statusPublished - 2021

Fingerprint

Dive into the research topics of 'Vertical Composition of Distributed Systems'. Together they form a unique fingerprint.

Cite this