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.
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.
- "Card-Based Cryptography Meets Formal Verification" in New Generation Computing 39(1)