List of publications
2022
-
[preprint (2019-10-23)] [bib (dblp)] [code repository]Factoring semi-primes with (quantum) SAT-solvers
, with Michele Mosca [article]Abstract
The assumed computationally difficulty of factoring large integers forms the basis of security for RSA public-key cryptography, which specifically relies on products of two large primes or semi-primes. The best-known factoring algorithms for classical computers run in sub-exponential time. Since integer factorization is in NP, one can reduce this problem to any NP-hard problem, such as Boolean Satisfiability (SAT). While reducing factoring to SAT has proved to be useful for studying SAT solvers, attempting to factor large integers via such a reduction has not been found to be successful.
Shor's quantum factoring algorithm factors any integer in polynomial time, although large-scale fault-tolerant quantum computers capable of implementing Shor's algorithm are not yet available, so relevant benchmarking experiments for factoring via Shor's algorithm are not yet possible. In recent years, however, several authors have attempted factorizations with the help of quantum processors via reductions to NP-hard problems. While this approach may shed some light on some algorithmic approaches for quantum solutions to NP-hard problems, in this paper we study and question the practical effectiveness of this approach for factoring large numbers. We find no evidence that this is a viable path toward factoring large numbers, even for scalable fault-tolerant quantum computers, as well as for various quantum annealing or other special purpose quantum hardware.
-
[.pdf (mirror)] [.bib]Quantum information in security protocols
[PhD thesis]Abstract
Information security deals with the protection of our digital infrastructure. Achieving meaningful real-world security requires powerful cryptographic models that can give strong security guarantees and it requires accuracy of the model. Substantial engineering effort is required to ensure that a deployment meets the requirements imposed by the model.
Quantum information impacts the field of security in two major ways. First, it allows more efficient cryptanalysis of currently widely deployed systems. New "post-quantum" cryptographic algorithms are designed to be secure against quantum attacks, but do not require quantum technology to be implemented. Since post-quantum algorithms have different properties, substantial effort is required to integrate these in the existing infrastructure. Second, quantum cryptography leverages quantum-mechanical properties to build new cryptographic systems with potential advantages, however these require a more substantial overhaul of the infrastructure.
In this thesis I highlight the necessity of both the mathematical rigour and the engineering efforts that go into security protocols in the context of quantum information. This is done in three different contexts.
First, I analyze the impact of key exhaustion attacks against quantum key distribution, showing that they can lead to substantial loss of security. I also provide two mitigations that thwart such key exhaustion attacks by computationally bounded adversaries, without compromising the information theoretically secure properties of the protocol output. I give various security considerations for secure implementation of the mitigations.
Second, I consider how quantum adversaries can successfully attack quantum distance bounding protocols that had previously been claimed to be secure by informal reasoning. This highlights the need for mathematical rigour in the analysis of quantum adversaries.
Third, I propose a post-quantum replacement for the socialist millionaire protocol in secure messaging. The protocol prevents some of the usability problems that have been observed in other key authentication ceremonies. The post-quantum replacement utilizes techniques from private set intersection to build a protocol from primitives that have seen much scrutiny from the cryptographic community.
Keywords
Quantum Information, Information Security, Quantum Key Distribution, Distance Bounding, Key Authentication
Supervisor
2019
-
[preprint] [.pdf] [bib (dblp)] [code repository]On speeding up factoring with quantum SAT solvers
, with Michele Mosca and João Marcos Vensi Basso [article]Abstract
There have been several efforts to apply quantum SAT solving methods to factor large integers. While these methods may provide insight into quantum SAT solving, to date they have not led to a convincing path to integer factorization that is competitive with the best known classical method, the Number Field Sieve. Many of the techniques tried involved directly encoding multiplication to SAT or an equivalent NP-hard problem and looking for satisfying assignments of the variables representing the prime factors. The main challenge in these cases is that, to compete with the Number Field Sieve, the quantum SAT solver would need to be superpolynomially faster than classical SAT solvers. In this paper the use of SAT solvers is restricted to a smaller task related to factoring: finding smooth numbers, which is an essential step of the Number Field Sieve. We present a SAT circuit that can be given to quantum SAT solvers such as annealers in order to perform this step of factoring. If quantum SAT solvers achieve any asymptotic speedup over classical brute-force search, then our factoring algorithm is faster than the classical NFS.
2017
-
[.pdf (mirror)] [.bib]Privacy-Preserving Patent Search: Additively Homomorphic Encryption Techniques for Private Text Mining over Public Datasets
, with Jennifer Katherine Fernick [pdf]Abstract
Machine learning on encrypted data is an emerging field that can be used for a variety of real-world applications. A particular application might be where a user has an idea for an innovative technology, and would like to confidentially submit their idea to an external platform that can semantically analyze their idea and return whether this idea has already been patented, without anyone other than the user being privy to her idea. The generalization of such a construction would be when a user wishes to make a private query to a public or third-party dataset, while maintaining the confidentiality of their query. In this paper, we make use of somewhat-homomorphic privacy- preserving building blocks for machine learning to enable this type of analysis, while extending and optimizing known theoretical constructions.
Keywords
Machine Learning, Encrypted Data, Text Mining, Data Mining, Natural Language Processing, Semantic Analysis, Patent Search, Cryptography, Additively Homomorphic Encryption, Privacy-Preserving Data Mining
2016
-
[.pdf (mirror)] [bib (dblp)](In-)Secure messaging with the Silent Circle instant messaging Protocol
, with Tanja Lange [preprint]Abstract
Silent Text, the instant messaging application by the company Silent Circle, provides its users with end-to-end encrypted communication on the Blackphone and other smartphones. The underlying protocol, SCimp, has received many extensions during the update to version 2, but has not been subjected to critical review from the cryptographic community. In this paper, we analyze both the design and implementation of SCimp by inspection of the documentation (to the extent it exists) and code. Many of the security properties of SCimp version 1 are found to be secure, however many of the extensions contain vulnerabilities and the implementation contains bugs that affect the overall security. These problems were fed back to the SCimp maintainers and some bugs were fixed in the code base. In September 2015, Silent Circle replaced SCimp with a new protocol based on the Signal Protocol.
Keywords
Cryptographic Protocols, SCimp, Silent Circle, Instant Messaging Protocol
-
[.pdf (mirror)] [.bib]OMEMO: Cryptographic Analysis Report
[report]The OMEMO protocol is a Jabber/XMPP implementation of the Signal protocol. The report contains the analysis the cryptographic properties of the specification and conducts a code-review of the reference implementation in the Conversations application for Android.
This assignment was carried out for Radically Open Security and the Pacific Research Alliance.
-
[.pdf (mirror)] [.bib]Secure messaging in mobile environments
[Masters' thesis]Abstract
Silent Text, the instant messaging application by the company Silent Circle, provides its users with secure end-to-end encrypted communication on the Blackphone and other smartphones. The underlying protocol, SCimp, has received many extensions during the update to version 2, but has not been subjected to critical review from the cryptographic community. In September 2015, Silent Circle replaced SCimp with the TextSecure protocol in the Silent Phone application. In my master thesis, I analyze both the design and implementation of SCimp by inspection of the documentation and code, and I build a formal model of the protocol using Proverif. Many of the security properties provided by the core protocol are proven in the formal model, however many of the extensions contain vulnerabilities and the implementation contains bugs that affect the overall security. A comparison between SCimp and TextSecure highlights the improvements that the latter has over the former.
Keywords
SCimp, Instant Messaging, Smartphone, ECDHE, AES, CCM mode, Silent Circle, TextSecure, Axolotl, Off the Record, C, Proverif
Supervisors
2012
-
[.pdf (mirror)] [.bib]Analysis of the Euclidean Feature Transform algorithm
[Bachelor's thesis]Abstract
In this thesis I mechanically verify the correctness and linear time complexity of the core of the Euclidean Feature Transform (EFT) algorithm, using the proof assistant PVS. The EFT algorithm computes the EFT function for a data grid of arbitrary dimension. The EFT function calculates the set of nearest "background" data points, for each data point in the grid. The distance between data points is measured by the standard Euclidean distance.
Supervisors