Verification^2 of ADEM

Verifying the verification code for ADEM

Our Research Projects

1 minute

ADEM is a proposal for a digital emblem and was developed at the Centre for Cyber Trust. A digital emblem is the digital equivalent to the protective, physical emblems of the red cross, red crescent, and red crystal. Follow the link of ADEM to learn more.

Digital emblems are cryptographically signed objects and as such must be verified. We implemented prototypes doing just that. The Programming Methodology and Information Security groups, both members of the Centre, collaboratively supervised a student thesis in which we formally verified the prototype’s verification code. This establishes that no matter what input an adversary provides to our code, the verification will always return correct results.

This project combines two aspects of our Centre’s research: (i) proving protocol implementations secure using Gobra, and (ii) ADEM, our proposal for a digital emblem.

Read More #

The thesis is available at the ETHZ Research Collection.

Project Members #

  • Felix Linker
  • Lasse Meinen
  • Linard Arquint