Institut für Informationssicherheit und Verlässlichkeit (KASTEL) – Anwendungsorientierte Formale Verifikation
  • DE
Institut für Informationssicherheit und Verlässlichkeit (KASTEL) – Anwendungsorientierte Formale Verifikation
Startseite

An Automated Approach to Generating Card-Based Cryptographic Protocols

Forschungsthema:Protocol Generation
Typ: BA
Datum: 2023-03-30
Betreuer: Michael Kirsten
Aushang:

Abstract

Card-based cryptographic protocols provide a simple and illustrative way of performing multi-party computation without computers, but instead use just a set of playing cards. A lot of research has been done on finding minimal protocols, with respect to the number of cards or the number of protocol steps, for various functions. To automate the process of finding new card-based protocols, Koch, Schrempp, and Kirsten (2021) employed the technique of software bounded model checking for a symbolic program that implements the basic actions and states. The bounded model checker is then used to synthesize a secure protocol by automatically generating a bounded (symbolic) program run, or, if there exists no such run, prove impossibility within the given bounds.

In this thesis, we evaluate and extend the above technique for a generalization to more boolean functions, for an introduction of modularity so that (more) complex protocols can be found more efficiently, and finally for using bitwise datatype encodings so that finding protocols can be done more efficiently. From the increased efficiency and more universal applicability, we were able to extend the scope of the automated approach for generating card-based protocols to further impossibility proofs and various more protocols, for which some of them had already been found manually (but not formally verified) within literature.

Literature