Skip to content

GitLab

Commit 399c5be6 authored by Luc Libralesso's avatar Luc Libralesso
Browse files

update writers

parent 90747200
Hide whitespace changes
Inline Side-by-side
cryptosystems/aes/aes128.rb
View file @ 399c5be6
......@@ -3,133 +3,69 @@
require_relative './constants.rb'
require_relative '../../cryptodag.rb'
require_relative '../../simulate_cryptodag.rb'
require_relative '../../cryptonodes/input.rb'
require_relative '../../cryptonodes/constant.rb'
require_relative '../../cryptonodes/output.rb'
require_relative '../../cryptonodes/keyseparation.rb'
require_relative '../../cryptonodes/xor.rb'
require_relative '../../cryptonodes/subcell.rb'
require_relative '../../cryptonodes/shufflecell.rb'
require_relative '../../cryptonodes/mixcolumn.rb'
require_relative '../../nodes/input.rb'
require_relative '../../nodes/xor.rb'
require_relative '../../nodes/subbytes.rb'
require_relative '../../nodes/shiftrows.rb'
require_relative '../../nodes/mixcolumn.rb'
require_relative '../../nodes/aeskeyschedule.rb'
# implements the AES key schedule
class AESKeyScheduleNode < CryptoDagNode
# implements the AES 128 DAG
class AES128_Dag < CryptoDag
def initialize(input, name, rcon)
def initialize(nb_rounds=10)
# prepare constants
@rcon = rcon
super(x:input.x, y:input.y, inputs:[input], name:name)
end
def compute_call()
input = @inputs[0].compute()
return expand_key(input)
return res
end
def expand_key(input)
res = Array.new(input.length()) { |i| Array.new(input[0].length()) { |j| 0 } }
# FIRST RES COLUMN
# take the last column of the input and rotate it (first becomes last)
4.times do |i|
res[0][i] = input[3][(i+1)%4]
end
# applies a S-box
4.times do |i|
res[0][i] = subcell_function(0, i, res[0][i])
end
# xor result + first column of input + Rcon(4)
4.times do |i|
res[0][i] = res[0][i] ^ input[0][i]
end
res[0][0] = res[0][0] ^ @rcon
# SECOND RES COLUMN
# xor second input column + first res column
# THIRD RES COLUMN
# xor third input column + second res column
# LAST RES COLUMN
# xor last input column + third res column
3.times do |j|
4.times do |i|
res[j+1][i] = input[j+1][i] ^ res[j][i]
@mc = mixcolumns_matrix()
@sbox = s_box()
# define input nodes
nodes = []
@nb_rounds = nb_rounds
@x = InputNode.new(name:"X", dimensions:[4,4])
nodes.push(@x)
@k = InputNode.new(name:"K", dimensions:[4,4])
nodes.push(@k)
#define internal nodes
addkey = XorNode.new(name:"ARK_0", inputs:[@x.outputs[0],@k.outputs[0]])
nodes.push(addkey)
kprev = @k
for i in 1..nb_rounds do
ki = AESKeyScheduleNode.new(name:"K_#{i}", input:kprev.outputs[0], subtable:@sbox, rcon:@rcon[i])
nodes.push(ki)
kprev = ki
subbytes = SubBytesNode.new(name:"SB_#{i}", input:addkey.outputs[0], subtable:@sbox)
nodes.push(subbytes)
shiftrows = ShiftRowsNode.new(name:"SR_#{i}", input:subbytes.outputs[0])
nodes.push(shiftrows)
if i < nb_rounds
mixcolumns = MixColumnNode.new(name:"MC_#{i}", input:shiftrows.outputs[0], m:@mc)
nodes.push(mixcolumns)
else
mixcolumns = shiftrows
end
addkey = XorNode.new(name:"ARK_#{i}", inputs:[mixcolumns.outputs[0],ki.outputs[0]])
nodes.push(addkey)
end
return res
end
end
def print_matrix(title, m)
puts "===== #{title} ====="
for e in m
puts e.map{|a| "%02X" % a}.join("\t")
end
end
class AES128_Dag < CryptoDag
def initialize(nb_rounds=16)
# # inputs and first add round key
# # TODO key_matrices (how to compute them?) in keys[i] (i in 0..nb-rounds-1)
# @nb_rounds = nb_rounds
# @x = InputNode.new(4,4, name="X")
# @k = InputNode.new(4,4, name="K")
# ark = XorNode.new([@x, @k], name="ARK")
# # rounds
# (nb_rounds-1).times do |i|
# subbytes = SubCellNode.new(ark, method(:subcell_function, name="subCell_%d"%[i])
# shiftrows = ShiftRowsNode.new(subbytes, name="shiftRows_%d"%[i])
# mixcolumns = MixColumnNode.new(shiftrows, mixcolumns_matrix, name="mixColumns_%d"%[i])
# ark = XorNode([mixcolumns, keys[i]], name="ark_%d"%[i])
# end
# # define end operations
# subbytes = SubCellNode.new(ark, method(:subcell_function, name="subCell_end")
# shiftrows = ShiftRowsNode.new(subbytes, name="shiftRows_end")
# ark = XorNode.new([shiftrows, keys[nb_rounds]], name="ark_end")
# # define output
# super(OutputNode.new(ark, "C"))
# define dag inputs/outputs
super([@x,@k], [addkey], nodes)
end
##
# @param x [2DVec<u8>] input message
# @param k [2DVec<u8>] input key
# @returns [2DVec<u8>] crypted message
def simulate_behavior(x,k)
# simulates x,k input
@x.simulate_input(x)
@k.simulate_input(k)
# recursively computes c value and returns it
return @output.compute()
end
def test_components()
puts "test AES components"
x = InputNode.new(4,4, name="X")
k = InputNode.new(4,4, name="K")
x.simulate_input([
[0X32, 0X88, 0X31, 0XE0],
[0X43, 0X5A, 0X31, 0X37],
[0XF6, 0X30, 0X98, 0X07],
[0XA8, 0X8D, 0XA2, 0X34]
])
print_matrix("X", x.compute())
k.simulate_input([
[0X2B, 0X28, 0XAB, 0X09],
[0X7E, 0XAE, 0XF7, 0XCF],
[0X15, 0XD2, 0X15, 0X4F],
[0X16, 0XA6, 0X88, 0X3C]
])
print_matrix("K", k.compute())
k0 = AESKeyScheduleNode.new(k, "K0", rcon()[1])
print_matrix("K0", k0.compute())
sr1 = XorNode.new([x,k], name="SR1")
print_matrix("SR1", sr1.compute())
computed_outputs = compute_set_of_operators(
x.flatten()+k.flatten(), # input values
@x.flatten_output(0)+@k.flatten_output(0), # input variables
@output_nodes[0].flatten_output(0), # output variables
@nodes.map{|n| n.operators}.reduce([], :+)
)
return computed_outputs
end
end
def main
dag = AES128_Dag.new()
dag.test_components()
end
main
\ No newline at end of file
end
\ No newline at end of file
cryptosystems/aes/constants.rb
View file @ 399c5be6
......@@ -22,10 +22,6 @@ def s_box()
]
end
def subcell_function(i, j, v)
s_box[v]
end
###################### MIX COLUMNS ########################
......
tests/cryptosystems/aes128stepbystep.rb
View file @ 399c5be6
......@@ -8,7 +8,6 @@ require_relative "../../writers/graphviz_atomic.rb"
require_relative '../../cryptodag.rb'
require_relative '../../simulate_cryptodag.rb'
require_relative '../../nodes/input.rb'
require_relative '../../nodes/indexedsubbytes.rb'
require_relative '../../nodes/subbytes.rb'
require_relative '../../nodes/shiftrows.rb'
require_relative '../../nodes/mixcolumn.rb'
......
tests/cryptosystems/integration_aes128.rb 0 → 100755
View file @ 399c5be6
#!/usr/bin/ruby
require 'minitest/autorun'
require_relative "../../cryptosystems/aes/aes128.rb"
class TestAES128 < Minitest::Unit::TestCase
def test_a()
# create DAG
dag = AES128_Dag.new()
# simulate behavior
output = dag.simulate_behavior(
[
0x32, 0x88, 0x31, 0xe0,
0x43, 0x5a, 0x31, 0x37,
0xf6, 0x30, 0x98, 0x7 ,
0xa8, 0x8d, 0xa2, 0x34
],
[
0x2b, 0x28, 0xab, 0x9 ,
0x7e, 0xae, 0xf7, 0xcf,
0x15, 0xd2, 0x15, 0x4f,
0x16, 0xa6, 0x88, 0x3c
]
)
assert_equal(output, [
0x39, 0x2, 0xdc, 0x19,
0x25, 0xdc, 0x11, 0x6a,
0x84, 0x9, 0x85, 0xb ,
0x1d, 0xfb, 0x97, 0x32
])
end
end
\ No newline at end of file
tests/writers/abstract_aes128.rb 0 → 100755
View file @ 399c5be6
#!/usr/bin/ruby
require_relative "../../cryptodag.rb"
require_relative "../../cryptosystems/aes/aes128.rb"
require_relative "../../writers/abstract_constraints_atomic.rb"
require_relative "../../backends/minizinc"
require_relative "../../writers/graphviz_atomic.rb"
require "minitest/autorun"
# require "minitest/color"
require "pry"
class TestWriterGraphviz < Minitest::Unit::TestCase
def test_aes128()
# create dag
nb_rounds = 4
dag = AES128_Dag.new(nb_rounds = nb_rounds)
# shave dag
atoms,operators = *shave_dag(dag.atoms, dag.operators)
writefile_graphviz(atoms, operators, "aes128_#{nb_rounds}.dot")
# create initial model
obj_values = {}
obj_values[3] = 5
obj_values[4] = 12
obj_values[5] = 17
model,variable_dict,xor_clauses = *create_abstract_model(
atoms,
operators,
# "solve minimize obj",
"constraint obj=#{obj_values[nb_rounds]}; solve satisfy",
mds_set=Set[0,5,6,7,8]
)
# add diff variables
xor_clauses = xor_clauses + add_diff_variables_mixcolumn_lines(model, atoms, operators, variable_dict, mds_set=Set[0,5,6,7,8])
# generate new xor clauses and add them to the model
puts("ADDING XOR CLAUSES")
puts("\tstarting with #{xor_clauses.length} clauses")
xor_clauses = generate_xors(atoms, operators, xor_clauses, max_size=4)
puts("\tnow having: #{xor_clauses.length} clauses")
xor_clauses.each do |xor|
model.add_constraints(Diff1.new(*(xor.map{|v| variable_dict.fetch(v,v)})))
end
file = File.open("aes128_#{nb_rounds}.mzn", "w")
file.puts(Minizinc.new.generate_code(model))
file.close
puts "FILE: aes128_#{nb_rounds}.mzn correctly written"
assert_equal(true, true)
end
end
writers/abstract_constraints_atomic.rb
View file @ 399c5be6
require 'union_find'
require_relative '../cryptodag.rb'
require_relative '../operators/elementary.rb'
require_relative '../constraints/all.rb'
require_relative './graphviz_atomic.rb'
require_relative './dag_shaving.rb'
### DIRTY HACK (modify union_find datastructure)
class UnionFind::UnionFind
public :find_root
end
##############
def shave_dag(atoms, operators)
return *shave_equalities(
*shave_simple_input_xor(
*shave_constants_dag(
*shave_end_dag(
atoms,operators
)
)
)
)
end
##
# simplifies the dag by removing equalities
# @param atoms [Vec<CryptoAtom=Variable>]
# @param operators [Vec<CryptoOperators>]
# @return [new_atoms, new_operators]
def shave_equalities(atoms, operators)
union_find = UnionFind::UnionFind.new(Set.new(atoms))
untouched_atoms = Set.new(atoms)
operators.filter{|op| op.class <= EqualityOperator}.each do |op|
union_find.union(op.inputs[0], op.outputs[0])
untouched_atoms.delete(op.inputs[0])
untouched_atoms.delete(op.outputs[0])
end
old_to_root = {}
root_set = Set.new()
atoms.each do |a|
root_set.add(union_find.find_root(a))
old_to_root[a] = union_find.find_root(a)
end
raise "union find: inconsistent results" unless root_set.length == union_find.count_isolated_components
root_to_new = {}
new_atoms = []
root_set.each do |a|
new_a = Variable.new(a.name, 0..1, value=a.value)
root_to_new[a] = new_a
new_atoms.push(new_a)
end
puts "ELIMINATE EQUALITIES (vars: #{atoms.length} -> #{new_atoms.length})"
# define operators
new_operators = []
operators.filter{|op| !(op.class <= EqualityOperator)}.each do |op|
res = op.dup
res.inputs = op.inputs.map{|a| root_to_new[old_to_root[a]]}
res.outputs = op.outputs.map{|a| root_to_new[old_to_root[a]]}
raise "shave_equalities: different size between new and old input op #{res.inputs.length} should be #{op.inputs.length}" unless res.inputs.length == op.inputs.length
raise "shave_equalities: different size between new and old outputs op" unless res.outputs.length == op.outputs.length
res.inputs.each do |a|
raise "atom non existing in new_atoms set (input of #{res}, #{a})" unless Set.new(new_atoms).include?(a)
end
new_operators.push(res)
end
return [new_atoms, new_operators]
end
##
# returns new xors that can be used to improve the relaxations
# @param atoms [Vec<CryptoAtom=Variable>]
......@@ -121,136 +58,7 @@ def generate_xors(atoms, operators, custom_xors, max_size=4)
end
##
# removes operators and atoms to be shaved and returns a new dag
# @param atoms [Vec<CryptoAtom=Variable>]
# @param operators [Vec<CryptoOperators>]
# @param to_shave [Set<CryptoAtom|CryptoOperator>]
# @return [new_atoms, new_operators]
def get_dag_subset(atoms, operators, to_shave)
# create new dag with shaved nodes
atom_map = {}
new_atoms = []
# create new set of atoms
atoms.each do |atom|
if !to_shave.include?(atom)
new_atom = Variable.new(atom.name, 0..1, value=atom.value)
atom_map[atom] = new_atom
new_atoms.push(new_atom)
end
end
# create new set of operators
new_operators = []
operators.each do |op|
if !to_shave.include?(op)
new_inputs = op.inputs.filter{|e| !to_shave.include?(e)}.map{|e| atom_map[e]}
new_outputs = op.outputs.filter{|e| !to_shave.include?(e)}.map{|e| atom_map[e]}
new_op = op.dup
# p "#{op.class <= XorOperator}\t#{new_inputs.length}"
if (op.class <= XorOperator) && (new_inputs.length == 1)
# p "###"
raise "get_dag_subset: node with multiple outputs detected #{op}" unless new_outputs.length == 1
new_op = EqualityOperator.new(new_inputs[0], new_outputs[0])
else
new_op.inputs = new_inputs
new_op.outputs = new_outputs
end
new_operators.push(new_op)
end
end
return [new_atoms, new_operators]
end
##
# simplifies the dag
# @param atoms [Vec<CryptoAtom=Variable>]
# @param operators [Vec<CryptoOperators>]
# @return [new_atoms, new_operators]
def shave_simple_input_xor(atoms, operators)
# compute precedence and successors relations
preds, succs = *compute_precedences(atoms, operators)
# get input nodes with 1 output which is a xor
inputs = atoms.filter do |n|
preds.fetch(n, []).length == 0 &&
succs.fetch(n, []).length == 1 &&
succs.fetch(n, [])[0].class <= XorOperator
end
# for each input, replace the xor by
to_shave = Set.new()
inputs.each do |atom|
to_shave.add(atom)
to_shave.add(succs[atom][0])
end
return get_dag_subset(atoms, operators, to_shave)
end
##
# removes constants from the input nodes
# @param atoms [Vec<CryptoAtom=Variable>]
# @param operators [Vec<CryptoOperators>]
# @return [new_atoms, new_operators]
def shave_constants_dag(atoms, operators)
# compute precedence and successors relations
preds, succs = *compute_precedences(atoms, operators)
# get input nodes (should be CryptoAtoms)
constants = atoms.filter{ |n| n.value != nil }
to_shave = Set.new() # nodes to remove in the shaved model
constants.each do |c|
to_shave.add(c)
end
return get_dag_subset(atoms, operators, to_shave)
end
##
# removes end operators and atoms before S-boxes
# @param atoms [Vec<CryptoAtom=Variable>]
# @param operators [Vec<CryptoOperators>]
# @return [new_atoms, new_operators]
def shave_end_dag(atoms, operators)
# compute precedence and successors relations
preds, succs = *compute_precedences(atoms, operators)
# get input nodes (should be CryptoAtoms)
outputs = atoms.filter{ |n| succs.fetch(n, []).empty? }
to_shave = Set.new() # nodes to remove in the shaved model
outputs.each do |output_atom|
if preds[output_atom].length == 0
to_shave.add(output_atom)
elsif preds[output_atom].length == 1
op = preds[output_atom][0]
# if op is not a SOperator and has only one output, the atom (and operator) can be shaved
if !(op.class <= SOperator) && (succs[op].length == 1)
to_shave.add(output_atom)
to_shave.add(op)
end
else
raise "shave_end_dag: output #{output_atom.name.name} has too many preds (#{preds[output_atom]} should be <= 1)"
end
end
return get_dag_subset(atoms, operators, to_shave)
end
def compute_precedences(atoms, operators)
preds = {}
succs = {}
operators.each do |op|
op.inputs.each do |inp|
preds[op] = preds.fetch(op, []).push(inp)
succs[inp] = succs.fetch(inp, []).push(op)
end
op.outputs.each do |out|
preds[out] = preds.fetch(out, []).push(op)
succs[op] = succs.fetch(op, []).push(out)
end
end
return [preds, succs]
end
def create_abstract_model(atoms, operators, solve_instructions)
def create_abstract_model(atoms, operators, solve_instructions, mds_set=Set[0,4,5,6,7,8])
model = Model.new()
variable_dict = {} # Atom -> Variable
# add atoms as booleans
......@@ -264,10 +72,6 @@ def create_abstract_model(atoms, operators, solve_instructions)
operators.each do |op|
case op.class.name
when "XorOperator"
# model.add_constraints(Diff1.new(
# *op.inputs.map {|atom| variable_dict[atom]},
# *op.outputs.map {|atom| variable_dict[atom]}
# ))
xor_clauses.push(Set.new(
op.inputs.map {|atom| variable_dict[atom]}+
op.outputs.map {|atom| variable_dict[atom]}
......@@ -288,7 +92,7 @@ def create_abstract_model(atoms, operators, solve_instructions)
*op.inputs.map {|atom| variable_dict[atom]},
*op.outputs.map {|atom| variable_dict[atom]}
),
Set[0,4,5,6,7,8]
mds_set
))
model.add_constraints(Equivalence.new(
Equals.new(Sum.new(*op.inputs.map {|atom| variable_dict[atom]}), 0),
......@@ -318,7 +122,7 @@ end
##
#
#
def add_diff_variables_mixcolumn_lines(model, atoms, operators, atom_to_variable)
def add_diff_variables_mixcolumn_lines(model, atoms, operators, atom_to_variable, mds_set=Set[0,4,5,6,7,8])
res_xors = []
mc_operators = operators.filter{|op| op.class <= MixColumnsOperator}
op_to_ids = {}
......@@ -354,22 +158,12 @@ def add_diff_variables_mixcolumn_lines(model, atoms, operators, atom_to_variable
diffs.each do |d|
o1,o2,row,t = d[0],d[1],d[2],d[3]
if t == "I"
# model.add_constraints(Diff1.new(*[
# atom_to_variable[ids_to_op[o1].inputs[row]],
# atom_to_variable[ids_to_op[o2].inputs[row]],
# diffs_to_var[d]
# ]))
res_xors.push(Set.new([
ids_to_op[o1].inputs[row],
ids_to_op[o2].inputs[row],
diffs_to_var[d]
]))
else
# model.add_constraints(Diff1.new(*[
# atom_to_variable[ids_to_op[o1].outputs[row]],
# atom_to_variable[ids_to_op[o2].outputs[row]],
# diffs_to_var[d]
# ]))
res_xors.push(Set.new([
ids_to_op[o1].outputs[row],
ids_to_op[o2].outputs[row],
......@@ -377,40 +171,29 @@ def add_diff_variables_mixcolumn_lines(model, atoms, operators, atom_to_variable
]))
end
end
# add symmetry
diffs.each do |d1|
diffs.each do |d2|
if d1[0] < d1[1] && d1[0] == d2[1] && d1[1] == d2[0] && d1[3] == d2[3] && d1[2] == d2[2] && d1[0] != d2[0]
model.add_constraints(Equality.new(
diffs_to_var[d1],
diffs_to_var[d2]
))
# add transitivity
mc_operators.each do |o1|
mc_operators.each do |o2|
mc_operators.each do |o3|
if o1 != o2 && o2 != o3 && o1 != o3
id1, id2, id3 = op_to_ids[o1], op_to_ids[o2], op_to_ids[o3]
if id1 < id2 && id2 < id3
4.times do |row|
["I","O"].each do |t|
vars = [
diffs_to_var[[id1,id2,row,t]],
diffs_to_var[[id1,id3,row,t]],
diffs_to_var[[id2,id3,row,t]]
]
# model.add_constraints(Diff1.new(*vars))
res_xors.push(Set.new(vars))
end
end
end
end
end
end
end
# add transitivity
# mc_operators.each do |o1|
# mc_operators.each do |o2|
# mc_operators.each do |o3|
# if o1 != o2 && o2 != o3 && o1 != o3
# id1, id2, id3 = op_to_ids[o1], op_to_ids[o2], op_to_ids[o3]