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
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
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
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.
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.