Blindable signature schemes

A signature scheme whose keys can be blinded by a scalar, such that a signature made with a blinded private key verifies under the correspondingly blinded public key. PrivateKey is the scalar itself, so blinding is closed on one key type; seed expansion belongs to key generation.

structure Cryptlib.Primitives.Sign.Blindable.Blindable : Type 1

Blinding laws hold for Valid public keys and Invertible factors only: a decodable point with a small-order component breaks g · (f · pk) = (f g) · pk, and f = 0 has no inverse.

• base : Sign.Signature
• Scalar : Type

  Blinding factors.

• Valid : self.base.PublicKey → Prop

  Public keys on which blinding obeys the laws below.

• Invertible : self.Scalar → Prop

  Blinding factors that can be undone.

• Regular : self.base.PublicKey → Prop

  Keys whose blindings are pairwise distinct. Excludes the identity, which every factor fixes.

• mul : self.Scalar → self.Scalar → self.Scalar
• inv : self.Scalar → self.Scalar

  Inverse of a blinding factor.

• scalarOfBytes : ByteArray → self.Scalar

  Turn KDF output into a blinding factor.

• blindPriv : self.base.PrivateKey → self.Scalar → self.base.PrivateKey
• blindPub : self.base.PublicKey → self.Scalar → self.base.PublicKey
• blind_hom (sk : self.base.PrivateKey) (f : self.Scalar) : self.base.pub (self.blindPriv sk f) = self.blindPub (self.base.pub sk) f

  Blinding the private key then deriving agrees with deriving then blinding the public key.

• valid_pub (sk : self.base.PrivateKey) : self.Valid (self.base.pub sk)

  Every derived public key is valid.

• valid_blind (pk : self.base.PublicKey) (f : self.Scalar) : self.Valid pk → self.Valid (self.blindPub pk f)

  Blinding a valid key gives a valid key.

• blind_assoc (pk : self.base.PublicKey) : self.Valid pk → ∀ (f g : self.Scalar), self.blindPub (self.blindPub pk f) g = self.blindPub pk (self.mul f g)

  Blinding twice is blinding by the product.

• blind_comm (f g : self.Scalar) : self.mul f g = self.mul g f

  Blinding factors commute.

• blind_inv (pk : self.base.PublicKey) : self.Valid pk → ∀ (f : self.Scalar), self.Invertible f → self.blindPub (self.blindPub pk f) (self.inv f) = pk

  Unblinding inverts blinding.

• blind_injective (pk : self.base.PublicKey) : self.Regular pk → Function.Injective (self.blindPub pk)

  Distinct blinding factors give distinct keys, for a regular key.

theorem Cryptlib.Primitives.Sign.Blindable.verify_blinded (B : Blindable) (sk : B.base.PrivateKey) (f : B.Scalar) (m : ByteArray) (s : B.base.State) : B.base.verify (B.blindPub (B.base.pub sk) f) m (B.base.sign (B.blindPriv sk f) m s).1 = true

A signature made with a blinded private key verifies under the blinded public key.

theorem Cryptlib.Primitives.Sign.Blindable.blindPriv_assoc (B : Blindable) (sk : B.base.PrivateKey) (f g : B.Scalar) : B.base.pub (B.blindPriv (B.blindPriv sk f) g) = B.base.pub (B.blindPriv sk (B.mul f g))

Blinding a private key twice derives the same public key as blinding once by the product.

theorem Cryptlib.Primitives.Sign.Blindable.blindPriv_inv (B : Blindable) (sk : B.base.PrivateKey) (f : B.Scalar) (hf : B.Invertible f) : B.base.pub (B.blindPriv (B.blindPriv sk f) (B.inv f)) = B.base.pub sk

Blinding and then unblinding a private key returns to the original public key.

theorem Cryptlib.Primitives.Sign.Blindable.blindPub_swap (B : Blindable) (pk : B.base.PublicKey) (hpk : B.Valid pk) (f g : B.Scalar) : B.blindPub (B.blindPub pk f) g = B.blindPub (B.blindPub pk g) f

The order in which two blindings are applied is unobservable.

theorem Cryptlib.Primitives.Sign.Blindable.blind_unlinkable (B : Blindable) [Fintype B.Scalar] [SampleableType B.Scalar] [DecidableEq B.base.PublicKey] (pk : B.base.PublicKey) (hpk : B.Regular pk) {target : B.base.PublicKey} (htarget : target ∈ Set.range (B.blindPub pk)) : Pr[= true | do let f ← $ᵗ B.Scalar pure (decide (B.blindPub pk f = target))] = (↑(Fintype.card B.Scalar))⁻¹

For a regular key pk, a uniform blinding factor gives each key in the orbit of pk with probability 1/|Scalar|.

@[instance_reducible]

instance Cryptlib.Primitives.Sign.Blindable.instInhabitedBlindable : Inhabited Blindable

The trivial blindable scheme, where every blinding is the identity.

Equations

• One or more equations did not get rendered due to their size.