Commit 3678edbe authored by Viguier Benoit's avatar Viguier Benoit
Browse files

Backup to please maman

parents
--2015-12-23 19:46:29-- https://raw.github.com/robbyrussell/oh-my-zsh/master/tools/install.sh
Résolution de raw.github.com (raw.github.com)… 185.31.18.133
Connexion à raw.github.com (raw.github.com)|185.31.18.133|:443… connecté.
requête HTTP transmise, en attente de la réponse… 301 Moved Permanently
Emplacement : https://raw.githubusercontent.com/robbyrussell/oh-my-zsh/master/tools/install.sh [suivant]
--2015-12-23 19:46:29-- https://raw.githubusercontent.com/robbyrussell/oh-my-zsh/master/tools/install.sh
Résolution de raw.githubusercontent.com (raw.githubusercontent.com)… 185.31.18.133
Connexion à raw.githubusercontent.com (raw.githubusercontent.com)|185.31.18.133|:443… connecté.
requête HTTP transmise, en attente de la réponse… 200 OK
Taille : 4236 (4,1K) [text/plain]
Sauvegarde en : « install.sh »
0K .... 100% 114M=0s
2015-12-23 19:46:30 (114 MB/s) — « install.sh » sauvegardé [4236/4236]
.bash*
Bureau*
.cache*
.config*
coq*
crypto*
.dbus*
dwm*
.fehbg*
FoxitSoftware*
.gconf*
.gitconfig*
.gnupg*
.gstreamer-0.10*
.histfile
.ICEauthority*
I*
i*
.l*
.l*
m*ex
.mozilla*
mri*
mshared.sh*
.oh-my-zsh*
.profile*
scripts*
slock*
.ssh*
st*
T*
.texmf-var*
ui*
.vi*
.x*
.X*
x*
.z*
# Created by https://www.gitignore.io/api/latex
### LaTeX ###
*.acn
*.acr
*.alg
*.aux
*.bbl
*.bcf
*.blg
*.dvi
*.fdb_latexmk
*.fls
*.glg
*.glo
*.gls
*.idx
*.ilg
*.ind
*.ist
*.lof
*.log
*.lot
*.maf
*.mtc
*.mtc0
*.nav
*.nlo
*.out
*.pdfsync
*.ps
*.run.xml
*.snm
*.synctex.gz
*.toc
*.vrb
*.xdy
*.tdo
{
"folders":
[
{
"path": "."
}
]
}
{
"auto_complete":
{
"selected_items":
[
[
"nb",
"nbrow"
],
[
"in",
"inputsize"
]
]
},
"buffers":
[
],
"build_system": "Packages/Makefile/Make.sublime-build",
"build_system_choices":
[
[
[
[
"Packages/C++/C++ Single File.sublime-build",
""
],
[
"Packages/C++/C++ Single File.sublime-build",
"Run"
],
[
"Packages/Makefile/Make.sublime-build",
""
],
[
"Packages/Makefile/Make.sublime-build",
"Clean"
]
],
[
"Packages/Makefile/Make.sublime-build",
""
]
]
],
"build_varint": "",
"command_palette":
{
"height": 392.0,
"last_filter": "ma",
"selected_items":
[
[
"ma",
"Build With: Make"
],
[
"make",
"Build With: Make"
],
[
"git bra",
"Git: New Branch"
],
[
"color",
"Colorsublime: Browse Themes"
],
[
"instal",
"Package Control: Install Package"
],
[
"insta",
"Colorsublime: Install Theme"
],
[
"pack",
"Package Control: Install Package"
]
],
"width": 521.0
},
"console":
{
"height": 126.0,
"history":
[
"import urllib.request,os,hashlib; h = '2915d1851351e5ee549c20394736b442' + '8bc59f460fa1548d1514676163dafc88'; pf = 'Package Control.sublime-package'; ipp = sublime.installed_packages_path(); urllib.request.install_opener( urllib.request.build_opener( urllib.request.ProxyHandler()) ); by = urllib.request.urlopen( 'http://packagecontrol.io/' + pf.replace(' ', '%20')).read(); dh = hashlib.sha256(by).hexdigest(); print('Error validating download (got %s instead of %s), please try manual install' % (dh, h)) if dh != h else open(os.path.join( ipp, pf), 'wb' ).write(by)"
]
},
"distraction_free":
{
"menu_visible": true,
"show_minimap": false,
"show_open_files": false,
"show_tabs": false,
"side_bar_visible": false,
"status_bar_visible": false
},
"expanded_folders":
[
"/home/biv/MRI"
],
"file_history":
[
"/home/biv/crypto/analysis/differentials.cpp",
"/home/biv/crypto/analysis/differentials.h",
"/home/biv/crypto/main.cpp",
"/home/biv/crypto/Makefile",
"/home/biv/crypto/cipher/des.h",
"/home/biv/crypto/cipher/feal.h",
"/home/biv/crypto/includes/cipher.h",
"/home/biv/dwm/config.h",
"/home/biv/dwm/config.mk",
"/home/biv/dwm/config.def.h"
],
"find":
{
"height": 0.0
},
"find_in_files":
{
"height": 0.0,
"where_history":
[
]
},
"find_state":
{
"case_sensitive": false,
"find_history":
[
],
"highlight": true,
"in_selection": false,
"preserve_case": false,
"regex": false,
"replace_history":
[
],
"reverse": false,
"show_context": true,
"use_buffer2": true,
"whole_word": false,
"wrap": true
},
"groups":
[
{
"sheets":
[
]
}
],
"incremental_find":
{
"height": 0.0
},
"input":
{
"height": 31.0
},
"layout":
{
"cells":
[
[
0,
0,
1,
1
]
],
"cols":
[
0.0,
1.0
],
"rows":
[
0.0,
1.0
]
},
"menu_visible": true,
"output.exec":
{
"height": 251.0
},
"output.find_results":
{
"height": 0.0
},
"output.git":
{
"height": 100.0
},
"pinned_build_system": "",
"project": "MRI.sublime-project",
"replace":
{
"height": 0.0
},
"save_all_on_build": true,
"select_file":
{
"height": 0.0,
"last_filter": "",
"selected_items":
[
],
"width": 0.0
},
"select_project":
{
"height": 0.0,
"last_filter": "",
"selected_items":
[
],
"width": 0.0
},
"select_symbol":
{
"height": 0.0,
"last_filter": "",
"selected_items":
[
],
"width": 0.0
},
"selected_group": 0,
"settings":
{
},
"show_minimap": true,
"show_open_files": false,
"show_tabs": true,
"side_bar_visible": true,
"side_bar_width": 250.0,
"status_bar_visible": true,
"template_settings":
{
}
}
\contentsline {lstlisting}{\numberline {2.1}Code sample for a differential attack}{3}{lstlisting.2.1}
\contentsline {lstlisting}{\numberline {2.2}Xor function to calculate linear expression}{4}{lstlisting.2.2}
\contentsline {lstlisting}{\numberline {6.1}C example}{10}{lstlisting.6.1}
\documentclass[11pt,insa]{sdm}
%One of:
% ens esir insa ENIB rennes UBO enssat Ubs telbr supelec
\usepackage{amsfonts}
\usepackage{amsmath}
\usepackage{zed-csp}
\usepackage{mathrsfs}
\usepackage{multicol}
\usepackage{numprint}
\usepackage{caption}
\usepackage[framemethod=TikZ]{mdframed}
\usetikzlibrary{calc}
\usetikzlibrary{backgrounds}
\usetikzlibrary{arrows}
\newcommand{\headerline}[3]{%
\makebox[\textwidth][s]{\rlap{#1}\hfill#2\hfill\llap{\texttt{#3}}}%
}
%numeroter les pages
\pagestyle{plain}
\title{Formal methods in differential and linear trail search}
\author{Beno\^it \textsc{Viguier}}
\supervisorOne{Gilles \textsc{Van Assche}}
\supervisorTwo{Joan \textsc{Daemen}}
\team{D\&I - {STMicroelectronics}}
%One of:
% ens-Rennes esir insa-rennes logoENIB rennes1 UBO
% enssat header logo_ENIB logoUbs tel-br supelec
\school{insa-rennes}
\domain{Domain: Cryptography and Security}
\definecolor{myyellowbg}{HTML}{FFFFCC}
\mdfdefinestyle{Note}{%
linecolor=notefg,
outerlinewidth=0pt,
roundcorner=0pt,
topline=false,
leftline=false,
rightline=false,
bottomline=false,
innertopmargin=5pt,
innerbottommargin=5pt,
innerrightmargin=20pt,
innerleftmargin=5pt,
backgroundcolor=myyellowbg,
footnoteinside=false,
}
\usepackage{hyperref}
\usepackage{cleveref}
\crefformat{equation}{eq.~#2#1#3}
\crefformat{listing}{code~#2#1#3}
\crefformat{figure}{fig.~#2#1#3}
\crefformat{chapter}{chap.~#2#1#3}
\crefformat{section}{sect.~#2#1#3}
\crefformat{table}{tab.~#2#1#3}
\begin{document}
\maketitle
\frontmatter
% \begin{prerequisites}
% \begin{centering}
% Basic knowledge in cryptography.\\
% Knowledge in Set theory.\\
% \end{centering}
% \end{prerequisites}
\abstract{The aim of this internship is to evaluate how formal methods can help in the search of bounds and trail. I present the state of my knowledge about cryptography and formal methods. This report is mainly focused on Differential and Linear Cryptanalysis. It then introduces the hashing algorithm \textsc{Keccak} and its sponge construction. A brief introduction of Formal Methods (B and the use of Coq) is provided, with some example of their current usages.}
\tableofcontents
%*****************************************************************%
\setlength{\parskip}{10pt}
\mainmatter
\chapter{Introduction}
Block cipher are divided into two kind: Feistel networks (e.g. DES \cite{NIST:1999:FPD}) and Substitution Permutation Network (e.g. AES \cite{FIPS:2001:AES},\cite{Daemen:2002:DRA}). Both of them are composed of multiple rounds and often relies on S-boxes.
\begin{minipage}[t]{.5\textwidth}
\centering
\resizebox{\textwidth}{!}{%
\input{tikz/feistel3}
}%
\label{fig:feistel3}
\captionof{figure}{A 3 round Feistel Network}
\end{minipage}
\hfill
\begin{minipage}[t]{.5\textwidth}
\centering
\resizebox{\textwidth}{!}{%
\input{tikz/spn}
}%
\label{fig:spn}
\captionof{figure}{A 3 round Substitution Permutation Network}
\end{minipage}
%
\chapter{Cryptanalysis}
\textit{``Cryptanalysis is the study of mathematical techniques for attempting to defeat cryptographic techniques, and, more generally, information services.''}\\
\headerline{}{}{Handbook of applied cryptography\cite{Menezes:1997:HAC}}
Cryptographic algorithm are mainly divided into two categories: block ciphers (such as DES, AES\ldots) which use a key and hash function (i.e. SHA-1, SHA-256, SHA-3\ldots\cite{Anonymous:2012:SHS}). The first one is an encryption device used to provide confidentiality over a piece of information. Encrypted data can be deciphered while the second one mainly aims to provide integrity.
The goals of cryptanalysis in the case of a block cipher is to retrieve the key used for the encryption. In order to do so, the academic world mainly rely on chosen-plaintext attack. The attacker has access to the device and is allowed to encrypt any data. In the case of a hash function, because of the absence key, cryptanalysis aim to find a collision. Differential and linear cryptanalysis are the roots of modern attacks.
In the case of block ciphers, they aim to mesure the changes between input and output with a probability. The goal is to predict what the result will be before the last round and try to extract the key. \cite{Swenson:2008:MCT}
\section{Differential Cryptanalysis}
Differential Cryptanalysis has been introduced by Biham and Shamir at Crypto 90\cite{Biham:1990:DCD}. The idea is to exploit statistical informations on differences between chosen plaintexts to dermine the value of key bits.
Given two text $t_1$ and $t_2$, a \mrired{differential} $\Omega$ is the value of $t_1 \oplus t_2$.
A \mrired{characteristic} is composed of two differential and written as $(\Omega_X \Rightarrow \Omega_Y)$. The idea behind characteristic is to show that given an input differential $\Omega_X$, chances are that a differential $\Omega_Y$ will occur. As an example in FEAL\cite{ShimizuMi88}, the characteristic (\cref{eq:FealCarac}) has a probability of $1$ for one round\cite{Biham:1991:DCFb}.
\begin{equation} \label{eq:FealCarac}
(L\ ||\ 80\ 80\ 80\ 80_x) \Rightarrow (L \oplus 02\ 00\ 00\ 02_x\ ||\ 80\ 80\ 80\ 80_x)
\end{equation}
In any cipher the characteristic $(0 \Rightarrow 0)$ always holds.
Given characteristics of a round function or S-boxes of a cipher, it is possible to build an \mrired{iterative characteristic}: the combinaison of consecutive characteristics. Each characteristic is supposed to be indepdendant of the other, therefore the probability of an iterative characteristic is the product of its components. The difficulty here is to find the \textit{good} combinaison of characteristics: the higher its probability, the less pair of chosen text is required.
Once an iterative caracteristic with a good probability $(\Omega_X \implies \Omega_Y)$ is found (e.g. \cref{fig:differential}), we encrypt random pairs of plain text with an $\Omega_X$ differential. Then we attempt to guess the condidate bytes of the key by undoing the last round of each enciphered pair with cadidate keys and compare with the predicted characteristic (see \cref{pycode}).\\
\begin{lstlisting}[language=Python, caption=Code sample for a differential attack, label=pycode]
number_pair # number of pair to generate
initial_diff # initial differential
ciphertext1 = []
ciphertext2 = []
# generate pairs of cipher text
for i in range(number_pair)
p1 = random.randint(0, 2**bits) # generate a random plaintext
p2 = p1 ^ initial_diff # generate associated plaintext
ciphertext1.append(encrypt(p1))
ciphertext2.append(encrypt(p2))
count = [] # table to count the statistics for each key
maxcount = -1 # count best candidate
maxkey = -1 # best candidate
predicted_diff # the value of the differential we are looking for
# When in doubt, use brute force - Ken Thomson
for k1 in range(0, number of keys) :
k = k1 # adjust the key.
for j in range(0, number_pair)
c1 = ciphertext1[j]
c2 = ciphertext2[j]
t1 = unround(c1,k) # undo last round
t2 = unround(c2,k) # undo last round
diff = t1 ^ t2 # ouput differential
if diff == predicted_diff :
count[k1] = count[k1] + 1
if count[k1] >= maxcount : # if best key, save it
maxcount = count[k1]
maxkey = k1
\end{lstlisting}
\resizebox{\textwidth}{!}{%
\input{tikz/differential}
}%
\captionof{figure}{Example of a differential trail on a SPN}
\begin{figure}
\label{fig:differential}
\end{figure}
~\\\\
S-boxes with a null-differential are called \textit{inactive}, e.g. in (\cref{fig:differential}) S-boxes $S_2$ and $S_4$ are active. Also note in most cases the key does not impact on the characteristic (e.g. S-boxes of Twofish\cite{Schneier:1998:TBBa} are key-dependent).
\begin{mdframed}[style=Note]
\textbf{Proof (simplified):}\\
let $K$ the key and $f$ the round function composed of a substitution $\sigma$ followed by a key addition.\\
For all $x_1, x_2$ such as $x_1 \oplus x_2 = \Omega_X$ and $\Omega_Y = f(x_1) \oplus f(x_2)$.\\
\begin{align*}
(\Omega_X \implies \Omega_Y) & = (\Omega_X \implies f(x_1) \oplus f(x_2))\\
& = (\Omega_X \implies K \oplus \sigma(x_1) \oplus K \oplus \sigma(x_2))\\
& = (\Omega_X \implies \sigma(x_1) \oplus \sigma(x_2))
\end{align*}
Therefore the characteristic $(\Omega_X \implies \Omega_Y)$ does not depend on the key $K$.
\end{mdframed}
From this attack are derivated truncated and high-order differentials\cite{conf:fse:Knudsen94}, impossible differentials\cite{Biham:1998:CSR} and boomerang attack\cite{Wagner:1999:BA} \cite{Swenson:2008:MCT}.\\
\section{Linear Cryptanalysis}
\setlength{\parskip}{10pt}
Linear Cryptanalysis is a known-plaintext attack (KPA). It has been introduced by Matsui and Yamagishi at EURCOCPYT'93 \cite{Matsui:1993:LCM}. The idea is to obtain one or multiple linear approximate expression of a cipher algorithm and to use known plaintexts.
Equations involve bits of plaintext, ciphertext and keys :
\begin{equation} \label{eq:lineqsample}
P_0 \oplus P_2 \oplus \ldots \oplus C_1 \oplus C_2 \oplus \ldots = K_1 \oplus K_3 \oplus \ldots
\end{equation}
where $X_i$ denote $i^{th}$ bit in $X$. This equation (\cref{eq:lineqsample}) holds with a probability $p \neq \frac{1}{2}$. The quantity $\epsilon = p - \frac{1}{2}$ represent the bias of the equation. Its magnitude $|\epsilon|$ represent the effectiveness.
To simplify the expressions M. Matsui introduced a notation :
\begin{equation} \label{eq:lineqmatsui}
A[i_1, i_2, \ldots, i_n] = A_{i_1} \oplus A_{i_1} \oplus \ldots \oplus A_{i_n}
\end{equation}
As in the differential cryptanalysis, we first analyze the round function and/or S-boxes in order to get the cipher algorithm approximate expression.
Bits present in a linear equation can be translated to a 1 or 0 if absent. Thus the equation $A[0,2,3,6] = A_0 \oplus A_2 \oplus A_3 \oplus A_6$ could be represented by the bit selection $01001101$ or $4D_x$. Using such a mask (see \cref{pyxorlinear}) helps in the search for the best linear expression of S-boxes.
\begin{lstlisting}[language=Python, caption=Xor function to calculate linear expression, label=pyxorlinear]
# procedure for quick extraction of linear bits given a mask
def XorBits(val, size, mask)
res = 0l
val = val & mask # apply mask to select bits
for i in range(size)
{
res = res ^ (val & 1l);
val = val >> 1
}
return res
\end{lstlisting}
Results of the linear analysis of an S-box is often presented as a table. As an example, the equation (\cref{eq:lineeq}) happens 2 times. Thus its bias is $2 - 8 = -6$.
\begin{equation} \label{eq:lineeq}
x_1 \oplus x_0 = y_3 \oplus y_0\\
\end{equation}
Therefore the value in the table at coordinates $(3\semicolon 9)$ is $-6$ (\cref{eq:lineeq1,eq:lineeq2,eq:lineeq3}).
\begin{align} \label{eq:lineeq1}
x_1 \oplus x_0 & \mapsto 0011 = 3\\
y_3 \oplus y_0 & \mapsto 1001 = 9\label{eq:lineeq2}\\
x_1 \oplus x_0 = y_3 \oplus y_0 & \iff X[3] = Y[9]\label{eq:lineeq3}
\end{align}
\begin{table}[h!]
\begin{tabular}{ c c | c c c c c c c c c c c c c c c c }
~ & ~ & ~ & ~ & ~ & ~ & ~ & O & U & T & P & U & T & ~ & ~ & ~ & ~ & ~\\
~ & ~ & 0 & 1 & 2 & 3 & 4 & 5 & 6 & 7 & 8 & 9 & A & B & C & D & E & F\\
\hline
~ & 0 & +8 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0\\
~ & 1 & 0 & 0 & $-$2 & $-$2 & 0 & 0 & $-$2 & +6 & +2 & +2 & 0 & 0 & +2 & +2 & 0 & 0\\
~ & 2 & 0 & 0 & $-$2 & $-$2 & 0 & 0 & $-$2 & $-$2 & 0 & 0 & +2 & +2 & 0 & 0 & $-$6 & +2\\
~ & 3 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & +2 & \mrired{$-$6} & $-$2 & $-$2 & +2 & +2 & $-$2 & $-$2\\
~ & 4 & 0 & +2 & 0 & $-$2 & $-$2 & $-$4 & $-$2 & 0 & 0 & $-$2 & 0 & +2 & +2 & $-$4 & +2 & 0\\
~ & 5 & 0 & $-$2 & $-$2 & 0 & $-$2 & 0 & +4 & +2 & $-$2 & 0 & $-$4 & +2 & 0 & $-$2 & $-$2 & 0\\
I & 6 & 0 & +2 & $-$2 & +4 & +2 & 0 & 0 & +2 & 0 & $-$2 & +2 & +4 & $-$2 & 0 & 0 & $-$2\\
N & 7 & 0 & $-$2 & 0 & +2 & +2 & $-$4 & +2 & 0 & $-$2 & 0 & +2 & 0 & +4 & +2 & 0 & +2\\
P & 8 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & $-$2 & +2 & +2 & $-$2 & +2 & $-$2 & $-$2 & $-$6\\
U & 9 & 0 & 0 & $-$2 & $-$2 & 0 & 0 & $-$2 & $-$2 & $-$4 & 0 & $-$2 & +2 & 0 & +4 & +2 & $-$2\\
T & A & 0 & +4 & $-$2 & +2 & $-$4 & 0 & +2 & $-$2 & +2 & +2 & 0 & 0 & +2 & +2 & 0 & 0\\
~ & B & 0 & +4 & 0 & $-$4 & +4 & 0 & +4 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0\\
~ & C & 0 & $-$2 & +4 & $-$2 & $-$2 & 0 & +2 & 0 & +2 & 0 & +2 & +4 & 0 & +2 & 0 & $-$2\\
~ & D & 0 & +2 & +2 & 0 & $-$2 & +4 & 0 & +2 & $-$4 & $-$2 & +2 & 0 & +2 & 0 & 0 & +2\\
~ & E & 0 & +2 & +2 & 0 & $-$2 & $-$4 & 0 & +2 & $-$2 & 0 & 0 & $-$2 & $-$4 & +2 & $-$2 & 0\\
~ & F & 0 & $-$2 & $-$4 & $-$2 & $-$2 & 0 & +2 & 0 & 0 & $-$2 & +4 & $-$2 & $-$2 & 0 & +2 & 0\\
\end{tabular}
\label{tab:dist-linear}
\caption{A linear distribution table of S-box}
\end{table}
Linear expression of S-boxes can be combined in order to get a linear approximation of the cipher algorithm. The formula to compute the bias of this approximation has been proven by Matsui \cite{Matsui:1993:LCM} and is known as ``Piling-up Lemma''.
\begin{mdframed}[style=Note]
\textbf{Piling-up Lemma :}\\
Let $X_i\ (1 \leq i \leq n)$ be independant random variables whose values are $0$ with a probability $p_i$ or $1$ with a probability $1-p_i$. Then the probability that $X_1 \oplus X_2 \oplus \ldots \oplus X_n = 0$ is
\begin{equation}