The Iterated Even-Mansour (IEM) construction was introduced by Bogdanov et al. at EUROCRYPT 2012 and can be seen as an abstraction or idealization of blockciphers like AES. IEM provides insights into the soundness of this blockcipher structure and the best possible security for any number of rounds. IEM with r permutations on n-bit blocks is secure up to q≈2^(rn/(r+1)) queries to the cipher and each permutation. Forkciphers, introduced at ASIACRYPT 2019 as expanding symmetric ciphers, have since found applications in encryption, authenticated encryption and key derivation. Kim et al. (ToSC 2020) proposed the first IEM-style forkcipher, FTEM, but their security proof is limited to a 2-round design with tweak processing based on XORing AXU hashes. This offers limited insight into practical forkciphers like ForkSkinny, which use 40 to 56 rounds and a different tweak schedule. No security results currently exist for forked IEM constructions with more than two rounds. We propose a generalized forked IEM construction called GIEM which integrates any tweakey schedule (including tweak-dependent round keys or constant keys) and thus encompasses IEM, FTEM and similar IEM-related constructions. We define three forkcipher-related instantiations, FEM (2 branches and no tweaks), FTEMid (2 branches and idealized tweakey schedule) and MFTEM (unlimited branches and AXU-based tweakey schedule). We prove that each construction achieves security similar to the respective non-forked construction. This shows the soundness of the forking design strategy and can serve as a basis for new constructions with more than two branches. In their work, Bogdanov et al. also propose an attack against IEM using q≈2^(rn/(r+1)) queries, which is used in a number of follow-up works to argue the tightness of IEM-related security bounds. In this work, we demonstrate that the attack is ineffective with the specified query complexity. To salvage the purported tightness results, we turn to an attack by Gazi (CRYPTO 2013) against cascading block ciphers and provide the necessary parameters to apply it to IEM. This validates the tightness of the known IEM security bound.

Most cryptographic applications use randomness that is generated by pseudo-random number generators (PRNGs). A popular PRNG practical choice is the NIST standardized CTR_DRBG. In their recent ACNS 2023 publication, Andreeva and Weninger proposed a new and more efficient and secure PRNG called FCRNG. FCRNG is based on CTR_DRBG and uses the 𝑛-to-2𝑛 forkcipher expanding primitive ForkSkinny as a building block. In this work, we create a new BKRNG PRNG, which is based on FCRNG and employs the novel 𝑛-to-8𝑛 expanding primitive Butterknife. Butterknife is based on the Deoxys tweakable blockcipher (and thus AES) and realizes a tweakable expanding pseudo-random function. While both blockciphers and forkciphers are invertible primitives, tweakable expanding pseudo-random functions are not. This functional simplification enables security benefits for BKRNG in the robustness security game - the standard security goal for a PRNG. Contrary to the security bound of CTR_DRBG, we show that the security of our BKRNG construction does not degrade with the length of the random inputs, nor the number of requested output pseudo-random bits. We also empirically verify the BKRNG security with the NIST PRNG test suite and the TestU01 suite. Furthermore, we show the 𝑛-to-8𝑛 multi-branch expanding nature of Butterknife contributes to a significant speed-up in the efficiency of BKRNG compared to FCRNG. More concretely, producing random bits with BKRNG is 30.0% faster than FCRNG and 49.2% faster than CTR_DRBG.

Good randomness is needed for most cryptographic applications. In practice pseudo-random number generators (PRNGs) are employed. CTR_DRBG is a popular choice and among the recommended PRNGs by NIST. It is defined for use with primitives like AES or TDEA, which are not always suited for lightweight applications. In this work we propose FCRNG, a new PRNG, similar to CTR_DRBG, that is optimized for the lightweight setting (e.g. the Internet of Things). Our FCRNG construction utilizes the expanding and tweakable forkcipher primitive instantiated with ForkSkinny, which was introduced by Andreeva et al. at ASIACRYPT 2019. FCRNG employs internally a forkcipher-based counter-style mode FCTR. We propose two FCTR variants: FCTR-c for optimized speed and FCTR-T for optimized security. We then show that FCRNG with ForkSkinny can be 33% faster than CTR_DRBG when instantiated with the AES blockcipher. FCRNG achieves also a better security bound in the robustness security game - first introduced by Dodis et al. at CCS’13 and now the standard security goal for PRNGs. Contrary to the CRYPTO 2020 security bound by Hoang and Shen established for CTR_DRBG, the security of our construction with FCTR-T does not degrade with the length of the random inputs, nor the amount of requested output pseudorandom bits. FCRNG passes all tests of the NIST test suite for pseudorandom number generators.

Privacy preserving authenticated key exchange (PPAKE) protocols are authenticated key exchange (AKE) protocols that aim to hide the identities of the communicating parties from third parties. Hence the security models of AKE are extended with additional properties. PPAKE protocols have been studied previously. Our aim is to strengthen the existing privacy properties of such protocols. Most notably we additionally consider attacks in which the adversary does not complete the protocol run (e.g. due to the inability to authenticate itself). These attacks are relevant because since some adversaries might not even care if the protocol run is aborted after they deanonymize their target. Furthermore we introduce a formal model that incorporates these properties and several protocols that fulfill different levels of privacy. One of the protocols is a generic construction from generic cryptographic building blocks and hence allows for a post-quantum secure instantiation. Additonally we present formal proofs of all protocols in our model. The second part of this thesis deals with the automated verification of the privacy properties of the main protocol of the first part. Automated verification is used to either find an attack or conclude that the specified properties indeed hold. This gives additional confidence in the correctness of the security proofs contained in this work. First we evaluated the protocol using the Tamarin Prover, which however is unable to finish its proof or find a contradiction with the given resources (approx. 60 GB memory). Then we utilized the verification software ProVerif and were able to prove the security of the protocol. We will present both the Tamarin Prover encoding as well as the ProVerif encoding.