-
Notifications
You must be signed in to change notification settings - Fork 4
/
Copy pathindex.html
545 lines (512 loc) · 39 KB
/
index.html
1
2
3
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
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
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
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
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
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
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
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
<!doctype html>
<html lang="en">
<head>
<meta charset="utf-8">
<meta http-equiv="x-ua-compatible" content="ie=edge">
<title>Tamarin Prover</title>
<meta name="description"
content="The Tamarin prover is a security protocol verification tool that supports both falsification and unbounded verification in the symbolic model.">
<meta name="viewport" content="width=device-width, initial-scale=1, shrink-to-fit=no">
<link rel="icon" href="favicon.ico" type="image/x-icon">
<link rel="apple-touch-icon" href="icon.png">
<link rel="icon" type="image/png" sizes="256x256" href="favicon-256x256.png">
<link rel="icon" type="image/png" sizes="128x128" href="favicon-128x128.png">
<link rel="icon" type="image/png" sizes="64x64" href="favicon-64x64.png">
<link rel="icon" type="image/png" sizes="32x32" href="favicon-32x32.png">
<link rel="icon" type="image/png" sizes="16x16" href="favicon-16x16.png">
<link rel="stylesheet" href="https://stackpath.bootstrapcdn.com/bootstrap/4.4.1/css/bootstrap.min.css"
integrity="sha384-Vkoo8x4CGsO3+Hhxv8T/Q5PaXtkKtu6ug5TOeNV6gBiFeWPGFN9MuhOf23Q9Ifjh" crossorigin="anonymous">
<link type="text/css" rel="stylesheet" href="assets/css/bootstrap-responsive.min.css" />
<!-- Custom CSS for the site -->
<link type="text/css" rel="stylesheet" href="assets/css/custom.css" />
<link rel="stylesheet" href="assets/css/font-awesome.min.css">
</head>
<body>
<div class="container-fluid">
<nav class="navbar navbar-expand-lg fixed-top navbar-dark bg-dark">
<a class="navbar-brand" href="#">
<img src="icon-top.png" width="34" height="34" class="d-inline-block align-top" alt="">
Tamarin Prover
</a>
<button class="navbar-toggler" type="button" data-toggle="dropdown" data-target="#navbarText"
aria-controls="navbarText" aria-expanded="false" aria-label="Toggle navigation">
<span class="navbar-toggler-icon"></span>
</button>
<div class="collapse navbar-collapse" id="navbarText">
<ul class="navbar-nav mr-auto">
<li class="nav-item">
<a class="nav-link" href="#documentation">Documentation</a>
</li>
<li class="nav-item">
<a class="nav-link" href="#screenshots">Screenshots</a>
</li>
<li class="nav-item">
<a class="nav-link" href="#sourcecode_and_mailing_list">Sourcecode and Mailing List</a>
</li>
<li class="nav-item">
<a class="nav-link" href="#installation">Installation</a>
</li>
<li class="nav-item">
<a class="nav-link" href="#research_papers_and_theses">Publications</a>
</li>
</ul>
</nav>
</div>
<section class="jumbotron text-center">
<div class="container">
<h1 class="jumbotron-heading">Tamarin Prover</h1>
<p class="lead text-muted">The Tamarin prover is a security protocol verification tool that supports both
falsification (attack finding) and unbounded verification (proving) in the symbolic model. Security protocols
are specified as multiset rewriting systems and analyzed with respect to temporal
first-order properties.
<!--and a message theory that models Diffie-Hellman exponentiation and exclusive-or (XOR), combined with a user-defined rewriting theory that has the Finite Variant Property, which includes subterm-convergent theories.-->
</p>
<p class="lead text-muted">Tamarin has been successfully used to analyze and support the development of modern
security
protocols [<a href="https://hal.archives-ouvertes.fr/hal-03586826" target="_blank">1</a>,<a
href="https://ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/publications/pub2017/siglog-tamarin.pdf"
target="_blank">2</a>], including TLS 1.3 [<a
href="https://tls13tamarin.github.io/TLS13Tamarin/docs/tls13tamarin-draft21.pdf" target="_blank">3</a>,<a
href="https://cispa.saarland/group/cremers/downloads/papers/CHSV2016-TLS13.pdf" target="_blank">4</a>],
5G‑AKA [<a href="https://arxiv.org/pdf/1806.10360" target="_blank">5</a>,<a
href="https://cispa.saarland/group/cremers/downloads/papers/CrDe2018-5G.pdf" target="_blank">6</a>],
Noise [<a href="https://cispa.saarland/group/cremers/downloads/papers/Noise-Usenix2020.pdf"
target="_blank">7</a>],
EMV (Chip-and-pin) [<a href="https://arxiv.org/pdf/2006.08249.pdf" target="_blank">8</a>], and
Apple iMessage [<a href="https://security.apple.com/blog/imessage-pq3/" target="_blank">9</a>].</p>
<p>
<a href="manual/index.html" class="btn btn-primary" target="_blank"><i class="fa fa-book"
aria-hidden="true"></i> Get the docs</a>
<a href="manual/master/book/002_installation.html" class="btn btn-secondary" target="_blank"><i
class="fa fa-download" aria-hidden="true"></i> Install Tamarin</a>
<!-- <a href="#" class="btn btn-secondary">Secondary action</a> -->
</p>
</div>
</section>
<div class="main">
<div class="container">
<h2>About / Core team:</h2>
<p>
<a href="https://www.inf.ethz.ch/personal/basin/">David Basin</a>,
<a href="https://cispa.saarland/group/cremers/index.html">Cas Cremers</a><a rel="me"
href="https://infosec.exchange/@cascremers"></a>,
<a href="https://www.jannikdreier.net/">Jannik Dreier</a>,
<a href="mailto:[email protected]">Simon Meier</a>,
<a href="https://people.inf.ethz.ch/rsasse/">Ralf Sasse</a>,
<a href="https://beschmi.net">Benedikt Schmidt</a><br />
Tamarin is a collaborative effort: see the <a href="manual/index.html">manual</a> for a more extensive overview
of its development and additional contributors.<br />
Current maintainers: <a href="https://cispa.saarland/group/cremers/index.html">Cas Cremers</a>, <a
href="https://www.jannikdreier.net/">Jannik Dreier</a>, <a href="http://www.kunnemann.de/">Robert
Künnemann</a>, <a href="https://people.inf.ethz.ch/rsasse/">Ralf Sasse</a>
</p>
</div>
<div class="container">
<a name="documentation"></a>
<h2>Documentation<a class="anchorlink" href="#documentation"></a></h2>
<p>
The Tamarin user manual is available <a href="manual/index.html">here</a>.<br />
We also have a GitHub repository for other <a href="https://github.com/tamarin-prover/teaching">teaching
materials</a>, such as tutorials.<br />
For general information, also see the <a href="https://en.wikipedia.org/wiki/Tamarin_Prover">Wikipedia
article</a>.
</p>
</div>
<div class="container">
<a name="screenshots"></a>
<h2>Screenshots<a class="anchorlink" href="#screenshots"></a></h2>
<div class="row">
<div class="col-md-4">
<a target="_self" href="assets/img/Tamarin-home.png">
<img class="centre-img" src="assets/img/Tamarin-home-small.png" alt="Tamarin introduction page" />
</a>
<p class="card-text">Introduction page</p>
</div>
<!-- /col -->
<div class="col-md-4">
<a target="_self" href="assets/img/Tamarin-overview.png">
<img class="centre-img" src="assets/img/Tamarin-overview-small.png" alt="Tamarin introduction page" />
</a>
<p class="card-text">Overview</p>
</div>
<!-- /col -->
<div class="col-md-4">
<a target="_self" href="assets/img/Tamarin-attack.png">
<img class="centre-img" src="assets/img/Tamarin-attack-small.png" alt="Tamarin introduction page" />
</a>
<p class="card-text">Tamarin Attack Display</p>
</div>
<!-- /col -->
</div>
<!-- /row -->
</div>
<!-- /container -->
<div class="container">
<a name="sourcecode_and_mailing_list"></a>
<h2>Sourcecode and Mailing List<a class="anchorlink" href="#sourcecode_and_mailing_list"></a></h2>
<p>The Tamarin prover is open-source software. Its <b>code and issue tracker</b> are available at <a
href="https://github.com/tamarin-prover/tamarin-prover">https://github.com/tamarin-prover/tamarin-prover</a>.
Note
that the issue tracker is only intended for tool issues, i.e., reporting potential bugs, and not for asking
questions.</p>
<p>Tamarin's low-volume <b>mailing list/forum</b> for announcements, asking questions,
and discussion is
<a href="https://groups.google.com/group/tamarin-prover">https://groups.google.com/group/tamarin-prover</a>. The
mailing list can be used if you have questions related to the theory, modeling, or using the tool.
</p>
<p>
For other inquiries (not bug reports!) you can reach the current maintainers of the Tamarin Prover via mail at
<a href="mailto:[email protected]">[email protected]</a>.
</p>
</div>
<div class="container">
<a name="installation"></a>
<h2>Installation<a class="anchorlink" href="#installation"></a></h2>
<p>Installation instructions are in the <a href="manual/index.html">manual</a>.</p>
</div>
<div class="container">
<a name="research_papers_and_theses"></a>
<h2>Research Papers and Theses<a class="anchorlink" href="#research_papers_and_theses"></a></h2>
<h4>Overview Papers on Tamarin</h4>
<ul class="list">
<li>IEEE Security and Privacy Magazine 2022 paper <a href="https://hal.archives-ouvertes.fr/hal-03586826"
target="_blank">[PDF]</a>: the paper published in the <a href="https://www.computer.org/csdl/magazine/sp"
target="_blank">IEEE Security and Privacy Magazine</a>, presenting an overview of some of Tamarin's early
success stories:
"Tamarin: Verification of Large-Scale, Real World, Cryptographic Protocols", by David Basin, Cas Cremers,
Jannik Dreier, Ralf Sasse.</li>
<li>SIGLOG Newsletter 2017 paper <a
href="https://ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/publications/pub2017/siglog-tamarin.pdf"
target="_blank">[PDF]</a>: the paper published in the <a href="http://siglog.org/newsletter-october-2017/"
target="_blank">SIGLOG Newsletter October 2017</a>, presenting an overview of Tamarin and its features:
"Symbolically Analyzing Security Protocols using TAMARIN", by David Basin, Cas Cremers, Jannik Dreier, Ralf
Sasse.</li>
</ul>
<h4>Papers on Tamarin and its theory</h4>
<ul class="list">
<li>JCS 2022 paper <a href="https://hal.archives-ouvertes.fr/hal-03767104" target="_blank">[PDF]</a>: the
extended journal paper published in the <a
href="https://www.iospress.nl/journal/journal-of-computer-security/" target="_blank">Journal of Computer
Security</a>, about automatic generation of sources lemmas: "Automatic generation of sources lemmas in
TAMARIN: towards automatic proofs of security protocols", by Véronique Cortier, Stéphanie Delaune, Jannik
Dreier, Elise Klein.</li>
<li>ESORICS 2020 paper <a href="https://hal.archives-ouvertes.fr/hal-02903620" target="_blank">[PDF]</a>: the
paper presented at <a href="http://esorics2020.sccs.surrey.ac.uk/" target="_blank">ESORICS</a>, about the
automatic generation of sources lemmas: " Automatic generation of sources lemmas in Tamarin: towards automatic
proofs of security protocol", by Véronique Cortier, Stéphanie Delaune, Jannik Dreier.</li>
<li>JCS 2020 paper <a href="https://hal.archives-ouvertes.fr/hal-02358878" target="_blank">[PDF]</a>: the
extended journal paper published in the <a
href="https://www.iospress.nl/journal/journal-of-computer-security/" target="_blank">Journal of Computer
Security</a>, about the support for Exclusive-Or: "Verification of stateful cryptographic protocols with
exclusive OR", by Jannik Dreier, Lucca Hirschi, Saša Radomirović, Ralf Sasse.</li>
<li>CSF 2019 paper <a href="https://people.cispa.io/cas.cremers/downloads/papers/prime_order_please.pdf"
target="_blank">[PDF]</a>: the paper presented at <a href="https://web.stevens.edu/csf2019/"
target="_blank">CSF</a>, about adding support and models for capturing Diffie-Hellman-like protocols even
more accurately: "Prime, Order Please! Revisiting Small Subgroup and Invalid Curve Attacks on Protocols using
Diffie-Hellman", by Cas Cremers and Dennis Jackson.</li>
<li>CSF 2018 paper <a href="https://hal.archives-ouvertes.fr/hal-01780544" target="_blank">[PDF]</a>: the paper
presented at <a href="https://www.cs.ox.ac.uk/conferences/csf2018/" target="_blank">CSF</a>, about adding
support for Exclusive-Or: "Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive
OR", by Jannik Dreier, Lucca Hirschi, Saša Radomirović, Ralf Sasse.</li>
<li>POST 2017 paper <a href="https://hal.inria.fr/hal-01430490/document" target="_blank">[PDF]</a>: the paper
presented at <a href="http://www.etaps.org/2017/post" target="_blank">POST</a>, about allowing user-defined
equational theories to be non-subterm-convergent: "Beyond Subterm-Convergent Equational Theories in Automated
Verification of Stateful Protocols", by Jannik Dreier, Charles Duménil, Steve Kremer, Ralf Sasse.</li>
<li>CCS 2015 paper <a
href="http://www.infsec.ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/publications/pub2015/ASPObsEq.pdf"
target="_blank">[PDF]</a>: the paper presented at <a href="http://www.sigsac.org/ccs/CCS2015/"
target="_blank">CCS</a>, also available as <a
href="http://www.infsec.ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/publications/pub2015/ASPObsEq_full.pdf"
target="_blank">Extended Version with proofs</a>; about observational equivalence for Tamarin: "Automated
Symbolic Proofs of Observational Equivalence", by David Basin, Jannik Dreier, Ralf Sasse.</li>
<li>S&P 2014 paper <a
href="http://www.infsec.ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/software/tamarin_group_sp.pdf"
target="_blank">[PDF]</a>: the paper presented at <a href="http://www.ieee-security.org/TC/SP2014/"
target="_blank">S&P</a>, about group protocols and bilinear pairing extensions: "Automated Verification
of Group Key Agreement Protocols", by Benedikt Schmidt, Ralf Sasse, Cas Cremers, David Basin.</li>
<li>CAV 2013 paper <a href="http://link.springer.com/chapter/10.1007/978-3-642-39799-8_48#"
target="_blank">[PDF]</a>: the paper presented at <a href="http://cav2013.forsyte.at/index.html"
target="_blank">CAV</a>, presenting the tool in more detail: "The TAMARIN Prover for the Symbolic Analysis
of Security Protocols", by Simon Meier, Benedikt Schmidt, Cas Cremers, David Basin.</li>
<li>CSF 2012 paper <a
href="http://www.infsec.ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/software/dh_tamarin_csf.pdf"
target="_blank">[PDF]</a>: the paper presented at <a href="http://csf2012.seas.harvard.edu/"
target="_blank">CSF</a>, also available as extended version <a
href="http://www.infsec.ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/software/dh_tamarin_extended_v1.pdf"
target="_blank">[PDF]</a>: extended version that contains the full proofs and additional examples; original
paper introducing Tamarin Prover: "Automated Analysis of Diffie-Hellman Protocols and Advanced Security
Properties", by Benedikt Schmidt, Simon Meier, Cas Cremers, David Basin.</li>
<!-- </ul>
<h4>Papers on Tamarin and its theory - theses</h4>
<ul class="list"> -->
<li>Meier's PhD thesis <a href="http://dx.doi.org/10.3929/ethz-a-009790675" target="_blank">[PDF]</a>:
provides a detailed explanation of the theory and implementation of Tamarin including inductive invariants and
type assertions.</li>
<li>Schmidt's PhD thesis <a href="http://e-collection.library.ethz.ch/view/eth:7065"
target="_blank">[PDF]</a>: provides a detailed explanation of the theory and application of Tamarin
including the reasoning about Diffie-Hellman exponentiation
and bilinear pairing.
<li>Staub's bachelor thesis <a href="http://dx.doi.org/10.3929/ethz-a-007554462" target="_blank">[PDF]</a>:
about the implementation of the original version of Tamarin's GUI.</li>
</li>
</ul>
<h4>Tamarin Extensions</h4>
<ul class="list">
<li> "Hash Gone Bad: Automated discovery of protocol attacks that exploit hash function weaknesses" <a
href="https://eprint.iacr.org/2022/1314.pdf" target="_blank">[PDF]</a>, by Vincent Cheval, Cas Cremers,
Alexander Dax, Lucca Hirschi, Charlie Jacomme, and Steve Kremer, presented at <a
href="https://www.usenix.org/conference/usenixsecurity23/glance">USENIX 2023</a>.
</li>
<li> "Subterm-based proof techniques for improving the automation and scope of security protocol analysis" <a
href="https://eprint.iacr.org/2022/1130.pdf" target="_blank">[PDF]</a>, by Cas Cremers, Charlie Jacomme, and
Philip Lukert, presented at <a href="https://csf2023.ieee-security.org/program.html">IEEE CSF 2023</a>.
</li>
<li>"Seems Legit: Automated Analysis of Subtle Attacks on Protocols that use Signatures" <a
href="https://people.cispa.io/cas.cremers/downloads/papers/JCCS2019-signatures.pdf"
target="_blank">[PDF]</a>, by Dennis Jackson, Cas Cremers, Katriel Cohn-Gordon, and Ralf Sasse, presented at
<a href="https://www.sigsac.org/ccs/CCS2019/">ACM CCS 2019</a>.
</li>
<li>"Distance-Bounding Protocols: Verification without Time and Location" <a
href="http://satoss.uni.lu/members/jorge/shareable/SP18_shareable.pdf" target="_blank">[PDF]</a>, by Sjouke
Mauw, Zach Smith, Jorge Toro-Pozo, Rolando Trujillo-Rasua, presented at <a
href="https://www.ieee-security.org/TC/SP2018/" target="_blank">S&P 2018</a>.</li>
<li>"A Novel Approach for Reasoning about Liveness in Cryptographic Protocols and its Application to Fair
Exchange" <a href="https://hal.inria.fr/hal-01396282/file/fairexchange-long.pdf" target="_blank">[PDF]</a>, by
Michael Backes, Jannik Dreier, Steve Kremer, Robert Künnemann, presented at <a
href="https://www.ieee-security.org/TC/EuroSP2017/" target="_blank">EuroS&P 2017</a>.</li>
<li>"Modeling Human Errors in Security Protocols" <a
href="https://www.ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/projects/hisp/human_errors_fullVersion.pdf"
target="_blank">[PDF]</a>, by David Basin, Saša Radomirović, Lara Schmid, presented at <a
href="http://csf2016.tecnico.ulisboa.pt/" target="_blank">CSF 2016</a>.</li>
<li>"Alice and Bob Meet Equational Theories" <a
href="https://www.ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/software/anb_festschrift.pdf"
target="_blank">[PDF]</a>, by David Basin, Michel Keller, Saša Radomirović, Ralf Sasse, paper presented at
<a href="http://meseguer-fest.ifi.uio.no/" target="_blank">Logic, Rewriting, and Concurrency 2015 -
Festschrift Symposium in Honor of José Meseguer</a>.
</li>
<li>"Automated analysis of security protocols with global state" <a
href="http://hal.inria.fr/docs/00/95/58/69/PDF/sapic.pdf" target="_blank">[PDF]</a>, by Steve Kremer, Robert
Künnemann, paper presented at <a href="http://www.ieee-security.org/TC/SP2014/" target="_blank">S&P
2014</a>, also available extended journal version at <a
href="https://www.iospress.nl/journal/journal-of-computer-security/" target="_blank">Journal of Computer
Security</a>: <a href="https://hal.inria.fr/hal-01351388/document" target="_blank">[PDF]</a>.</li>
<!-- </ul>
<h4>Tamarin Extensions - student theses</h4>
<ul class="list"> -->
<li>Xenia Hofmeier's master thesis <a
href="https://www.ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/software/ma-21-hofmeier-aggsign.pdf"
target="_blank">[PDF]</a>: Formalizing Aggregate Signatures in the Symbolic Model
<a href="https://www.ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/software/hofmeier-aggsign.zip"
target="_blank">[zip]</a>.
</li>
<li>Andrina Denzler's bachelor Thesis <a
href="https://www.ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/projects/hisp/report_final_andrina.pdf"
target="_blank">[PDF]</a>: on how to automate the
analysis of communications protocols with human errors.</li>
<li>Dorela Kozmai's bachelor Thesis <a
href="https://www.ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/software/Kozmai-Tamarin-to-AnB.pdf"
target="_blank">[PDF]</a>: on how to translate Tamarin specifications
into Alice&Bob protocol notation, with implementation available <a
href="https://www.ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/software/tamarin_to_anb.zip"
target="_blank">[zip]</a>.</li>
<li>Lara Schmid's master Thesis <a
href="https://www.ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/projects/hisp/MA_LaraSchmid.pdf"
target="_blank">[PDF]</a>: on how one can model human errors in secure communication protocols.</li>
<li>Michel Keller's bachelor thesis <a
href="http://www.infsec.ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/software/thesis_keller_alicebob.pdf"
target="_blank">[PDF]</a>: about translating Alice&Bob
protocol notation into Tamarin's input language, with implementation available <a
href="http://www.infsec.ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/software/anb.tar.gz"
target="_blank">[tar.gz]</a>.</li>
</ul>
<h4>Papers using Tamarin</h4>
<ul class="list">
<li> "Formal Analysis of Session-Handling in Secure Messaging: Lifting Security from Sessions to Conversations"
<a href="https://eprint.iacr.org/2022/1710.pdf" target="_blank">[PDF]</a>, by Cas Cremers, Charlie Jacomme,
and Aurora Naska, presented at <a href="https://www.usenix.org/conference/usenixsecurity23/glance">USENIX
2023</a>.
</li>
<li> "Automated Analysis of Protocols that use Authenticated Encryption: How Subtle AEAD Differences can impact
Protocol Security" <a href="https://inria.hal.science/hal-04126116" target="_blank">[PDF]</a>, by Cas Cremers,
Alexander Dax, Charlie Jacomme, and Mang Zhao, presented at <a
href="https://www.usenix.org/conference/usenixsecurity23/glance">USENIX 2023</a>.
</li>
<li> "Formal Analysis of SPDM: Security Protocol and Data Model version 1.2" <a
href="https://eprint.iacr.org/2022/1724.pdf" target="_blank">[PDF]</a>, by Cas Cremers, Alexander Dax, and
Aurora Naska, presented at <a href="https://www.usenix.org/conference/usenixsecurity23/glance">USENIX
2023</a>.
</li>
<li>"A formal analysis of IKEv2’s post-quantum extension" <a
href="https://www.mnm-team.org/pub/Publikationen/gggh21b/PDF-Version/gggh21b.pdf" target="_blank">[PDF]</a>,
by Stefan-Lukas Gazdag, Sophia Grundner-Culemann, Tobias Guggemos, Tobias Heider and Daniel Loebenberger,
presented at <a href="https://www.acsac.org/2021/">ACSAC 2021</a>.
</li>
<li>"Card Brand Mixup Attack: Bypassing the PIN in non-Visa Cards by Using Them for Visa Transactions " <a
href="https://www.usenix.org/system/files/sec21fall-basin.pdf" target="_blank">[PDF]</a>, by David Basin,
Ralf Sasse, and Jorge Toro-Pozo, presented at <a
href="https://www.usenix.org/conference/usenixsecurity21/fall-accepted-papers">Usenix Security 2021</a>.
</li>
<li>"The EMV Standard: Break, Fix, Verify" <a href="https://arxiv.org/pdf/2006.08249.pdf"
target="_blank">[PDF]</a>, by David Basin, Ralf Sasse, and Jorge Toro-Pozo, presented at <a
href="https://www.ieee-security.org/TC/SP2021/program-papers.html">IEEE Security and Privacy 2021</a>.
</li>
<li>"Clone Detection in Secure Messaging: Improving Post-Compromise Security in Practice" <a
href="https://people.cispa.io/cas.cremers/downloads/papers/CFKN2020-messaging_cloning.pdf"
target="_blank">[PDF]</a>, by Cas Cremers, Benjamin Kiesl, Jaiden Fairoze, and Aurora Naska, presented at <a
href="https://www.sigsac.org/ccs/CCS2020/">ACM CCS 2020</a>.
</li>
<li>"Formal Analysis and Implementation of a TPM 2.0-based Direct Anonymous Attestation Scheme" <a
href="https://ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/publications/pub2020/eccdaaimp-asiaccs20.pdf"
target="_blank">[PDF]</a>, by Jorden Whitefield, Liqun Chen, Ralf Sasse, Steve Schneider, Helen Treharne,
Stephan Wesemeyer, presented at <a href="https://asiaccs2020.cs.nthu.edu.tw/" target="_blank">ACM ASIACCS
2020</a>.</li>
<li>"A Formal Analysis of IEEE 802.11's WPA2: Countering the Kracks Caused by Cracking the Counters" <a
href="https://www.usenix.org/conference/usenixsecurity20/presentation/cremers" target="_blank">[PDF]</a>, by
Cas Cremers, Benjamin Kiesl, and Niklas Medinger, presented at <a
href="https://www.usenix.org/conference/usenixsecurity20">USENIX 2020</a>.
</li>
<li>"A Spectral Analysis of Noise: A Comprehensive, Automated, Formal Analysis of Diffie-Hellman Protocols" <a
href="https://cispa.saarland/group/cremers/downloads/papers/Noise-Usenix2020.pdf" target="_blank">[PDF]</a>,
by Guillaume Girol, Lucca Hirschi, Ralf Sasse, Dennis Jackson, Cas Cremers, and David Basin, presented at <a
href="https://www.usenix.org/conference/usenixsecurity20">USENIX 2020</a>.
</li>
<li>"A Symbolic Analysis of ECC-based Direct Anonymous Attestation" <a href="http://epubs.surrey.ac.uk/851685/"
target="_blank">[PDF]</a>, by Jorden Whitefield, Liqun Chen, Ralf Sasse, Steve Schneider, Helen Treharne,
Stephan Wesemeyer, presented at <a href="https://www.ieee-security.org/TC/EuroSP2019/" target="_blank">IEEE
EuroS&P 2019</a>.</li>
<li>"Component-Based Formal Analysis of 5G-AKA: Channel Assumptions and Session Confusion" <a
href="https://cispa.saarland/group/cremers/downloads/papers/CrDe2018-5G.pdf">[PDF]</a>, by Cas Cremers and
Martin Dehnel-Wild, presented at <a href="https://www.ndss-symposium.org/ndss2019/">NDSS 2019</a>.
<li>"Secure Authentication in the Grid: A formal analysis of DNP3: SAv5" <a
href="https://people.cispa.io/cas.cremers/downloads/papers/CDM-2019-DNP3_SAv5.pdf"
target="_blank">[PDF]</a>, by Cas Cremers, Martin Dehnel-Wild, Kevin Milner, published in <a
href="https://www.iospress.nl/journal/journal-of-computer-security/" target="_blank">Journal of Computer
Security</a>, 2018.</li>
<li>"A Formal Analysis of 5G Authentication" <a href="https://arxiv.org/pdf/1806.10360"
target="_blank">[PDF]</a>, by David Basin, Jannik Dreier, Lucca Hirschi, Saša Radomirović, Ralf Sasse,
Vincent Stettler, presented at <a href="https://www.sigsac.org/ccs/CCS2018/" target="_blank">CCS 2018</a>.
</li>
<li>"Alethea: A Provably Secure Random Sample Voting Protocol" <a
href="https://www.ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/publications/pub2018/Alethea_CSF18_BasinRadomirovicSchmid.pdf"
target="_blank">[PDF]</a>, by David Basin, Saša Radomirović, Lara Schmid, presented at <a
href="https://www.cs.ox.ac.uk/conferences/csf2018/" target="_blank">CSF 2018</a>.</li>
<li>"A Comprehensive Symbolic Analysis of TLS 1.3" <a
href="https://tls13tamarin.github.io/TLS13Tamarin/docs/tls13tamarin-draft21.pdf" target="_blank">[PDF]</a>,
by Cas Cremers, Marko Horvat, Jonathan Hoyland, Sam Scott, Thyla van der Merwe, presented at <a
href="http://www.sigsac.org/ccs/CCS2017/" target="_blank">CCS 2017</a>.</li>
<li>"Formal Analysis of Combinations of Secure Protocols" <a
href="https://hal.archives-ouvertes.fr/hal-01558552/" target="_blank">[PDF]</a>, by Elliott Blot, Jannik
Dreier, Pascal Lafourcade, presented at <a href="http://fps2017.loria.fr/" target="_blank">FPS 2017</a>.</li>
<li>"Towards a Mechanized Proof of Selene Receipt-Freeness and Vote-Privacy" <a
href="https://link.springer.com/chapter/10.1007/978-3-319-68687-5_7" target="_blank">[PDF]</a>, by
Alessandro Bruni, Eva Drewsen, Carsten Schürmann, presented at <a href="https://www.e-vote-id.org/"
target="_blank">E-Vote-ID 2017</a>.</li>
<li>"Secure Authentication in the Grid: A formal analysis of DNP3: SAv5" <a
href="https://cispa.saarland/group/cremers/downloads/papers/CDM-2019-DNP3_SAv5.pdf"
target="_blank">[PDF]</a>, by Cas Cremers, Martin Dehnel-Wild, Kevin Milner, presented at <a
href="https://www.ntnu.edu/web/esorics2017/" target="_blank">ESORICS 2017</a>.</li>
<li>"Formal Analysis of V2X Revocation Protocols" <a href="http://epubs.surrey.ac.uk/841862/"
target="_blank">[PDF]</a><a
href="http://www.computing.surrey.ac.uk/personal/st/H.Treharne/papers/2017/rewire.html" target="_blank">
[Source]</a>, by Jorden Whitefield, Liqun Chen, Frank Kargl, Andrew Paverd, Steve Schneider, Helen Treharne,
Stephan Wesemeyer, presented at <a href="http://stm2017.di.unimi.it/" target="_blank">STM 2017</a>.</li>
<li>"Formally Verifying Flow Integrity Properties in Industrial Systems" <a
href="http://hal.univ-grenoble-alpes.fr/hal-01527913/file/secrypt17.pdf" target="_blank">[PDF]</a>, by
Jannik Dreier, Maxime Puys, Marie-Laure Potet, Pascal Lafourcade, Jean-Louis Roch, presented at <a
href="http://www.secrypt.icete.org/?y=2017" target="_blank">SECRYPT 2017</a>.</li>
<li>"Designing and proving an EMV-compliant payment protocol for mobile devices" <a
href="https://hal.inria.fr/hal-01408584/document" target="_blank">[PDF]</a>, by Véronique Cortier, Alicia
Filipiak, Saïd Gharout, Jacques Traoré, presented at <a href="https://www.ieee-security.org/TC/EuroSP2017/"
target="_blank">EuroS&P 2017</a>.</li>
<li>"Automated Analysis of Secure Internet of Things Protocols" <a
href="https://dl.acm.org/citation.cfm?id=3134624" target="_blank">[PDF]</a>, by Jun Young Kim, Ralph Holz,
Wen Hu, Sanjay Jha, presented at <a href="https://www.acsac.org/2017/" target="_blank">ACSAC 2017</a>.</li>
<li>"Automated Analysis and Verification of TLS 1.3: 0-RTT, Resumption and Delayed Authentication" <a
href="https://cispa.saarland/group/cremers/downloads/papers/CHSV2016-TLS13.pdf" target="_blank">[PDF]</a>,
by Cas Cremers, Marko Horvat, Sam Scott, Thyla van der Merwe, presented at <a
href="http://www.ieee-security.org/TC/SP2016/" target="_blank">S&P 2016</a>.</li>
<li>"Automated Backward Analysis of PKCS#11 v2.20" <a href="http://dx.doi.org/10.1007/978-3-662-46666-7_12"
target="_blank">[PDF]</a>, by Robert Künnemann, presented at <a href="http://www.etaps.org/2015/post"
target="_blank">POST 2105</a>.</li>
<li>"ARPKI: Attack Resilient Public-Key Infrastructure" <a
href="https://www.ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/publications/pub2014/arpki.pdf"
target="_blank">[PDF]</a>, by David Basin, Cas Cremers, Tiffany Hyun-Jin Kim, Adrian Perrig, Ralf Sasse,
Pawel Szalachowski, presented at <a href="http://www.sigsac.org/ccs/CCS2014/" target="_blank">CCS 2014</a>,
also available extended journal version at <a href="https://www.computer.org/web/tdsc"
target="_blank">Transactions on Dependable and Secure Computing</a>: <a
href="https://www.ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/publications/pub2016/ARPKI-journal.pdf"
target="_blank">[PDF]</a>.</li>
<!-- Add bachelor, master, and PhD theses below -->
<li>Jorden Whitefield's PhD thesis <a href="http://epubs.surrey.ac.uk/852100/" target="_blank">[PDF]</a>:
Formal Analysis and Applications of Direct Anonymous Attestation
<a href="https://doi.org/10.5281/zenodo.3256109" target="_blank">[zip]</a>.
</li>
<li>Sabina Fischlin's master thesis <a
href="https://www.ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/software/ma-21-fischlin-zkp.pdf"
target="_blank">[PDF]</a>: Formalizing Zero-Knowledge Proofs in the Symbolic Model
<a href="https://www.ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/software/fischlin-zk_src.zip"
target="_blank">[zip]</a>.
</li>
<li>Mauro Zenoni's master thesis <a
href="https://www.ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/software/ma-20-zenoni-scion-hps.pdf"
target="_blank">[PDF]</a>: SCION's Hidden Paths Design Formal Security Analysis
<a href="https://www.ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/software/scion-hps-zenoni.zip"
target="_blank">[zip]</a>.
</li>
<li>Angela Rellstab's master thesis <a
href="https://www.ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/software/ma-19-rellstab-AKA.pdf"
target="_blank">[PDF]</a>: Formalizing and Verifying Generations of AKA Protocols
<a href="https://www.ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/software/aka-gens-rellstab.zip"
target="_blank">[zip]</a>.
</li>
<li>Sandra Dünki's master thesis <a
href="https://www.ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/software/ma-19-duenki-webmodel.pdf"
target="_blank">[PDF]</a>: Modelling and Analysis of Web Applications in Tamarin
<a href="https://www.ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/software/duenkis-webmodel.zip"
target="_blank">[zip]</a>.
</li>
<li>Xenia Hofmeier's bachelor thesis <a
href="https://www.ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/software/ba-19-hofmeier-oidc.pdf"
target="_blank">[PDF]</a>: Formal Analysis of Web Single-Sign On Protocols using Tamarin
<a href="https://www.ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/software/hofmeier-oidc.zip"
target="_blank">[zip]</a>.
</li>
<li>Guillaume Girol's master thesis <a
href="https://www.ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/software/ma-19-girol-noise.pdf"
target="_blank">[PDF]</a>: Formalizing and Verifying the Security Protocols from the Noise Framework
<a href="https://www.ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/software/noise-ggirol.zip"
target="_blank">[zip]</a>.
</li>
<li>Andris Suter-Dörig's bachelor thesis <a
href="https://www.ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/software/noise_suter-doerig.pdf"
target="_blank">[PDF]</a>: Formalizing and Verifying the Security Protocols from the Noise Framework
<a href="https://www.ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/software/noise.zip"
target="_blank">[zip]</a>.
</li>
<li>David Lanzenberger's bachelor thesis <a
href="https://www.ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/software/5G_lanzenberger.pdf"
target="_blank">[PDF]</a>: 5G protocols analysis and model
for Tamarin
<a href="https://www.ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/software/5G_lanzenberger.zip"
target="_blank">[zip]</a>.
</li>
<li>Vincent Stettler's bachelor thesis <a
href="https://www.ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/software/TLS-1.3_thesis_vincent_stettler.pdf"
target="_blank">[PDF]</a>: TLS1.3,v13 analysis
and model for Tamarin <a
href="https://www.ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/software/TLS-1.3-v13.zip"
target="_blank">[zip]</a>.</li>
</ul>
</div>
</div>
<script src="https://code.jquery.com/jquery-3.4.1.slim.min.js"
integrity="sha384-J6qa4849blE2+poT4WnyKhv5vZF5SrPo0iEjwBvKU7imGFAV0wwj1yYfoRSJoZ+n"
crossorigin="anonymous"></script>
<script src="https://cdn.jsdelivr.net/npm/[email protected]/dist/umd/popper.min.js"
integrity="sha384-Q6E9RHvbIyZFJoft+2mJbHaEWldlvI9IOYy5n3zV9zzTtmI3UksdQRVvoxMfooAo"
crossorigin="anonymous"></script>
<script src="https://stackpath.bootstrapcdn.com/bootstrap/4.4.1/js/bootstrap.min.js"
integrity="sha384-wfSDF2E50Y2D1uUdj0O3uMBJnjuUD4Ih7YwaYd1iqfktj0Uod8GCExl3Og8ifwB6"
crossorigin="anonymous"></script>
</body>
</html>