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)

sbox_cnf.patch (7.3 KB) - added by malb 10 years ago.

Download all attachments as: .zip

Change History (10)

comment:1 follow-up: Changed 10 years ago by malb

Minh, can I ask you to review this ticket?

comment:2 in reply to: ↑ 1 Changed 10 years ago by mvngu

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 malb

Hi Minh,

the standard reference for SAT-solvers in block cipher cryptanalysis is:

http://eprint.iacr.org/2007/024

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 malb

  • Cc rpw burcin added

Hi Burcin, Ralf,

can I ask for this (hopefully) easy review?

comment:5 Changed 10 years ago by ylchapuy

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 malb

comment:6 Changed 10 years ago by malb

The attached updated patch addresses the reviewer's comments. Is that a positive review then?

comment:7 Changed 10 years ago by ylchapuy

  • 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 mvngu

  • Authors set to Martin Albrecht
  • Reviewers set to Yann Laigle-Chapuy

comment:9 Changed 10 years ago by ncalexan

  • Merged in set to 4.0.2.alpha0
  • Resolution set to fixed
  • Status changed from new to closed
Note: See TracTickets for help on using tickets.