Opened 13 years ago
Closed 13 years ago
#6185 closed enhancement (fixed)
[with patch, positive review] Add SBox -> CNF Conversion
Reported by: | Martin Albrecht | Owned by: | Martin Albrecht |
---|---|---|---|
Priority: | major | Milestone: | sage-4.0.2 |
Component: | cryptography | Keywords: | crypto, cnf |
Cc: | Minh Van Nguyen, rpw, Burcin Erocal | Merged in: | 4.0.2.alpha0 |
Authors: | Martin Albrecht | Reviewers: | Yann Laigle-Chapuy |
Report Upstream: | N/A | Work issues: | |
Branch: | Commit: | ||
Dependencies: | Stopgaps: |
Description
While not really complicated it is nice to have a direct conversion from S-Boxes to CNF since SAT-solves enjoy some attention right now in crypto.
Attachments (1)
Change History (10)
comment:1 follow-up: 2 Changed 13 years ago by
comment:2 Changed 13 years ago by
Replying to malb:
Minh, can I ask you to review this ticket?
Hi Martin. Sorry for my simple question: Is there a reference or paper that describes the algorithm you use for converting an S-box to CNF? I only know about the application of SAT to cryptanalysis by reading this ticket. I usually find it much easier to understand code if I can access a reference somewhere that describes the algorithm.
comment:3 Changed 13 years ago by
Hi Minh,
the standard reference for SAT-solvers in block cipher cryptanalysis is:
I've implemented a converter along those lines at
http://bitbucket.org/malb/algebraic_attacks/src/tip/anf2cnf.py
which isn't ready for inclusion yet. This ticket follows a different approach and converts the S-Box directly. The algorithm used is the standard algorithm for computing CNF from a truth table,
cf.
sage.sage.logic.boolformula
comment:4 Changed 13 years ago by
Cc: | rpw Burcin Erocal added |
---|
Hi Burcin, Ralf,
can I ask for this (hopefully) easy review?
comment:5 Changed 13 years ago by
My 2 cents:
- the complexity is 'n * 2m' (instead of 'm * 2n'):
for x in X: <-- 2^m for output_bit in output_bits: <-- n
- typos:
- line 866: evaluate instead of evaulate
- line 840: endianness instead of endianess
- maybe add an exception if xi or yi has wrong size
- maybe (but as you like) construct x's on the fly:
for e in xrange(2**m): x = self.to_bits(e)
otherwise seems good to me.
Changed 13 years ago by
Attachment: | sbox_cnf.patch added |
---|
comment:6 Changed 13 years ago by
The attached updated patch addresses the reviewer's comments. Is that a positive review then?
comment:7 Changed 13 years ago by
Summary: | [with patch, needs review] Add SBox -> CNF Conversion → [with patch, positive review] Add SBox -> CNF Conversion |
---|
Yes it is. Positive review.
comment:8 Changed 13 years ago by
Authors: | → Martin Albrecht |
---|---|
Reviewers: | → Yann Laigle-Chapuy |
comment:9 Changed 13 years ago by
Merged in: | → 4.0.2.alpha0 |
---|---|
Resolution: | → fixed |
Status: | new → closed |
Minh, can I ask you to review this ticket?