@misc{Shoup2004IACR,
  author = {Victor Shoup},
  title = {Sequences of Games: A tool for taming complexity in security proofs},
  howpublished = {Cryptology ePrint Archive, Report 2004/332},
  year = {2004},
}

@inproceedings{Lochbihler2016ESOP,
  author = {Andreas Lochbihler},
  title = {Probabilistic Functions and Cryptographic Oracles in Higher Order Logic},
  editor = {Peter Thiemann},
  booktitle = {Programming Languages and Systems (ESOP 2016)},
  volume = 9632,
  series = {LNCS},
  year = 2016,
  publisher = {Springer},
  pages = {503--531},
  doi = {10.1007/978-3-662-49498-1_20},
}

@inproceedings{BellareRogaway2006EUROCRYPT,
  author = {Mihir Bellare and Phillip Rogaway},
  title = {The Security of Triple Encryption and a Framework for Code-Based Game-Playing Proofs},
  editor_long = {Serge Vaudenay},
  booktitle_long = {Advances in Cryptology (EUROCRYPT 2006)},
  booktitle = {EUROCRYPT 2006},
  year = {2006},
  volume = {4004},
  series = {LNCS},
  doi = {10.1007/11761679_25},
  publisher = {Springer},
  pages = {409--426},
}

@inproceedings{BellareBoldyrevaMicali2000EUROCRYPT,
  author = {Mihir Bellare and Alexandra Boldyreva and Silvio Micali},
  title = {Public-Key Encryption in a Multi-user Setting: Security Proofs and Improvements},
  editor = {Bart Preneel},
  booktitle = {Advances in Cryptology (EUROCRYPT 2000)},
  year = {2000},
  volume = {1807},
  series = {Lecture Notes in Computer Science},
  doi = {10.1007/3-540-45539-6_18},
  publisher = {Springer Berlin Heidelberg},
  pages = {259--274},
}

@inproceedings{PetcherMorrisett2015POST,
  author = {Adam Petcher and Greg Morrisett},
  title = {The Foundational Cryptography Framework},
  editor_long = {Riccardo Focardi and Andrew Myers},
  booktitle_long = {Principles of Security and Trust (POST 2015)},
  booktitle = {POST 2015},
  year = {2015},
  volume = {9036},
  series = {LNCS},
  doi = {10.1007/978-3-662-46666-7_4},
  publisher = {Springer},
  pages = {53--72},
}

@Article{Diffie1976,
  author={Diffie, Whitfield and Hellman, Martin},
  title={New Directions in Cryptography},
  journal={IEEE Transactions on Information Theory},
  year={1976},
  volume={22},
  number={6},
  pages={644--654}
}

@InProceedings{Goldwasser1982,
  author={Goldwasser, Shafi and Micali, Silvio},
  title={Probabilistic Encryption \& How to Play Mental Poker Keeping Secret All Partial Information},
  booktitle={ACM Symposium on Theory of Computing  ({STOC} 1982), Proceedings},
  year={1982},
  pages={365--377}
}

@Article{Goldwasser1984,
  author={Goldwasser Shafi and Silvio Micali},
  title={Probabilistic Encryption},
  journal={Journal of Computer and System Sciences},
  year={1984},
  volume={28},
  number={2},
  pages={270--299}
}

@Article{Elgamal1985,
  author={ElGamal, Taher},
  title={A Public Key Cryptosystem and a Signature Scheme Based on Discrete Logarithms},
  journal={IEEE Transactions on Information Theory},
  year={1985},
  volume={31},
  number={4},
  pages={469--472}
}

@InProceedings{Mitchell1986,
  author = {Mitchell, John C},
  title = {Representation Independence and Data Abstraction},
  booktitle = {ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages ({POPL} 1986), Proceedings},
  year = {1986},
  pages = {263--276}
} 

@InProceedings{Wadler1989,
  author={Wadler, Philip and Blott, Stephen},
  title={How to Make Ad-Hoc Polymorphism Less Ad Hoc},
  booktitle={ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages ({POPL} 1989), Proceedings},
  year={1989},
  pages={60--76}
}

@InProceedings{Wenzel1999,
  author= {Wenzel, Markus},
  title= {Isar --- A Generic Interpretative Approach to Readable Formal Proof Documents},
  booktitle={International Conference on Theorem Proving in Higher Order Logics ({TPHOL} 1999), Proceedings},
  year={1999},
  pages={167--183}
}

@Book{Nipkow2002,
  author    = {Nipkow, Tobias and Paulson, Lawrence C and Wenzel, Markus},
  title     = {Isabelle/HOL - {A} Proof Assistant for Higher-Order Logic},
  publisher = {Springer},
  year      = {2002},
  volume    = {2283},
  series    = {Lecture Notes in Computer Science}
}

@PhdThesis {Krauss2009,
  author = {Krauss, Alexander},
  title = {Automating Recursive Definitions and Termination Proofs in Higher-Order Logic},
  type = {Dissertation},
  school = {Technische Universit\"at M\"unchen},
  year = {2009}
}

@InProceedings{Huffman2013,
  author = {Huffman, Brian and Kun{\v{c}}ar, Ond{\v{r}}ej},
  title = {Lifting and {Transfer}: A Modular Design for Quotients in {Isabelle/HOL}},
  booktitle = {Certified Programs and Proofs ({CPP} 2013), Proceedings},
  year = {2013},
  pages = {131--146}
}

@Article{Ballarin2014,
  author={Ballarin, Clemens},
  title={Locales: A Module System for Mathematical Theories},
  journal={Journal of Automated Reasoning},
  year={2014},
  month={Feb},
  volume={52},
  number={2},
  pages={123--153}
}

@Article{Eberl2015,
  author  = {Eberl, Manuel},
  title   = {Landau Symbols},
  journal = {Archive of Formal Proofs},
  month   = {Jul},
  year    = {2015},
  note    = {\url{http://isa-afp.org/entries/Landau_Symbols.html},
            Formal proof development},
  ISSN    = {2150-914x}
}

@Article{Schneider2017,
  author  = {Schneider, Joshua and Eberl, Manuel and Lochbihler, Andreas},
  title   = {Monad normalisation},
  journal = {Archive of Formal Proofs},
  month   = {May},
  year    = {2017},
  note    = {\url{http://isa-afp.org/entries/Monad_Normalisation.html},
            Formal proof development},
  ISSN    = {2150-914x}
}

@InProceedings{Lochbihler2016,
  author    = {Lochbihler, Andreas},
  title     = {Probabilistic Functions and Cryptographic Oracles in Higher Order Logic},
  booktitle = {European Symposium on Programming ({ESOP} 2016), Proceedings},
  year      = {2016},
  pages     = {503--531}
}

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

@Article{Lochbihler2017b,
  author    = {Lochbihler, Andreas and Sefidgar, S Reza and Bhatt, Bhargav},
  title     = {Game-based cryptography in HOL},
  journal   = {Archive of Formal Proofs},
  year      = {2017},
  note      = {~\url{http://isa-afp.org/entries/Game\_Based\_Crypto.shtml},
            Formal proof development}
}

@Article{Basin2017,
  author    = {Basin, David A and Lochbihler, Andreas and Sefidgar, S Reza},
  title     = {CryptHOL: Game-based Proofs in Higher-order Logic},
  journal   = {{IACR} Cryptology ePrint Archive},
  year      = {2017},
  volume    = {2017},
  pages     = {753}
}






