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.
Category / Keywords: cryptographic protocols / Protocol verification, computational soundness Publication Info: A short version appears at ACM CCS 2010 Date: received 26 Jul 2010 Contact author: unruh at mmci uni-saarland de Available format(s): PDF | BibTeX Citation Version: 20100727:152523 (All versions of this report) Short URL: ia.cr/2010/416