[Haskell-cafe] Well-typed design issue
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
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?
>
More information about the Haskell-Cafe
mailing list