Universität Stuttgart
Permanent URI for this communityhttps://elib.uni-stuttgart.de/handle/11682/1
Browse
2 results
Search Results
Item Open Access Privacy-preserving web single sign-on : formal security analysis and design(2019) Schmitz, Guido; Küsters, Ralf (Prof. Dr.)Web-based single sign-on (SSO) systems enable Web sites, so-called relying parties (RPs), to outsource user authentication to other entities, so-called identity providers (IdPs). Such systems are widely deployed in the Web, e.g., Facebook Login or Google Sign-in. RPs do not need to maintain authentication data of their users, and users can log in at RPs in a convenient way. Fundamental to SSO is security: The SSO protocol must not permit an attacker to impersonate anyone else, nor must it allow a false identity to be imposed on anyone. If this is not the case, attacks are possible that have devastating effects on the security of RPs and their users. While aiming at security, most SSO systems, however, neglect privacy. IdPs can track their users as they (by design) learn at which RP a user logs in. This lack of privacy allows IdPs to create extensive user profiles and might cause some users not to use SSO at all. Moreover, IdPs are enabled to decide ad-hoc whether they allow a user to log in at a specific RP. Therefore, privacy-preserving systems, which do not reveal to IdPs to which RP a user would like to log in or has logged in, are highly desirable in many situations. The design of such systems, however, is very challenging because privacy can easily be compromised. So far, only one SSO system has been proposed with this kind of privacy in mind: Mozilla's BrowserID (a.k.a. Mozilla Persona). In this thesis, we use the Web Infrastructure Model (WIM) to analyze the security of SSO protocols. The WIM is the most comprehensive formal model of the Web infrastructure to date, which applies to a wide range of Web applications and standards. We also extend the WIM to be able to analyze privacy. We use the extended WIM to, for the first time, carry out a systematic and rigorous formal analysis of privacy for Web SSO systems. Using our approach, we analyze the Web SSO system BrowserID. As a result of this first rigorous analysis of an SSO system in the Web infrastructure, we find severe attacks. These attacks not only affect the security of BrowserID but also show that BrowserID's unique privacy claim does not hold. We propose fixes for BrowserID and prove that the fixed system provides security. Regarding privacy, we show that BrowserID, unfortunately, is broken beyond repair. Inspired by BrowserID's goal, we propose the first privacy-preserving Web SSO system, called SPRESSO (for Secure Privacy-REspecting Single Sign-On). SPRESSO is easy to use, decentralized and based solely on native Web features. We design SPRESSO within the WIM right from the start and prove that SPRESSO satisfies strong security and privacy guarantees.Item Open Access Design and cryptographic security analysis of e-voting protocols(2019) Müller, Johannes; Küsters, Ralf (Prof. Dr.)Electronic voting (e-voting) systems are used in numerous countries for political elections, but also for less critical elections within clubs and associations, and hence affect the lives of millions of people. It is therefore important to ensure that single voters' choices remain private, and to be able to verify that an election result coincides with the voters' intention. Unfortunately, for most e-voting systems employed in real elections, these fundamental security and privacy properties cannot be guaranteed, so that in particular the legitimacy of such political elections is challenged. This demonstrates the importance of employing e-voting systems that are rootedly designed to guarantee the required security. However, it turned out to be highly challenging to construct secure yet practical e-voting systems since one always has to find a balance between the (possibly conflicting) requirements of the given kind of election. In the first two chapters of the thesis' main part, we present two practical e-voting systems which are both meant for low-risk and non-political elections, e.g., within clubs or associations. We have implemented both systems to demonstrate their practicability. The first system, called sElect, is designed to be as simple as possible while still guaranteeing a good level of security. The second system, called Ordinos, provides a superior level of privacy as it only reveals the most necessary information about the election outcome, e.g., solely the winner's name but nothing else. We will rigorously analyze the security of sElect and Ordinos. To do this, we formally define the required security properties and then mathematically prove that sElect and Ordinos achieve them. In the third chapter of the thesis' main part, we provide substantial work on the fundamental notion of verifiability of e-voting systems. We analyze and compare all formal verifiability definitions from the literature regarding how meaningful, expressive, or general they are.