[Haskell-cafe] Well-typed design issue

Richard Eisenberg eir at cis.upenn.edu
Thu Oct 8 16:51:00 UTC 2015


What's going wrong? It looks like you're off to a solid start here.

I don't know about these cryptographic primitives you speak of, but it sounds like the type conversion functions you're railing against are indeed necessary -- that is, they perform a runtime action. So where's the problem? Richly typed interfaces are sometimes more verbose (especially when you're just setting things up), but you're getting safety guarantees for that payment.

Richard

On Oct 8, 2015, at 9:48 AM, Alex <alex323 at gmail.com> 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?
> 
> -- 
> Alex
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe



More information about the Haskell-Cafe mailing list