Opened 14 years ago

Closed 14 years ago

# [with patch, positive review] Add SBox -> CNF Conversion

Reported by: Owned by: malb malb major sage-4.0.2 cryptography crypto, cnf mvngu, rpw, burcin 4.0.2.alpha0 Martin Albrecht Yann Laigle-Chapuy N/A

### 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.

### comment:1 follow-up:  2 Changed 14 years ago by malb

Minh, can I ask you to review this ticket?

### comment:2 in reply to:  1 Changed 14 years ago by mvngu

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 14 years ago by malb

Hi Minh,

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

I've implemented a converter along those lines at

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 14 years ago by malb

Hi Burcin, Ralf,

can I ask for this (hopefully) easy review?

### comment:5 Changed 14 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.

### comment:6 Changed 14 years ago by malb

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

### comment:7 Changed 14 years ago by ylchapuy

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 14 years ago by mvngu

Authors: → Martin Albrecht → Yann Laigle-Chapuy

### comment:9 Changed 14 years ago by ncalexan

Merged in: → 4.0.2.alpha0 → fixed new → closed
Note: See TracTickets for help on using tickets.