What formal guarantees should a secure messaging application provide? Do the most widely-used protocols provide them? Can we do better? In this thesis we answer these questions and with them give a formal study of modern secure messaging protocols, which encrypt the personal messages of billions of users. We give definitions and analyses of two protocols: one existing (Signal) and one new (ART). For Signal, we begin by extending and generalising classic computational models, in order to apply them to its complex ratcheting key derivations. With a threat model in mind we also define a security property, capturing strong secrecy and authentication guarantees including a new one which we call "post-compromise security". We instantiate Signal as a protocol in our model, stating its security theorem and sketching a computational reduction. Signal only supports encrypting messages between two devices, and so most implementers have built custom protocols on top of it to support group conversations. These protocols usually provide weaker security guarantees, and in particular usually do not have post-compromise security. We propose a new protocol called ART, whose goal is to bring Signal's strong security properties to conversations with multiple users and devices. We give a design rationale and a precise definition of ART, and again generalise existing computational models in order to formally specify its security properties and sketch a security reduction. ART has enjoyed widespread interest from industry, and we aim to turn it into an open standard for secure messaging. To that end, we have brought it to the IETF and formed a working group called Messaging Layer Security, with representatives from academia as well as Facebook, Google, Twitter, Wire, Cisco and more. Through MLS, we hope to bring ART's strong guarantees to practical implementations across industry. After concluding our analyses we pause for a moment, and start looking towards the future. We argue that for complex protocols like Signal and ART we are reaching the limits of computational methods, and that the future for their analysis lies with symbolic verification tools. To that end we return to the symbolic model and give a number of case studies, in each one showing how a traditional limitation of symbolic models can in fact be seen as a modelling artefact.

End-to-end encryption is becoming a standard feature in popular mobile chat appli-cations (apps) with millions of users. In the two years a number of leading chat apps have added end-end encryption features including LINE, KakaoTalk, Viber, Facebook Messenger, and WhatsApp.However, most of these apps are closed-source and there is little to no independent ver-ification of their end-to-end encryption system design. These implementations may be a major concern as proprietary chat apps may make use of non-standard cryptographic algorithms that may not follow cryptography and security best practices. In addition, governments authorities may force chat app providers to add easily decryptable export-grade cryptography to their products. Further, mainstream apps have a large attack surface as they offer a variety of features. As a result, there may be software vulnera-bilities that could be exploited by an attacker in order to compromise user’s end-to-end privacy. Another problem is that, despite being closed-source software, providers often market their apps as being so secure that even the provider is not able to decrypt messages. These marketing claims may be potentially misleading as most users do not have the technical knowledge to verify them.In this Master’s thesis we use KakaoTalk – the most popular chat app in South Korea – as a case study to perform a security and privacy assessment and audit of its “Secure Chat” opt-in end-to-end encryption feature. Also, we examine KakaoTalk’s Terms of Service policies to verify claims such as “[. . . ] Kakao’s server is unable to decrypt the encryption [. . . ]” from a technical perspective.The main goal of this work is to show how various issues in a product can add up to the potential for serious attack vectors against end-to-end privacy despite there being multiple layers of security. In particular, we show how a central public-key directory server makes the end-to-end encryption system vulnerable to well-known operator-site man-in-the-middle attacks. While this naive attack may seem obvious, we argue that (KakaoTalk) users should know about the strength and weaknesses of a particular design in order to make an informed decision whether to trust the security of a chat app or not. / End-to-end kryptering är en allt mer vanligt förekommande funktionalitet bland populära mobila chatttjänster (händanefter appar) med miljontals användare. Under de två senaste åren har många ledande chattappar, bland annat LINE, KakaoTalk, Viber, Facebook Messenger, och WhatsApp, börjat använda end-to-end kryptering. Dock så är de flesta av dessa appar closed-source och det finns begränsad, eller ingen, fristående granskning av systemdesignen för deras end-to-end kryptering. Dessa implementationer kan innebära en stor risk då proprietära chattappar kan använda sig av kryptografiska algoritmer som inte följer best practice för säkerhet eller kryptografi. Vidare så kan statliga myndigheter tvinga de som tillhandahåller chattappar att använda lättdekrypterad export-grade kryptografi för sina produkter. Lägg till det att de flesta vanliga appar har många ytor som kan attackeras, till följd av all funktionalitet de erbjuder. Som ett resultat av detta finns en risk för mjukvarubrister som kan utnyttjas av en hackare för att inkräkta på en användares end-to-end integritet. Ytterligare ett problem är att trots att det är closed-source mjukvara så marknadsför ofta appleverantörerna sina appar som att vara är så säkra att inte ens leverantörerna själva kan dekryptera användarnas meddelanden. Det som hävdas i marknadsföringen riskerar vara missledande eftersom de flesta användarna inte har den tekniska kunskap som krävs för att kunna verifiera att det som hävdas är sant. I den här Master-uppsatsen använder vi KakaoTalk – den mest populära chattappen i Sydkorea – som en fallstudie för att granska och bedömma säkerhetens- och integritets-aspekterna hos deras valbara “Secure Chat” med end-to-end krypteringsfunktionalitet. Vi granskar även KakaoTalk’s användarvillkor för att kunna verifiera påståenden som att “[. . . ] Kakao’s server is unable to decrypt the encryption [. . . ]” från ett tekniskt perspektiv. Det huvudsakliga syftet med denna studien är att belysa hur olika brister i en produkt sammantagna kan skapa en risk för allvarliga vektorattacker mot end-to-end integriteten även fast det finns flera skyddslager. Mer specifikt visar vi hur en central katalogserver för public-keys gör end-to-end krypteringssystemet sårbart mot välkända operator-site man-in-the-middle-attacker. Trots att denna naiva typ av attack kan verka uppenbar, argumenterar vi för att (KakaoTalk) användare borde veta om styrkorna och svagheterna med en särskild systemdesign för att kunna göra ett informerat val för om de ska lita på säkerheten hos en chattapplikation eller inte.

Local-first software has the potential to offer users a great experience by combining the best aspects of traditional applications with cloud-based applications. However, not much has been documented regarding developing backends for local-first software, particularly one that is scalable while still supporting end-to-end encryption. This thesis presents a backend architecture that was then implemented and evaluated. The implementation was shown to be scalable and was able to maintain an estimated end-to-end latency of around 30-50ms as the number of simulated clients increased. The architecture supports end-to-end encryption to offer user privacy and to ensure that neither cloud nor service providers can access user data. Furthermore, by occasionally performing snapshots the encryption overhead was shown to be manageable compared to the raw data, at around 18.2% in the best case and 118.9% when using data from automerge-perf, a standard benchmark. Lastly, the processing times were shown to be upwards of 50 times faster when using snapshots compared to handling individual changes.

None of the three largest webmail service providers (serving over 1 billion users) support end-to-end message encryption. Encrypted email has never seen mass adoption because it is prohibitive for non-experts to use. Private WebMail (Pwm) is our extension to popular webmail systems that lets users easily encrypt sensitive messages without having to first contact the recipient and share information. It is designed to spread quickly in a grassroots fashion so that a user receiving their first encrypted message can quickly and easily start using the system. This thesis describes the design and implementation of Pwm, then measures its usability through analysis and a user study.

Billions of web-based email and chat messages are sent over the Internet every day. However, very few service providers support end-to-end privacy protection. While providing security for these messages is technically feasible, usability remains a challenge in this field. Recent research attempts to hide security details like key management and encryption in order to make the system more usable. However usability studies demonstrated that hiding these details may confuse the user and contribute to mistakes (e.g., sending out an email in plaintext when the user thought it would be encrypted). In an effort to increase trust and eliminate mistakes, this thesis presents the design of a browser-based manual encryption mechanism that supports automatic key-management and manual encryption. It also describes the Message Protector (MP) prototype. An evaluations of MP is presented based on a user study conducted on the campus of BYU.

Users share private information on the web through a variety of applications, such as email, instant messaging, social media, and document sharing. Unfortunately, recent revelations have shown that not only is users' data at risk from hackers and malicious insiders, but also from government surveillance. This state of affairs motivates the need for users to be able to encrypt their online data.In this dissertation, we explore how to help users encrypt their online data, with a special focus on securing email. First, we explore the design principles that are necessary to create usable, secure email. As part of this exploration, we conduct eight usability studies of eleven different secure email tools including a total of 347 participants. Second, we develop a novel, paired-participant methodology that allows us to test whether a given secure email system can be adopted in a grassroots fashion. Third, we apply our discovered design principles to PGP-based secure email, and demonstrate that these principles are sufficient to create the first PGP-based system that is usable by novices. We have also begun applying the lessons learned from our secure email research more generally to content-based encryption on the web. As part of this effort, we develop MessageGuard, a platform for accelerating research into usable, content-based encryption. Using MessageGuard, we build and evaluate Private Facebook Chat (PFC), a secure instant messaging system that integrates with Facebook Chat. Results from our usability analysis of PFC provided initial evidence that our design principles are also important components to usable, content-based encryption on the Web.

Participants from recent secure email user studies have expressed a need to use secure email tools only a few times a year. At the same time, Internet users are expressing concerns over the permanence of personal information on the Internet. Support for short-lived keys has the potential to address both of these problems. However, the short-lived keys usability and security space is underdeveloped and unexplored. In this thesis, we present an exploration of the short-lived keys usability and security design space. We implement both a short-lived keys and a long-term keys secure email prototype. With these two prototypes, we conduct a within-subjects user study. Results from our study show that participants believe the short-lived keys prototype is more secure and more trusted. Participants also provide feedback on what they want in a system supporting short-lived keys. They also discuss how concerned they are about the permanence of their information on the Internet and on their devices.

Secure mobile apps, including end-to-end encrypted messaging apps such as Whats-App and Signal, are increasingly popular today. These apps require trust in a centralized key directory to automatically exchange the public keys used to secure user communication. This trust may be abused by malicious, subpoenaed, or compromised directories. A public key infrastructure (PKI) solution that requires less trust would increase the security of these commonly used apps.CONIKS is a recent PKI proposal that features transparent key directories which publish auditable digests of the public keys they present to queriers. By monitoring its key every time a new digest is published, a client can verify that its key is published correctly, reducing the need to trust the directory. CONIKS features improved security at the cost of unique auditing and monitoring requirements. In this thesis, we examine CONIKS' suitability as a PKI solution for secure mobile apps. We present a threat analysis of possible attacks on the CONIKS protocol and explore several important implications of CONIKS' system description, including recommendations for whistleblowing and key change policies. We also analyze mobile device usage data to estimate whether typical mobile device Internet connectivity is sufficient to fulfill CONIKS' monitoring requirement.

The threat of government and corporate surveillance around the world, as well as the publicity surrounding major cybersecurity attacks, have increased interest in secure and private end-to-end communications. In response to this demand, numerous secure messaging applications have been developed in recent years. These applications have been welcomed and publically used not just by political activists and journalists but by everyday users as well. Most of these popular secure messaging applications are usable because they hide many of the details of how encryption is provided. The strength of the security properties of these applications relies on the authentication ceremony, wherein users validate the keys being used for encryption that is exchanged through the service providers. The validation process typically involves verifying the fingerprints of encryption keys to protect the communication from being intercepted.In this dissertation, we explore how to help users enhance the privacy of their communica- tions, with a particular focus on secure messaging applications. First, we explore whether secure messaging applications are meeting the security and privacy needs of their users, especially in countries that practice censorship and restrict civil liberties, including blocking access to social media and communication applications. Second, we studied existing popular secure messaging applications to explore how users interact with these applications and how well they are using the authentication ceremony during lab studies. Third, we applied design principles to improve the interfaces for the authentication ceremony, and also to help users find and perform the authentication ceremony faster. Forth, we applied the lessons from our interviews with participants in our user studies to help users comprehend the importance of authentication. As part of the effort, we developed an authentication ceremony using social media accounts to map key fingerprints to social features, pushing the ceremony to a more natural domain for users. We modified the Signal secure messaging application to include this social authentication ceremony and used a user study to compare this method to other common methods. We found that social authentication has some promising features, but that social media companies are too distrusted by users. Based on our results, we make several recommendations to improve the use of security and privacy features in secure messaging applications and outline areas for future work.

In the contemporary digital landscape, ensuring secure communication amid widespread data exchange is imperative. This dissertation focuses on enhancing the security and privacy of end-to-end encryption (E2EE) applications while maintaining or improving usability. The dissertation first investigates and proposes improvements in two areas of existing E2EE applications: countering man-in-the-middle and impersonation attacks through automated key verification and studying user perceptions of cryptographic deniability. Insights from privacy-conscious users reveal concerns about the lack of E2EE support, app siloing, and data accessibility by client apps. To address these issues, we propose an innovative user-controlled encryption system, enabling encryption before data reaches the client app. Finally, the dissertation evaluates local threats in the FIDO2 protocol and devises defenses against these risks. Additionally, it explores streamlining FIDO2 authentication management across multiple websites for user convenience and security.