idris-hackers / idris-crypto Goto Github PK

When I try to build the package, this error message is displayed. I am currently using Windows 8.

Type checking .\Data\Crypto\Hash\MD5.idr
.\Data\Crypto\Hash\MD5.idr:85:15:
   |
85 | shouldMatch_a : hashMessage dummyMD5 (map (intToBits {n=8}) [97]) = intToBits 0x0cc175b9c0f1b6a831c399e269772661
   |               ^
When checking type of Data.Crypto.Hash.MD5.shouldMatch_a:
Can't find implementation for Hash phTy b outputLength

There's a port of inductive binary number arithmetics in the works at https://github.com/sbp/idris-bi/, which I suspect will work much faster than Fin (though the analogue of Fin still has to be defined).

I found the Probabilistic relational verification types work in the F* project very interesting:

Recall that non-interference means that public results do not
depend on secrets. If an expression e with base type a that computes
over some secret information can be given the type

type eq a = x:a{|L x = R x|}

then its result can be safely published, since the execution of e
reveals no information about the secrets.
...
In cryptography, confidentiality is usually stated
as resistance against chosen-plaintext attacks (CPA) ... Instead of reasoning about
two messages selected by b, we just need to show that the function
let cpa’ p = encrypt (sample n) p has the type block → eq block .

I'm not quite sure how well F* effects translate to idris effects, but it seems to me that it's essential to represent these security properties in the types, and not just the number of bits and bytes in the input and output parameters.

All this type tells me is that the function goes from some number of bits to bits; it doesn't express any actual security properties:

encryptBlock : k -> Bits bitsPerBlock -> Bits bitsPerBlock

The identity function satisfies that type, as do constant functions, etc.