Documentation

Cryptlib.Protocols.BACAP.Impl

source
def Cryptlib.Protocols.BACAP.Impl.getBlindScalar (m : Types.MessageBoxIndex) (ctx : ByteArray) :
Primitives.Sign.Ed25519Blinded.Scalar
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Cryptlib.Protocols.BACAP.Impl.getEncKey (m : Types.MessageBoxIndex) (ctx : ByteArray) :
    Primitives.Cipher.AESGCMSIV.Scheme.Key
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Cryptlib.Protocols.BACAP.Impl.implDeriveBoxID (rootPub : Primitives.Sign.Ed25519Blinded.PubBytes) (m : Types.MessageBoxIndex) (ctx : ByteArray) :
      Primitives.Sign.Ed25519Blinded.PubBytes

      The root public key blinded by K_i^ctx.

      Equations
      Instances For
        source
        def Cryptlib.Protocols.BACAP.Impl.implDeriveMessageBoxID (rootPub : Primitives.Sign.Ed25519Blinded.PubBytes) (m : Types.MessageBoxIndex) :
        Primitives.Sign.Ed25519Blinded.PubBytes

        The root public key blinded by K_i, with no context.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Cryptlib.Protocols.BACAP.Impl.implSignBox (rootPriv : Primitives.Sign.Ed25519Blinded.Scalar) (m : Types.MessageBoxIndex) (ctx ct : ByteArray) :
          Primitives.Sign.Ed25519Blinded.PubBytes × Primitives.Sign.Ed25519Blinded.SigBytes
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Cryptlib.Protocols.BACAP.Impl.implVerifyBox (boxId : Primitives.Sign.Ed25519Blinded.PubBytes) (ct : ByteArray) (sig : Primitives.Sign.Ed25519Blinded.SigBytes) :
            Bool
            Equations
            Instances For
              source
              def Cryptlib.Protocols.BACAP.Impl.implEncryptBox (rootPriv : Primitives.Sign.Ed25519Blinded.Scalar) (rootPub : Primitives.Sign.Ed25519Blinded.PubBytes) (m : Types.MessageBoxIndex) (ctx pt : ByteArray) :
              Primitives.Sign.Ed25519Blinded.PubBytes × ByteArray × Primitives.Sign.Ed25519Blinded.SigBytes
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Cryptlib.Protocols.BACAP.Impl.implDecryptBox (boxId : Primitives.Sign.Ed25519Blinded.PubBytes) (m : Types.MessageBoxIndex) (ctx ct : ByteArray) (sig : Primitives.Sign.Ed25519Blinded.SigBytes) :
                Option ByteArray
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  theorem Cryptlib.Protocols.BACAP.Impl.implDecrypt_implEncrypt (sk : Primitives.Sign.Ed25519Blinded.Scalar) (pk : Primitives.Sign.Ed25519Blinded.PubBytes) (idx : Types.MessageBoxIndex) (ctx pt : ByteArray) (hpk : pk = Primitives.Sign.Ed25519Blinded.publicKey sk) :
                  implDecryptBox (implEncryptBox sk pk idx ctx pt).1 idx ctx (implEncryptBox sk pk idx ctx pt).2.1 (implEncryptBox sk pk idx ctx pt).2.2 = some pt

                  Decrypting a box produced by implEncryptBox returns the plaintext.

                  source
                  theorem Cryptlib.Protocols.BACAP.Impl.implDecrypt_sound (sk : Primitives.Sign.Ed25519Blinded.Scalar) (pk boxId : Primitives.Sign.Ed25519Blinded.PubBytes) (idx : Types.MessageBoxIndex) (ctx ct : ByteArray) (sig : Primitives.Sign.Ed25519Blinded.SigBytes) (pt : ByteArray) (hid : implDeriveBoxID pk idx ctx = boxId) (hdec : implDecryptBox boxId idx ctx ct sig = some pt) (hct : ct.size > 0) :
                  (implEncryptBox sk pk idx ctx pt).2.1 = ct

                  A non-tombstone ciphertext that decrypts to pt is the one implEncryptBox produces.

                  source
                  @[instance_reducible]
                  noncomputable def Cryptlib.Protocols.BACAP.Impl.scalarFintypeInst :
                  Fintype Primitives.Sign.Ed25519Blinded.Scalar

                  noncomputable so the compiler does not build List.finRange ℓ at program start.

                  Equations
                  Instances For
                    source
                    @[instance_reducible]
                    noncomputable def Cryptlib.Protocols.BACAP.Impl.scalarSampleableInst :
                    SampleableType Primitives.Sign.Ed25519Blinded.Scalar
                    Equations
                    Instances For
                      source
                      @[instance_reducible]
                      noncomputable def Cryptlib.Protocols.BACAP.Impl.pubDecEqInst :
                      DecidableEq Primitives.Sign.Ed25519Blinded.PubBytes
                      Equations
                      Instances For
                        source
                        noncomputable def Cryptlib.Protocols.BACAP.Impl.bacapSpec :
                        Protocol.BACAPSpec
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For