diff options
Diffstat (limited to 'tfm.tex')
| -rwxr-xr-x | tfm.tex | 51 |
1 files changed, 51 insertions, 0 deletions
@@ -90,10 +90,52 @@ understand EasyCrypt and implement bla bla bla) \pagenumbering{arabic} \setcounter{page}{1} +In the last years, society is becoming ever more dependent on computer +systems. People manage their bank accounts via web, are constantly in touch with +their contacts thanks to instant messaging applications, and have huge amounts +of personal data stored in the \textit{cloud}. All this personal information +flowing through computer networks need to be protected by correctly implementing +adequate security measures regarding both information transmission and +storage. Building strong security systems is not an easy task, because there are +lots of parts that must be studied in order to assure the system as a whole +behaves as intended. + +One of the most fundamental tools used to build security computer systems is +\textbf{cryptography}. Due to its heavy mathematical roots, cryptography today +is a mature science that, when correctly implemented, can provide strong +security guarantees to the systems using it. In fact, it is usually the case +that cryptography is one of the \textit{most secure} parts of the system, and a +lot of other concerns should be taken care of, such as underlying operating +systems, security policies, or the human factor. + +At this point, one could be tempted of just ``using strong, NIST-approved +cryptography'' and focusing on the security of other parts of the system. The +reality is that correctly implementing cryptography is a pretty difficult task +on its own, mainly because there is not a one-size-fits-all construction that +covers all security requirements. Every cryptographic primitive has its own +security assumptions and guarantees, so one must be exceptionally cautious when +combining them in order to build larger systems. For example, a given +cryptographic construction could be well suited for a concrete scenario and +totally useless in some others. In turn, this situation can produce a false +sense of security, potentially worse that not having any security at all. + +In order to have the best guarantee that some cryptographic construction meets +its security requirements, we can use use formal methods to prove that the +requirements follow from the assumptions (scenario). + +(TODO: maybe a sub-section on sequences of games, Hoare logic, etc.) + \section{Problem} %% +(TODO: Need of Computer-assisted proofs) + + +\subsection{EasyCrypt} + +(TODO: What is EasyCrypt (Coq-like, screens, etc)) + \section{Contributions} %% @@ -149,6 +191,15 @@ ciphertext ($C$). \section{Sequences of games} %% +While mathematical proofs greatly enhance the confidence we have in that a given +cryptosystem behaves as expected, with the recent increase in complexity it has +become more and more difficult to write and verify the proofs by hand, to the +point of being practically non-viable. In 2004 \cite{Shoup04}, Victor Shoup +introduced the concept of \textbf{sequences of games} as a method of taming the +complexity of cryptography related proofs. A game is like a program written in a +well-defined, probabilistic programming language, and a sequence of games is the +result of applying transformations over the initial one. + \section{Verification: EasyCrypt} %% |