Publications 2019

César Sánchez, Gerardo Schneider, Wolfgang Ahrendt, Ezio Bartocci, Domenico Bianculli, Christian Colombo, Yliés Falcone, Adrian Francalanza, Srđan Krstić, João M. Lourenço, Dejan Nickovic, Gordon J. Pace, Jose Rufino, Julien Signoles, Dmitriy Traytel, Alexander Weiss
A Survey of Challenges for Runtime Verification from Advanced Application Domains (Beyond Software)
In Formal Methods in System Design, 54(3), pp. 279–335
[external pageBIB | external pagePDF | external pageDOI]

David Basin, Bhargav Bhatt, Srđan Krstić, Dmitriy Traytel
Almost Event-Rate Independent Monitoring
In Formal Methods in System Design, 54(3), pp. 449–478
[BIB | PDF | external pageDOI]

Martin Raszyk, David Basin, Srđan Krstić, Dmitriy Traytel
Multi-Head Monitoring of Metric Temporal Logic
In Chen, Y.-F., Cheng, C.-H., and Esparza, J. (eds.) 17th International Symposium on Automated Technology for Verification and Analysis (ATVA 2019), LNCS 11781, 151–170, Springer
[BIB | PDF | external pageDOI]

Matthias Brun, Dmitriy Traytel
Generic Authenticated Data Structures, Formally
In Tolmach, A., Harrison, J., O'Leary, J. (eds.) 10th Conference on Interactive Theorem Proving (ITP 2019), LIPIcs 141, pp. 10:1–10:18, Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik
[external pageBIB | external pagePDF | external pageDOI]

Andrei Popecsu, Dmitriy Traytel
A Formally Verified Abstract Account of Gödel's Incompleteness Theorems
In Fontaine, P. (ed.) 27th International Conference on Automated Deduction (CADE-27), LNCS 11716, pp. 442–461, Springer
[external pageBIB | external pagePDF | external pageDOI]

Martin Raszyk, David Basin, Dmitriy Traytel
From Nondeterministic to Multi-Head Deterministic Finite-State Transducers
In Baier, C. (ed.) 46th International Colloquium on Automata, Languages and Programming (ICALP 2019), LIPIcs 132, pp. 127:1–127:14, Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik
[BIB | PDF | external pageDOI]

Jasmin Christian Blanchette, Lorenzo Gheri, Andrei Popescu, Dmitriy Traytel
Bindings as Bounded Natural Functors
In Weirich, S. (ed.) 46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019), Article 22, pp. 22:1–22:34, ACM
[external pageBIB | external pagePDF | external pageDOI]

Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel
A Verified Prover Based on Ordered Resolution
In Mahboubi, A., Myreen, M. O. (eds.) 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2019), 152–165, ACM
[external pageBIB | external pagePDF | external pageDOI]

David M. Sommmer, Sebastian Meiser, Esfandiar Mohammadi
Privacy Loss Classes: The Central Limit Theorem in Differential Privacy
In Proceedings on Privacy Enhancing Technologies
[DownloadBIB (BIB, 487 Bytes) | DownloadPDF (PDF, 1.9 MB) | external pageDOI]

Joshua Schneider, David Basin, Frederik Brix, Srđan Krstić, Dmitriy Traytel
Adaptive Online First-Order Monitoring
In: 17th International Symposium on Automated Technology for Verification and Analysis (ATVA), Taipei, Taiwan, 2019
[DownloadBIB (BIB, 2 KB) | DownloadPDF (PDF, 269 KB) | external pageDOI]

Joshua Schneider, David Basin, Srđan Krstić, Dmitriy Traytel
A Formally Verified Monitor for Metric First-Order Temporal Logic
In: 19th International Conference on Runtime Verification (RV), Porto, Portugal, 2019
[DownloadBIB (BIB, 1 KB) | DownloadPDF (PDF, 276 KB) | external pageDOI]

Andreas Lochbihler, Seyed Reza Sefidgar, David Basin, Ueli Maurer
Formalizing Constructive Cryptography using CryptHOL
In: IEEE 32nd Computer Security Foundations Symposium (CSF), 2019
[DownloadBIB (BIB, 486 Bytes) | DownloadPDF (PDF, 550 KB) | external pageDOI]

Sjouke Mauw, Zach Smith, Jorge Toro-Pozo, and Rolando Trujillo-Rasua
Post-Collusion Security and Distance Bounding
In: ACM Conference on Computer and Communications Security (CCS), 2019.
[DownloadBIB (BIB, 882 Bytes) | external pagePDF | external pageDOI]

Sven Hammann, Sasa Radomirovic, Ralf Sasse, and David Basin
User Account Access Graphs
In: ACM Conference on Computer and Communications Security (CCS), 2019.
[DownloadBIB (BIB, 660 Bytes) | DownloadPDF (PDF, 774 KB) | external pageDOI]

Dennis Jackson, Cas Cremers, Katriel Cohn-Gordon, Ralf Sasse
Seems Legit: Automated Analysis of Subtle Attacks on Protocols that Use Signatures
In: ACM Conference on Computer and Communications Security (CCS), 2019.
[DownloadBIB (BIB, 768 Bytes) | external pagePDF (long version) | external pageDOI]

David Basin, Lucca Hirschi, Ralf Sasse
Symbolic Analysis of Identity-Based Protocols
In: Foundations of Security, Protocols, and Equational Reasoning - Essays Dedicated to Catherine A. Meadows -- CathyFest 2019, LNCS volume 11565, 2019
[DownloadBIB (BIB, 1 KB) | DownloadPDF (PDF, 454 KB) | external pageDOI]

Jorden Whitefield, Liqun Chen, Ralf Sasse, Steve Schneider, Helen Treharne, Stephan Wesemeyer
A Symbolic Analysis of ECC-based Direct Anonymous Attestation
In: EuroS&P 2019, 2019
[DownloadBIB (BIB, 1 KB) | DownloadPDF (PDF, 475 KB) | external pageDOI]

Peter Lammich, Seyed Reza Sefidgar
Formalizing Network Flow Algorithms: A Refinement Approach in Isabelle/HOL
In: Journal of Automated Reasoning, 62(2): 261-280, 2019
[DownloadBIB (BIB, 376 Bytes) | external pagePDF | external pageDOI]

Damien Desfontaines, Andreas Lochbihler, and David Basin
Cardinality Estimators do not Preserve Privacy
In: Proceedings on Privacy Enhancing Technologies, 2019 (2)
[DownloadBIB (BIB, 2 KB) | DownloadPDF (PDF, 825 KB) | external pageDOI]

Pern Hui Chia, Damien Desfontaines, Milinda Perera, Chao Li, Daniel Simmons-Marengo, Wei-Yen Day, Qiushi Wang, and Miguel Guevara
KHyperLogLog: Estimating Reidentifiability and Joinability of Large Data at Scale
In: 40th IEEE Symposium on Security and Privacy (S&P), San Francisco, CA, USA, 2019
[DownloadBIB (BIB, 413 Bytes) | external pagePDF | external pageDOI]

David Sommer, Aritra Dhar, Esfandiar Mohammadi, Daniel Ronzani, and Srdjan Capkun.
Deniable Upload and Download via Passive Participation.
In: USENIX Symposium on Networked Systems Design and Implementation (NSDI), Boston USA, 2019.
[external pageBIB | DownloadPDF (PDF, 1.6 MB) | external pageDOI]