[langsec-discuss] Cryptol

Andrew munin at mimisbrunnr.net
Sat Apr 12 17:43:55 UTC 2014


Cryptol as described (and as I understand it) is a map from their DSL to VHDL, but it can also output software implementations of cryptographic specifications into C, C++, Haskell, etc. So if someone sat down and wrote out TLS in cryptol, then they wouldn’t need to worry about getting the implementation details correct. Cryptol also includes checking of implementations and the idea is I think loosely connected to miTLS and F7. 

On Apr 12, 2014, at 1:29 PM, Will Sargent <will.sargent at gmail.com> wrote:

> A DSL specifically for designing cryptographic algorithms.
> 
> http://corp.galois.com/cryptol/ 
> 
> Not that it would have helped with TLS, but it's interesting.
> 
> Will.
> _______________________________________________
> langsec-discuss mailing list
> langsec-discuss at mail.langsec.org
> https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.langsec.org/pipermail/langsec-discuss/attachments/20140412/e5156d31/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 495 bytes
Desc: Message signed with OpenPGP using GPGMail
URL: <https://mail.langsec.org/pipermail/langsec-discuss/attachments/20140412/e5156d31/attachment.pgp>


More information about the langsec-discuss mailing list