Hi, I've seen references to Cryptol before and it is definitely a great idea to have cryptographic protocols formally verified. I did not know that Galois released the codebase though!
Some other formally verified crypto libraries: http://senier.net/libsparkcrypto/ Libsparkcrypto is a formally verified implementation of several widely used symmetric cryptographic algorithms using the SPARK programming language and toolset. For the complete library proofs of the absence of run-time errors like type range violations, division by zero and numerical overflows are available. Some of its subprograms include proofs of partial correctness. SPARKSkein -- a reference implementation to the Skein hash function. http://www.skein-hash.info/SPARKSkein-release On Sat, Apr 26, 2014 at 8:00 AM, <langsec-discuss-requ...@mail.langsec.org>wrote: > Send langsec-discuss mailing list submissions to > langsec-discuss@mail.langsec.org > > To subscribe or unsubscribe via the World Wide Web, visit > https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss > or, via email, send a message with subject or body 'help' to > langsec-discuss-requ...@mail.langsec.org > > You can reach the person managing the list at > langsec-discuss-ow...@mail.langsec.org > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of langsec-discuss digest..." > > > Today's Topics: > > 1. Cryptol (Yardley, Tim) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Fri, 25 Apr 2014 13:10:16 +0000 > From: "Yardley, Tim" <yard...@illinois.edu> > To: "langsec-discuss@mail.langsec.org" > <langsec-discuss@mail.langsec.org> > Subject: [langsec-discuss] Cryptol > Message-ID: <0e454b0f-7825-4d4d-877e-d2d3743c3...@illinois.edu> > Content-Type: text/plain; charset="us-ascii" > > I ran across this and thought it might be of interest. Anyone have more in > depth thoughts on the work? > > Cryptol - A Domain Specific Language for Implementing Cryptographic > Algorithms > > http://cryptol.net/index.html > > There is a case study linked on the main page as well. > > /tmy > > ------------------------------ > > _______________________________________________ > langsec-discuss mailing list > langsec-discuss@mail.langsec.org > https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss > > > End of langsec-discuss Digest, Vol 20, Issue 9 > ********************************************** >
_______________________________________________ langsec-discuss mailing list langsec-discuss@mail.langsec.org https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss
