Commit Graph

37 Commits

Author SHA1 Message Date
Adam C. Foltzer
adcd96fa47 make notebook distributable
This commit brings the notebook into the rest of the distribution
infrastructure set up for cryptol. The main points are:

- new icryptol-kernel executable
- new icryptol shell script that wraps ipython and makes sure the
  cryptol profile is set up
- Makefile target for friendly local testing (`make notebook`)
- moved example notebooks to examples subdirectory
2015-02-11 16:21:43 -08:00
Adam C. Foltzer
22df9717cb properties and cleanup for new contrib examples 2015-01-18 12:46:03 -08:00
Adam C. Foltzer
d7e9b9b3c6 add README for contrib 2015-01-18 12:45:39 -08:00
Adam C. Foltzer
473b175922 move RC4 to contrib directory 2015-01-18 11:47:40 -08:00
orchid
1f3c9b8203 RC4 2015-01-18 11:47:40 -08:00
Adam C. Foltzer
85e1725b29 Merge pull request #69 from mknight-tag/master
Add MKRAND RBG to contrib
2015-01-18 11:42:21 -08:00
Dylan McNamee
16bca156d7 Salsa20 working better with type checker improvements (thanks, Sean!) 2014-12-17 06:44:39 -05:00
Dylan McNamee
675ca65c9a fixes to Salsa20 spec suggested by Sean (thanks!) 2014-10-10 12:37:10 -07:00
M Knight
ee86eb87fd Back out ND until Cryptol exposes IO Monad [fd4f4] 2014-09-24 09:13:28 -05:00
Thomas M. DuBuisson
31f0015e8c Merge pull request #29 from TomMD/fnv1a-example
Add an FNV-1a example (non-cryptographic hash).
2014-09-14 15:05:24 -07:00
Dylan McNamee
75852a2596 Merge branch 'master' of https://github.com/GaloisInc/cryptol 2014-09-10 14:27:26 -07:00
Dylan McNamee
81adb95a37 tweaks to documentation and Salsa20 fix from Sean 2014-09-10 14:27:08 -07:00
Adam C. Foltzer
a0bb572388 add note about solvers for ZUC theorem 2014-09-08 14:45:10 -07:00
Adam C. Foltzer
4622a1d177 add ZUC example, translated from Cryptol 1 2014-09-04 11:05:42 -07:00
Adam C. Foltzer
d409116160 Merge branch 'devel'
This was the branch I originally set up for git flow, but we're moving
to production=release and develop=master, so this branch is obsolete.
2014-08-19 10:31:31 -07:00
M Knight
502816fbd3 Add MKRAND RBG 2014-08-10 10:47:19 -05:00
Joey Dodds
7300f29606 changed collision properties to require inputs to be different 2014-08-06 10:16:14 -07:00
Joey Dodds
72fefff367 added malicious sha example 2014-08-05 14:08:30 -07:00
Joey Dodds
d248b50b40 finished test vectors
created function AeadConstruction that is used to generate tags in
AEAD encryption and decryption
2014-08-04 10:52:50 -07:00
Joey Dodds
72c870cb12 small fixes for push 2014-08-01 09:15:58 -07:00
Joey Dodds
00ad314681 added most of the test cases 2014-07-29 16:39:50 -07:00
Dylan McNamee
5faf927b3e Initial (incomplete, but mostly working) version of ChaChaPoly IETF draft.
Original document: https://datatracker.ietf.org/doc/draft-irtf-cfrg-chacha20-poly1305/
2014-07-29 09:32:14 -07:00
Thomas M. DuBuisson
97488c0cc1 Add an FNV-1a example (non-cryptographic hash). 2014-05-29 22:13:28 -07:00
Dylan McNamee
87042d4604 fixing lone bad reference in doc, added syntax chapter, replaced Salsa spec
PDF with pointer to it, fixed table in section 1.2.2
2014-04-30 11:37:15 -07:00
Adam C. Foltzer
2cf71679c6 Merge branch 'master' into devel 2014-04-27 20:51:56 -07:00
David Lazar
fe67268088 Simplify type constraints. 2014-04-24 17:33:43 -04:00
David Lazar
bda2596f30 Minor whitespace tweak. 2014-04-24 17:28:25 -04:00
David Lazar
e1c2ddec55 Fix formatting in speck.cry. 2014-04-24 17:27:34 -04:00
David Lazar
46c93d1a33 spec.cry should be speck.cry. 2014-04-24 17:19:20 -04:00
Dylan McNamee
bba0c10cf7 keccak is version 1, and proving too tricky to convert for now.
Moving simon and spec to contrib, to "seed the pool" of contributed
examples.
2014-04-22 17:26:11 -07:00
Dylan McNamee
72d690bd9f a little "how to run this" added to funstuff 2014-04-22 10:44:02 -07:00
Dylan McNamee
a04a2444a5 Note: NIST 180-4 has an inconsistency in section 4.1.1 - the prose
says 0<=t<=80, but the formula says 0<=t<=79. Later, they refer to
80 elements, so we're going with the formula's specification
2014-04-21 13:50:00 -07:00
Dylan McNamee
744808f67f Making the SHA1 "f" look more like the NIST SHA1 "f" 2014-04-21 13:42:56 -07:00
Adam C. Foltzer
bca8d997f5 add David's Keccak implementation 2014-04-21 11:46:55 -07:00
Dylan McNamee
4f57c0a93f polishing 2014-04-21 11:40:07 -07:00
Adam C. Foltzer
63b77b82d3 add David's Keccak implementation 2014-04-21 11:39:07 -07:00
Adam C. Foltzer
ba0a0e8576 Initial import from internal repo 2014-04-17 15:34:25 -07:00