Explicit Randomness is not Necessary when Modeling Probabilistic Encryption

Véronique Cortier, Heinrich Hördegen, Bogdan Warinschi

Although good encryption functions are probabilistic, most symbolic models do not capture this aspect explicitly. A typical solution, recently used to prove the soundness of such m…