fact: Definition MOD_CCA (ζ : PKE_scheme) : package MOD_CCA_loc MOD_CCA_in MOD_CCA_out := [package #def #[ PKGEN ] (_ : 'unit) : 'pkey { #import {sig #[ KEMGEN ] : 'unit → 'pkey } as KEMGEN ;; pk ← get pk_loc ;; #assert (pk == None) ;; KEMGEN Datatypes.tt } ; #def #[ PKENC ] (m : 'plain) : 'ekey × 'cipher { #import {sig #[ ENCAP ] : 'unit → 'ekey } as ENCAP ;; #import {sig #[ ENC ] : 'plain → 'cipher } as ENC ;; pk ← get pk_loc ;; #assert (isSome pk) ;; ek ← get ek_loc ;; #assert (ek == None) ;; c ← get c_loc ;; #assert (c == None) ;; ek ← ENCAP Datatypes.tt ;; #put ek_loc := Some ek ;; c ← ENC m ;; #put c_loc := Some c ;; @ret (chProd 'ekey 'cipher) (ek, c) } ; #def #[ PKDEC ] ('(ek', c') : 'ekey × 'cipher) : 'plain { #import {sig #[ DECAP ] : 'ekey → 'key } as DECAP ;; #import {sig #[ DEC ] : 'cipher → 'plain } as DEC ;; pk ← get pk_loc ;; #assert (isSome pk) ;; ek ← get ek_loc ;; c ← get c_loc ;; #assert ((ek, c) != (Some ek', Some c')) ;; if ek == Some ek' then ( DEC c' ) else ( k' ← DECAP ek' ;; ret (θ.(DEM_dec) k' c') ) } ].
imports: Relational(OrderEnrichedCategory GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr fingroup.fingroup realsum ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq) Crypt(Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb UniformStateProb Package Prelude pkg_composition) Coq(Utf8 Lia) extructures(ord fset fmap) Equations(Equations)