Sensitive and critical personal and business information is stored and managed by a multitude of electronic devices. Integrity and confidentiality of that data is threatened by software errors and malicious attacks. Yet, designing secure and verifiable systems is inherently difficult: The correct use of cryptography requires expert knowledge, the sheer complexity of the systems defies manual analysis; minor mistakes in implementation and analysis can completely destroy all security and correctness guarantees. For a high level of trust in a system, this system needs to be designed properly (using state-of-the-art cryptographic schemes where needed), and its proper operation (both security and correct behavior) needs to be proven (ideally with the help of a computer as humans are likely to make mistakes). In this project, we will study methods for designing secure systems (based on cryptographic primitives and protocols), and methods for computer-aided verification of their security and correctness.