Side-channel attacks (SCA) play a crucial role in assessing the security of the implementation of cryp- tographic algorithms. Still, traditional profiled attacks require a nearly identical reference device to the target, limiting their practicality. This thesis focuses on non-profiled SCA, which provides a re- alistic alternative when the attacker lacks access to a profiling device. Specifically, we investigate non-profiled deep learning-based SCA techniques. Our evaluation first explores existing unsupervised deep learning-based side-channel analysis approaches: differential deep learning analysis (DDLA) and multi-output regression (MOR). We show that using a validation set for key distinguishing, rather than the training set, improves the overall success rate across various datasets.
In the context of multi-output regression SCA, we comprehensively evaluate different loss functions. The thesis proposes a novel approach that outperforms existing methods by employing the normalized Z-score MSE (Z-MSE) loss function. Additionally, we introduce two key distinguishing methods, one based on the smallest Z-MSE loss and the other on the highest Pearson correlation between actual and predicted labels during validation. The experimental results show the efficacy of the novel approach in breaking traces protected by countermeasures. Notably, even with high levels of desynchronization (250) for ASCADf traces, the attack succeeds within a limited number of epochs (15).
Moreover, we demonstrate that the performance of the novel approach can be further enhanced through ensembles. This leads to a reduction in the number of traces required to break the key for most datasets and a decrease in the average guessing entropy. Data augmentation also proves beneficial in some instances, resulting in improved success rates.

agda2hs is a project that aims to combine the best parts of Haskell and Agda by providing a common subset between them. It allows programmers to im- plement libraries in Agda, verify their correctness and then translate the result to Haskell so they can be used by Haskell programmers. In this paper, a verified Agda implementation of the Ranged-sets Haskell library is provided, using agda2hs. In or- der to produce a verified implementation of this li- brary, we proved its preconditions, invariants and properties.