Skip to content

rucpbase_issue #424

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
MGwynne wants to merge 2 commits into
base: master
Choose a base branch
from
Open

rucpbase_issue #424

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
ec5296d
Adding todos on checking that all computed AES 1-bases are actually 1…
MGwynne Jun 15, 2012
72c2882
The current "1-base" for 8-bit AES Sbox isn't an S-box.
MGwynne Jun 22, 2012
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 4 additions & 1 deletion ...on/Investigations/Cryptography/AdvancedEncryptionStandard/plans/Representations/Inv_8.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
// Matthew Gwynne, 12.1.2011 (Swansea)
/* Copyright 2011 Oliver Kullmann
/* Copyright 2011, 2012 Oliver Kullmann
This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
it and/or modify it under the terms of the GNU General Public License as published by
the Free Software Foundation and included in this library; either version 3 of the
Expand Down Expand Up @@ -148,6 +148,9 @@ R> subset(E, min == 359)

\todo r_1-bases : mincl_r1 <= 4200
<ul>
<li> The 1-bases below need to be checked to ensure they are actually
1-bases; see "Computing r_1-bases for a set of prime implicates" in
Satisfiability/Reductions/Bases/plans/UcpBase.hpp. </li>
<li> Current minimum clause-count of an r_1-base: 4200. </li>
<li> Iterating through the random seeds, while sorting inputs in
ascending order of clause-length into RUcpGen, and descending into
Expand Down
5 changes: 4 additions & 1 deletion ...Investigations/Cryptography/AdvancedEncryptionStandard/plans/Representations/Mul_11_8.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
// Matthew Gwynne, 7.1.2011 (Swansea)
/* Copyright 2011 Oliver Kullmann
/* Copyright 2011, 2012 Oliver Kullmann
This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
it and/or modify it under the terms of the GNU General Public License as published by
the Free Software Foundation and included in this library; either version 3 of the
Expand Down Expand Up @@ -53,6 +53,9 @@ c's = 1, n = 16, c = 15008, tc = 0, ntc = 15008, tl = 119824, l = 119824, finish

\todo r_1-bases : mincl_r1 <= 1376
<ul>
<li> The 1-bases below need to be checked to ensure they are actually
1-bases; see "Computing r_1-bases for a set of prime implicates" in
Satisfiability/Reductions/Bases/plans/UcpBase.hpp. </li>
<li> Computing an r_1-base:
\verbatim
shell> QuineMcCluskey-n16-O3-DNDEBUG AES_byte_field_mul_full_11.cnf > AES_byte_field_mul_pi_11.cnf
Expand Down
5 changes: 4 additions & 1 deletion ...Investigations/Cryptography/AdvancedEncryptionStandard/plans/Representations/Mul_13_8.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
// Matthew Gwynne, 7.1.2011 (Swansea)
/* Copyright 2011 Oliver Kullmann
/* Copyright 2011, 2012 Oliver Kullmann
This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
it and/or modify it under the terms of the GNU General Public License as published by
the Free Software Foundation and included in this library; either version 3 of the
Expand Down Expand Up @@ -53,6 +53,9 @@ c's = 1, n = 16, c = 15312, tc = 0, ntc = 15312, tl = 122816, l = 122816, finish

\todo r_1-bases : mincl_r1 <= 1040
<ul>
<li> The 1-bases below need to be checked to ensure they are actually
1-bases; see "Computing r_1-bases for a set of prime implicates" in
Satisfiability/Reductions/Bases/plans/UcpBase.hpp. </li>
<li> Computing an r_1-base:
\verbatim
shell> QuineMcCluskey-n16-O3-DNDEBUG AES_byte_field_mul_full_13.cnf > AES_byte_field_mul_pi_13.cnf
Expand Down
5 changes: 4 additions & 1 deletion ...Investigations/Cryptography/AdvancedEncryptionStandard/plans/Representations/Mul_14_8.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
// Matthew Gwynne, 7.1.2011 (Swansea)
/* Copyright 2011 Oliver Kullmann
/* Copyright 2011, 2012 Oliver Kullmann
This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
it and/or modify it under the terms of the GNU General Public License as published by
the Free Software Foundation and included in this library; either version 3 of the
Expand Down Expand Up @@ -55,6 +55,9 @@ c's = 1, n = 16, c = 14300, tc = 0, ntc = 14300, tl = 114252, l = 114252, finish

\todo r_1-bases : mincl_r1 <= 1052
<ul>
<li> The 1-bases below need to be checked to ensure they are actually
1-bases; see "Computing r_1-bases for a set of prime implicates" in
Satisfiability/Reductions/Bases/plans/UcpBase.hpp. </li>
<li> Computing an r_1-base:
\verbatim
shell> QuineMcCluskey-n16-O3-DNDEBUG AES_byte_field_mul_full_14.cnf > AES_byte_field_mul_pi_14.cnf
Expand Down
5 changes: 4 additions & 1 deletion .../Investigations/Cryptography/AdvancedEncryptionStandard/plans/Representations/Mul_2_8.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
// Matthew Gwynne, 7.1.2011 (Swansea)
/* Copyright 2011 Oliver Kullmann
/* Copyright 2011, 2012 Oliver Kullmann
This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
it and/or modify it under the terms of the GNU General Public License as published by
the Free Software Foundation and included in this library; either version 3 of the
Expand Down Expand Up @@ -89,6 +89,9 @@ maxima> Mul2_min_F_hd_l : setify(create_list(hardness_wpi_cs(setify(Mul2_min_F_l

\todo r_1-bases : mincl_r1 <= 22
<ul>
<li> The 1-bases below need to be checked to ensure they are actually
1-bases; see "Computing r_1-bases for a set of prime implicates" in
Satisfiability/Reductions/Bases/plans/UcpBase.hpp. </li>
<li> Current minimum clause-count of an r_1-base: 22. </li>
<li> For the mincl_rinf representations, see "Minimising using hypergraph
transversal tools". </li>
Expand Down
5 changes: 4 additions & 1 deletion .../Investigations/Cryptography/AdvancedEncryptionStandard/plans/Representations/Mul_3_8.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
// Matthew Gwynne, 7.1.2011 (Swansea)
/* Copyright 2011 Oliver Kullmann
/* Copyright 2011, 2012 Oliver Kullmann
This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
it and/or modify it under the terms of the GNU General Public License as published by
the Free Software Foundation and included in this library; either version 3 of the
Expand Down Expand Up @@ -103,6 +103,9 @@ maxima> hardness_wpi_cs(setify(ev_hm(ss_field_cnfs,[8,3])[2]),Mul3_F_primes[2]);

\todo r_1-bases : mincl_r1 <= 80
<ul>
<li> The 1-bases below need to be checked to ensure they are actually
1-bases; see "Computing r_1-bases for a set of prime implicates" in
Satisfiability/Reductions/Bases/plans/UcpBase.hpp. </li>
<li> Computing three r_1-bases:
\verbatim
> seed=1; RandomShuffleDimacs-O3-DNDEBUG ${seed} < AES_byte_field_mul_pi_3.cnf | RUcpBase-O3-DNDEBUG | tee AES_byte_field_mul_bases_${seed}.cnf | ExtendedDimacsFullStatistics-O3-DNDEBUG
Expand Down
5 changes: 4 additions & 1 deletion .../Investigations/Cryptography/AdvancedEncryptionStandard/plans/Representations/Mul_9_8.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
// Matthew Gwynne, 7.1.2011 (Swansea)
/* Copyright 2011 Oliver Kullmann
/* Copyright 2011, 2012 Oliver Kullmann
This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
it and/or modify it under the terms of the GNU General Public License as published by
the Free Software Foundation and included in this library; either version 3 of the
Expand Down Expand Up @@ -54,6 +54,9 @@ c's = 1, n = 16, c = 7840, tc = 0, ntc = 7840, tl = 60352, l = 60352, finished =

\todo r_1-bases : mincl_r1 <= 272
<ul>
<li> The 1-bases below need to be checked to ensure they are actually
1-bases; see "Computing r_1-bases for a set of prime implicates" in
Satisfiability/Reductions/Bases/plans/UcpBase.hpp. </li>
<li> Computing an r_1-base:
\verbatim
shell> QuineMcCluskey-n16-O3-DNDEBUG AES_byte_field_mul_full_9.cnf > AES_byte_field_mul_pi_9.cnf
Expand Down
3 changes: 3 additions & 0 deletions ...gations/Cryptography/AdvancedEncryptionStandard/plans/Representations/RoundColumn_2_4.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -151,6 +151,9 @@ maxima> output_fcs("16-bit AES Round",bf2relation_fullcnf_fcs(lambda([V],ss_roun

\todo r_1-bases : mincl_r1 <= 2712
<ul>
<li> The 1-bases below need to be checked to ensure they are actually
1-bases; see "Computing r_1-bases for a set of prime implicates" in
Satisfiability/Reductions/Bases/plans/UcpBase.hpp. </li>
<li> We can compute r_1-base statistics by:
\verbatim
shell> RandomRUcpBases round_column_16_full.cnf
Expand Down
35 changes: 33 additions & 2 deletions ...n/Investigations/Cryptography/AdvancedEncryptionStandard/plans/Representations/Sbox_8.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -302,9 +302,40 @@ Error: Impossible to solve the PI chart (too many possible combinations).
</ul>


\todo r_1-bases : mincl_r1 <= 4398
\todo r_1-bases : mincl_r1 <= ????
<ul>
<li> Current minimum clause-count of an r_1-base: 4398. </li>
<li> The 1-bases below need to be checked to ensure they are actually
1-bases; see "Computing r_1-bases for a set of prime implicates" in
Satisfiability/Reductions/Bases/plans/UcpBase.hpp. </li>
<li> The current "best 1-base" with 4398 clauses is not a 1-base!
\verbatim
maxima> output_rijnsbox_fullcnf_stdname();
shell> QuineMcCluskey-n16-O3-DNDEBUG AES_Sbox_full.cnf > AES_Sbox_PI.cnf
shell> cat AES_Sbox_PI.cnf | RandomShuffleDimacs-O3-DNDEBUG 103 | SortByClauseLength-O3-DNDEBUG > AES_Sbox_PI_randsort_103.cnf
shell> RUcpGen-O3-DNDEBUG AES_Sbox_PI_randsort_103.cnf > AES_Sbox_gen_103.cnf
shell> cat AES_Sbox_gen_103.cnf | RandomShuffleDimacs-O3-DNDEBUG 1 | SortByClauseLengthDescending-O3-DNDEBUG | RUcpBase-O3-DNDEBUG > AES_Sbox_base_gs103_bs1.cnf
maxima> Sbox_1base : read_fcl_f("AES_Sbox_base_gs103_bs1.cnf")$
maxima> Sbox_PI : read_fcl_f("AES_Sbox_PI.cnf")$
maxima> hardness_wpi_cs(setify(Sbox_1base[2]),setify(Sbox_PI[2]));
2
\endverbatim
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:
\verbatim
ksoft_primes_cs(F,F_PI,k) :=
subset(map(comp_sl,F_PI),
lambda([C], is(hardness_wpi_cs(apply_pa_cs(C, F),{{}}) <= k)))$
Sbox_1base_1soft_primes : ksoft_primes_cs(setify(Sbox_1base[2]),setify(Sbox_PI[2]),1)$
print(length(Sbox_1base_1soft_primes), "/", length(Sbox_PI[2]));
132025 / 136253

Sbox_min_1soft_primes : ksoft_primes_cs(setify(ev_hm(ss_sbox_cnfs,8)[2]),setify(Sbox_PI[2]),1)$
print(length(Sbox_min_1soft_primes),"/", length(Sbox_PI[2]));
3474 / 136253
\endverbatim
</li>
<li> Current minimum clause-count of an r_1-base: ???. </li>
<li> Starting with a generating set, created from scratch:
\verbatim
> RUcpGen-O3-DNDEBUG AES_PK.cnf > AES_gen.cnf
Expand Down