Proving cryptographic protocols: the complex relationship between symbolic and computation models

Mar 8 11:00 ₂₀₂₂

Abstract: A number of different models coexist for proving cryptographic protocols. They can roughly be divided in two classes. First, the so called computational model deals with probabilistic Turing machines, precise reductions to specific cryptographic hypotheses often with explicit bounds, and provides very strong guarantees against adversaries that are close to real world. Second the symbolic models, that abstract away probabilities, and model the adversary as a specific list of capabilities. While the computational model provides stronger guarantees, proofs in this model are generally rather complex, hard to check, and not amenable to automation. On the other hand symbolic models typically allow for automated or quasi automated proofs in a much simpler framework. In this talk we will first explore why it is so hard to obtain symbolic models that soundly abstract the computation models. We will then present a fairly recent development, the computationally complete symbolic attacker, developed by Bana and Comon, that takes the opposite approach of usual symbolic models and model what the attacker cannot do rather than modelling the attacker through a list of capabilities. We will explore how this model allows for more modular proofs and proof composition results, and may even allow for efficiently deriving explicit bounds of reductions without ever dealing with the complexity of computational models.