Paper 2010/416

Computationally Sound Verification of Source Code

Michael Backes, Matteo Maffei, and Dominique Unruh

Abstract

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.

Metadata
Available format(s)
PDF
Category
Cryptographic protocols
Publication info
Published elsewhere. A short version appears at ACM CCS 2010
Keywords
Protocol verificationcomputational soundness
Contact author(s)
unruh @ mmci uni-saarland de
History
2010-07-27: received
Short URL
https://ia.cr/2010/416
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2010/416,
      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{https://eprint.iacr.org/2010/416}},
      url = {https://eprint.iacr.org/2010/416}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.