[Haskell-cafe] Well-typed design issue

[Dimitri DeFigueiredo]

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
     padding :: ...
     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?
>