BACAP unlinkability (Echomix §4.3, arXiv:2501.02933)

Assuming uniformly random blinding factors, box IDs are perfectly unlinkable (δ = 0): their distribution does not depend on whether they share a root secret.

theorem Cryptlib.Protocols.BACAP.Unlinkability.unlinkable {F G : Type} [Field F] [AddCommGroup G] [Module F G] [Fintype F] [SampleableType (F × F)] [DecidableEq G] {P Q : G} (hP : Function.Injective fun (x : F) => x • P) (hQ : Function.Injective fun (x : F) => x • Q) {m n : G} (hm : m ∈ Set.range fun (x : F) => x • P) (hn : n ∈ Set.range fun (x : F) => x • Q) : Pr[= true | do let kk ← $ᵗ (F × F) pure (decide ((kk.1 • P, kk.2 • Q) = (m, n)))] = (↑(Fintype.card (F × F)))⁻¹

Independent uniform scalars applied to P and Q hit any target pair in the image with probability 1 / |F × F|, provided · • P and · • Q are injective.

theorem Cryptlib.Protocols.BACAP.Unlinkability.unlinkable_delta_zero {F G : Type} [Field F] [AddCommGroup G] [Module F G] [Fintype F] [SampleableType (F × F)] [DecidableEq G] {P Q P' Q' : G} (hP : Function.Injective fun (x : F) => x • P) (hQ : Function.Injective fun (x : F) => x • Q) (hP' : Function.Injective fun (x : F) => x • P') (hQ' : Function.Injective fun (x : F) => x • Q') {m n : G} (hm : m ∈ Set.range fun (x : F) => x • P) (hn : n ∈ Set.range fun (x : F) => x • Q) (hm' : m ∈ Set.range fun (x : F) => x • P') (hn' : n ∈ Set.range fun (x : F) => x • Q') : Pr[= true | do let kk ← $ᵗ (F × F) pure (decide ((kk.1 • P, kk.2 • Q) = (m, n)))] = Pr[= true | do let kk ← $ᵗ (F × F) pure (decide ((kk.1 • P', kk.2 • Q') = (m, n)))]

The distribution of (Kx • P, Ky • Q) does not depend on P, Q: two box IDs reveal nothing about whether they share a root secret.