Billions of computers around the world communicate with each other every day via the Internet. According to estimates, the annual global data volume has long been in the multiple zettabyte range. A zettabyte consists of a trillion bytes. To ensure that all this data is secure, be it when running a program on a single computer or when communicating via the Internet, computer systems must meet certain requirements and protocols must precisely define which rules apply during communication.
Finding new research approaches to prove and guarantee the security and functionality of protocols and hardware is what equally drives researchers at CISPA in Saarbrücken and the Loria research network in Nancy, Lorraine. Since 2020, they have been pooling their expertise within the framework of the Franco-German Center for Cybersecurity. Its organizers, Prof. Dr. Antoine Joux from CISPA and Prof. Dr. Marine Minier from Loria, invited researchers and interested parties to the new cross-border exchange on Thursday.
After introductory remarks, the researchers talked about the latest developments in the field of automatic analysis tools for security protocols and addressed the question of how to formulate complex correctness properties for computer systems.
CISPA faculty Prof. Dr. Cas Cremers opened the day with his talk "That nagging thing in the back of your mind: Rethinking how symbolic analysis tools model cryptographic primitives", in which he looked at new research approaches to the foundations of automated analysis tools designed to prove the correctness of security protocols or find possible attacks on them.
Dr. Steve Kremer from the Institut national de recherche en sciences et technologies du numérique (INRIA) showed what results automated analysis tools have already delivered so far with his presentation "Formal verification in action: an in-depth case study of LAKE-EDHOC". Together with CISPA and other Loria researchers, Kremer studied the novel key exchange protocol EDHOC (Ephemeral Diffie-Hellman Over COSE). The researchers were able to confirm security promises and identify weaknesses. They made suggestions on how the protocol can be further strengthened.
Tim Würtele and Pedram Hosseyni study under the chair of Prof. Dr. Ralf Küsters at the University of Stuttgart. They were invited as external guests and presented in their talk "A Modular Symbolic Verification Framework for Executable Cryptographic Protocol Code" their new verification tool DY*, which is used for security analysis of cryptographic protocol codes.
Dr. Stephan Merz spoke in his talk "Prophecy Made Simple" about a new practical approach to finding refinement mappings for specifications for which - at least at first glance - no refinement mappings seem to exist.
CISPA PhD student Jana Hofmann showed in her talk "Logics for the Specification of Hyperproperties" which logics are best suited for which classes of so-called hyperproperties. She also presented a logic approach for systems with infinite states and showed its expressiveness using the example of smart contracts.
CISPA faculty Dr. Rayna Dimitrova concluded the day's series of talks with her presentation "Logics for the Specification of Hyperproperties." She spoke about the possibilities and limitations of the recently introduced logical approach Probabilistic Hyper Logic (PHL), which can be used for the specification of hyperproperties in so-called Markov decision processes.
Following the presentations, a joint brainstorming session took place outside in a relaxed atmosphere in the best weather. The next workshop is planned for autumn in Saarbrücken.
About the Franco-German Center for Cybersecurity
The Center is an association of the largest and most renowned cybersecurity research centers in Europe. The CISPA Helmholtz Center for Information Security and the INRIA/Loria in Nancy have been pursuing joint paths in cybersecurity research since 2020 and are dedicated to strengthening transfer and innovation activities between France and Germany. Leaders on the German side are Prof. Dr. Dr. h. c. Michael Backes and Prof. Dr. Antoine Joux and on the French side Prof. Dr. Jean-Yves Marion and Prof. Dr. Marine Minier.
About Loria
Loria is the French acronym for "Lorraine Research Laboratory in Computer Science and its Applications" and is a joint research unit of the CNRS, the University of Lorraine, and INRIA. This unit was officially created in 1997. Loria's missions consist mainly of fundamental and applied research in computer sciences. The laboratory is a member of the Fédération Charles Hermite, which brings together the four main research laboratories in mathematics, information and communication sciences, and control and automation. The scientific work is carried out by the laboratory's 400 collaborators in 28 teams, 15 of which work jointly with INRIA. LORIA is today one of the largest research laboratories in Lorraine.
translated by Oliver Schedler
