Add deterministic symmetric encryption variant with IND$-CPA security game

[astefano]

SymmEncAlg has monadic encrypt : K → M → m C and decrypt : K → C → m (Option M).
Given that one-time encryption schemes have deterministic encryption, would you consider worth it adding something like DetSEAlg?

The main motivation is that NRS14 (Namprempre, Rogaway, Shrimpton 2014) uses IND$-CPA as the base cipher assumption in Encrypt-then-MAC proofs.

[dtumad]

I think this is worth having. In theory #402 plus this cslib PR should make it possible to just use the existing Cslib.Crypto.EncScheme for this, but I'd also be happy to merge something earlier if you don't want to wait out a whole lean version life-cycle.

[astefano]

Thanks, using Cslib.Crypto.EncScheme for the scheme syntax sounds great. For now, I'll keep a local deterministic-encryption + IND$-CPA stub in my EtM formalization and swap the syntax part when cslib/#581 + VCV-io/#402 land. The IND$-CPA game itself would still need to live in VCVio isn't it?

[dtumad]

The IND$-CPA game itself would still need to live in VCVio?

For now yes, although much longer term I'd hope Cslib will eventually have the type-classes needed to represent this over a generic monad as well and we can just sepecialize that to OracleComp.