From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham
	autolearn_force=no version=3.4.4
X-Google-Thread: 103376,8011b6965ae859a1,start
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news1.google.com!news1.google.com!npeer01.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!nntp.club.cc.cmu.edu!feeder.erje.net!eternal-september.org!feeder.eternal-september.org!.POSTED!not-for-mail
From: Alexander Senier <mail@senier.net>
Newsgroups: comp.lang.ada
Subject: ANN: libsparkcrypto
Date: Thu, 9 Sep 2010 00:08:53 +0200
Organization: A noiseless patient Spider
Message-ID: <20100909000853.5ac18f5e@t60>
Mime-Version: 1.0
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
Injection-Date: Wed, 8 Sep 2010 22:08:54 +0000 (UTC)
Injection-Info: mx02.eternal-september.org;
 posting-host="hgseNTinQUJ5sqy98WiAlQ";
	logging-data="25540"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX1+SGwZS7mD5WmjXvYBTmjUb"
X-Newsreader: Claws Mail 3.7.4 (GTK+ 2.20.1; x86_64-pc-linux-gnu)
Cancel-Lock: sha1:tugG2mw+75VyPDEwDNixxQ3nNdU=
Xref: g2news1.google.com comp.lang.ada:13988
Date: 2010-09-09T00:08:53+02:00
List-Id: <comp.lang.ada>

Hello,

I'm happy to announce the first release of libsparkcrypto.

Further information, license and source code is available here:

  http://senier.net/libsparkcrypto/

Version 0.1.0 of libsparkcrypto can be downloaded here:

  http://senier.net/libsparkcrypto/libsparkcrypto-0.1.0.tgz

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.

The distribution contains test cases for all implemented algorithms and
a benchmark to compare its performance with the OpenSSL library. The
achieved speed has been found to be very close to the optimized C and
Assembler implementations of OpenSSL.

Have fun!

Regards,
Alex