fstar
  1. Overview
  2. Docs
package fstar
Legend:
Library
Module
Module type
Parameter
Class
Class type
type 'n nbytes = FStar_Bytes.bytes
type tag = Prims.unit nbytes
val sha1 : FStar_Bytes.bytes -> tag
type hmac_key = Prims.unit nbytes
val hmac_sha1_keygen : Prims.unit -> hmac_key
val hmac_sha1 : hmac_key -> FStar_Bytes.bytes -> tag
val hmac_sha1_verify : hmac_key -> FStar_Bytes.bytes -> tag -> Prims.bool
type block = Prims.unit nbytes
type cipher = Prims.unit nbytes
type aes_key = Prims.unit nbytes
type aes_iv = Prims.unit nbytes
val aes_128_keygen : Prims.unit -> aes_key
val aes_128_decrypt : aes_key -> cipher -> block
val aes_128_encrypt : aes_key -> block -> cipher
val aes_128_ivgen : Prims.unit -> aes_iv
val aes_128_cbc_decrypt : aes_key -> aes_iv -> FStar_Bytes.bytes -> FStar_Bytes.bytes
val aes_128_cbc_encrypt : aes_key -> aes_iv -> FStar_Bytes.bytes -> FStar_Bytes.bytes
type rsa_pkey = {
  1. modulus : FStar_Bytes.bytes;
  2. exponent : FStar_Bytes.bytes;
}
val __proj__Mkrsa_pkey__item__modulus : rsa_pkey -> FStar_Bytes.bytes
val __proj__Mkrsa_pkey__item__exponent : rsa_pkey -> FStar_Bytes.bytes
type rsa_skey = rsa_pkey * FStar_Bytes.bytes
val rsa_keygen : Prims.unit -> rsa_skey
val rsa_pk : rsa_skey -> rsa_pkey
val rsa_pkcs1_encrypt : rsa_pkey -> FStar_Bytes.bytes -> FStar_Bytes.bytes
val rsa_pkcs1_decrypt : rsa_skey -> FStar_Bytes.bytes -> FStar_Bytes.bytes
type sigv = FStar_Bytes.bytes
val rsa_sha1 : rsa_skey -> FStar_Bytes.bytes -> sigv
val rsa_sha1_verify : rsa_pkey -> FStar_Bytes.bytes -> sigv -> Prims.bool