Want to read Slashdot from your mobile device? Point it at m.slashdot.org and keep reading!

 



Forgot your password?
typodupeerror
×

Cryptol, Language of Cryptography, Now Available To the Public 140

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.
This discussion has been archived. No new comments can be posted.

Cryptol, Language of Cryptography, Now Available To the Public

Comments Filter:
  • Crack this! (Score:2, Funny)

    by mugnyte ( 203225 )

      41R5T 3N6RI27ED P057 !

  • Kudos to NSA (Score:5, Interesting)

    by rindeee ( 530084 ) on Friday December 26, 2008 @02:56PM (#26236389)
    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).
    • Re: (Score:1, Funny)

      by Anonymous Coward

      So, how DO you factor large semiprimes fast?

      • by caramelcarrot ( 778148 ) on Friday December 26, 2008 @03:44PM (#26236621)
        That "M+" button on your calculator that no-one knows how to use. That's what it does.
        • Re: (Score:2, Funny)

          by Anonymous Coward
          I use that to store "5318008" in memory so I always have one on hand.
          • Re: (Score:2, Funny)

            by Anonymous Coward
            Is there anything that little button can't do? I have a feeling "M+" stands for "More magic".
      • Re: (Score:2, Funny)

        by v1 ( 525388 )

        So, how DO you factor large semiprimes fast?

        can someone explain why this is hard to do? It seems like a straghtforward process since the number of primes is essentially fixed. (there are quite a few of them but we keep hearing announcements about a new ONE being found, so there can't be that many of them that are known, someone's got a book I'm sure)

        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 anythin

        • Re:Kudos to NSA (Score:5, Informative)

          by Chyeld ( 713439 ) <chyeld@g m a i l . com> on Friday December 26, 2008 @06:03PM (#26237329)

          There are infinitely many prime numbers. [wikipedia.org]

          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.

          • by MichaelSmith ( 789609 ) on Saturday December 27, 2008 @12:52AM (#26239705) Homepage Journal

            The GP said the number of primes is essentially fixed which is consistent with the number of primes being infinite, I suppose.

        • Re:Kudos to NSA (Score:4, Interesting)

          by cromar ( 1103585 ) on Friday December 26, 2008 @06:19PM (#26237411)
          Interesting question. You always hear that it's because of "prime factorization" or something, and to tell the truth I hadn't thought about what that actually meant. The article on RSA at Wikipedia seems informative:

          The RSA problem is defined as the task of taking eth roots modulo a composite n: recovering a value m such that c=me mod n, where (n, e) is an RSA public key and c is an RSA ciphertext.

          Keep in mind these are typically 1024-bit (or more) numbers -- 2 ^ 1024 possible numbers to factor. Also, the world's record for factorization at the moment is for factoring a 668-bit number that took "several months of computer time using the combined power of 80 AMD Opteron CPUs. [wikipedia.org]"

        • Re: (Score:2, Informative)

          While I am no expert in the area, nor do I know a huge amount about mathematics, wikipedia says that there are:2,220,819,602,560,918,840 primes below 10^20, which is 20 digits long. Considering that the largest known prime is almost 13 million digits long,and most of these numbers are unimaginably vast, it appears that it is not trivial to find the prime factors of a number. For instance, If a computer can test 10 billion primes a second (which is more than a consumer grade computer can (I think)), then it
        • Re: (Score:3, Informative)

          It's not so hard to factor a 32-bit number with a 64-bit computer. It is very hard to efficiently factor a 2048-bit number with a 64-bit computer. Even if you had a list of all prime numbers that can be expressed in 2k or fewer bits, streaming all that data to your CPU would take a lot of bandwidth.

          • by Jeremi ( 14640 )

            It's not so hard to factor a 32-bit number with a 64-bit computer. It is very hard to efficiently factor a 2048-bit number with a 64-bit computer.

            Hmm, that raises the question... has anyone tried to build a 2048-bit computer?

            Sounds like it might be fun project for the right TLA with a multi-billion dollar budget...

            • I don't think that a 2kbit architecture would be particularly useful. Sure, it might work well for factoring large numbers, but for many other cryptography-related tasks, the lack of granularity would make it rather inefficient. If you're going to build a computer for factoring large numbers, you might as well build TWIRL [wikipedia.org].

        • by MarkusQ ( 450076 ) on Friday December 26, 2008 @07:00PM (#26237625) Journal

          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

        • Re: (Score:2, Informative)

          by akaariai ( 921081 )
          The short answer is that there is just too many primes to list. There is about x/log(x) prime numbers smaller than x. If you have a 512 bit number then you have about sqrt(2^512) / log(sqrt(2^512)) numbers to check. So, there is 1.5 * 10^75 numbers you need to list. This is simply impossible. Moore's law will not help here, as adding one bit to the number to check about doubles the search space. That is, after a year of you can check a number that is just one bit larger!
        • The primes you want are around 300 digits long. And I'm guessing that even at ultra high numbers primes occur every google or so....

        • There are an infinite number of primes. Any elementary book on number theory will have the proof of that in it.

          There's *a lot* of literature out there on how to factor integers. If you want something more readable, then look up the quadratic sieve. It's the second fastest algorithm out there. That being said, it *is* a general algorithm so its speed will likely be improved by making some modifications due to crypto using almost primes. But, that gets somewhat convoluted. Just stick to the quadratic si

    • Re:Kudos to Galois (Score:4, Interesting)

      by j1m+5n0w ( 749199 ) on Friday December 26, 2008 @04:02PM (#26236695) Homepage Journal

      Clarification:

      Cryptol, as I understand it, was developed by Galois [galois.com] (who, for some reason, is not mentioned in the summary) and not by the NSA. It would be interesting to know whether it was a joint decision between Galois and the NSA to release cryptol, or just Galois' decision alone.

      • Galois does high assurance computation for the NSA, and others. (Which is to say, the NSA expects Galois to do theorem proving on their code)

        Does anybody have any good information about Cryptol? Is it a Haskell subset/extension? Most of what I know about Galois is in relation to Haskell.

        • There's some documentation [galois.com] on Galois' web page. I looked at it once awhile back, and it seemed a lot like Haskell, but with extra syntax for doing common cryptographic operations.

          Chapter 8 of the programming guide [galois.com] has example cryptol implementations of DES, RC5, and AES.

    • Re:Kudos to NSA (Score:5, Informative)

      by collinstocks ( 1295204 ) on Friday December 26, 2008 @04:17PM (#26236741) Journal

      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.

  • really? (Score:5, Funny)

    by gclef ( 96311 ) on Friday December 26, 2008 @02:56PM (#26236391)

    So, wait, the NSA just released math?

  • Cryptol? (Score:4, Funny)

    by larry bagina ( 561269 ) on Friday December 26, 2008 @02:58PM (#26236401) Journal

    Sounds more like a drug than a programming language.

    • Re: (Score:1, Funny)

      by Anonymous Coward

      Sounds more like a drug than a programming language.

      I thought it was Superman's dog's name.

    • by jd ( 1658 )
      Kittehs hab been uzing cryptlol for yeers.
    • When I saw the name for the first time, I thought about thinkpol. Maybe I'll release a programming language that is *actually* named "thinkpol" in the future.
    • Blue flag hanging from the left side, yeah that's the Cryptol side.

  • Why the precision? (Score:2, Interesting)

    by Anonymous Coward

    Available To the Public on Friday December 26, @02:44PM

    Is there something intrinsic to cryptographic protocols that requires a timed release?

    • by Gori ( 526248 )

      Well, clearly it is. They would not have bothered otherwise...

      You would like to know the moment you booted cryptoSkyNet :)

    • by Chyeld ( 713439 )

      More to the point, wouldn't you like to know why they released it at 2:44pm instead of 2:45pm?

      What do they know that we don't?

      Who is lurking in the shadows outside your window?

      Was that thump just a wild varmit messing around outside, or...

      BOOOO!

    • by VE3MTM ( 635378 )

      Steganography?

  • Doesn't it seem probable that anything created with an NSA tool will be more reversible with other NSA tools?

    • Re: (Score:2, Insightful)

      by Anonymous Coward

      Watch out. SELinux is made by NSA.

    • As I understand it, cryptol was developed by Galois, a private company, and not by the NSA. Whether you find this reassuring or not is up to you. However, if a tool for developing cryptographic protocols were to, say, substitute a weak algorithm in place of a strong one, in many cases it would simply fail to interoperate with any reference implementation not developed using cryptol.

    • Doesn't it seem probable that anything created with an NSA tool will be more reversible with other NSA tools?

      How do you "back door" math?

  • by Animats ( 122034 ) on Friday December 26, 2008 @03:40PM (#26236603) Homepage

    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.

    • by Jeremi ( 14640 )

      Neat. There's some similarity to Matlab, and some to Renderman, and some of the syntax is borrowed from Haskell.

      Sure, but the real fun is trying to find the cleverly concealed back door so that will allow the NSA to trivially bypass any "secure" algorithm you develop. Don't look for it in the reference implementation, as that would be too obvious and easy to work around. No, it will be somewhere in the language specification itself...

      (adjusts tinfoil hat)

  • Why would they release this? Don't get me wrong, I, personally, am all for donating to the community and further advancing technology as a species; however, why would the NSA deliver something to the public that would, in the long run, possibly make life harder on themselves by possibly furthering the advances of private encryption? I'm not trying to play Devil's Advocate, I just genuinely don't understand why they would (possibly) make life harder for themselves.

    • Re: (Score:3, Funny)

      by Bazzargh ( 39195 )

      Why would they release this? Don't get me wrong, I, personally, am all for donating to the community and further advancing technology as a species; however, why would the NSA deliver something to the public that would, in the long run, possibly make life harder on themselves by possibly furthering the advances of private encryption? I'm not trying to play Devil's Advocate, I just genuinely don't understand why they would (possibly) make life harder for themselves.

      Yes, why? This is as dangerous as releasing

      • Re: (Score:1, Funny)

        by Anonymous Coward

        ... postings with fewer spelling mistakes.

        Moral: Practice what you preach.

        • He spelled "less" correctly. His was a grammar, not a spelling error. Oh, and they released this to subtly remind us that they can break (or think that they can break) any crypto out there and so don't have to worry about people using math. Hey, at least now people may be more able to use it correctly.
    • Re: (Score:2, Informative)

      by Garridan ( 597129 )

      Because building hardware & software is profitable for very many companies; and getting something certified as secure enough for the NSA is pretty hard work. If they release the toolchain, it's one less thing to worry about leaking from the developer, and they have more access to better software.

      • Ok, in that capacity it makes sense. I'm not sure why that didn't occur to me earlier. Thank you, Garridan.

      • by wkk2 ( 808881 )
        Hopefully they have a lint like process to look for known but secret deficiencies once the design is specified in this language.
    • Re:Wait... what? (Score:4, Informative)

      by bhima ( 46039 ) <Bhima,Pandava&gmail,com> on Friday December 26, 2008 @04:33PM (#26236803) Journal

      There is no such thing as trusted private encryption. Effective secure encryption is astoundingly complicated and you can not devise effective encryption in a vacuum. Lots of companies show us ineffective untrustworthy encryption which they develop in secret and which fail in short order... like CSS which is used on DVDs or the DRM in popular games and other digital media. Haven't you read folks on Slashdot mocking them for it?

      So the best way is do everything out in the open and have people find the weakness in it before it goes into production. Because once it goes into production you don't need to be code breaker to enjoy the stunning stupidity of the fools that rely on private encryption... you only need to be able to find the app with google and download it.

      Have a look at look at the ongoing contest for SHA-3. It's been reported here I think. Or you could the about how they came up with AES.

      Here's the zoo: http://ehash.iaik.tugraz.at/wiki/The_SHA-3_Zoo [tugraz.at]

      As a side note: Contests and prizes are remarkably effective method of spending the public's money for public good... as long as the results are open and patent free.

      • I actually didn't mean private in a "security through obscurity" sense, I meant in the private sector. It just seemed that in modern times, the United States government wouldn't want to give anything to the community in terms of improving security for individuals. (These were just the thoughts at the time, I can see why now... just thought I'd throw it out there)

    • Firstly, cryptol is being released by Galois, a private company, and not the NSA directly. I don't know the details of Galois' relationship with the NSA, but my understanding is that cryptol was developed by Galois, and it's quite likely that the NSA doesn't have any say in whether cryptol is released or not.

      Secondly, there are a lot of social benefits to widespread access to good cryptography. Bad security is a constant drain on the economy, in the form of stolen credit card numbers and the like.

      Thir

  • Finally! (Score:4, Funny)

    by tobiasly ( 524456 ) on Friday December 26, 2008 @03:51PM (#26236645) Homepage
    At last, we now have a programming language that implements rot13() natively! Now my website's login authentication system will really fly...
  • by burning-toast ( 925667 ) on Friday December 26, 2008 @03:52PM (#26236649)

    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

    • by Dun Malg ( 230075 ) on Friday December 26, 2008 @05:21PM (#26237065) Homepage

      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.

      • From the download page:

        This free trial version lets you explore the Cryptol language. It compiles and interprets Cryptol specifications but does not translate the specification into an implementation and only QuickCheck verification is enabled. The download includes the documentation suite and many examples.

        So, they're providing a compiler and an interpreter. It sounds like there's enough restrictions that it would be hard to use anything cryptol-derived as part of a commercial product (or even an open-sou

      • and the "full-featured" version costs money and uses a dongle or something.

        Yes, a 1048576-node supercomputer, 1 billion wire taps, and root access to the internet.

      • by deblau ( 68023 )

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

        Now there's a problem. Galois has been dead for over 175 years.

    • Considering we paid for its development with public funds, it best not be 'commercially' released.

    • So if someone used Galois to release a binary, and released the Cryptol source under the GPL, would the resulting binary be considered Free Software per the FSF's definition?
      • Yes, that program would be free but see "Free But Shackled - The Java Trap [gnu.org]" for more on why this situation is not desirable.

        • RMS is a nutter.

          • *sigh*
            I wish that I had mod points for you. :/

          • How sad that you choose to engage in name-calling instead of spelling out your apparent disagreement respectfully. Before you get into that, should you choose to explain your earlier statement, you should keep in mind the remarkable history of achievement and prescience Stallman shares with us. I don't seek perfection in anyone but I can't think of too many people who have given us all so much practical useful stuff and wisdom to think about. Specifcally, it's not every hacker who writes wildly popular l

            • I don't think nutter is a particularly harsh term. Have you heard him sing?

              Java is not a trap. Never was. Something like Java could have contributed to a world in which Linux on the desktop might have been more useful to more people. Java pre-installs on Windows fizzled because of legal issues, and on Linux fizzled because of unfounded fears.

              Now the only de-facto universal platform is web+flash. Stallman will tell you that's a trap too.

  • by Anonymous Coward

    Use Cryptol + AJAX!

  • Cryptol/Signali (Score:1, Interesting)

    by Anonymous Coward

    As someone that's worked with Cryptol, I can tell you that it is indeed a very cool language. You can generate very efficient hardware off of a Cryptol spec, prove logical equivalence between two versions of an algorithm, and play with your specification interactively from a command line. There's even a startup called Signali that's been founded to expand the usage of Cryptol to the commercial sector and algorithms other than cryptography.

  • $ root yum install libedit
    Loaded plugins: refresh-packagekit
    Setting up Install Process
    Parsing package install arguments
    Package libedit-2.11-1.20080712cvs.fc9.i386 already installed and latest version
    Nothing to do

    $ root rpm -i cryptol-academic-1.8.1-0.i386.rpm
    error: Failed dependencies:
    libedit.so is needed by cryptol-academic-1.8.1-0.i386

    $ cat /etc/issue
    Fedora release 9 (Sulphur)
    Kernel \r on an \m (\l)

    Next...

  • IANAC (I am not a cryptographer.) but wouldn't this be a useful tool for criminals and terrorists? It would seem the height of folly to give such a tool away to them ... unless there was a way of mitigating it's usefulness.

    There is no free lunch.

  • Ok, there still seems to be confusion on it being "publicly" available. This is payware with a limited trial version. The headline is about that this advanced suite (I presume, I haven't used it myself) has become available *at all*. Previously, I presume, you could not just buy it. Of course, I also presume you could freely download it from some hacking site, but that's beside the point. Law only counts for law abiding citicens.

"I'm a mean green mother from outer space" -- Audrey II, The Little Shop of Horrors

Working...