|
| |
|
| |
|
|
Vulnerabilities and security proofs of communication protocols used by malware
Med, Ondřej ; Středa, Adolf (advisor) ; Boháček, Milan (referee)
Cryptographic games with their transitions are a useful tool for proving cryptographic properties of various security protocols. We have explored together the notions of neg- ligible functions, cryptographic games and their transitions, computational, and perfect security. This served as our basis when analyzing malware protocols, we translated each into a game that tested the property we were trying to expose. Then, using transitions based on negligible functions, we simplified said games to reach desired results. We have decided to employ Cryptoverif as our tool for implementing these games, it is designed to create sequences of games that lead to games exposing specified properties. We translated the games into series of primitives that form an interface of this tool. Using the theory described above we anchored individual transitions in mathematical arguments and documented the proof strategy Cryptoverif employs. To illustrate the usage, we have selected a few communication protocols used by several malware families (Emotet, Mirai, Lockcrypt) and used the tooling to prove a few characteristic properties. While this has been challenging for a few cases (especially when the techniques were not entirely inside Cryptoverif's scope) we have managed to design our games accordingly to reach the desired...
|
|
| |
|
|
Bitcoin digital currency
Deptová, Lucie ; Boháček, Milan (advisor) ; Hojsík, Michal (referee)
In 2009 Satoshi Nakamoto started the electronic payment system and virtual cash Bitcoin for the first time. Bitcoin has to guarantee some level of security as well as other digital currencies. It's necessary to prevent double- spending or it's required to provide anonymity of payments. The diference between Bitcoin and most of the other virtual currencies is absence of any trusted party which would provide demands mentioned above. In this paper we describe the structure and properties of basic elements of this payment system. In the mean time we explain methods how to deal with the fact that Bitcoin is completely decentralized. The paper gives complex and detailed information which you can find only in official source code of bitcoin client or in many separated and particular articles. 1
|
|
| |
|
|
Analysis of voice over IP protocols
Boháček, Milan ; El Bashir, Robert (advisor) ; Hojsík, Michal (referee)
In the presented work we focus on both implementation and protocol of the voice over IP application Skype. We analyse several versions of Skype clients and deduce inner workings of the Skype protocol. We present details about the cryptographic primitives used by the Skype clients and their impact on the security of the communication. We emphasize several places of suspicious leaks of the internal states of random generators and deduce rules for the detection of the Skype traffic on the firewall. In the end, we mention a simple enhancement of the current Skype clients that, in practice, can detect an ongoing eavesdropping.
|
|
|
Key reconstruction from the inner state of RC4
Sladký, Lukáš ; Boháček, Milan (advisor) ; Drápal, Aleš (referee)
In the present work we analyse the key scheduling algorithm of the RC4 stream cipher. The internal permutation generated by the algorithm is biased towards the secret key which can be utilized in the key recovery attempts. Multiple sources were combined to provide proven formulae for these biases. We have completed missing proofs, experimentally verified resulting probabilities and created examples to illustrate usage of the biases in key recovery attempts. This together with methods for extracting information about the secret key gives analysis of the key scheduling algorithm. We have also selected an efficient key retrieval algorithm and implemented an improved version which results in better success probabilities of the key recovery. We have also provided a tool for extracting the key from a permutation obtained by the key scheduling algorithm. Powered by TCPDF (www.tcpdf.org)
|
|
|
Crytographic attacks on TLS protocol
Oupický, Jan ; Tůma, Jiří (advisor) ; Boháček, Milan (referee)
The aim of this work is to introduce the reader to the protocol TLS and a few selected attacks against the protocol. In the first part we will define the necessary cryptographic definitions used in the following chapters. In the second part we will briefly talk about the history of procotols TLS and SSL and then we will closely look into how they work. The last part is about the analysis of the chosen cryptographically interesting attacks (Padding oracle on CBC mode, POODLE, BEAST and CRIME) against protocols TLS and SSL. 1
|
|
| |
guest ::
RSS feed.