source

hkdf_ada

0.1.0

SPARK-proved HKDF (RFC 5869) - HKDF_SHA256 proved at Level 2

GitHub Community CIResults All crate versions Download JSON

0.1.0

SPARK-proved HKDF (RFC 5869) for Ada 2022, built on hmac_ada. The HKDF-SHA-256 instantiation is fully proved at SPARK Level 2 (266 checks, zero pragma Assume). Uses System.Storage_Elements.Storage_Array for embedded and constrained-runtime (Light, ZFP) compatibility, no heap allocation, pragma Pure. A separate generic HKDF package provides an unproved convenience layer for other HMAC functions.

Authors: Baris Erdem
Maintainers: Baris Erdem <baris@erdem.dev>
Maintainer profiles: @b-erdem
Licenses: Apache-2.0
Website: https://github.com/b-erdem/hkdf_ada
Repository: github.com/b-erdem/hkdf_ada
Source revision: cdde31c8e98c
Tags: hkdf, rfc5869, kdf, cryptography, spark, embedded, security
Manifest: index/hk/hkdf_ada/hkdf_ada-0.1.0.toml