Cryptographic primitives¶
PublicKey¶
Public key for public-key cryptography.
type PublicKey := | Curve25519PubKey ByteString;
Auxiliary Juvix code
deriving instance
PublicKeyEq : Eq PublicKey;
instance
PublicKeyOrd : Ord PublicKey :=
mkOrd@{
cmp := \{ := Equal};
};
PrivateKey¶
PrivateKey¶
Private key for public-key cryptography.
type PrivateKey := | Curve25519PrivKey ByteString;
Auxiliary Juvix code
deriving instance
PrivateKeyEq : Eq PrivateKey;
instance
PrivateKeyOrd : Ord PrivateKey :=
mkOrd@{
cmp := \{ := Equal};
};
SecretKey¶
Secret key for secret-key cryptography.
type SecretKey := | ChaCha20Key;
Auxiliary Juvix code
deriving instance
SecretKeyEq : Eq SecretKey;
deriving instance
SecretKeyOrd : Ord SecretKey;
Signature¶
Cryptographic signature.
type Signature := | Ed25519Signature ByteString;
Digest¶
Message digest. Output of a cryptographic hash function.
type Digest := | Blake3Digest ByteString;
hash¶
axiom hash {A} : A -> Digest;