@INPROCEEDINGS{kyber,

  author={Joppe Bos and L{\'e}o Ducas and Eike Kiltz and Tancr{\`e}de Lepoint and Vadim Lyubashevsky and John M. Schanck and Peter Schwabe and Gregor Seiler and Damien Stehl{\'e}},
  booktitle={2018 IEEE European Symposium on Security and Privacy}, 
  title={{CRYSTALS --- Kyber: A CCA-Secure Module-Lattice-Based KEM}}, 
  year={2018},
  volume={},
  number={},
  pages={353-367},
}

@inproceedings{KyberAS,
  title={{CRYSTALS-Kyber Algorithm Specifications And Supporting Documentation}},
  author={Roberto Maria Avanzi and Joppe W. Bos and L{\'e}o Ducas and Eike Kiltz and Tancr{\`e}de Lepoint and Vadim Lyubashevsky and John M. Schanck and Peter Schwabe and Gregor Seiler and Damien Stehl{\'e}},
  year={2017}
}


@inproceedings{KyberRound2,
  title={{CRYSTALS-Kyber Algorithm Specifications And Supporting Documentation (version 2.0)}},
  author={Roberto Maria Avanzi and Joppe W. Bos and L{\'e}o Ducas and Eike Kiltz and Tancr{\`e}de Lepoint and Vadim Lyubashevsky and John M. Schanck and Peter Schwabe and Gregor Seiler and Damien Stehl{\'e}},
  year={30/03/2019}
}

@inproceedings{KyberRound3,
  title={{CRYSTALS-Kyber Algorithm Specifications And Supporting Documentation (version 3.0)}},
  author={Roberto Maria Avanzi and Joppe W. Bos and L{\'e}o Ducas and Eike Kiltz and Tancr{\`e}de Lepoint and Vadim Lyubashevsky and John M. Schanck and Peter Schwabe and Gregor Seiler and Damien Stehl{\'e}},
  year={01/10/2020}
}

@misc{report3rdroundNIST,
  author = {Gorjan Alagic and David A. Cooper and Quynh Dang and Thinh Dang and John M. Kelsey and Jacob Lichtinger and Yi-Kai Liu and Carl A. Miller and Dustin Moody and Rene Peralta and Ray Perlner and Angela Robinson and Daniel Smith-Tone and Daniel Apon},
  title = {{Status Report on the Third Round of the NIST Post-Quantum Cryptography Standardization Process}},
  year = {2022},
  month = {2022-07-05 04:07:00},
  publisher = {NIST Interagency/Internal Report (NISTIR), National Institute of Standards and Technology, Gaithersburg, MD},
  language = {en},
}

@article{NTT,
  author  = {Thomas Ammer and Katharina Kreuzer},
  title   = {Number Theoretic Transform},
  journal = {Archive of Formal Proofs},
  month   = {August},
  year    = {2022},
  note    = {\url{https://isa-afp.org/entries/Number_Theoretic_Transform.html},
            Formal proof development},
  ISSN    = {2150-914x},
}

@article{Formalization,
  author  = {Katharina Kreuzer},
  title   = {{CRYSTALS}-{K}yber},
  journal = {Archive of Formal Proofs},
  month   = {September},
  year    = {2022},
  note    = {\url{https://isa-afp.org/entries/CRYSTALS-Kyber.html},
            Formal proof development},
  ISSN    = {2150-914x},
}

@misc{CryptHOLTutorial,
      author = {Andreas Lochbihler and S.  Reza Sefidgar},
      title = {A tutorial introduction to {C}rypt{HOL}},
      howpublished = {Cryptology ePrint Archive, Paper 2018/941},
      year = {2018},
      note = {\url{https://eprint.iacr.org/2018/941}},
      url = {https://eprint.iacr.org/2018/941}
}

@article{CryptHOL-AFP,
  author  = {Andreas Lochbihler},
  title   = {Crypt{HOL}},
  journal = {Archive of Formal Proofs},
  month   = {May},
  year    = {2017},
  note    = {\url{https://isa-afp.org/entries/CryptHOL.html},
            Formal proof development},
  ISSN    = {2150-914x},
}

@article{moduleLWE,
	title = {Worst-{C}ase to {A}verage-{C}ase {R}eductions for {M}odule {L}attices},
	volume = {75},
	number = {3},
	journal = {Des. Codes Cryptogr.},
	author = {Adeline Langlois and Damien Stehlé},
	month = jun,
	year = {2015},
	pages = {565--599},
}

@INPROCEEDINGS {PaperTBD,
author = {Katharina Kreuzer},
booktitle = {2024 IEEE 37th Computer Security Foundations Symposium (CSF)},
title = {{V}erification of {C}orrectness and {S}ecurity {P}roperties for {CRYSTALS-KYBER}},
year = {2024},
volume = {},
issn = {},
pages = {TBD},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA}
}

