Re: [Haskell-cafe] Well-typed design issue

8 Oct 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
     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?

Re: [Haskell-cafe] Well-typed design issue

Dimitri DeFigueiredo