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;