Wrap-resistance (§4.3) #
A fresh uniform blinding factor hits any fixed target group element with probability 1/N,
since blinding by a generator is a bijection. Single-query case only. KEM-Sphinx has no
analogue: it has no group element to re-blind.
Sphinx's blinding step, for X25519 #
theorem
Cryptlib.Protocols.Sphinx.WrapResistance.blind_wrapResistance
{N : ℕ}
[NeZero N]
(pk target : Primitives.NIKE.X25519.Point)
(hbij : Function.Bijective fun (b : Fin N) => ↑b • pk)
:
Single-query wrap-resistance of the blinding step, assuming scalar multiplication by pk is a
bijection on Fin N: the probability of hitting target is 1/N.