Dimitri DeFigueiredo defigueiredo at ucdavis.edu
Thu Oct 8 18:32:13 UTC 2015

```The cryptographic building blocks we use every day (e.g. blockciphers,
symmetric encryption schemes, message authentication schemes, etc) have
been formalized. I suggest the library follows the mathematical notions.
A good place to see the definitions of the cryptographic building blocks
are Phil Rogaway's lecture notes [1].

For example, there are 2 types of ciphers: blockciphers and
streamciphers. A blockcipher is family of permutations, but a cipher is
a distinct thing from a symmetric encryption scheme. I would say they
have different types. You can build a symmetric encryption scheme using:
1. a blockcipher;
2. a mode of operation (such as Cipher-Block-Chaining, a.k.a CBC); and,
3. a random number (a nonce).

Blockciphers are also distinct from message authentication schemes. The
most famous message authentication scheme is HMAC. It can use a variety
of underlying hash functions (such as SHA1, SHA256, etc).

With this in mind, I find it that the classes you propose should
separate the concepts as they have been formalized. Here's a first rough
pass at a reorg:

class SymEncryptionScheme c where
data Ciphertext   c :: *
data SymmetricKey c :: *
data Nonce        c :: *
data Plaintext   c :: *
KeyGenerationAlgo :: Int -> IO (SymmetricKey c) -- this is
necessarily probabilistic
EncryptionAlgo :: Nonce c -> SymmetricKey c -> Plaintext c ->
Ciphertext c
DecryptionAlgo :: SymmetricKey c -> Ciphertext c -> Plaintext c

class Blockcipher c where
data PlaintextBlock      c :: *
data CiphertextBlock   c :: *
data SymmetricKey      c :: *
blockSize :: c -> Int
encipher :: SymmetricKey c -> PlaintextBlock c -> CiphertextBlock c
decipher :: SymmetricKey c -> CiphertextBlock c -> PlaintextBlock c

class MAC c where
data Plaintext  c :: *
data MessageDigest c :: *
data SymmetricKey c :: *
HashFunction :: Plaintext c -> MessageDigest c
mac :: SymmetricKey c -> Plaintext c -> MessageDigest c

class HashFunction f where
data inputBlock f :: *
data ouputBlock f :: *
compressionFunction :: inputBlock f -> inputBlock f -> ouputBlock f
hash :: ...

I think it is a great idea to use the types to makes sure those building
blocks are assembled together in ways that make sense. I have a feeling
constraints will come in handy.

Hope this helps,

Dimitri

[1] http://cseweb.ucsd.edu/~mihir/cse207/classnotes.html

On 10/8/15 7:48 AM, Alex wrote:
> Hello:
>
> I am implementing a high-level protocol which requires the use of
> various cryptographic primitives. I have the following goals in mind:
>
> 1. Allow others to extend the library to use different underlying
> crypto implementations, ciphers, curves, etc, and
> 2. Have the library be well-typed so that cryptographic operations are
> unambiguous, leading to code which can be easily audited.
>
> According to the spec, the user is allowed to instantiate the protocol
> with any combination of supported ciphers and curves, but the
> high-level operations always remain the same regardless of what
> primitives are used.
>
> Pursuant to the above goals, I've defined two typeclasses, "Cipher" and
> "Curve". I'm using TypeFamilies to facilitate the creation of data
> types that are independent of the underlying crypto library.
>
> The Cipher typeclass is as follows:
>
> class Cipher c
> where
>    data Ciphertext   c :: *
>    data SymmetricKey c :: *
>    data Nonce        c :: *
>    data Digest       c :: *
>
>    cipherName       :: c -> ByteString
>    cipherEncrypt    :: SymmetricKey c -> Nonce c -> AssocData -> Plaintext -> Ciphertext c
>    cipherDecrypt    :: SymmetricKey c -> Nonce c -> AssocData -> Ciphertext c -> Maybe Plaintext
>    cipherZeroNonce  :: Nonce c
>    cipherIncNonce   :: Nonce c -> Nonce c
>    cipherGetKey     :: SymmetricKey c -> Nonce c -> SymmetricKey c
>    cipherHashToKey  :: Digest c -> SymmetricKey c
>    cipherHashToAD   :: Digest c -> AssocData
>    cipherHash       :: ScrubbedBytes -> Digest c
>    cipherConcatHash :: Digest c -> ScrubbedBytes -> Digest c
>    cipherHMAC       :: SymmetricKey c -> ScrubbedBytes -> Digest c
>
> newtype Plaintext = Plaintext ScrubbedBytes
> newtype AssocData = AssocData ScrubbedBytes
>
> Unfortunately, the spec as written assumes that all variables are blobs
> of bytes. The issue I'm running in to is that, in my goal to have
> everything well-typed, my typeclasses are filling up with conversion
> functions like "cipherHashToKey" and "cipherHashToAD". These type
> conversions are necessary because I'm required to compute values like
> "HMAC-HASH(GETKEY(k, n), data)" (which returns "Digest c") and assign
> it to a variable whose type is "SymmetricKey c" (hence the need for
> cipherHashToKey).
>
> Is all my effort to write a well-typed library being done in vain?
> Should I just give up and have all the functions use ByteStrings?
>

```