An Automated Approach to Generating Card-Based Cryptographic Protocols

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.
... mehr

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.

Spielkartenbasierte kryptografische Protokolle bieten eine einfache und anschauliche Möglichkeit, Mehrparteienberechnungen ohne Computer durchzuführen, indem sie stattdessen nur einen Satz Spielkarten verwenden. Es wurde viel Forschung betrieben, um minimale Protokolle hinsichtlich der Anzahl der Karten oder der Anzahl der Protokollschritte für verschiedene Funktionen zu finden. Um den Suchprozess nach neuen spielkartenbasierten Protokollen zu automatisieren, verwendeten Koch, Schrempp und Kirsten (2021) die Technik Software Bounded Model Checking für ein symbolisches Programm, das die grundlegenden Aktionen und Zustände implementiert. ... mehrDer Bounded Model Checker wird dann verwendet, um ein sicheres Protokoll zu synthetisieren, indem automatisch ein begrenzter (symbolischer) Programmablauf generiert wird oder, falls kein solcher Ablauf existiert, die Unmöglichkeit innerhalb der gegebenen Grenzen nachgewiesen wird.

In dieser Arbeit bewerten und erweitern wir die oben genannte Technik für eine Verallgemeinerung auf mehr boolesche Funktionen, für die Einführung von Modularität, damit (komplexere) Protokolle effizienter gefunden werden können, und schließlich für die Verwendung von bitweisen Datentyp-Kodierungen, damit das Finden von Protokollen effizienter erfolgen kann. Durch die gesteigerte Effizienz und die universellere Anwendbarkeit konnten wir den Anwendungsbereich des automatisierten Ansatzes zur Generierung von spielkartenbasierten Protokollen auf weitere Unmöglichkeitsbeweise und verschiedene weitere Protokolle ausweiten, von denen einige bereits manuell (aber nicht formal verifiziert) in der Literatur gefunden worden waren.