Research Areas

Applied Cryptography

Prof. Kenny Paterson
Cryptography provides a fundamental set of techniques that underpin secure systems. It includes basic techniques to enable services such as confidentiality and integrity of data in secure communication systems, as well as much more advanced methods such as cryptographic schemes that enable searches over encrypted data. It draws broadly from theoretical computer science (algorithms, complexity theory), mathematics (number theory, probability) and engineering (both electronic- and software-engineering). Our research in Applied Cryptography brings all of these strands together to produce impactful research that improves the security of today’s and tomorrow’s cryptographic systems.

Blockchain Technology

Prof. Srdjan Capkun
Blockchain technologies promise many attractive advantages for digital currencies, financial applications and digital society in general. These advantages include reduced trust assumptions, increased transparency, reduced costs and improved user privacy. However, the current state-of-the-art solutions suffer from significant limitations. In our research we investigate the limitations of current blockchain solutions and develop novel systems with improved security, privacy and performance guarantees. Examples of our research results include new types of smart contract execution environments, improved solutions for client privacy and novel digital currencies with regulatory support.

Constructive Cryptography

Prof. Ueli Maurer
Constructive cryptography is a new paradigm for defining the security of cryptographic schemes. It allows to take a new look at cryptography and the design of cryptographic protocols. One can give explicit meaning to various types of game-based security notions of confidentiality, integrity, and malleability, one can design key agreement, secure communication, certification, and other protocols in a modular and composable manner, and one can separate the understanding of what cryptography achieves from the technical security definitions and proofs, which is useful for didactic purposes and protocol design.

Secure Positioning and Localization
Secure Positioning

Prof. Srdjan Capkun
In our daily lives, we increasingly rely on location and proximity measurements for important applications. Already today, people issue contactless payments simply by bringing their credit card close to a card reader. Modern cars automatically detect the key in proximity to unlock the doors. We see first instances of autonomous transportation drones navigate using GPS or Galileo. The security of many existing and future applications surrounding navigation, access control, and secure routing critically depends on the correctness of the underlying location and proximity estimates.

Smartphone Security
Smartphone Security

Prof. Srdjan Capkun
Smartphones are mobile devices carried around by billions of people everyday and used for both personal and business activities, more often than not on the same device. Many people use their smartphones for social-media interaction (e.g., Facebook, Twitter, Instagram), for their day-to-day private life (e.g., making and receiving calls and messages from relatives or friends, taking pictures, accessing their online banking accounts), as well as for their business activities (e.g., receiving and composing e-mails, reading work-related documents, accessing corporate functions or data through a VPN).

Future Internet Architecture SCION
SCION Internet Architecture

Prof. Adrian Perrig
SCION is the first clean-slate Internet architecture designed to provide route control, failure isolation, and explicit trust information for end-to-end communications. SCION organizes existing ASes into groups of independent routing sub-planes, called isolation domains, which then interconnect to form complete routes. Isolation domains provide natural isolation of routing failures and human misconfiguration, give endpoints strong control for both inbound and outbound traffic, provide meaningful and enforceable trust, and enable scalable routing updates with high path freshness. As a result, the SCION architecture provides strong resilience and security properties as an intrinsic consequence of good design principles, avoiding piecemeal add-on protocols as security patches.

Monitoring
Monitoring

Prof. David Basin
It is a growing concern for companies, administrations, and end users alike whether IT systems comply with policies regulating the usage of sensitive data. Checking compliance is particularly acute as our modern infrastructures (communication, entertainment, finance, etc.) collect, process, and share data. A prominent approach to compliance checking is runtime monitoring. Here, system actions are observed and automatically checked for compliance against a given policy. We develop efficient and scalable monitoring algorithms for expressive policy specification languages, e.g., metric first-order temporal logic. We are also interested in policy enforcement, that is, preventing policy violations instead of only detecting them.

Access control
Access control

Prof. David Basin
Access control has wide range of applications, from physical access control, e.g., to buildings, over to access control in single applications, to enterprise-wide access control solutions for an entire company’s data management. Our work covers multiple facets of the challenges in effective access control. We work on languages for efficiently analyzable yet expressive access control policies, techniques for ensuring that no security-critical access control queries are omitted, mining access control policies, and modern systems for access control in physical systems.

Security Protocol Verification
Security protocol verification

Prof. David Basin
We develop tools for security protocol analysis in the symbolic model, particularly the Tamarin-prover. Security protocols are well-known to be error-prone, thus having a formal analysis enhances trust in the protocol’s correctness. Our tools have theoretic foundations guaranteeing their conceptual correctness. The symbolic model has a high level of abstraction compared to bitstrings over the wire, but provides automation and the ability to consider all modes of operation of a protocol at once. Practical results and impact has been seen in the standardization of TLS v1.3 and the analysis of the next-generation 5G mobile communication key exchange protocol 5G-AKA.