January 2024
Physical Object Authentication
How to protect documents through the whole life-cycle?
For a long time, physical paper has been one of the main ways to store information. Nevertheless, given a paper document, it has always been a challenge to verify that its content is legit. To address this, some primitive solutions were used, like official signatures or stamps that certify the document’s authenticity. Notice that these elements do not ensure that the paper’s content has not been modified after it was issued.
3 minutes
November 2023
Proving protocol implementations secure
Security protocol implementations are obiquitious. We use them daily to perform electronic payments, communicate with friends and coworkers, and they are even present in our electronic passports. However, designing and implementing security protocols is notoriously difficult. Since security protocols aim to secure communication against malicious attackers, usually active ones, all possible attacks have to be considered at design and implementation time. Subtle bugs, like forgetting a simple comparison check, can render an implementation completely insecure.
5 minutes
How can Tamarin handle loops automatically?
Tamarin is a state-of-the art, automated protocol verifier that was used to prove real-world and complex protocols secure, for example, TLS 1.3 or 5G. Nevertheless, Tamarin only supports a limited induction mechanism. Induction is required to handle loops and unbounded data structures, which become more and more common in modern protocols such as in Signal and Certificate Transparency. In the Centre for Cyber Trust, we currently explore a new induction mechanism for Tamarin that implements so-called cyclic proofs.
1 minute
SOAP: A Social Authentication Protocol
SOAP is an OpenID Connect-based authentication protocol, which we applied to messaging applications.
SOAP is an OpenID Connect-based Social Authentication Protocol, which we applied to messaging applications. When performing social authentication, users verify that their chat partner controls accounts at different identity providers (IdPs) which they know are controlled by their intended chat partner. Using social authentication, users can verify, for example, that their messaging application chat is not intercepted by a MITM. By building on top of the popular OpenID Connect protocol, SOAP automates the authentication ceremony and does not require adoption from any OpenID Connect-IdP.
1 minute
Attitudes On Government Surveillance
What are people’s opinions on Internet-safety legislation?
In 2022, the EU has confirmed legislation mandating the implementation of chat control to help fight online child abuse. This has been met with public controversy. We were able to show that, for a general population sample from Germany, trust in physical entities (like law enforcement agencies) impacts the trust that the general population has in digital measures, even on occasion superseding concerns about the potential danger to individual privacy that such technology represents.
2 minutes
Trusted Introductions for the Signal messenger
A more convenient way to keep devils off the line
We entrust our digital devices with many of our intimate secrets. We likewise assume that these stay confidential as we send them to our friends through private messaging apps. Russian users now learned that this assumption is fragile. In a suspected government wiretap , an actor inserted itself between them and the servers. The trust users had in the messaging application was betrayed and sensitive conversations exposed. While such stories seem rare, consider that only the ones caught are reported.
3 minutes
June 2023
Gobra: Modular Specification and Verification of Go Programs
Ensuring correct programs since 2019 🐍
Gobra is an automated, modular verifier for Go programs, based on the Viper verification infrastructure. Go is targeted at high performance applications running in potentially distributed settings and on multicore machines. Hence, Go provides some built-in concurrency primitives, like channel-based communication. Gobra is intended to verify correctness and security properties of such programs, scaling to substantial codebases. Read More Visit our project website! Gobra’s initial publication is available here. Gobra is open-source.
1 minute
F-PKI: The Flexible Public Key Infrastructure
Strengthening the web PKI through flexible trust
Our new Flexible Public-Key Infrastructure (F-PKI) allows users to define which certificate authorities (CAs) they consider highly trusted based on their individual trust preference. F-PKI mitigates the problem that all CAs are omnipotent in today’s Internet PKI, by preventing attacks by less trusted CAs on the certificates created by highly trusted CAs. This notion of trustworthiness also depends on the actual domain that is being validated, allowing users to also define the scope in which a CA is highly trusted (e.
2 minutes
ADEM: An Authentic Digital Emblem
How can we transfer the physical red cross into the digital world?
In times of armed conflict, the emblems of the red cross, red crescent, and red crystal are used to mark physical infrastructure. This enables military units to identify assets as protected under international humanitarian law to avoid attacking them. In 2020, we challenged ourselves with the novel security problem of how to extend such protection to digital, network-connected infrastructure through a digital emblem. In 2021, we finalized a first version proposal for a digital emblem, that we call ADEM: An Authentic Digital Emblem.
2 minutes