<html><head><meta http-equiv="Content-Type" content="text/html charset=windows-1252"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;">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. <div><div><br><div><div>On Apr 12, 2014, at 1:29 PM, Will Sargent <<a href="mailto:will.sargent@gmail.com">will.sargent@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><div dir="ltr">A DSL specifically for designing cryptographic algorithms.<br><div><br></div><div><a href="http://corp.galois.com/cryptol/">http://corp.galois.com/cryptol/</a> <br></div><div><br></div><div>Not that it would have helped with TLS, but it's interesting.</div>

<div><br></div><div>Will.</div></div>
_______________________________________________<br>langsec-discuss mailing list<br><a href="mailto:langsec-discuss@mail.langsec.org">langsec-discuss@mail.langsec.org</a><br>https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss<br></blockquote></div><br></div></div></body></html>