Modular Code-Based Cryptographic Verification - Archive ouverte HAL Access content directly
Conference Papers Year : 2011

Modular Code-Based Cryptographic Verification

(1) , (1) , (2)
1
2
Cédric Fournet
  • Function : Author
  • PersonId : 901974
Markulf Kohlweiss
  • Function : Author
  • PersonId : 907490
Pierre-Yves Strub
  • Function : Author
  • PersonId : 857170

Abstract

Type systems are effective tools for verifying the security of cryptographic programs. They provide automation, modularity and scalability, and have been applied to large security protocols. However, they traditionally rely on abstract assumptions on the underlying cryptographic primitives, expressed in symbolic models. Cryptographers usually reason on security assumptions using lower level, computational models that precisely account for the complexity and success probability of attacks. These models are more realistic, but they are harder to formalize and automate. We present the first modular automated program verification method based on standard cryptographic assumptions. We show how to verify ideal functionalities and protocols written in ML by typing them against new cryptographic interfaces using F7, a refinement type checker coupled with an SMT-solver. We develop a probabilistic core calculus for F7 and formalize its type safety in Coq. We build typed module and interfaces for MACs, signatures, and encryptions, and establish their authenticity and secrecy properties. We relate their ideal functionalities and concrete implementations, using game-based program transformations behind typed interfaces. We illustrate our method on a series of protocol implementations.
Fichier principal
Vignette du fichier
cst-ccs-2011.pdf (154.75 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

inria-00614372 , version 1 (08-11-2011)

Identifiers

  • HAL Id : inria-00614372 , version 1

Cite

Cédric Fournet, Markulf Kohlweiss, Pierre-Yves Strub. Modular Code-Based Cryptographic Verification. 18th ACM Conference on Computer and Communications Security, Oct 2011, Chicago, United States. ⟨inria-00614372⟩

Collections

INRIA
187 View
571 Download

Share

Gmail Facebook Twitter LinkedIn More