Michael Backes, Birgit Pfitzmann, et al.
Int. J. Inf. Secur.
Bridging the gap between formal methods and cryptography has recently received a lot of interest, i.e., investigating to what extent proofs of cryptographic protocols made with abstracted cryptographic operations are valid for real implementations. This led to the notion of cryptographically faithful (sound) abstractions. These abstractions allow for a provably secure cryptographic implementation; however their incorporation into machine-aided verification of security protocols has not been properly adressed yet. The panel should serve as an opportunity to discuss the current state-of-the-art in this area of research as well as the suitability of these abstractions for tool-supported verification of cryptographic protocols. We hope that the discussion will shed light on how far both communities are still apart.
Michael Backes, Birgit Pfitzmann, et al.
Int. J. Inf. Secur.
Nikolai Joukov, Birgit Pfitzmann, et al.
SCC 2009
Carl E. Abrams, Juerg von Känel, et al.
IBM Systems Journal
Birgit Pfitzmann, Nikolai Joukov
SCC 2011