Opened 10 years ago
Closed 10 years ago
#6185 closed enhancement (fixed)
[with patch, positive review] Add SBox -> CNF Conversion
Reported by: | malb | Owned by: | malb |
---|---|---|---|
Priority: | major | Milestone: | sage-4.0.2 |
Component: | cryptography | Keywords: | crypto, cnf |
Cc: | mvngu, rpw, burcin | Merged in: | 4.0.2.alpha0 |
Authors: | Martin Albrecht | Reviewers: | Yann Laigle-Chapuy |
Report Upstream: | 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 10 years ago by
comment:2 in reply to: ↑ 1 Changed 10 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 10 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 10 years ago by
- Cc rpw burcin added
Hi Burcin, Ralf,
can I ask for this (hopefully) easy review?
comment:5 Changed 10 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 10 years ago by
comment:6 Changed 10 years ago by
The attached updated patch addresses the reviewer's comments. Is that a positive review then?
comment:7 Changed 10 years ago by
- Summary changed from [with patch, needs review] Add SBox -> CNF Conversion to [with patch, positive review] Add SBox -> CNF Conversion
Yes it is. Positive review.
comment:8 Changed 10 years ago by
- Reviewers set to Yann Laigle-Chapuy
comment:9 Changed 10 years ago by
- Merged in set to 4.0.2.alpha0
- Resolution set to fixed
- Status changed from new to closed
Minh, can I ask you to review this ticket?