[langsec-discuss] langsec-discuss Digest, Vol 20, Issue 9

GreyHat LispHacker greyhatlisphacker at gmail.com
Thu May 1 08:41:11 UTC 2014


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-request at mail.langsec.org>wrote:

> Send langsec-discuss mailing list submissions to
>         langsec-discuss at 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-request at mail.langsec.org
>
> You can reach the person managing the list at
>         langsec-discuss-owner at 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" <yardley at illinois.edu>
> To: "langsec-discuss at mail.langsec.org"
>         <langsec-discuss at mail.langsec.org>
> Subject: [langsec-discuss] Cryptol
> Message-ID: <0E454B0F-7825-4D4D-877E-D2D3743C375B at 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 at mail.langsec.org
> https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss
>
>
> End of langsec-discuss Digest, Vol 20, Issue 9
> **********************************************
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.langsec.org/pipermail/langsec-discuss/attachments/20140501/dae06c95/attachment.html>


More information about the langsec-discuss mailing list