| Dominique Unruh |  |
 |
Date of the talk: 20 January 2012
Computationally sound protocol verification
Formal methods provide powerful tools for the security verification of cryptographic protocols. They are, however, typically based on a strongly simplified model: messages sent over the network are assumed to be symbolic terms instead of bitstrings. This idealization does not take into account the properties of the cryptographic algorithms (such as encryption) and may thus overlook attacks."Computational soundness results" can be used to overcome this limitation. These show that in some cases a symbolic analysis can give security guarantees that are as strong as when taking the cryptographic algorithms into account.
We explain how computational soundness results can be proven, the limitations of the approach, and how to manage the complexity arising when trying to apply these results to the verification of actual source code.
