A cryptographic framework, proven for correctness in SPARK
Requires GNAT Community 2020, as we are making use of SPARK's Relaxed_Initialization.
Algorithms contained
-
Phelix - Fast Encryption and Authentication in a Single Cryptographic Primitive
Doug Whiting, Bruce Schneier, Stefan Lucks, and Frédéric Muller
ECRYPT Stream Cipher Project Report 2005/027, 2005.
ABSTRACT: Phelix¹ is a high-speed stream cipher with a built-in MAC functionality. It is efficient in both hardware and software. On current Pentium CPUs, Phelix has a per-packet overhead of less than 900 clocks, plus a per-byte cost well under 8 clocks per byte, comparing very favorably with the best AES (encryption-only) implementations, even for small packets.
¹ Pronounced "felix" (rhymes with "helix").