Denne oppgaven beskriver kryptosystemene ElGamal, Kyber, og gir en skisse for hvor- dan man kan bruke EasyCrypt for å verifisere sikkerheten til systemene. Oppgaven begyn- ner med en beskrivelse av ElGamal, komplementert av et skriftlig bevis av korrekthet, og et for IND-CPA sikkerhet. Videre beskrives Kyber IND-CPA PKE spesifikasjonen, igjen komplementert av et skriftlig bevis av korrekthet, og et for IND-CPA sikkerhet. Videre vil Fujisaka-Okamoto transformen beskrives, noe som gir oss Kyber IND-CCA KEM. Etter dette beskrives verktøyet EasyCrypt, som så blir brukt til å bevise korrektheten og IND- CPA sikkerhet i ElGamal. Til slutt er det en kort diskusjon rundt utfordringer med bevis av Kyber i EasyCrypt.

This thesis describes the cryptographic schemes ElGamal and Kyber, and outlines how EasyCrypt can be used to verify the security of these systems. It begins with a description of ElGamal, accompanied by a written proof of correctness and a proof of IND-CPA security. Next, the Kyber IND-CPA PKE specification is presented, also supported by written proofs of correctness and IND-CPA security. The Fujisaki–Okamoto transform is then described, yielding Kyber IND-CCA KEM. Following this, the EasyCrypt tool is introduced and used to prove the correctness and IND-CPA security of ElGamal. Finally, the thesis includes a brief discussion of the challenges involved in proving the security of Kyber in EasyCrypt.