dc.contributor.author Nejati, Saeed dc.date.accessioned 2020-05-15 16:55:28 (GMT) dc.date.available 2020-05-15 16:55:28 (GMT) dc.date.issued 2020-05-15 dc.date.submitted 2020-05-15 dc.identifier.uri http://hdl.handle.net/10012/15868 dc.description.abstract Over the last two decades, we have seen a dramatic improvement in the efficiency of conflict-driven clause-learning Boolean satisfiability (CDCL SAT) solvers over industrial problems from a variety of applications such as verification, testing, security, and AI. The availability of such powerful general-purpose search tools as the SAT solver has led many researchers to propose SAT-based methods for cryptanalysis, including techniques for finding collisions in hash functions and breaking symmetric encryption schemes. en A feature of all of the previously proposed SAT-based cryptanalysis work is that they are \textit{blackbox}, in the sense that the cryptanalysis problem is encoded as a SAT instance and then a CDCL SAT solver is invoked to solve said instance. A weakness of this approach is that the encoding thus generated may be too large for any modern solver to solve it efficiently. Perhaps a more important weakness of this approach is that the solver is in no way specialized or tuned to solve the given instance. Finally, very little work has been done to leverage parallelism in the context of SAT-based cryptanalysis. To address these issues, we developed a set of methods that improve on the state-of-the-art SAT-based cryptanalysis along three fronts. First, we describe an approach called \cdcl (inspired by the CDCL($T$) paradigm) to tailor the internal subroutines of the CDCL SAT solver with domain-specific knowledge about cryptographic primitives. Specifically, we extend the propagation and conflict analysis subroutines of CDCL solvers with specialized codes that have knowledge about the cryptographic primitive being analyzed by the solver. We demonstrate the power of this framework in two cryptanalysis tasks of algebraic fault attack and differential cryptanalysis of SHA-1 and SHA-256 cryptographic hash functions. Second, we propose a machine-learning based parallel SAT solver that performs well on cryptographic problems relative to many state-of-the-art parallel SAT solvers. Finally, we use a formulation of SAT into Bayesian moment matching to address heuristic initialization problem in SAT solvers. dc.language.iso en en dc.publisher University of Waterloo en dc.subject SAT Solvers en dc.subject Cryptography en dc.subject machine learning en dc.title CDCL(Crypto) and Machine Learning based SAT Solvers for Cryptanalysis en dc.type Doctoral Thesis en dc.pending false uws-etd.degree.department Electrical and Computer Engineering en uws-etd.degree.discipline Electrical and Computer Engineering en uws-etd.degree.grantor University of Waterloo en uws-etd.degree Doctor of Philosophy en uws.contributor.advisor Ganesh, Vijay uws.contributor.advisor Gebotys, Catherine uws.contributor.affiliation1 Faculty of Engineering en uws.published.city Waterloo en uws.published.country Canada en uws.published.province Ontario en uws.typeOfResource Text en uws.peerReviewStatus Unreviewed en uws.scholarLevel Graduate en
﻿

### This item appears in the following Collection(s)

UWSpace

University of Waterloo Library
200 University Avenue West