Cryptol, Language of Cryptography, Now Available To the Public

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.

Using an NSA tool..

[TechForensics]

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

Re:Using an NSA tool..

[Anonymous Coward]

Watch out. SELinux is made by NSA.

Lack of Functionality

[burning-toast]

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

Can Cryptol programs be Free Software?

[Krishnoid]

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?

Re:Kudos to NSA

[Chyeld]

Start with a small set to see the logic if you need to.

Say just (2, 3, and 5). All prime numbers.

Now the product of 2, 3, and 5 is 30. Add 1 to this and you get 31.

31 is not divisable by 2. The closest you can get to 31 in mulitples of two is 30 (which is 3 times 5 times... you guessed it 2.) and you have 1 left over.

31 is not divisable by 3. It's the same as 2. The closest you get is 30 (2 times 5 times... 3!) and you have 1 left over.

The same goes for 5. Because you are adding 1 to the product of all three, you can't divide into the result cleanly.

This is going to be the same for any group of prime numbers you pick. By adding 1 to their product, the result can't be broken down cleanly as a product of those numbers. You'll always be 1 away (because you actually took their product and added 1).

Now the definition of a prime number is a number that can only be cleanly divided by two numbers. Itself and 1. Every other number has more possible divisors. As a result of this, every number out there is either a prime, because you can't divide something into it, or a product of primes.

31 therefore is either a prime number itself, or it can be broken down into a product of prime numbers.

But we've shown that the prime numbers in our list can't be the primes that do that, since none of them can divide into our result cleanly.

That means, by default, our group of numbers can't contain all the prime numbers. Either they are missing our result (and btw, 31 is a prime) or they are missing the prime factors of our result. And since this works for any group of prime numbers you can put together, effectively you've just proven that the actual set of prime numbers itself is infinite.