5 Matching Annotations
1. Dec 2020
2. eprint.iacr.org eprint.iacr.org
1. Intuitively, in order to prove that a processQ0satisfiesa non-injective correspondenceψ⇒φ, we collect all factsthat hold at events inψand show that these facts implyφusing the equational prover.

How CryptoVerif proves non-injective correspondence properties

2. 6.3. Injective CorrespondencesInjective correspondences are more difficult to checkthan non-injective ones, because they require distinguishingbetween several executions of the same event. We achievethat as follows

How CryptoVerif proves injective correspondence properties

#### URL

3. eprint.iacr.org eprint.iacr.org
1. 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

#### URL

4. Apr 2020
5. eprint.iacr.org eprint.iacr.org
1. 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.

2. Q|Rx≈Q|R′x

When proving a “query secret k” for Q, CryptoVerif proves the indistinguishability of Q|R_x and Q|R'_x. One could imagine that CryptoVerif appends the oracle R_x to Q by parallel composition.