RC532/12/9 converted to 3SAT
 From: Willow <wrschlanger@xxxxxxxxx>
 Date: Fri, 10 Sep 2010 22:38:54 0700 (PDT)
I just converted the RC532/12/9 contest into a set of 3SAT problems.
To do this, I relied on these facts:
u = a ^ b ==> (u + a + b')(u + a' + b)(u' + a + b)(u' + a' + b')
u = a & b ==> (u + a' + b')(u' + a + a)(u' + b + b)
I converted the RC5 decryption algorithm to a directed acyclic graph
with only XOR and AND operators, and some terminal operands consisting
of the key bits, 0, 1, and any unknown plaintext bits.
I used two blocks of known plaintext and a third unknown block (which
is block 4 from the old RSA challenges).
Here is an excerpt from 3sat_rc5test_192_0.txt, which is 38,006,229
bytes in size:
u0 + k0' + k1'
u0' + k0' + 0
u0' + k1' + 0
u1 + k2 + 1'
....
u384972' + u384969 + u384971
u384972' + u384969' + u384971'
0 + u384972 + 1
0 + u384972' + 1'
Here is an excerpt from 3sat_rc5test_192_1.txt, which is 60,195,346
bytes in size:
u0 + k0' + k1'
u0' + k0' + 0
u0' + k1' + 0
u1 + k2 + 1'
....
u602538' + 1 + u602537
u602538' + 1' + u602537'
0 + u602536 + u602538
0 + u602536' + u602538'
The apostrophes mean "not" and + means OR. Each line is a clause that
is to be ANDed together.
kvariables are the unknown keys and uvariables are substitutions
introduced by the process of converting arbitrary graphs of AND & XOR
into 3SAT. The value of the uvariables is irrelevant to the problem,
as long as there exists some CONSTANT value, the same for each clause,
without any contradictions arising.
Using the first two known plaintext blocks, we have a relation on the
key. For the above 3SAT, I used 128 known plaintext equations as the
source, and added one more plaintext equation for which the ciphertext
for an unknown plaintext was substituted, and I plugged in 0 for that
plaintext value for the first file and 1 for that plaintext value for
the second file.
If there is only one key that decrypts the first two RC5 blocks for
which we know the plaintext, then exactly one of the two 3SAT problems
will be satisfiable. For example, if 3sat_rc5test_192_1.txt has NO
SOLUTIONS then I know plaintext bit 0 must be 0, as using a value of 1
lead to no solutions. Likewise, if 3sat_rc5test_192_0.txt has NO
SOLUTIONS then I know plaintext bit 0 must be 1 because using a value
of 0 lead to no solutions.
There is a chance that knowledge of the first 128 plaintext bits leads
to multiple keys, and that among these keys sometimes plaintext bit 0
is 0, and sometimes 1, for the unknown plaintext block. If so, then
BOTH 3sat_rc5test_192_0.txt and 3sat_rc5test_192_1.txt will be
satisfiable.

Statistics.
3sat_rc5test_192_0.txt
Number of clauses: 1,350,411
Number of unknown boolean variables: 72 + 384,972
3sat_rc5test_192_1.txt:
Number of clauses: 2,115,294
Number of unknown boolean variables: 72 + 602,538

It is very probable that one of the above two 3SATs has NO SOLUTION.
How to find out which one, and thus discover the RC5 challenge's
secret plaintext?
A similar process can be used to recover the key if 3SAT can be
solved.
At a glance, it looks like we have a MORE DIFFICULT problem than we
started with. Maybe we do.
After all we now have substantially more unknown variables. However,
it's easy to determine the internal variables (the substitutions, or u
variables) from the kvariables.
If anyone wants to take a stab at solving the above really hard 3SAT
problems, I've posted a ZIP of the above listed files here:
http://options.googlecode.com/files/rc5_3sat_test_pt0_v1.zip

Willow
.
 FollowUps:
 Re: RC532/12/9 converted to 3SAT
 From: Paul Rubin
 Re: RC532/12/9 converted to 3SAT
 Prev by Date: Re: Open Transactions: untraceable digital cash
 Next by Date: Re: Let us discuss keyexpansion and POTP
 Previous by thread: calculating ECDSA with an ECDH oracle
 Next by thread: Re: RC532/12/9 converted to 3SAT
 Index(es):
Relevant Pages
