Anonymous communication networks offer technological solutions to provide privacy protection in online communications. As I will detail in my talk, a key enabler for the improvement of anonymous communication networks are strong formal foundations. Formal privacy definitions and proof strategies not only make solutions comparable, but also strengthen them by uncovering and provably fixing security flaws. Additionally, formal foundations allow us to fundamentally understand the technologies and their limits.

To ensure the security of a software system, it is vital to keep up with changing security precautions, attacks, and mitigations. Although model-based development enables addressing security already at design-time, design models are often inconsistent with the implementation or among themselves, hindering the effective realization and verification of secure software systems. In addition, variants of software systems are another burden to developing secure systems. To ensure security, in the thesis, we present GRaViTY, an approach that allows security experts to specify security requirements on the most suitable system representation based on continuous automated change propagation. To preserve security, GRaViTY automatically checks all system representations against these requirements and provides security-preserving refactorings. For both, we show the application to variant-rich software systems. To support legacy systems, GRaViTY allows to automatically reverse-engineer variability-aware UML models and semi-automatically map existing design models to the implementation. Besides evaluations of the individual contributions, we demonstrate the approach in two real-world case studies, the iTrust electronics health records system and the Eclipse Secure Storage.

The provable security paradigm is an important tool to show security of cryptographic primitives. Here, security follows from showing that an adversary cannot break a scheme with respect to some security notion. Standard security notions, however, often do not cover scenarios that might happen in practice. Examples are side-channel leakage as well as usage of keys and random coins that are somehow related. Another setting that often is not considered is security with respect to adversaries that have quantum computing power.

In this thesis we study security of schemes in advanced security notions; these notions model more sophisticated attacks which can happen when using such schemes. We develop new advanced security notions, analyse existing primitives with respect to these, and construct primitives that achieve such advanced security notions.

The talk will focus on two results of the thesis. In the first, we present a generic blueprint for a leakage-resilient authenticated encryption scheme from leakage-resilient functions. We then describe an instantiation entirely built from sponges. In the second, we develop a quantum security notion for public key encryption schemes which allows for a quantum challenge phase; we provide both positive and negative results with respect to this security notion.