rucpbase_issue

[MGwynne]

Branch: rucpbase_issue.

Adding todos on checking that all computed AES 1-bases are actually 1-bases.

Matthew

[OKullmann]

In Sbox_8.hpp you wrote:

• The current "best 1-base" with 4398 clauses is not a 1-base!

But for this assertion you do not give any justification.
Some actions are done then, with only one output:

+maxima> hardness_wpi_cs(setify(Sbox_1base[2]),setify(Sbox_PI[2]));
+2

So we have hardness 2, but nothing about whether the boolean function is the SBox or not!

It is continued with a comment

• However, far more prime implicates follow by UCP for the "current 1-base"
• than for the current best minimum representation, which may help to
• explain any differences in the performance of SAT solvers:

which is completely unclear to me: To what does the "However" refer to?
What is to be explained??

[MGwynne]

Hi,

Sorry for the late reply, I don't check this e-mail address (360678@swan.ac.uk) much any more as there is a lot of university spam.

On 4 Nov 2012, at 12:45, Oliver Kullmann wrote:

In Sbox_8.hpp you wrote:

The current "best 1-base" with 4398 clauses is not a 1-base!
But for this assertion you do not give any justification.
Some actions are done then, with only one output:

+maxima> hardness_wpi_cs(setify(Sbox_1base[2]),setify(Sbox_PI[2]));
+2

So we have hardness 2, but nothing about whether the boolean function is the SBox or not!

I will rerun the various necessary tests to also check that it is an S-box and send over the instructions and data.

It is continued with a comment

However, far more prime implicates follow by UCP for the "current 1-base"
than for the current best minimum representation, which may help to
explain any differences in the performance of SAT solvers:
which is completely unclear to me: To what does the "However" refer to?
What is to be explained??

Call the minimum translation Sbox_min and the "1-base" (not a 1-base) Sbox_1base.

The intention was to convey that the number of prime implicates C for the Sbox for which phi_C * Sbox_1base has hardness 1 is more than the number for which phi_C * Sbox_min has hardness 1. Of course this requires evidence, and is also insufficient, we want data on whether the set of prime implicates which have hardness 1 for Sbox_1base completely subsumes that for Sbox_min, or whether Sbox_min is till 1-soft for some prime implicates that Sbox_1base isn't.

As with the hardness check, I will rerun the appropriate tests in Maxima and send you the commands, information and data.

Should I update a branch of the OKlibrary with the information I produce and make a pull request?

Matthew