[hacspec] Welcome to the hacspec mailing list

[Franziskus Kiefer]

 Hi all,

let's get this mailing list started.

The goal of HacSpec is to define a new specification language for crypto
primitives that is succinct, that is easy to read and implement, and that
lends itself to formal verification.

During the recent HACS workshop we started working on HacSpec. Karthik and
I improved a little on that over the last couple of weeks and we would like
to get more of you involved.

HacSpec lives on Github [1].

There is a HacSpec demo of ChaCha20Poly1305 [2] and a very experimental
HacSpec to F* compiler from Karthik [3]

There are also spec examples in F*,  coq, cryptol, and easycryp [4] as well
as an experimental spec checker from Aaron [5].


We would like to invite anyone to contribute to any part of HacSpec. In
particular we invite people to contribute specs, test-vectors, code, and
translation tools.

Note that HacSpec does _not_ aim to be general enough to express protocols
at this point. While this might be a target in the future the first
iteration of HacSpec is only targeting crypto primitives.


Fore reference:
* The mailing list can be accessed at https://moderncrypto.org/mailm
an/listinfo/hacspec
* I wrote a short blog post [6] about HacSpec and what we want to achieve.

Cheers,
Franziskus

[1] https://github.com/HACS-workshop/hacspec
[2] https://github.com/HACS-workshop/hacspec/tree/master/specs
[3] https://github.com/HACS-workshop/hacspec/tree/master/spec-compilers
[4] https://github.com/HACS-workshop/hacspec/tree/master/formal-models
[5] https://github.com/HACS-workshop/hacspec/tree/master/spec-checker
[6] https://www.franziskuskiefer.de/post/hacspec1/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://moderncrypto.org/mail-archive/hacspec/attachments/20180208/e4bc9197/attachment.html>