34th IEEE Computer Security Foundations Symposium

June 21-24, 2021 - Virtual Conference

CSF 2021 Program

All times are listed in US Eastern Daylight Saving Time (EDT), and also in parentheses in Central European Summer Time (CEST).

CSF 2021 Workshop Monday, June 21
09:00-16:00 (15:00-22:00) Foundations of Computer Security (FCS) Workshop
CSF 2021: Day 1 Tuesday, June 22
08:50-09:00 (14:50-15:00) Opening remarks
09:00-10:00 (15:00-16:00) Invited talk 1 (session chair: David Naumann)
Limin Jia - (Bridging) the gap between formal information flow security analysis and real world applications
10:00-10:30 (16:00-16:30) Coffee break
10:30-11:30 (16:30-17:30) Session 1: Information flow (session chair: Musard Balliu)
  1. Statistical Model Checking for Hyperproperties - Yu Wang, Siddhartha Nalluri, Borzoo Bonakdarpour, Miroslav Pajic
  2. On Compositional Information Flow Aware Refinement - Christoph Baumann, Mads Dam, Roberto Guanciale, Hamed Nemati
  3. Backwards-directed information flow analysis for concurrent programs - Kirsten Winter, Graeme Smith, NIcholas Coughlin
  4. Gradual Security Types and Gradual Guarantees - Abhishek Bichhawat, McKenna McCall, Limin Jia
11:30-11:45 (17:30-17:45) Coffee break
11:45-12:45 (17:45-18:45) Session 2: Information Flow and Language-Based Security (session chair: Andrei Sabelfeld)
  1. Dynamic IFC Theorems for Free - Maximilian Algehed, Jean-Philippe Bernardy, Catalin Hritcu
  2. Towards Language-Based Mitigation of Traffic Analysis Attacks - Jeppe Blaabjerg, Aslan Askarov
  3. A Quantale of Information - Sebastian Hunt, David Sands
  4. Resource-Aware Session Types for Digital Contracts - Ankush Das, Stephanie Balzer, Jan Hoffmann, Frank Pfenning, Ishani Santurkar
12:45-13:00 (18:45-19:00) Coffee break
13:00-13:45 (19:00-19:45) Lunch/dinner break
13:45-14:45 (19:45-20:45) Session 3: E-Voting and Accountability (session chair: Veronique Cortier)
  1. Fixing the Achilles Heel of E-Voting: The Bulletin Board - Lucca Hirschi, Lara Schmid, David Basin
  2. Election Verifiability Revisited: Automated Security Proofs and Attacks on Helios and Belenios - Sevdenur Baloglu, Sergiu Bursuc, Sjouke Mauw, Jun Pang
  3. Accountability in the Decentralised-Adversary Setting - Robert Künnemann, Deepak Garg, Michael Backes
  4. Verifying Accountability for Unbounded Sets of Participants - Kevin Morio, Robert Künnemann
14:45-15:00 (20:45-21:00) Coffee break
15:00-15:45 (21:00-21:45) Session 4: Cryptography (session chair: Sabine Oechsner)
  1. Concise UC Zero-Knowledge Proofs for Oblivious Updatable Databases - Jan Camenisch, Maria Dubovitskaya, Alfredo Rial
  2. Efficient Constructions of Pairing Based Accumulators - Ioanna Karantaidou, Foteini Baldimtsi
  3. Cooking Cryptographers: Secure Multiparty Computation Based on Balls and Bags - Daiki Miyahara, Yuichi Komano, Takaaki Mizuki, Hideaki Sone
15:45-16:00 (21:45-22:00) Coffee break
16:00-16:30 (22:00-22:30) Five minute talks I (session chair: Guido Schmitz)
CSF 2021: Day 2 Wednesday, June 23
09:00-10:00 (15:00-16:00) Invited talk 2 (session chair: Ante Derek)
Peter Sewell - CHERI capability-enhanced Arm (Morello), RISC-V, and MIPS: semantics, semantics-based testing, and security-property proofs
10:00-10:30 (16:00-16:30) Coffee break
10:30-11:30 (16:30-17:30) Session 5: Language-Based Security (session chair: Aslan Askarov)
  1. Secure Compilation of Constant-Resource Programs - Gilles Barthe, Sandrine Blazy, Rémi Hutin, David Pichardie
  2. Relational Analysis of Sensor Attacks on Cyber-Physical Systems - Jian Xiang, Nathan Fulton, Stephen Chong
  3. CapablePtrs: Securely Compiling Partial Programs using the Pointers-as-Capabilities Principle - Akram El-Korashy, Stelios Tsampas, Marco Patrignani, Dominique Devriese, Deepak Garg, Frank Piessens
  4. Language Support for Secure Software Development with Enclaves - Aditya Oak, Amir M. Ahmadian, Musard Balliu, Guido Salvaneschi
11:30-11:45 (17:30-17:45) Coffee break
11:45-12:45 (17:45-18:45) Session 6: Security Protocols (session chair: Robert Künnemann)
  1. Performing Security Proofs of Stateful Protocols - Andreas V. Hess, Sebastian Mödersheim, Achim D. Brucker, Anders Schlichtkrull
  2. Formal Verification of Secure Forwarding Protocols - Tobias Klenze, Christoph Sprenger, David Basin
  3. Vertical Composition and Sound Payload Abstraction for Stateful Protocols - Sébastien Gondron, Sebastian Mödersheim
  4. On the Soundness of Infrastructure Adversaries - Alexander Dax, Robert Künnemann
12:45-13:00 (18:45-19:00) Coffee break
13:00-13:45 (19:00-19:45) Lunch/dinner break
13:45-14:45 (19:45-20:45) Session 7: Security Metrics and Policy Inference (session chair: Catuscia Palamidessi)
  1. Formal impact metrics for cyber-physical attacks - Ruggero Lanotte, Massimo Merro, Simone Tini, Andrei Munteanu
  2. Efficient Algorithms for Quantitative Attack Tree Analysis - Carlos E. Budde, Mariëlle Stoelinga
  3. Concavity, Core-concavity, Quasiconcavity: A Generalizing Framework for Entropy Measures - Arthur Américo, Pasquale Malacaria
  4. Automating Audit with Policy Inference - Abhishek Bichhawat, Matt Fredrikson, Jean Yang
14:45-15:00 (20:45-21:00) Coffee break
15:00-15:45 (21:00-21:45) Session 8: Blockchains and Smart Contracts (session chair: Aggelos Kiayias)
  1. Kachina - Foundations of Private Smart Contracts - Thomas Kerber, Aggelos Kiayias, Markulf Kohlweiss
  2. Computationally sound Bitcoin tokens - Massimo Bartoletti, Stefano Lande, Roberto Zunino
  3. Formalizing Nakamoto-Style Proof of Stake - Søren Eller Thomsen, Bas Spitters
15:45-16:00 (21:45-22:00) Coffee break
16:00-16:30 (22:00-22:30) Five minute talks II (session chair: Guido Schmitz)
16:30-17:30 (22:30-23:30) PhD mentoring session I
CSF 2021: Day 3 Thursday, June 24
09:00-10:00 (15:00-16:00) Invited talk 3 (session chair: Ralf Küsters)
Carmela Troncoso - Designing technology in pandemic times
10:00-10:30 (16:00-16:30) Coffee break
10:30-11:30 (16:30-17:30) Session 9: Machine Learning, Privacy, and Cryptography (session chair: Joshua D Guttman)
  1. DDUO: General-Purpose Dynamic Analysis for Differential Privacy - Chike Abuah, Alex Silence, David Darais, Joe Near
  2. Yes We can: Watermarking Machine Learning Models beyond Classification - Sofiane Lounici, Mohamed Njeh, Orhan Ermis, Melek Önen, Slim Trabelsi
  3. Consistency for Functional Encryption - Christian Badertscher, Aggelos Kiayias, Markulf Kohlweiss, Hendrik Waldner
  4. A Formal Information-Theoretic Leakage Analysis of Order-Revealing Encryption - Mireya Jurado, Catuscia Palamidessi, Geoffrey Smith
11:30-11:45 (17:30-17:45) Coffee break
11:45-12:45 (17:45-18:45) Session 10: Cryptography and Verification I (session chair: Cas Cremers)
  1. A Coq proof of the correctness of X25519 in TweetNaCl - Peter Schwabe, Benoît Viguier, Timmy Weerwag, Freek Wiedijk
  2. Machine-Checking Unforgeability Proofs for Signature Schemes with Tight Reductions to the Computational Diffie-Hellman Problem - François Dupressoir, Sara Zain
  3. Abstract Modeling of System Communication in Constructive Cryptography using CryptHOL - David Basin, Andreas Lochbihler, Ueli Maurer, S. Reza Sefidgar
  4. SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq - Carmine Abate, Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Catalin Hritcu, Kenji Maillard, Bas Spitters
12:45-13:00 (18:45-19:00) Coffee break
13:00-13:45 (19:00-19:45) Lunch/dinner break
13:45-14:30 (19:45-20:30) Session 11: Cryptography and Verification II (session chair: Ran Canetti)
  1. Mechanised Models and Proofs for Distance-Bounding - Ioana Boureanu, Constantin Catalin Dragan, François Dupressoir, David Gerault, Pascal Lafourcade
  2. Formal security analysis of MPC-in-the-head zero-knowledge protocols - Nikolaj Sidorenco, Sabine Oechsner, Bas Spitters
  3. Verified Multiple-Time Signature Scheme from One-Time Signatures and Timestamping - Denis Firsov, Henri Lakk, Ahto Truu
14:30-14:45 (20:30-20:45) Coffee break
14:45-15:15 (20:45-21:15) Session 12: Network Security and Policy Verification (session chair: Limin Jia)
  1. Heuristic Approach for Countermeasure Selection Using Attack Graphs - Orly Stan, Ron Bitton, Michal Ezrets, Moran Dadon, Yuval Elovici, Asaf Shabtai, Masaki Inokuchi, Yoshinobu Ohta, Tomohiko Yagyu
  2. Verifying Hyperproperties with TLA - Leslie Lamport, Fred B. Schneider
15:15-15:30 (21:15-21:30) Coffee break
15:30-16:30 (21:30-22:30) Business and awards
16:30-17:15 (22:30-23:15) Virtual social hangout (bring your own favorite drink)
17:15-18:15 (23:15-00:15) PhD mentoring session II