Documentation

Cryptlib.Primitives.Sign.Ed25519_blinded

Blinded Ed25519 #

Scalar-based Ed25519: private keys are scalars in ZMod ell, public keys are compressed Edwards points, and the signing nonce is derived from SHA-512(sk)[32:] || message || SHA-512(sk)[33:]. The only assumption is ell_prime.

source
@[reducible, inline]
abbrev Cryptlib.Primitives.Sign.Ed25519Blinded.Scalar :
Type
Equations
Instances For
    source
    @[reducible, inline]
    abbrev Cryptlib.Primitives.Sign.Ed25519Blinded.PubBytes :
    Type
    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev Cryptlib.Primitives.Sign.Ed25519Blinded.SigBytes :
      Type
      Equations
      Instances For
        source
        axiom Cryptlib.Primitives.Sign.Ed25519Blinded.ell_prime :
        Nat.Prime Ed25519Math.ell
        source
        instance Cryptlib.Primitives.Sign.Ed25519Blinded.instFactPrimeEll :
        Fact (Nat.Prime Ed25519Math.ell)
        source
        instance Cryptlib.Primitives.Sign.Ed25519Blinded.instNeZeroNatEll :
        NeZero Ed25519Math.ell
        source
        def Cryptlib.Primitives.Sign.Ed25519Blinded.scalarOfBytes (bytes : ByteArray) :
        Scalar
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Cryptlib.Primitives.Sign.Ed25519Blinded.scalarFromSeed (seed : Vector UInt8 32) :
          Scalar
          Equations
          Instances For
            source
            def Cryptlib.Primitives.Sign.Ed25519Blinded.publicKey (sk : Scalar) :
            PubBytes
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Cryptlib.Primitives.Sign.Ed25519Blinded.signNative (sk : Scalar) (message : ByteArray) :
              SigBytes
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Cryptlib.Primitives.Sign.Ed25519Blinded.verifyNative (pk : PubBytes) (message : ByteArray) (sig : SigBytes) :
                Bool
                Equations
                Instances For
                  source
                  def Cryptlib.Primitives.Sign.Ed25519Blinded.blindPriv (sk factor : Scalar) :
                  Scalar
                  Equations
                  Instances For
                    source
                    def Cryptlib.Primitives.Sign.Ed25519Blinded.blindPub (pk : PubBytes) (factor : Scalar) :
                    PubBytes
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      def Cryptlib.Primitives.Sign.Ed25519Blinded.inv (factor : Scalar) :
                      Scalar
                      Equations
                      Instances For
                        source
                        theorem Cryptlib.Primitives.Sign.Ed25519Blinded.ell_lt :
                        Ed25519Math.ell < 256 ^ 32
                        source
                        theorem Cryptlib.Primitives.Sign.Ed25519Blinded.blindPub_publicKey (s f : Scalar) :
                        blindPub (publicKey s) f = publicKey (f * s)

                        Blinding the public key of s is the public key of f * s.

                        source
                        theorem Cryptlib.Primitives.Sign.Ed25519Blinded.blind_hom (sk factor : Scalar) :
                        publicKey (blindPriv sk factor) = blindPub (publicKey sk) factor
                        source
                        theorem Cryptlib.Primitives.Sign.Ed25519Blinded.verify_signNative (sk : Scalar) (m : ByteArray) :
                        verifyNative (publicKey sk) m (signNative sk m) = true

                        RFC 8032 correctness of the scalar-based signer.

                        source
                        theorem Cryptlib.Primitives.Sign.Ed25519Blinded.psi_injective {P Q : Ed25519Group.W} (h : Ed25519Group.psi P = Ed25519Group.psi Q) :
                        P = Q

                        ψ is injective: ψ P = ψ Q makes ψ (P + -Q) the Edwards identity.

                        source
                        theorem Cryptlib.Primitives.Sign.Ed25519Blinded.G_ne_zero :
                        NIKE.X25519.G ≠ 0
                        source
                        theorem Cryptlib.Primitives.Sign.Ed25519Blinded.addOrderOf_G :
                        addOrderOf NIKE.X25519.G = Ed25519Math.ell

                        The basepoint has order exactly ℓ.

                        source
                        theorem Cryptlib.Primitives.Sign.Ed25519Blinded.smul_G_inj {a b : ℕ} (ha : a < Ed25519Math.ell) (hb : b < Ed25519Math.ell) (h : a • NIKE.X25519.G = b • NIKE.X25519.G) :
                        a = b
                        source
                        theorem Cryptlib.Primitives.Sign.Ed25519Blinded.publicKey_injective :
                        Function.Injective publicKey
                        source
                        theorem Cryptlib.Primitives.Sign.Ed25519Blinded.blindPub_injective (s : Scalar) (hs : s ≠ 0) :
                        Function.Injective (blindPub (publicKey s))

                        Blinding a nonzero root key by different factors gives different public keys.

                        source
                        def Cryptlib.Primitives.Sign.Ed25519Blinded.signature :
                        Sign.Signature
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          def Cryptlib.Primitives.Sign.Ed25519Blinded.blindable :
                          Blindable.Blindable
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For