Paper 2010/416

Computationally Sound Verification of Source Code

Michael Backes, Matteo Maffei, and Dominique Unruh


Increasing attention has recently been given to the formal verification of the source code of cryptographic protocols. The standard approach is to use symbolic abstractions of cryptography that make the analysis amenable to automation. This leaves the possibility of attacks that exploit the mathematical properties of the cryptographic algorithms themselves. In this paper, we show how to conduct the protocol analysis on the source code level (F# in our case) in a computationally sound way, i.e., taking into account cryptographic security definitions. We build upon the prominent F7 verification framework (Bengtson et al., CSF 2008) which comprises a security type-checker for F# protocol implementations using symbolic idealizations and the concurrent lambda calculus RCF to model a core fragment of F#. To leverage this prior work, we give conditions under which symbolic security of RCF programs using cryptographic idealizations implies computational security of the same programs using cryptographic algorithms. Combined with F7, this yields a computationally sound, automated verification of F# code containing public-key encryptions and signatures. For the actual computational soundness proof, we use the CoSP framework (Backes, Hofheinz, and Unruh, CCS 2009). We thus inherit the modularity of CoSP, which allows for easily extending our proof to other cryptographic primitives.

Available format(s)
Cryptographic protocols
Publication info
Published elsewhere. A short version appears at ACM CCS 2010
Protocol verificationcomputational soundness
Contact author(s)
unruh @ mmci uni-saarland de
2010-07-27: received
Short URL
Creative Commons Attribution


      author = {Michael Backes and Matteo Maffei and Dominique Unruh},
      title = {Computationally Sound Verification of Source Code},
      howpublished = {Cryptology ePrint Archive, Paper 2010/416},
      year = {2010},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.