CSF 2019 Program

CSF 2019 Workshops Monday, June 24
08:00 - 18:00 Registration Desk
CSF 2019: Day 1 Tuesday, June 25
08:30 - 09:00 Breakfast
09:00 - 9:15 Opening Remarks
Invited Talk I (Session Chair: Limin Jia)
09:15 - 10:30 Legal Theorems of Privacy
Kobbi Nissim, Georgetown University
10:30 - 11:00 Break
Session 1: Information Flow (Session Chair: Alejandro Russo)
11:00 - 11:30 Optimising Faceted Secure Multi-Execution
M. Algehed, A. Russo, C. Flanagan
11:30 - 12:00 Canonical Representations of k-Safety-Hyperproperties
B. Finkbeiner, L. Haas, H. Torfah
12:00 - 12:30 Timing Leaks and Coarse-Grained Clocks
P. Vasilikos, F. Nielson, H. Nielson, B. Köpf
12:30 - 14:30 Lunch
Session 2: Security Protocols I (Session Chair: Joshua Guttman)
14:30 - 15:00 Decidability of a Sound Set of Inference Rules for Computational Indistinguishability
A. Koutsos
15:00 - 15:30 How To Wrap It Up - A Formally Verified Proposal for the use of Authenticated Wrapping in PKCS#11
A. Dax, S. Tangermann, R. Künnemann, M. Backes
15:30 - 16:00 Prime, Order Please! Revisiting Small Subgroup and Invalid Curve Attacks on Protocols using Diffie-Hellman (Distinguished paper)
C. Cremers, D. Jackson
16:00 - 16:30 Break/Poster
Short Talks (Session Chair: Cas Cremers)
16:30 - 18:00 5-Minute Poster/Research Talks
18:00 - 20:00 Reception
CSF 2019: Day 2 Wednesday, June 26
08:30 - 09:00 Breakfast
Session 3: Blockchain (Session Chair: Mayank Varia)
09:00 - 09:30 Re-thinking Untraceability in the CryptoNote-Style Blockchain
J. Yu, M. Au, P. Esteves-Verissimo
09:30 - 10:00 Time-dependent Decision-making and Decentralization in Proof-of-Work Cryptocurrencies
Y. Zolotavkin, J. Garcia, J. Liu
10:00 - 10:30 Analysis of Deterministic Longest-Chain Protocols
E. Shi
10:30 - 11:00 Break
Session 4: Computer-Aided Crypto (Session Chair: Véronique Cortier)
11:00 - 11:30 Symbolic Methods in Computational Cryptography Proofs
G. Barthe, B. Grégoire, C. Jacomme, S. Kremer, P. Strub
11:30 - 12:00 Formalizing Constructive Cryptography using CryptHOL
A. Lochbihler, S. Sefidgar, D. Basin, U. Maurer
12:00 - 12:30 EasyUC: Using EasyCrypt to Mechanize Proofs of Universally Composable Security
R. Canetti, A. Stoughton, M. Varia
12:30 - 14:30 Lunch
Invited Talk II (Session Chair: Andrei Sabelfeld)
14:30 - 15:30 Adversarial Machine Learning (AML): Research Trends and Directions
Somesh Jha, University of Wisconsin-Madison
15:30 - 16:00 Break/Poster
Session 5: Formal Methods and Verification — Attacker Model (Session Chair: Cas Cremers)
16:00 - 16:30 On the Meaning and Purpose of Attack Trees
H. Mantel, C. Probst
16:30 - 17:00 Efficient Attack-Defense Tree Analysis using Pareto Attribute Domains
B. Fila, W. Wideł
17:00 - 17:30 Games for Security under Adaptive Adversaries
T. Antonopoulos, T. Terauchi
17:30 - 18:00 Business Meeting (Chair: Andrei Sabelfeld)
CSF 2019: Day 3 Thursday, June 27
08:30 - 09:00 Breakfast
Session 6: Formal Methods and Verification — Secure Compilation (Session Chair: Catuscia Palamidessi)
09:00 - 09:30 Information-Flow Preservation in Compiler Optimisations
A. Dang, F. Besson, T. Jensen
09:30 - 10:00 Temporal Safety for Stack Allocated Memory on Capability Machines
S. Tsampas, D. Devriese, F. Piessens
10:00 - 10:30 Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation (Distinguished paper)
C. Abate, R. Blanco, D. Garg, C. Hritcu, M. Patrignani, J. Thibault
10:30 - 11:00 Break
Session 7: Hardware-based security (Session Chair: Musard Balliu)
11:00 - 11:30 Using Information Flow to Design an ISA that Controls Timing Channels
D. Zagieboylo, G. Suh, A. Myers
11:30 - 12:00 A Formal Approach to Secure Speculation
K. Cheang, C. Rasmussen, S. Seshia, P. Subramanyan
12:00 - 12:30 Information Flow Control for Distributed Trusted Execution Environments
A. Gollamudi, S. Chong, O. Arden
12:30 - 14:30 Lunch
Invited Talk III (Session Chair: Stéphanie Delaune)
14:30 - 15:30 WIM: An Expressive Formal Model of the Web Infrastructure
Ralf Küsters, University of Stuttgart
15:30 - 16:00 Break/Poster
Session 8: Language-based Security (Session Chair: David Naumann)
16:00 - 16:30 Securing Cross-App Interactions in IoT Platforms
M. Balliu, M. Merro, M. Pasqua
16:30 - 17:00 Static Enforcement of Security in Runtime Systems
M. Pedersen, A. Askarov
17:00 - 17:30 Beyond Labels: Permissiveness for Dynamic Information Flow Enforcement
E. Kozyri, F. Schneider, A. Bedford, J. Desharnais, N. Tawbi
18:00 - 21:30 Boat Cruise
CSF 2019: Day 4 Friday, June 28
08:30 - 09:00 Breakfast
Session 9: Security Protocols II (Session Chair: Bruno Blanchet)
09:00 - 09:30 BeleniosVS: Secrecy and Verifiability Against a Corrupted Voting Device
V. Cortier, A. Filipiak, J. Lallemand
09:30 - 10:30 Resource-Bounded Intruders in Denial of Service Attacks
A. Urquiza, M. AlTurki, M. Kanovich, T. Kirigin, V. Nigam, A. Scedrov, C. Talcott
10:00 - 10:30 Automated Verification of Accountability in Security Protocols (Distinguished paper)
R. Künnemann, I. Esiyok, M. Backes
10:30 - 11:00 Break
Session 10: Quantitative Information Flow (Session Chair: Stephen Chong)
11:00 - 11:30 Quantifying information Flow in Interactive Systems
D. Mestel
11:30 - 12:00 Deterministic Channel Design for Minimum Leakage
A. Américo, M. Khouzani, P. Malacaria
12:00 - 12:30 Comparing Systems: Max-Case Refinement Orders and Application to Differential Privacy
K. Chatzikokolakis, N. Fernandes, C. Palamidessi
12:30 Concluding Remarks

Invited Talk Abstracts

Legal Theorems of Privacy
Kobbi Nissim, Georgetown University, USA

There are significant gaps between legal and technical thinking around data privacy. Technical standards such as differential privacy and k-anonymity are described using mathematical language whereas legal standards often resort to concepts such as de-identification and anonymization which they do not define mathematically. As a result, arguments about the adequacy of technical privacy measures for satisfying legal privacy often lack rigor, and their conclusions are uncertain. The uncertainty is exacerbated by a litany of successful privacy attacks on privacy measures thought to meet legal expectations but then shown to fall short of doing so.

We ask whether it is possible to introduce mathematical rigor into such analyses, so as to make formal claims and prove “legal theorems” that technical privacy measures meet legal expectations. For that, we explore some of the gaps between these two very different approaches, and present initial strategies towards bridging these gaps considering examples from US and EU law.

Adversarial Machine Learning (AML): Research Trends and Directions
Somesh Jha, University of Wisconsin-Madison, USA

In this talk, we will discuss what happens to Machine Learning (ML) algorithms in the presence of an adversary. This field is called adversarial machine learning (AML), and in recent years the interest in this topic has exploded. We will systematically cover state-of-the art in AML and discuss various attacks (e.g. data poisoning, test-time attacks, and model stealing) and corresponding defenses. We will then explore "technical gaps" in the current state of the art in AML, which will lead to a discussion of open problems. We will also discuss lack of formal definitions and semantics in AML.

WIM: An Expressive Formal Model of the Web Infrastructure
Ralf Küsters, University of Stuttgart, Germany

The World Wide Web is a complex infrastructure with a rich set of security requirements and entities, such as DNS servers, web servers, and web browsers, interacting using diverse technologies. As illustrated by numerous attacks, rigorous analysis of the web infrastructure and web applications is indispensable.

In the last five years, we have therefore developed what we call the Web Infrastructure Model (WIM) in order to be able to formally analyze the security of web standards and applications. The WIM is a Dolev-Yao-style model which aims to precisely capture the web infrastructure, with its various standards, on an appropriate level of abstraction. It is the most comprehensive model of the web to date. We have used the WIM in the past few years to analyze various widespread web Single Sign-On (SSO) standards, including OAuth 2.0 and OpenID Connect, finding various new and partly severe attacks. We also proposed fixes and proved, for the first time, that the fixed standards are secure under appropriate assumptions. We have been in close contact with standardization organizations and actively support improving and fixing the standards.

In this talk, we present the WIM and discuss some of the case studies we carried out.

The talk is based on joint work with Daniel Fett and Guido Schmitz, published at S&P 2014, ESORICS 2015, CCS 2015, CCS 2016, and CSF 2017.


Title Authors
Deciding Trace Equivalence for Protocols with Asymmetric Operations Véronique Cortier, Stéphanie Delaune and Vaishnavi Sundararajan
Flowstate: A Language for Fault Tolerant Decentralized Computation Priyanka Mondal and Owen Arden
A Symbolic Framework for Analyzing Distance Bounding Protocols Alexandre Debant, Stephanie Delaune and Cyrille Wiedling
Improving Rider Safety Using QR Code & Fingerprint Biometrics Raghu Avula and Cliff Zou
A Structured Semantic Domain for Smart Contracts Sören Bleikertz, Andreas Lochbihler, Ognjen Mari, Simon Meier, Matthias Schmalz and Ratko G. Veprek
Principled Detection of Speculative Information Flows Marco Guarnieri, Boris Köpf, José F. Morales, Jan Reineke and Andrés Sánchez
New Axiomatization of Information Leakage Based on Core-Concavity Arthur Américo, Mhr. Khouzani and Pasquale Malacaria
Trollthrottle — Raising the Cost of Astroturfing Ilkan Esiyok, Lucjan Hanzlik, Robert Kuennemann, Lena M. Budde and Michael Backes
Application of the Expectation-Maximization Framework to Privacy Ehab Elsalamouny and Catuscia Palamidessi