Security, protocols, protocol analysis, formal verification, logics, ethical hacking, electronic voting, privacy preserving technology, secure messaging/email, programming languages for security, applied pi-calculus, linear logic, session types.
Current and past theses
- Formal analysis of EDHOC, a protocol for IoT secure communication, Theis Grønbech Petersen and Thorvald Sahl Jørgensen, Spring 2018
- Security analysis for smart door lock, Steffen Mogensen, Spring 2018
- Deduplicated Storage Systems: Trade-offs between security and efficiency, Emma Arfelt Kock, Fall 2017
- Verifying Selene in Tamarin, Eva Drewsen, Spring 2017
- Voting Protocol in Ethereum, Adrian Brink, Spring 2017
- Transparent authentication with wearable devices, Jacob Cholewa and Rasmus Wismann, Spring 2017
- Hacking WinVote machines, Florin Vasile and Andreas Nielsen, Fall 2016
Analyze a security protocol
Security protocols are used in all aspects of our lives. TLS for example empowers secure communication over the internet, but is not the only protocol. Many protocols include flaws that go undetected even after years that they have been in use. Many of these flaws are logical errors, that is security problems that designers did not think were possible when designing the protocol. These can be detected using tools (like ProVerif) that allow you to model protocols and automatically check that certain security properties hold, or show an attack otherwise.
A successful thesis in this area would consider an interesting security protocol, and then conduct a formal analysis using these automated tools. Very often these theses lead to finding mistakes in the specifications or implementation. For example we have helped improve the EDHOC standard for secure IoT communication proposed by Ericsson, and showed some flaws in CAN-bus, a network for controlling electronic components in automobiles. Options for the analysis could be: the Apple keychain/Firefox password storage; a messaging protocol (WhatsApp/Telegram etc.); an Internet protocol; an IoT protocol.
Work on analysis/compilation of secure protocols
Often tools for analyzing security protocols come with limitations: certain properties cannot automatically be checked and require manual abstractions to complete the proofs, and there are certain equations that require special care. One particular problem is when analyzing stateful protocols: protocols that maintain state depending upon which certain actions are enabled or not.
Another problem is how to construct secure software once a protocol model has been proven correct: one option is to derive working code from the protocol model that is secure by construction.
If you like to work with programming languages, software analysis, logics, compilers, and think that security problems are very relevant in the software landscape, we can find a thesis for you!
Hack a connected device
Another option is to consider a particular hardware device whose security is important, and try to hack it. This thesis requires you to go through the process of doing forensics analysis of a real device and then responsible disclosure in case you find some bugs. It requires a diverse range of skills, including quick learning of new software and hardware analysis tools, analyzing and reconstructing encrypted communication between devices, good communication skills with the companies involved.
Examples of such a thesis are: hack a smart-lock, IoT camera or toy, a smart-meter, an industrial control system etc.