Skip to content

Commit

Permalink
Merge pull request #272 from Crypto-TII/feature/enhance-sat-and-smt-d…
Browse files Browse the repository at this point in the history 
…ocumentation

Enhance sat and smt documentation
  • Loading branch information
@peacker
peacker authored Sep 18, 2024
2 parents 7ffe84f + e7acefc commit 622f1a8
Show file tree
Hide file tree
Showing 18 changed files with 900 additions and 396 deletions.
19 changes: 13 additions & 6 deletions claasp/components/and_component.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -334,9 +334,11 @@ def get_byte_based_vectorized_python_code(self, params):

def sat_constraints(self):
"""
Return a list of variables and a list of clauses for AND operation in SAT CIPHER model.
Return a list of variables and a list of clauses representing AND for SAT CIPHER model
This method support AND operation using more than two operands.
This method translates in CNF the constraint ``z = And(x, y)``. In prefixed notation, it becomes:
``And(Or(x, Not(z)), Or(y, Not(z)), Or(z, Not(x), Not(y)))``.
This method supports AND operation using more than two inputs.
.. SEEALSO::
Expand All @@ -354,9 +356,12 @@ def sat_constraints(self):
sage: and_component.sat_constraints()
(['and_0_8_0',
'and_0_8_1',
'and_0_8_2',
...
'-and_0_8_11 xor_0_7_11',
'and_0_8_10',
'and_0_8_11'],
['-and_0_8_0 xor_0_7_0',
'-and_0_8_0 key_12',
...
'-and_0_8_11 key_23',
'and_0_8_11 -xor_0_7_11 -key_23'])
"""
Expand All @@ -370,9 +375,11 @@ def sat_constraints(self):

def smt_constraints(self):
"""
Return a variable list and SMT-LIB list asserts representing AND operation FOR SMT CIPHER model.
Return a variable list and SMT-LIB list asserts representing AND for SMT CIPHER model
This method support AND operation using more than two operands.
Since the AND operation is part of the SMT-LIB formalism, the operation can be modeled using the corresponding
builtin operation, e.g. ``z = And(x, y)`` becomes ``(assert (= z (and x y)))``.
This method support AND operation using more than two inputs.
INPUT:
Expand Down
88 changes: 74 additions & 14 deletions claasp/components/cipher_output_component.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -452,7 +452,7 @@ def minizinc_xor_differential_propagation_constraints(self, model):

def sat_constraints(self):
"""
Return a list of variables and a list of clauses for OUTPUT in SAT CIPHER model.
Return a list of variables and a list of clauses representing CIPHER OUTPUT for SAT CIPHER model
.. SEEALSO::
Expand All @@ -470,9 +470,12 @@ def sat_constraints(self):
sage: output_component.sat_constraints()
(['cipher_output_2_12_0',
'cipher_output_2_12_1',
'cipher_output_2_12_2',
...
'xor_2_10_14 -cipher_output_2_12_30',
'cipher_output_2_12_30',
'cipher_output_2_12_31'],
['cipher_output_2_12_0 -xor_2_8_0',
'xor_2_8_0 -cipher_output_2_12_0',
...
'cipher_output_2_12_31 -xor_2_10_15',
'xor_2_10_15 -cipher_output_2_12_31'])
"""
Expand All @@ -486,8 +489,7 @@ def sat_constraints(self):

def sat_bitwise_deterministic_truncated_xor_differential_constraints(self):
"""
Return a list of variables and a list of clauses for OUTPUT in SAT
DETERMINISTIC TRUNCATED XOR DIFFERENTIAL model.
Return a list of variables and a list of clauses representing CIPHER OUTPUT for SAT DETERMINISTIC TRUNCATED XOR DIFFERENTIAL model
.. SEEALSO::
Expand All @@ -505,9 +507,12 @@ def sat_bitwise_deterministic_truncated_xor_differential_constraints(self):
sage: output_component.sat_bitwise_deterministic_truncated_xor_differential_constraints()
(['cipher_output_2_12_0_0',
'cipher_output_2_12_1_0',
'cipher_output_2_12_2_0',
...
'xor_2_10_14_1 -cipher_output_2_12_30_1',
'cipher_output_2_12_30_1',
'cipher_output_2_12_31_1'],
['cipher_output_2_12_0_0 -xor_2_8_0_0',
'xor_2_8_0_0 -cipher_output_2_12_0_0',
...
'cipher_output_2_12_31_1 -xor_2_10_15_1',
'xor_2_10_15_1 -cipher_output_2_12_31_1'])
"""
Expand All @@ -521,12 +526,40 @@ def sat_bitwise_deterministic_truncated_xor_differential_constraints(self):

return out_ids_0 + out_ids_1, constraints

def sat_xor_differential_propagation_constraints(self, model):
def sat_xor_differential_propagation_constraints(self, model=None):
"""
Return a list of variables and a list of clauses representing CIPHER OUTPUT for SAT XOR DIFFERENTIAL model
.. SEEALSO::
:ref:`sat-standard` for the format.
INPUT:
- None
EXAMPLES::
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=3)
sage: output_component = speck.component_from(2, 12)
sage: output_component.sat_xor_differential_propagation_constraints()
(['cipher_output_2_12_0',
'cipher_output_2_12_1',
...
'cipher_output_2_12_30',
'cipher_output_2_12_31'],
['cipher_output_2_12_0 -xor_2_8_0',
'xor_2_8_0 -cipher_output_2_12_0',
...
'cipher_output_2_12_31 -xor_2_10_15',
'xor_2_10_15 -cipher_output_2_12_31'])
"""
return self.sat_constraints()

def sat_xor_linear_mask_propagation_constraints(self, model=None):
"""
Return a list of variables and a list of clauses for OUTPUT in SAT XOR LINEAR model.
Return a list of variables and a list of clauses representing CIPHER OUTPUT for SAT XOR LINEAR model
.. SEEALSO::
Expand All @@ -544,9 +577,12 @@ def sat_xor_linear_mask_propagation_constraints(self, model=None):
sage: output_component.sat_xor_linear_mask_propagation_constraints()
(['cipher_output_2_12_0_i',
'cipher_output_2_12_1_i',
'cipher_output_2_12_2_i',
...
'cipher_output_2_12_30_o -cipher_output_2_12_30_i',
'cipher_output_2_12_30_o',
'cipher_output_2_12_31_o'],
['cipher_output_2_12_0_i -cipher_output_2_12_0_o',
'cipher_output_2_12_0_o -cipher_output_2_12_0_i',
...
'cipher_output_2_12_31_i -cipher_output_2_12_31_o',
'cipher_output_2_12_31_o -cipher_output_2_12_31_i'])
"""
Expand All @@ -561,7 +597,7 @@ def sat_xor_linear_mask_propagation_constraints(self, model=None):

def smt_constraints(self):
"""
Return a variable list and SMT-LIB list asserts representing OUTPUT for SMT CIPHER constraints.
Return a variable list and SMT-LIB list asserts representing CIPHER OUTPUT for SMT CIPHER model
INPUT:
Expand Down Expand Up @@ -593,12 +629,36 @@ def smt_constraints(self):

return output_bit_ids, constraints

def smt_xor_differential_propagation_constraints(self, model):
def smt_xor_differential_propagation_constraints(self, model=None):
"""
Return a variable list and SMT-LIB list asserts representing CIPHER OUTPUT for SMT XOR DIFFERENTIAL model
INPUT:
- None
EXAMPLES::
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=3)
sage: output_component = speck.component_from(2, 12)
sage: output_component.smt_xor_differential_propagation_constraints()
(['cipher_output_2_12_0',
'cipher_output_2_12_1',
...
'cipher_output_2_12_30',
'cipher_output_2_12_31'],
['(assert (= cipher_output_2_12_0 xor_2_8_0))',
'(assert (= cipher_output_2_12_1 xor_2_8_1))',
...
'(assert (= cipher_output_2_12_30 xor_2_10_14))',
'(assert (= cipher_output_2_12_31 xor_2_10_15))'])
"""
return self.smt_constraints()

def smt_xor_linear_mask_propagation_constraints(self, model=None):
"""
Return a variable list and SMT-LIB list asserts for OUTPUT in SMT XOR LINEAR model.
Return a variable list and SMT-LIB list asserts representing CIPHER OUTPUT for SMT XOR LINEAR model
INPUT:
Expand Down
53 changes: 39 additions & 14 deletions claasp/components/constant_component.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -519,7 +519,9 @@ def minizinc_xor_differential_propagation_constraints(self, model):

def sat_constraints(self):
"""
Return a list of variables and a list of clauses for a CONSTANT in SAT CIPHER model.
Return a list of variables and a list of clauses representing CONSTANT for SAT CIPHER model
The list of the constraints is just the binary representation of the value of the constant.
.. SEEALSO::
Expand All @@ -537,9 +539,12 @@ def sat_constraints(self):
sage: constant_component.sat_constraints()
(['constant_2_0_0',
'constant_2_0_1',
'constant_2_0_2',
...
'-constant_2_0_13',
'constant_2_0_14',
'constant_2_0_15'],
['-constant_2_0_0',
'-constant_2_0_1',
...
'-constant_2_0_14',
'constant_2_0_15'])
"""
Expand All @@ -553,8 +558,11 @@ def sat_constraints(self):

def sat_bitwise_deterministic_truncated_xor_differential_constraints(self):
"""
Return a list of variables and a list of clauses for CONSTANT in SAT
DETERMINISTIC TRUNCATED XOR DIFFERENTIAL model.
Return a list of variables and a list of clauses representing CONSTANT for SAT DETERMINISTIC TRUNCATED XOR DIFFERENTIAL model
The list of the constraints is just the binary representation of the value of the constant.
Note that encoding symbols for deterministic truncated XOR differential model
requires two variables per each symbol.
.. SEEALSO::
Expand All @@ -572,9 +580,12 @@ def sat_bitwise_deterministic_truncated_xor_differential_constraints(self):
sage: constant_component.sat_bitwise_deterministic_truncated_xor_differential_constraints()
(['constant_2_0_0_0',
'constant_2_0_1_0',
'constant_2_0_2_0',
...
'-constant_2_0_13_1',
'constant_2_0_14_1',
'constant_2_0_15_1'],
['-constant_2_0_0_0',
'-constant_2_0_1_0',
...
'-constant_2_0_14_1',
'-constant_2_0_15_1'])
"""
Expand All @@ -584,7 +595,9 @@ def sat_bitwise_deterministic_truncated_xor_differential_constraints(self):

def sat_xor_differential_propagation_constraints(self, model=None):
"""
Return lists of variables and strings representing clauses for CONSTANT for SAT xor differential.
Return a list of variables and a list of clauses representing CONSTANT for SAT XOR DIFFERENTIAL model
The value encoded is always zero for any constant since its contribute to the difference is null.
.. SEEALSO::
Expand All @@ -602,9 +615,12 @@ def sat_xor_differential_propagation_constraints(self, model=None):
sage: constant_component.sat_xor_differential_propagation_constraints()
(['constant_2_0_0',
'constant_2_0_1',
'constant_2_0_2',
...
'-constant_2_0_13',
'constant_2_0_14',
'constant_2_0_15'],
['-constant_2_0_0',
'-constant_2_0_1',
...
'-constant_2_0_14',
'-constant_2_0_15'])
"""
Expand All @@ -615,7 +631,9 @@ def sat_xor_differential_propagation_constraints(self, model=None):

def sat_xor_linear_mask_propagation_constraints(self, model=None):
"""
Return a list of variables and a list of clauses for a CONSTANT in SAT XOR LINEAR model.
Return a list of variables and a list of clauses representing CONSTANT for SAT XOR LINEAR model
The list of the clauses is empty since in XOR linear analysis any constant flip the sign if needed.
.. SEEALSO::
Expand Down Expand Up @@ -646,7 +664,9 @@ def sat_xor_linear_mask_propagation_constraints(self, model=None):

def smt_constraints(self):
"""
Return a variable list and SMT-LIB list asserts representing a CONSTANT SMT CIPHER model.
Return a variable list and SMT-LIB list asserts representing CONSTANT for SMT CIPHER model
The list of the constraints is just the binary representation of the value of the constant.
INPUT:
Expand Down Expand Up @@ -679,7 +699,9 @@ def smt_constraints(self):

def smt_xor_differential_propagation_constraints(self, model=None):
"""
Return a variable list and SMT-LIB list asserts representing a CONSTANT for SMT xor differential.
Return a variable list and SMT-LIB list asserts representing CONSTANT for SMT XOR DIFFERENTIAL model
The value encoded is always zero for any constant since its contribute to the difference is null.
INPUT:
Expand Down Expand Up @@ -710,7 +732,9 @@ def smt_xor_differential_propagation_constraints(self, model=None):

def smt_xor_linear_mask_propagation_constraints(self, model=None):
"""
Return a variable list and SMT-LIB list asserts for a CONSTANT in SMT XOR LINEAR model.
Return a variable list and SMT-LIB list asserts representing CONSTANT for SMT XOR LINEAR model
The list of the clauses is empty since in XOR linear analysis any constant flip the sign if needed.
INPUT:
Expand All @@ -724,6 +748,7 @@ def smt_xor_linear_mask_propagation_constraints(self, model=None):
sage: constant_component.smt_xor_linear_mask_propagation_constraints()
(['constant_0_2_0_o',
'constant_0_2_1_o',
'constant_0_2_2_o',
...
'constant_0_2_30_o',
'constant_0_2_31_o'],
Expand Down
Loading

0 comments on commit 622f1a8

Please sign in to comment.