collection.bib 14.4 KB
Newer Older
Benoit Viguier's avatar
Benoit Viguier committed
1
2
3
@STRING{LNCS = {LNCS}}
@STRING{SV = {Springer}}

Benoit Viguier's avatar
Benoit Viguier committed
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
@article{1969-Hoare,
  author        = {C. A. R. Hoare},
  title         = {An Axiomatic Basis for Computer Programming},
  journal       = {Commun. ACM},
  issue_date    = {Oct. 1969},
  volume        = {12},
  number        = {10},
  month         = {oct},
  year          = {1969},
  issn          = {0001-0782},
  pages         = {576-580},
  numpages      = {5},
  note          = {\url{http://doi.acm.org/10.1145/363235.363259}},
  url           = {http://doi.acm.org/10.1145/363235.363259},
  doi           = {10.1145/363235.363259},
  acmid         = {363259},
  publisher     = {ACM}
}

@article{2007-Blazy-C-chronique,
  author        = {Sandrine Blazy},
  title         = {Comment gagner confiance en {C} ?},
  journal       = {Technique et Science Informatiques},
  year          = {2007},
  volume        = {26},
  number        = {9},
  pages         = {1195-1200},
  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},
  editor        = {Alwyn Goodloe and Suzette Person},
  publisher     = SV,
  series        = LNCS,
  volume        = {7226},
  year          = {2012},
  pages         = {2},
  url           = {https://doi.org/10.1007/978-3-642-28891-3_2},
Benoit Viguier's avatar
done    
Benoit Viguier committed
48
  note          = {\url{https://doi.org/10.1007/978-3-642-28891-3_2}},
Benoit Viguier's avatar
Benoit Viguier committed
49
  doi           = {10.1007/978-3-642-28891-3_2},
Benoit Viguier's avatar
Benoit Viguier committed
50
}
Benoit Viguier's avatar
Benoit Viguier committed
51
52
53
54
55
56
57
58
59

@article{2015-Appel,
  author        = {Andrew W. Appel},
  title         = {Verification of a Cryptographic Primitive: SHA-256},
  journal       = {ACM Trans. Program. Lang. Syst.},
  issue_date    = {April 2015},
  volume        = {37},
  number        = {2},
  month         = apr,
Benoit Viguier's avatar
Benoit Viguier committed
60
  year          = {2015},
Benoit Viguier's avatar
Benoit Viguier committed
61
62
63
64
65
  issn          = {0164-0925},
  pages         = {7:1--7:31},
  articleno     = {7},
  numpages      = {31},
  url           = {http://doi.acm.org/10.1145/2701415},
Benoit Viguier's avatar
done    
Benoit Viguier committed
66
  note          = {\url{http://doi.acm.org/10.1145/2701415}},
Benoit Viguier's avatar
Benoit Viguier committed
67
68
69
  doi           = {10.1145/2701415},
  acmid         = {2701415},
  publisher     = {ACM},
Benoit Viguier's avatar
Benoit Viguier committed
70
71
}

Benoit Viguier's avatar
Benoit Viguier committed
72
73
74
75
76
77
78
@book{Abrial:1996:BAP:236705,
  author    = {Jean-Raymond Abrial},
  title     = {The B-book: Assigning Programs to Meanings},
  year      = {1996},
  isbn      = {0-521-49619-5},
  publisher = {Cambridge University Press},
  address   = {New York, NY, USA},
Benoit Viguier's avatar
Benoit Viguier committed
79
}
Benoit Viguier's avatar
Benoit Viguier committed
80
note    = {\url{https://books.google.nl/books?id=T_ShHENlqBAC&lpg=PR4&pg=PP1#v=onepage&q&f=false}}
Benoit Viguier's avatar
Benoit Viguier committed
81

Benoit Viguier's avatar
Benoit Viguier committed
82
83
84
85
86
87
88
89
90
91
92
93
94
@inproceedings{Ber06,
  author        = {Daniel J. Bernstein},
  title         = {Curve25519: new {D}iffie-{H}ellman speed records},
  booktitle     = {Public Key Cryptography -- {PKC 2006}},
  editor        = {Moti Yung and Yevgeniy Dodis and Aggelos Kiayias and Tal Malkin},
  publisher     = SV,
  series        = LNCS,
  volume        = {3958},
  year          = {2006},
  pages         = {207--228},
  note          = {\url{http://cr.yp.to/papers.html\#curve25519}},
}

Benoit Viguier's avatar
Benoit Viguier committed
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
@misc{Ber14,
  title       = {25519 naming, Posting to the CFRG mailing list},
  author      = {Daniel J. Bernstein},
  year        = {2008},
  note        = {\url{https://www.ietf.org/mail-archive/web/cfrg/current/msg04996.html}}
}

@inproceedings{Beringer2015VerifiedCA,
  title      = {Verified Correctness and Security of OpenSSL HMAC},
  author     = {Lennart Beringer and Adam Petcher and Katherine Q. Ye and Andrew W. Appel},
  booktitle  = {USENIX Security Symposium},
  year       = {2015},
  note       = {\url{https://www.cs.cmu.edu/~kqy/resources/verified-hmac.pdf}}
}

@inproceedings{BGJ+15,
  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}},
  editor        = {Diego Aranha and Alfred Menezes},
  publisher     = SV,
  series        = LNCS,
  volume        = {8895},
  year          = {2015},
  pages         = {64--83},
  note          = {Document ID: c74b5bbf605ba02ad8d9e49f04aca9a2, \url{http://cryptojedi.org/papers/\#tweetnacl}},
}

@article{Blazy-Leroy-Clight-09,
  author        = {Sandrine Blazy and Xavier Leroy},
  title         = {Mechanized semantics for the {Clight}
                         subset of the {C} language},
  year          = {2009},
  journal       = {Journal of Automated Reasoning},
  volume        = {43},
  number        = {3},
  pages         = {263-288},
  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{BLS12,
  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}},
  editor        = {Alejandro Hevia and Gregory Neven},
  publisher     = SV,
  series        = LNCS,
  volume        = {7533},
  year          = {2012},
  pages         = {159--176},
  note          = {Document ID: 5f6fc69cc5a319aecba43760c56fab04, \url{http://cryptojedi.org/papers/\#coolnacl}},
}

Benoit Viguier's avatar
Benoit Viguier committed
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
@article{cao2018vst-floyd,
  author        = {Qinxiang Cao and Lennart Beringer and Samuel Gruetter and Josiah Dodds and Andrew W. Appel},
  year          = {2018},
  title         = {VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs},
  journal       = {Journal of Automated Reasoning},
  issn          = {0168-7433},
  doi           = {10.1007/s10817-018-9457-5},
  volume        = {61},
  month         = {6},
  pages         = {367--422},
  number        = {1-4},
  url           = {https://doi.org/10.1007/s10817-018-9457-5},
  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.}
}

Benoit Viguier's avatar
Benoit Viguier committed
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
@inproceedings{Chen2014VerifyingCS,
  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},
  booktitle = {ACM Conference on Computer and Communications Security},
  year      = {2014},
  note      = {\url{https://cryptojedi.org/papers/verify25519-20140428.pdf}}
}

@misc{coq-faq,
  title         = {{The Coq Proof Assistant} -- {Frequently Asked Questions}},
  author        = {},
  note          = {\url{https://coq.inria.fr/faq}},
}

@Article{CpdtJFR,
  author      = {Adam Chlipala},
  title       = {An Introduction to Programming and Proving with Dependent Types in Coq},
  volume      = {3(2)},
  pages       = {1-93},
  year        = {2010},
  journal     = {Journal of Formalized Reasoning},
  url         = {http://adam.chlipala.net/papers/CpdtJFR/},
  note        = {\url{http://adam.chlipala.net/papers/CpdtJFR/}}
}

@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}},
Benoit Viguier's avatar
Benoit Viguier committed
196
197
}

Benoit Viguier's avatar
Benoit Viguier committed
198
199
200
201
202
203
204
205
206
207
208
209
@inproceedings{DBLP:conf/itp/BartziaS14,
  author    = {Evmorfia-Iro Bartzia and Pierre-Yves Strub},
  title     = {A Formal Library for Elliptic Curves in the Coq Proof Assistant},
  booktitle = {Interactive Theorem Proving},
  editor    = {Gerwin Klein and Ruben Gamboa},
  publisher = SV,
  series    = LNCS,
  volume    = {8558},
  year      = {2014},
  pages     = {77-92},
  note      = {\url{https://hal.inria.fr/hal-01102288}}
}
Benoit Viguier's avatar
Benoit Viguier committed
210

Benoit Viguier's avatar
Benoit Viguier committed
211
212
213
214
215
216
217
218
219
220
221
222
223
@article{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}}},
  title     = {Verified Low-Level Programming Embedded in {F}},
Benoit Viguier's avatar
forward    
Benoit Viguier committed
224
225
226
227
  journal   = {Proceedings of the ACM on Programming Languages},
  volume    = {1},
  number    = {ICFP},
  pages     = {17},
Benoit Viguier's avatar
Benoit Viguier committed
228
  year      = {2017},
Benoit Viguier's avatar
forward    
Benoit Viguier committed
229
  publisher = {ACM},
Benoit Viguier's avatar
Benoit Viguier committed
230
  url       = {http://arxiv.org/abs/1703.00053},
Benoit Viguier's avatar
done    
Benoit Viguier committed
231
  note      = {\url{http://arxiv.org/abs/1703.00053}},
Benoit Viguier's avatar
Benoit Viguier committed
232
233
234
235
  eprint    = {1703.00053},
  timestamp = {Mon, 13 Aug 2018 16:46:57 +0200},
}

Benoit Viguier's avatar
Benoit Viguier committed
236
237
238
239
240
@inproceedings{Erbsen2016SystematicSO,
  title     = {Systematic Synthesis of Elliptic Curve Cryptography Implementations},
  author    = {Andres Erbsen and Jason Gross and Adam Chlipala},
  year      = {2016},
  note      = {\url{https://people.csail.mit.edu/jgross/personal-website/papers/2017-fiat-crypto-pldi-draft.pdf}}
Benoit Viguier's avatar
Benoit Viguier committed
241
242
243
}

@inproceedings{Erbsen2017CraftingCE,
Benoit Viguier's avatar
done    
Benoit Viguier committed
244
245
246
247
  title      = {Crafting certified elliptic curve cryptography implementations in Coq},
  author     = {Andres Erbsen},
  year       = {2017},
  note       = {\url{http://adam.chlipala.net/theses/andreser_meng.pdf}}
Benoit Viguier's avatar
Benoit Viguier committed
248
249
}

Benoit Viguier's avatar
done    
Benoit Viguier committed
250
251
252
253
254
255
256
257
258
259
260
@inproceedings{fiat-crypto,
  title       = {Simple High-Level Code For Cryptographic Arithmetic -- With Proofs, Without Compromises},
  author      = {Andres Erbsen and Jade Philipoom and Jason Gross and Robert Sloan and Adam Chlipala},
  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},
  code-github = {https://github.com/mit-plv/fiat-crypto},
  owner       = {jgross},
  timestamp   = {2018.06.01},
  url         = {https://people.csail.mit.edu/jgross/personal-website/papers/2019-fiat-crypto-ieee-sp.pdf},
  note        = {\url{https://people.csail.mit.edu/jgross/personal-website/papers/2019-fiat-crypto-ieee-sp.pdf}}
Benoit Viguier's avatar
Benoit Viguier committed
261
262
}

Benoit Viguier's avatar
forward    
Benoit Viguier committed
263
@article{gonthier2008formal,
Benoit Viguier's avatar
done    
Benoit Viguier committed
264
265
266
267
268
269
270
271
  title     = {Formal proof--the four-color theorem},
  author    = {Georges Gonthier},
  journal   = {Notices of the AMS},
  volume    = {55},
  number    = {11},
  pages     = {1382--1393},
  year      = {2008},
  note      = {\url{https://www.ams.org/notices/200811/tx081101382p.pdf}}
Benoit Viguier's avatar
forward    
Benoit Viguier committed
272
273
}

Benoit Viguier's avatar
Benoit Viguier committed
274
275
276
277
278
279
280
281
282
283
@incollection{Howard1995-HOWTFN,
	title = {The Formul\ae-as-Types Notion of Construction},
	author = {W. A. Howard},
	booktitle = {The Curry-Howard Isomorphism},
	year = {1995},
	editor = {Philippe De Groote},
	publisher = {Academia},
  note = {\url{https://www.cs.cmu.edu/~crary/819-f09/Howard80.pdf}}
}

Benoit Viguier's avatar
Benoit Viguier committed
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
@article{Leroy-backend,
  author        = {Xavier Leroy},
  title         = {A formally verified compiler back-end},
  journal       = {Journal of Automated Reasoning},
  volume        = {43},
  number        = {4},
  pages         = {363--446},
  year          = {2009},
  note          = {\url{http://gallium.inria.fr/~xleroy/publi/compcert-backend.pdf}},
  urlpublisher  = {http://dx.doi.org/10.1007/s10817-009-9155-4},
  hal           = {http://hal.inria.fr/inria-00360768/},
  pubkind       = {journal-int-mono}
}

@article{Mon85,
  author        = {Peter L. Montgomery},
  title         = {Modular Multiplication Without Trial Division},
  journal       = {Mathematics of Computation},
  publisher     = {American Mathematical Society},
  year          = {1985},
  volume        = {44},
  number        = {170},
  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}},
}

@article{MontgomerySpeeding,
  author  = {Peter L. Montgomery},
  title   = {Speeding the Pollard and Elliptic Curve Methods of Factorization. Math. Comp. 48, 243-264},
  month   = {01},
  volume  = {48},
  year    = {1987},
  pages   = {243-243},
  journal = {Mathematics of Computation - Math. Comput.},
  doi     = {10.1090/S0025-5718-1987-0866113-7},
  note    = {\url{http://links.jstor.org/sici?sici=0025-5718(198701)48:177<243:STPAEC>2.0.CO;2-3}}
}

@inproceedings{Philipoom2018CorrectbyconstructionFF,
  title     = {Correct-by-construction finite field arithmetic in Coq},
  author    = {Jade Philipoom},
  year      = {2018},
  note      = {\url{http://adam.chlipala.net/theses/jadep_meng.pdf}}
}

@article{Reynolds02separationlogic,
  author        = {John C. Reynolds},
  title         = {Separation Logic: A Logic for Shared Mutable Data Structures},
  journal       = {LICS},
  volume        = {17},
  year          = {2002},
  pages         = {55-74},
  note          = {\url{http://www.cs.cmu.edu/~jcr/seplogic.pdf}},
  url           = {http://www.cs.cmu.edu/~jcr/seplogic.pdf}
}

@misc{rfc4253,
  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},
  note        = {\url{https://tools.ietf.org/html/rfc7748}},
}
Benoit Viguier's avatar
forward    
Benoit Viguier committed
352
353

@misc{this-that-use-curve25519,
Benoit Viguier's avatar
done    
Benoit Viguier committed
354
355
356
357
  title   = {Things that use Curve25519},
  author  = {},
  url     = {https://ianix.com/pub/curve25519-deployment.html},
  note    = {\url{https://ianix.com/pub/curve25519-deployment.html}}
Benoit Viguier's avatar
forward    
Benoit Viguier committed
358
}
Benoit Viguier's avatar
done    
Benoit Viguier committed
359

Benoit Viguier's avatar
Benoit Viguier committed
360
361
362
363
364
365
366
367
368
@article{Zinzindohoue2016AVE,
  title   = {A Verified Extensible Library of Elliptic Curves},
  author  = {Jean Karim Zinzindohoue and Evmorfia-Iro Bartzia and Karthikeyan Bhargavan},
  journal = {2016 IEEE 29th Computer Security Foundations Symposium (CSF)},
  year    = {2016},
  pages   = {296-309},
  note      = {\url{https://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=7536383}}
}

Benoit Viguier's avatar
forward    
Benoit Viguier committed
369
@inproceedings{zinzindohoue2017hacl,
Benoit Viguier's avatar
done    
Benoit Viguier committed
370
371
372
373
374
375
376
  title         = {HACL*: A verified modern cryptographic library},
  author        = {Jean-Karim Zinzindohou{\'e} and Karthikeyan Bhargavan and Jonathan Protzenko and Benjamin Beurdouche},
  booktitle     = {Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security},
  pages         = {1789--1806},
  year          = {2017},
  organization  = {ACM},
  note          = {\url{https://eprint.iacr.org/2017/536.pdf}}
Benoit Viguier's avatar
forward    
Benoit Viguier committed
377
}
378

Benoit Viguier's avatar
Benoit Viguier committed
379
380
381
@misc{zmq,
  title         = {ZeroMQ},
  note          = {\url{http://zeromq.org/}}
382
}