CV2EC: Getting the Best of Both Worlds

Bruno Blanchet, Pierre Boutry, Christian Dockzal, Benjamin Grégoire, Pierre-Yves Stub. CV2EC: Getting the Best of Both Worlds. To appear at CSF'24.

The source files are also included in the directory cv2EasyCrypt of CryptoVerif version 2.08. The files in the CryptoVerif distribution will be updated if needed as CryptoVerif and EasyCrypt evolve.

• Helper files:
  • CV2EC.ec: EasyCrypt library
  • LR.eca: Generic "left or right" oracles
  • UnitRO.ec: Random oracles
• Section III: Translation
  • III.A IND-CPA CV source EC output
  • III.B IND-CCA2
    Version with tables: CV source EC output
    Version with find: CV source EC output
• Section IV: Case studies
  • IV.A IND-CCA2: CV source IND_CCA2.ec: EC output Proof: Main file RealIdeal_CCA2.ec: real/ideal IND-CCA2 definition IND_CCA2_hybrid.ec: Hybrid argument
  • IV.B OutsiderCCA for AKEM: CV source = Option type + Authenticated KEM + Macro usage (The translated equiv statement is outsider_cca(AuthEncap).) OUT_CCA.ec: EC output Proof: Main file OutsiderCCA.ec: Hybrid argument
  • IV.C CDH assumption: CV source CDH_RSR.ec: EC output Proof: Main file NominalGroup.ec: nominal groups CDH_RSR_NCDH.ec: mathematical proof
  • IV.D GDH assumption: CV source GDH_RSR.ec: EC output Proof: Main file NominalGroup.ec: nominal groups GDH_RSR_NGDH.ec: mathematical proof