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.