Commit 8136df9c authored by Peter Schwabe's avatar Peter Schwabe
Browse files

Minor fixes in collection.bib

parent 8332bb44
......@@ -57,8 +57,6 @@ machine code by refinement; the second is to formalize
a specification and then verify that some
implementation satisfies it.
% One of the earliest example of this first approach is the
% B-method~\cite{Abrial:1996:BAP:236705} in 1986.
The synthesis approach was used by Zinzindohou{\'{e}}, Bartzia, and Bhargavan to build a verified extensible
library of elliptic curves~\cite{Zinzindohoue2016AVE} in F*~\cite{DBLP:journals/corr/BhargavanDFHPRR17}.
This served as ground work for the cryptographic library HACL*~\cite{zinzindohoue2017hacl}
......
@STRING{LNCS = {LNCS}}
@STRING{SV = {Springer}}
@article{1969-Hoare,
author = {C. A. R. Hoare},
title = {An Axiomatic Basis for Computer Programming},
journal = {Commun. ACM},
year = {1969},
publisher = {ACM},
volume = {12},
number = {10},
year = {1969},
pages = {576-580},
month = {oct},
note = {\url{http://doi.acm.org/10.1145/363235.363259}},
_acmid = {363259},
_issn = {0001-0782},
}
@article{2007-Blazy-C-chronique,
author = {Sandrine Blazy},
title = {Comment gagner confiance en {C} ?},
journal = {Technique et Science Informatiques},
year = {2007},
publisher = {Lavoisier},
volume = {26},
number = {9},
year = {2007},
pages = {1195-1200},
month = {June},
note = {\url{http://hal.inria.fr/inria-00292049/}},
_hal = {http://hal.inria.fr/inria-00292049/},
_pubkind = {journal-fr-mono},
}
@inproceedings{2012-Appel,
author = {Andrew W. Appel},
title = {Verified Software Toolchain},
booktitle = {{NASA} Formal Methods - 4th International Symposium, {NFM} 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings},
year = {2012},
editor = {Alwyn Goodloe and Suzette Person},
volume = {7226},
publisher = SV,
series = LNCS,
volume = {7226},
year = {2012},
pages = {2},
publisher = SV,
note = {\url{https://doi.org/10.1007/978-3-642-28891-3_2}},
}
@article{2015-Appel,
author = {Andrew W. Appel},
title = {Verification of a Cryptographic Primitive: SHA-256},
title = {Verification of a Cryptographic Primitive: {SHA-256}},
journal = {{ACM} Transactions on Programming Languages and Systems},
year = {2015},
publisher = {ACM},
volume = {37},
number = {2},
year = {2015},
pages = {7:1--7:31},
month = {Apr},
note = {\url{http://doi.acm.org/10.1145/2701415}},
}
@book{Abrial:1996:BAP:236705,
author = {Jean-Raymond Abrial},
editor = {},
title = {The B-book: Assigning Programs to Meanings},
publisher = {Cambridge University Press},
year = {1996},
address = {New York, NY, USA},
_isbn = {0-521-49619-5},
}
@inproceedings{BGJ+15,
author = {Daniel J. Bernstein and
Bernard van Gastel and
Wesley Janssen and
Tanja Lange and
Peter Schwabe and
Sjaak Smetsers},
author = {Daniel J. Bernstein and Bernard van Gastel and Wesley Janssen and Tanja Lange and
Peter Schwabe and Sjaak Smetsers},
title = {{TweetNaCl}: A crypto library in 100 tweets},
booktitle = {Progress in Cryptology -- {LATINCRYPT 2014}},
year = {2015},
editor = {Diego Aranha and Alfred Menezes},
volume = {8895},
publisher = SV,
series = LNCS,
volume = {8895},
year = {2015},
pages = {64--83},
publisher = SV,
note = {Document ID: c74b5bbf605ba02ad8d9e49f04aca9a2, \url{http://cryptojedi.org/papers/\#tweetnacl}},
note = {\url{http://cryptojedi.org/papers/\#tweetnacl}},
}
@inproceedings{BLS12,
author = {Daniel J. Bernstein and
Tanja Lange and
Peter Schwabe},
author = {Daniel J. Bernstein and Tanja Lange and Peter Schwabe},
title = {The security impact of a new cryptographic library},
booktitle = {Progress in Cryptology -- {LATINCRYPT 2012}},
year = {2012},
editor = {Alejandro Hevia and Gregory Neven},
volume = {7533},
publisher = SV,
series = LNCS,
volume = {7533},
year = {2012},
pages = {159--176},
publisher = SV,
note = {Document ID: 5f6fc69cc5a319aecba43760c56fab04, \url{http://cryptojedi.org/papers/\#coolnacl}},
note = {\url{http://cryptojedi.org/papers/\#coolnacl}},
}
@inproceedings{BartziaS14,
author = {Evmorfia-Iro Bartzia and
Pierre-Yves Strub},
title = {A Formal Library for Elliptic Curves in the Coq Proof Assistant},
author = {Evmorfia-Iro Bartzia and Pierre-Yves Strub},
title = {A Formal Library for Elliptic Curves in the {Coq} Proof Assistant},
booktitle = {Interactive Theorem Proving},
year = {2014},
editor = {Gerwin Klein and Ruben Gamboa},
volume = {8558},
series = LNCS,
pages = {77-92},
address = {Cham},
publisher = SV,
series = LNCS,
volume = {8558},
year = {2014},
pages = {77--92},
note = {\url{https://hal.inria.fr/hal-01102288}},
}
......@@ -127,18 +95,16 @@
author = {Daniel J. Bernstein},
title = {Curve25519: new {D}iffie-{H}ellman speed records},
booktitle = {Public Key Cryptography -- {PKC 2006}},
year = {2006},
editor = {Moti Yung and Yevgeniy Dodis and Aggelos Kiayias and Tal Malkin},
volume = {3958},
publisher = SV,
series = LNCS,
volume = {3958},
year = {2006},
pages = {207--228},
publisher = SV,
note = {\url{http://cr.yp.to/papers.html\#curve25519}},
}
@misc{Ber14,
author = {Daniel J. Bernstein},
title = {25519 naming},
howpublished = {Posting to the CFRG mailing list},
......@@ -148,108 +114,68 @@
}
@inproceedings{Beringer2015VerifiedCA,
author = {Lennart Beringer and
Adam Petcher and
Katherine Q. Ye and
Andrew W. Appel},
title = {Verified Correctness and Security of OpenSSL {HMAC}},
booktitle = {24th {USENIX} Security Symposium ({USENIX} Security 15)},
author = {Lennart Beringer and Adam Petcher and Katherine Q. Ye and Andrew W. Appel},
title = {Verified Correctness and Security of {OpenSSL} {HMAC}},
booktitle = {Proceedings of the 24th {USENIX} Security Symposium},
publisher = {{USENIX} Association},
year = {2015},
pages = {207--221},
address = {Washington, D.C.},
publisher = {{USENIX} Association},
note = {\url{https://www.cs.cmu.edu/~kqy/resources/verified-hmac.pdf}},
}
@article{Blazy-Leroy-Clight-09,
author = {Sandrine Blazy and
Xavier Leroy},
author = {Sandrine Blazy and Xavier Leroy},
title = {Mechanized semantics for the {Clight} subset of the {C} language},
journal = {Journal of Automated Reasoning},
year = {2009},
publisher = SV,
volume = {43},
number = {3},
year = {2009},
pages = {263-288},
month = {Oct},
note = {\url{http://gallium.inria.fr/~xleroy/publi/Clight.pdf}},
_hal = {http://hal.inria.fr/inria-00352524/},
_urlpublisher = {http://dx.doi.org/10.1007/s10817-009-9148-3},
}
@inproceedings{Chen2014VerifyingCS,
author = {Yu-Fang Chen and
Chang-Hong Hsu and
Hsin-Hung Lin and
Peter Schwabe and
Ming-Hsien Tsai and
Bow-Yaw Wang and
Bo-Yin Yang and
Shang-Yi Yang},
title = {Verifying Curve25519 Software},
author = {Yu-Fang Chen and Chang-Hong Hsu and Hsin-Hung Lin and Peter Schwabe and
Ming-Hsien Tsai and Bow-Yaw Wang and Bo-Yin Yang and Shang-Yi Yang},
title = {Verifying {Curve25519} Software},
booktitle = {Proceedings of the 2014 {ACM} {SIGSAC} Conference on Computer and Communications Security},
publisher = {ACM},
year = {2014},
series = {CCS '14},
pages = {299--309},
address = {New York, NY, USA},
month = {Nov},
publisher = {ACM},
note = {\url{https://cryptojedi.org/papers/verify25519-20140428.pdf}},
note = {\url{https://cryptojedi.org/papers/\#verify25519.pdf}},
}
@article{CpdtJFR,
author = {Adam Chlipala},
title = {An Introduction to Programming and Proving with Dependent Types in Coq},
title = {An Introduction to Programming and Proving with Dependent Types in {Coq}},
journal = {Journal of Formalized Reasoning},
publisher = {University of Bologna},
year = {2010},
volume = {3(2)},
pages = {1-93},
note = {\url{http://adam.chlipala.net/papers/CpdtJFR/}},
}
@inproceedings{DBLP:journals/corr/BhargavanDFHPRR17,
author = {Karthikeyan Bhargavan and
Antoine Delignat{-}Lavaud and
C{\'{e}}dric Fournet and
Catalin Hritcu and
Jonathan Protzenko and
Tahina Ramananandro and
Aseem Rastogi and
Nikhil Swamy and
Peng Wang and
Santiago Zanella B{\'{e}}guelin and
Jean Karim Zinzindohou{\'{e}}},
author = {Karthikeyan Bhargavan and Antoine Delignat{-}Lavaud and C{\'{e}}dric Fournet and Catalin Hritcu and
Jonathan Protzenko and Tahina Ramananandro and Aseem Rastogi and Nikhil Swamy and
Peng Wang and Santiago Zanella B{\'{e}}guelin and Jean Karim Zinzindohou{\'{e}}},
title = {Verified Low-Level Programming Embedded in {F*}},
booktitle = {Proceedings of the {ACM} on Programming Languages},
year = {2017},
publisher = {ACM},
volume = {1},
number = {ICFP},
year = {2017},
pages = {17},
month = {Sep},
publisher = {ACM},
note = {\url{http://arxiv.org/abs/1703.00053}},
}
@misc{Erbsen2016SystematicSO,
author = {Andres Erbsen and
Jason Gross and
Adam Chlipala},
title = {Systematic Synthesis of Elliptic Curve Cryptography Implementations},
year = {2016},
note = {\url{https://people.csail.mit.edu/jgross/personal-website/papers/2017-fiat-crypto-pldi-draft.pdf}},
}
@mastersthesis{Erbsen2017CraftingCE,
author = {Andres Erbsen},
title = {Crafting certified elliptic curve cryptography implementations in Coq},
title = {Crafting certified elliptic curve cryptography implementations in {Coq}},
school = {Massachusetts Institute of Technology},
year = {2017},
note = {\url{http://adam.chlipala.net/theses/andreser_meng.pdf}},
}
......@@ -257,25 +183,21 @@
author = {W. A. Howard},
title = {The Formul\ae-as-Types Notion of Construction},
booktitle = {The Curry-Howard Isomorphism},
editor = {Philippe De Groote},
publisher = {Academia},
year = {1995},
editor = {Philippe De Groote},
note = {\url{https://www.cs.cmu.edu/~crary/819-f09/Howard80.pdf}},
}
@manual{ISO:C17,
title = {ISO C Standard 2017},
author = {ISO},
month = {Jun},
year = {2018},
note = {\url{https://www.iso.org/standard/74528.html}},
}
@manual{ISO:C99,
title = {ISO C Standard 1999},
author = {ISO},
year = {1999},
note = {\url{http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1124.pdf}},
......@@ -285,48 +207,41 @@
author = {Xavier Leroy},
title = {A formally verified compiler back-end},
journal = {Journal of Automated Reasoning},
year = {2009},
publisher = SV,
volume = {43},
number = {4},
year = {2009},
pages = {363--446},
note = {\url{http://gallium.inria.fr/~xleroy/publi/compcert-backend.pdf}},
_hal = {http://hal.inria.fr/inria-00360768/},
_urlpublisher = {http://dx.doi.org/10.1007/s10817-009-9155-4},
}
@article{Mon85,
author = {Peter L. Montgomery},
title = {Modular Multiplication Without Trial Division},
journal = {Mathematics of Computation},
year = {1985},
publisher = {AMS},
volume = {44},
number = {170},
year = {1985},
pages = {519--521},
note = {\url{http://www.ams.org/journals/mcom/1985-44-170/S0025-5718-1985-0777282-X/S0025-5718-1985-0777282-X.pdf}},
_publisher = {American Mathematical Society},
}
@article{MontgomerySpeeding,
author = {Peter L. Montgomery},
title = {Speeding the Pollard and Elliptic Curve Methods of Factorization. Math. Comp. 48, 243-264},
journal = {Mathematics of Computation - Math. Comput.},
year = {1987},
title = {Speeding the {Pollard} and Elliptic Curve Methods of Factorization},
journal = {Mathematics of Computation},
publisher = {AMS},
volume = {48},
pages = {243-243},
month = {01},
number = {177},
year = {1987},
pages = {243--243},
note = {\url{http://links.jstor.org/sici?sici=0025-5718(198701)48:177<243:STPAEC>2.0.CO;2-3}},
_doi = {10.1090/S0025-5718-1987-0866113-7},
}
@mastersthesis{Philipoom2018CorrectbyconstructionFF,
author = {Jade Philipoom},
title = {Correct-by-construction finite field arithmetic in Coq},
title = {Correct-by-construction finite field arithmetic in {Coq}},
school = {Massachusetts Institute of Technology},
year = {2018},
note = {\url{http://adam.chlipala.net/theses/jadep_meng.pdf}},
......@@ -336,140 +251,103 @@
author = {John C. Reynolds},
title = {Separation Logic: A Logic for Shared Mutable Data Structures},
booktitle = {Proceedings 17th Annual {IEEE} Symposium on Logic in Computer Science},
year = {2002},
volume = {17},
number = {July},
series = {LICS},
pages = {55-74},
publisher = {{IEEE}},
volume = {17},
year = {2002},
pages = {55--74},
note = {\url{http://www.cs.cmu.edu/~jcr/seplogic.pdf}},
}
@inproceedings{Zinzindohoue2016AVE,
author = {Jean Karim Zinzindohoue and
Evmorfia-Iro Bartzia and
Karthikeyan Bhargavan},
author = {Jean Karim Zinzindohoue and Evmorfia-Iro Bartzia and Karthikeyan Bhargavan},
title = {A Verified Extensible Library of Elliptic Curves},
booktitle = {2016 {IEEE} 29th Computer Security Foundations Symposium (CSF)},
year = {2016},
pages = {296-309},
publisher = {{IEEE}},
year = {2016},
pages = {296--309},
note = {\url{https://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=7536383}},
}
@article{cao2018vst-floyd,
author = {Qinxiang Cao and
Lennart Beringer and
Samuel Gruetter and
Josiah Dodds and
Andrew W. Appel},
title = {VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs},
author = {Qinxiang Cao and Lennart Beringer and Samuel Gruetter and Josiah Dodds and Andrew W. Appel},
title = {{VST-Floyd}: A Separation Logic Tool to Verify Correctness of {C} Programs},
journal = {Journal of Automated Reasoning},
year = {2018},
publisher = SV,
volume = {61},
number = {1-4},
year = {2018},
pages = {367--422},
month = {6},
_abstract = {The Verified Software Toolchain builds foundational machine-checked proofs of the functional correctness of C programs. Its program logic, Verifiable C, is a shallowly embedded higher-order separation Hoare logic which is proved sound in Coq with respect to the operational semantics of CompCert Clight. This paper introduces VST-Floyd, a verification assistant which offers a set of semiautomatic tactics helping users build functional correctness proofs for C programs using Verifiable C.},
_doi = {10.1007/s10817-018-9457-5},
_issn = {0168-7433},
_url = {https://doi.org/10.1007/s10817-018-9457-5},
}
@misc{coq-faq,
title = {{The Coq Proof Assistant} -- {Frequently Asked Questions}},
note = {\url{https://coq.inria.fr/faq}},
}
@misc{cryptoeprint:2011:646,
author = {Daniel J. Bernstein and
Tanja Lange and
Peter Schwabe},
title = {The security impact of a new cryptographic library},
howpublished = {Cryptology ePrint Archive, Report 2011/646},
year = {2011},
note = {\url{https://eprint.iacr.org/2011/646}},
}
@misc{cryptoeprint:2017:212,
author = {Craig Costello and
Benjamin Smith},
title = {Montgomery curves and their arithmetic: The case of large characteristic fields},
howpublished = {Cryptology ePrint Archive, Report 2017/212},
year = {2017},
note = {\url{https://eprint.iacr.org/2017/212}},
}
@inproceedings{fiat-crypto,
author = {Andres Erbsen and
Jade Philipoom and
Jason Gross and
Robert Sloan and
Adam Chlipala},
title = {Simple High-Level Code For Cryptographic Arithmetic -- With Proofs, Without Compromises},
booktitle = {Proceedings of the \href{https://www.ieee-security.org/TC/SP2019/}{40th IEEE Symposium on Security and Privacy (S\&P'19)}},
year = {2019},
month = {May},
note = {\url{https://people.csail.mit.edu/jgross/personal-website/papers/2019-fiat-crypto-ieee-sp.pdf}},
_code-github = {https://github.com/mit-plv/fiat-crypto},
@misc{Erbsen2016SystematicSO,
author = {Andres Erbsen and Jade Philipoom and Jason Gross and Rober Sloan and Adam Chlipala},
title = {Systematic Synthesis of Elliptic Curve Cryptography Implementations},
year = {2016},
note = {\url{https://people.csail.mit.edu/jgross/personal-website/papers/2017-fiat-crypto-pldi-draft.pdf}},
}
@article{gonthier2008formal,
author = {Georges Gonthier},
title = {Formal proof--the four-color theorem},
title = {Formal proof---the four-color theorem},
journal = {Notices of the AMS},
year = {2008},
publisher = {AMS},
volume = {55},
number = {11},
year = {2008},
pages = {1382--1393},
note = {\url{https://www.ams.org/notices/200811/tx081101382p.pdf}},
}
@misc{rfc4253,
author = {Tatu Yl\"{o}nen and
Chris Lonvick},
title = {{RFC 4253} - The Secure Shell {(SSH)} Transport Layer Protocol},
author = {Tatu Yl\"{o}nen and Chris Lonvick},
title = {{RFC~4253} -- The Secure Shell {(SSH)} Transport Layer Protocol},
note = {\url{https://tools.ietf.org/html/rfc4253}},
}
@misc{rfc7748,
author = {Adam Langley and
Mike Hamburg and
Sean Turner},
title = {{RFC 7748} - Elliptic Curves for Security},
author = {Adam Langley and Mike Hamburg and Sean Turner},
title = {{RFC 7748} -- Elliptic Curves for Security},
note = {\url{https://tools.ietf.org/html/rfc7748}},
}
@misc{things-that-use-curve25519,
title = {Things that use Curve25519},
month = {July},
key = {IANIX},
title = {Things that use {Curve25519}},
year = {2019},
note = {\url{https://ianix.com/pub/curve25519-deployment.html}},
}
@inproceedings{zinzindohoue2017hacl,
author = {Jean-Karim Zinzindohou{\'e} and
Karthikeyan Bhargavan and
Jonathan Protzenko and
Benjamin Beurdouche},
title = {{HACL*}: A verified modern cryptographic library},
author = {Jean-Karim Zinzindohou{\'e} and Karthikeyan Bhargavan and Jonathan Protzenko and Benjamin Beurdouche},
title = {{HACL$^*$}: A verified modern cryptographic library},
booktitle = {Proceedings of the 2017 {ACM} {SIGSAC} Conference on Computer and Communications Security},
publisher = {ACM},
year = {2017},
pages = {1789--1806},
organization = {ACM},
note = {\url{https://eprint.iacr.org/2017/536.pdf}},
}
@article{cryptoeprint:2017:212,
author = {Craig Costello and Benjamin Smith},
title = {{Montgomery} curves and their arithmetic: The case of large characteristic fields},
journal = {Journal of Cryptographic Engineering},
publisher = SV,
volume = {8},
number = {3},
year = {2018},
note = {\url{https://eprint.iacr.org/2017/212}},
}
@inproceedings{fiat-crypto,
author = {Andres Erbsen and Jade Philipoom and Jason Gross and Robert Sloan and Adam Chlipala},
title = {Simple High-Level Code For Cryptographic Arithmetic -- With Proofs, Without Compromises},
booktitle = {2019 IEEE Symposium on Security and Privacy},
year = {2019},
pages = {73--90},
note = {\url{https://people.csail.mit.edu/jgross/personal-website/papers/2019-fiat-crypto-ieee-sp.pdf}},
}
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment