5 Matching Annotations
 Dec 2020

eprint.iacr.org eprint.iacr.org128.pdf2

Intuitively, in order to prove that a processQ0satisfiesa noninjective correspondenceψ⇒φ, we collect all factsthat hold at events inψand show that these facts implyφusing the equational prover.
How CryptoVerif proves noninjective correspondence properties

6.3. Injective CorrespondencesInjective correspondences are more difficult to checkthan noninjective ones, because they require distinguishingbetween several executions of the same event. We achievethat as follows
How CryptoVerif proves injective correspondence properties
Tags
Annotators
URL


eprint.iacr.org eprint.iacr.org069.pdf1

Actually, the modifications of games can beseen as “rewriting rules” of the probability distributions of the variables involved in the games. Theymay consist of a simple renaming of some variables, and thus to perfectly identical distributions. Theymay introduce unlikely differences, and then the distributions are “statistically” indistinguishable.Finally, the rewriting rule may be true under a computational assumption only: then appears thecomputational indistinguishability
Tags
Annotators
URL

 Apr 2020

eprint.iacr.org eprint.iacr.org401.pdf2

findu′≤nsuchthat defined(y[u′],u1[u′],...,um[u′])∧u1[u′] =u1∧...∧um[u′] =umthenc〈y[u′]
If the same indices are queried again, return the same y.

QRx≈QR′x
When proving a “query secret k” for Q, CryptoVerif proves the indistinguishability of QR_x and QR'_x. One could imagine that CryptoVerif appends the oracle R_x to Q by parallel composition.
