-
Notifications
You must be signed in to change notification settings - Fork 1
/
thesis.tex
168 lines (143 loc) · 4.53 KB
/
thesis.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
\documentclass[fontsize=12pt,paper=A4,abstract=true]{scrreprt}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage[UKenglish]{babel}
\usepackage[backend=biber]{biblatex}
\usepackage{microtype}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{mathtools}
\usepackage{pifont}
%\usepackage{lmodern}
\usepackage{baskervald}
\usepackage{float}
%\usepackage{libertineRoman} % TODO: remove
\usepackage{graphicx}
\usepackage{hyperref}
\usepackage{scrpage2}
\usepackage[xindy]{glossaries}
\usepackage{listings}
\usepackage[normalem]{ulem}
\usepackage{makeidx}
\usepackage{multicol}
\usepackage{caption}
\usepackage{subcaption}
\usepackage{rotating}
\usepackage{xcolor}
\usepackage[ruled,vlined]{algorithm2e}
\addbibresource{thesis.bib}
\setcounter{secnumdepth}{3}
\setlength{\parskip}{\baselineskip}
\definecolor{contr}{RGB}{180,40,0}
% Other titles:
% 1. SAT solvers in cryptanalysis
% 2. Assumption-based hash collision search in differential cryptanalysis using SAT solvers
\title{
Using SAT Solvers to Detect Contradictions
in Differential Characteristics
}
\author{Lukas Prokop}
\date{22nd April 2014}
\makeglossaries
\makeindex
\makeatletter
\hypersetup{
pdftitle={\@title},
pdfauthor={\@author},
pdfsubject={SAT solvers in cryptanalysis},
pdfcreator={\LaTeX},
pdfkeywords={SAT solver, hash algorithms, differential cryptanalysis},
urlcolor=[rgb]{0.2,0.2,0.2},
linkcolor=[rgb]{0.2,0.2,0.2},
citecolor=[rgb]{0.1,0.1,0.1},
baseurl={http://lukas-prokop.at/proj/bakk_iaik},
pdfview=FitV,
pdflang={en-US},
unicode,
breaklinks,
colorlinks,
bookmarks
}
\makeatother
\newcommand{\nltool}{nltool}
\newcommand{\cmsat}{cryptominisat}
\newcommand{\yes}{\footnotesize\ding{51}}
\newcommand{\no}{\footnotesize\ding{55}}
\newcommand{\bc}[1]{#1} % BitCondition
\newcommand{\abs}[1]{\lvert #1\rvert}
\newcommand{\lifetime}[2]{*\,#1 \dag\,#2}
\renewcommand{\implies}{\rightarrow}
%\newcommand{\diffchar}[1]{\mbox{\ttfamily #1\obeylines}}
\newenvironment{diffchar}{\center\begingroup\ttfamily}{\endgroup\endcenter}
\newacronym{sat}{SAT}{satisfiability}
\newacronym{cnf}{CNF}{Conjunctive Normal Form}
\newacronym{dnf}{DNF}{Disjunctive Normal Form}
\newacronym{csp}{CSP}{Constraint Programming}
\floatstyle{plaintop}
\restylefloat{table}
\makeatletter
\def\UL@putbox{\ifx\UL@start\@empty \else % not inner
\vrule\@width\z@ \LA@penalty\@M
{\UL@skip\wd\UL@box \UL@leaders \kern-\UL@skip}%
\phantom{\box\UL@box}%
\fi}
\makeatother
\begin{document}
\input{titlepage.tex}
\newpage
\subsection*{\centerline{Statement of Originality}}
%
\vspace{14pt}\indent
This thesis contains no material that has been accepted for the recognition
of any other degree at any other university. To the best of my knowledge,
this thesis contains no material previously published or written
by another person, except where reference is made in the text.
\vspace{30pt}
\noindent\uline{--- Lukas Prokop ---} \\[5pt]
\phantom{---} Lukas Prokop \phantom{---}
\begingroup
\hypersetup{colorlinks=true,linktoc=all,linkcolor=contr}
\tableofcontents
\endgroup
\begin{abstract}
The NP-completeness of SAT has been proven in 1971 by Stephen Cook
and under the assumption of $P \neq N\!P$, the problem is infeasible
for large problem sizes. However, recent advances in the field of
SAT solver design make large SAT problems solvable on an industrial
level if enough computational resources are provided.
At the same time, hash algorithms' collision resistance depends
on the computational complexity of the algorithm which has successfully
been reduced by Wang~et~al.
Combining those techniques we might be able break the security of
modern hash algorithms.
In this bachelor's thesis we present an implementation for performing
(partial) SAT-based attacks on hash algorithms by evaluating the
satisfiability of differential characteristics. We evaluate three
possible CNF encodings for this problem.
\end{abstract}
\chapter{Introduction}
\label{chap:introduction}
\input{intro.tex}
\chapter{Automated search for differential characteristics}
\label{chap:search}
\input{search.tex}
\chapter{SAT solvers}
\label{chap:sat}
\input{sat.tex}
\chapter{Bridging differential cryptanalysis and SAT solving}
\label{chap:implementation}
\input{implementation.tex}
\chapter{Future work}
\label{chap:next}
\input{next_work.tex}
\appendix
\chapter{CNF transformations for boolean equations}
\label{appendix:cnf}
\input{cnf_transformations.tex}
\hypersetup{colorlinks=true,linktoc=all,linkcolor=contr}
\printbibliography
\listofalgorithms
\listoffigures
\listoftables
\printindex
\end{document}