% Copyright (c) The mldsa-native project authors
% SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT

@article{NeonNTT,
  author  = {Hanno Becker and Vincent Hwang and Matthias J. Kannwischer and Bo-Yin Yang and Shang-Yi Yang},
  title   = {{Neon NTT}: Faster {Dilithium}, {Kyber}, and {Saber} on {Cortex-A72} and {Apple M1}},
  journal = {{IACR} Transactions on Cryptographic Hardware and Embedded Systems},
  volume  = {2022},
  number  = {1},
  pages   = {221--244},
  year    = {2022},
  note    = {Available at \url{https://eprint.iacr.org/2021/986}},
  eprint  = {2021/986},
}

@misc{Becker2022NeonNTTtalk,
  author       = {Hanno Becker and Vincent Hwang and Matthias J. Kannwischer and Bo-Yin Yang and Shang-Yi Yang},
  title        = {{Neon NTT}: Faster {Dilithium}, {Kyber}, and {Saber} on {Cortex-A72} and {Apple M1}},
  howpublished = {Talk at CHES 2022. Video: \url{https://youtu.be/TSUtA5hmrtk?t=1483}. Slides: \url{https://iacr.org/submit/files/slides/2022/tches/ches2022/1_21/slides.pptx}},
  year         = {2022},
}

@misc{AutoCorrode,
  author       = {Becker, Hanno and Chong, Nathan and Dockins, Robert and Grundy, Jim and Hu, Jason Z. S. and Mulder, Ike and Mulligan, Dominic P. and Mure, Paul and Paulson, Lawrence C. and Slind, Konrad},
  title        = {{AutoCorrode} software verification framework for {Isabelle/HOL}},
  year         = {2025},
  howpublished = {\url{https://github.com/awslabs/autocorrode}},
}

@inproceedings{Klein2009seL4,
  author    = {Klein, Gerwin and Elphinstone, Kevin and Heiser, Gernot and Andronick, June and Cock, David and Derrin, Philip and Elkaduwe, Dhammika and Engelhardt, Kai and Kolanski, Rafal and Norrish, Michael and Sewell, Thomas and Tuch, Harvey and Winwood, Simon},
  title     = {{seL4}: Formal verification of an {OS} kernel},
  booktitle = {Proceedings of the 22nd ACM Symposium on Operating Systems Principles (SOSP)},
  year      = {2009},
}

@article{Klein2014seL4,
  author  = {Klein, Gerwin and Andronick, June and Elphinstone, Kevin and Murray, Toby and Sewell, Thomas and Kolanski, Rafal and Heiser, Gernot},
  title   = {Comprehensive formal verification of an {OS} microkernel},
  journal = {ACM Transactions on Computer Systems},
  volume  = {32},
  number  = {1},
  year    = {2014},
}

@article{Hales2017Kepler,
  author  = {Hales, Thomas and Adams, Mark and Bauer, Gertrud and Dang, Tat Dat and Harrison, John and Hoang, Le Truong and Kaliszyk, Cezary and Magron, Victor and McLaughlin, Sean and Nguyen, Tat Thang and others},
  title   = {A formal proof of the {Kepler} conjecture},
  journal = {Forum of Mathematics, Pi},
  volume  = {5},
  year    = {2017},
}

@misc{AppleCorecrypto2025,
  author       = {{Apple Security Engineering and Architecture}},
  title        = {Formal verification of {corecrypto}},
  year         = {2025},
  howpublished = {\url{https://security.apple.com/blog/formal-verification-corecrypto/}},
}

@misc{AWSNitro2025,
  author       = {{Amazon Web Services}},
  title        = {{Isabelle/HOL}: The proof assistant behind the {Nitro Isolation Engine}},
  year         = {2025},
  howpublished = {\url{https://www.amazon.science/blog/isabelle-hol-the-proof-assistant-behind-the-nitro-isolation-engine}},
  key          = {NIE},
}

@misc{AFP,
  author       = {{Archive of Formal Proofs}},
  title        = {Archive of Formal Proofs},
  howpublished = {\url{https://www.isa-afp.org}},
  key          = {AFP},
}

@article{CryptoLine2022,
  author  = {Hwang, Vincent and Liu, Jiaxiang and Seiler, Gregor and Shi, Xiaomu and Tsai, Ming-Hsien and Wang, Bow-Yaw and Yang, Bo-Yin},
  title   = {Verified {NTT} Multiplications for {NISTPQC} {KEM} Lattice Finalists: {Kyber}, {SABER}, and {NTRU}},
  journal = {IACR Transactions on Cryptographic Hardware and Embedded Systems},
  volume  = {2022},
  number  = {4},
  pages   = {718--750},
  year    = {2022},
}

@article{CryptoLine2025,
  author  = {Chiu, Chun-Ming and Liu, Jiaxiang and Tsai, Ming-Hsien and Shi, Xiaomu and Wang, Bow-Yaw and Yang, Bo-Yin},
  title   = {Algebraic Linear Analysis for Number Theoretic Transform in Lattice-Based Cryptography},
  journal = {IACR Transactions on Cryptographic Hardware and Embedded Systems},
  volume  = {2025},
  number  = {3},
  pages   = {668--692},
  year    = {2025},
}

@article{FormosaCrypto,
  author  = {Bacelar Almeida, Jos\'{e} and Barbosa, Manuel and Barthe, Gilles and Gr\'{e}goire, Benjamin and Laporte, Vincent and L\'{e}chenet, Jean-Christophe and Oliveira, Tiago and Pacheco, Hugo and Quaresma, Miguel and Schwabe, Peter and S\'{e}r\'{e}, Antoine and Strub, Pierre-Yves},
  title   = {Formally verifying {Kyber}: Episode {IV}: Implementation correctness},
  journal = {IACR Transactions on Cryptographic Hardware and Embedded Systems},
  volume  = {2023},
  number  = {3},
  pages   = {164--193},
  year    = {2023},
}

@misc{mlkemnative,
  author       = {{pq-code-package contributors}},
  title        = {\texttt{mlkem-native}: Secure, fast, and portable {C90} implementation of {ML-KEM} / {FIPS}~203},
  year         = {2025},
  howpublished = {\url{https://github.com/pq-code-package/mlkem-native}},
}

@misc{mldsanative,
  author       = {{pq-code-package contributors}},
  title        = {\texttt{mldsa-native}: Secure, fast, and portable {C90} implementation of {ML-DSA} / {FIPS}~204},
  year         = {2025},
  howpublished = {\url{https://github.com/pq-code-package/mldsa-native}},
}

@techreport{FIPS203,
  author       = {{National Institute of Standards and Technology}},
  title        = {{Module-Lattice-Based Key-Encapsulation Mechanism Standard}},
  institution  = {U.S. Department of Commerce},
  number       = {{Federal Information Processing Standards Publication (FIPS)} 203},
  year         = {2024},
  month        = aug,
  doi          = {10.6028/NIST.FIPS.203},
  key          = {FIPS203},
}

@techreport{FIPS204,
  author       = {{National Institute of Standards and Technology}},
  title        = {{Module-Lattice-Based Digital Signature Standard}},
  institution  = {U.S. Department of Commerce},
  number       = {{Federal Information Processing Standards Publication (FIPS)} 204},
  year         = {2024},
  month        = aug,
  doi          = {10.6028/NIST.FIPS.204},
  key          = {FIPS204},
}
