Slashdot Mirror

← Back to Stories (view on slashdot.org)

Cryptol, Language of Cryptography, Now Available To the Public

Posted by ryuzaki0 on from the new-toys-to-play-with dept.

solweil writes to mention that Cryptol, a 'domain specific language for the design, implementation and verification of cryptographic algorithms,' is now available to the public. Cryptol was originally designed for the NSA. It allows for a quick evaluation and continued revisions, and is available for Linux, OS X, and Windows.

11 of 140 comments (clear)

  1. Kudos to NSA by rindeee · · Score: 5, Interesting

    Having worked at the Agency I must say that the quality of the 'product' that they turn over to the public domain is second to none (well, except for that which they keep for themselves of course). They take a lot of heat at a leadership level, some warranted, some not. In the end, the caliber of the engineers, security professionals and JPG (just plain geeks) that work there is second to none. From SEL to crypto bake-offs to the submitter's topic, they've done a helluva lot of good for the community. Thanks guys! Now if they could just get 'Weed Man' to open an omelet shop out in town, all would be right with the world (inside joke, sorry).

    1. Re:Kudos to NSA by caramelcarrot · · Score: 5, Funny

      That "M+" button on your calculator that no-one knows how to use. That's what it does.

    2. Re:Kudos to NSA by collinstocks · · Score: 5, Informative

      Just a correction: Regardless of who developed this (there seems to be some disagreement), nobody turned it over to the public domain. Read the license agreement: it says that you are not allowed to even create derivative works, nor redistribute the program to multiple sources, nor use it for commercial purposes.

    3. Re:Kudos to NSA by Chyeld · · Score: 4, Informative

      There are infinitely many prime numbers.

      The oldest known proof for the statement that there are infinitely many prime numbers is given by the Greek mathematician Euclid in his Elements (Book IX, Proposition 20). Euclid states the result as "there are more than any given [finite] number of primes", and his proof is essentially the following:

      Consider any finite set of primes. Multiply all of them together and add 1 (see Euclid number). The resulting number is not divisible by any of the primes in the finite set we considered, because dividing by any of these would give a remainder of 1. Because all non-prime numbers can be decomposed into a product of underlying primes, then either this resultant number is prime itself, or there is a prime number or prime numbers which the resultant number could be decomposed into but are not in the original finite set of primes. Either way, there is at least one more prime that was not in the finite set we started with. This argument applies no matter what finite set we began with. So there are more primes than any given finite number.

  2. really? by gclef · · Score: 5, Funny

    So, wait, the NSA just released math?

    1. Re:really? by BitZtream · · Score: 5, Funny

      Math 2.0

      --
      Persistent Volume manager for Kubernetes - https://github.com/dwimsey/openshift-pvmanager
  3. Cryptol? by larry+bagina · · Score: 4, Funny

    Sounds more like a drug than a programming language.

    --
    Do you even lift?

    These aren't the 'roids you're looking for.

  4. Interesting for discrite math. by Animats · · Score: 5, Interesting

    Neat. There's some similarity to Matlab, and some to Renderman, and some of the syntax is borrowed from Haskell. The language is compilable to VHDL, so it's possible to generate hardware from the spec. The language is recursive and doesn't support iteration (there's no "for" statement) to make proof of correctness work easier.

    This language might also be useful as a way to express compression algorithms. Reference implementations of the various "zip" algorithms in Cryptol would be useful, and ones for JPEG and MPEG compression, which are often implemented in hardware, even more useful. It's not clear how well Cryptol deals with memory-heavy problems like motion recognition or Hamming table building for compression, though.

  5. Lack of Functionality by burning-toast · · Score: 5, Insightful

    FTFA:
    "The open version does not compile to VHDL, C/C++, or Haskell, and does not produce the formal models used for equivalence checking."

    So does this mean the open version (trial version) which we might have access to does not do much of what it is touted to be good for?

    Just another advertisement for a commercial product methinks. Maybe cool, but still a slashvertisement.

    - Toast

    1. Re:Lack of Functionality by Dun+Malg · · Score: 4, Informative

      FTFA: "The open version does not compile to VHDL, C/C++, or Haskell, and does not produce the formal models used for equivalence checking."

      So does this mean the open version (trial version) which we might have access to does not do much of what it is touted to be good for?

      Just another advertisement for a commercial product methinks. Maybe cool, but still a slashvertisement.

      - Toast

      Yep. Two lines down from the above quote it states:

      "Contact Galois to obtain a full-featured version for evaluation."

      It's classic crippleware. Free version doesn't do anything useful, and the "full-featured" version costs money and uses a dongle or something.

      --
      If a job's not worth doing, it's not worth doing right.
  6. You're off on your orders there by MarkusQ · · Score: 4, Interesting

    Just a matter of looping through all known primes, seeing if x divides by it. That's order 1 since the number of primes is "fixed". If you don't find anything it divides by, it's a new prime (add it to your list) or its smallest factor is larger than your biggest known prime. Otherwise remember that factor, and start working on the dividend.

    Check yourself there. It takes longer to perform division on larger numbers (say O(ln(N)^2), though a lot of this depends on the algorithm). If you plan to do the sieve of eratosthenes as you describe (the hard way), that's going to be another O(n*ln(ln(N)) for a total of O(n*ln(N)^2*ln(ln(n))) for each factor.

    The sort of numbers you are thinking about when you say that testing via division is O(1) with hardware are 64 bit integers. The sort of semi-primes used in cryptography are on the order of 512 bits, and so (by the formula above) would take roughly 147, 184, 841, 669, 860, 395, 336, 238, 071, 097, 320, 918, 206, 612, 375, 539, 181, 907, 207, 001, 765, 334, 079, 455, 842, 963, 079, 473, 553, 687, 769, 537, 122, 026, 054, 410, 625, 268, 901, 031, 540, 756, 829, 794, 467, 840, 000 times as long.

    So if your computer took a nanosecond to solve a 64 bit case (making it faster than the fastest consumer system presently available), and you had a million of them, and all 6 billion people on Earth were your friends, and each of them had a million of these uber boxes as well, and you had a way to collaborate on the problem with no overhead, it would still take you roughly 1, 920, 658, 729, 429, 876, 148, 289, 055, 386, 140, 718, 898, 913, 520, 422, 922, 263, 604, 244, 594, 006, 798, 154, 722, 944, 671, 495, 344, 450, 391, 916, 549, 249, 431, 238 times the age of the universe to factor one such number.

    That's why nobody does it that way, and why it's considered a hard problem even though it might sound easy.

    -- MarkusQ