Organization: Prof. Antoine Joux Program

10:00am-10:15am: Get together in the gather.town common space (15 min)

10:30am-10:50am: Benoît-Michel Cogliati (Researcher, CISPA) and Virginie Lallemand (Researcher, LORIA): Deterministic Authenticated Encryption GIAE from the Tweakable Pseudorandom Injection TableSpoon (20 min)

10:50am-11:00am: Discussion (10 min)

11:00am-11:20am: Bizhan Alipourpijani (PhD Student funded by DigiTrust, LORIA): Online Attacks on Picture Owner Privacy (20 min)

11:20am-11:30am: Discussion (10 min)

11:30am-01:00pm: Lunch break (90 min)

01:00pm-01:20pm: Robert Künnemann (Research group leader at CISPA): Accountability without bounds! (20 min)

01:20pm-01:30pm: Discussion (10 min)

01:30pm-01:35pm:  5-minute break

01:35pm-01:55pm: Jannik Dreier (Associate Professor at Université de Lorraine, member of the PESTO team at LORIA): Automatic Generation of Sources Lemmas in Tamarin: Towards Automatic Proofs of Security Protocols (20 min)

01:55pm-02:05pm: Discussion (10 min)

02:05pm-02:30pm: Final discussion (25 min)

Abstracts
Speakers: Benoît-Michel Cogliati (Research group leader at CISPA) and Virginie Lallemand (CNRS

researcher in the CARAMBA team at LORIA)

Title: Deterministic Authenticated Encryption GIAE from the Tweakable Pseudorandom Injection TableSpoon

Abstract: This paper explores the use of fixed-length Tweakable Pseudorandom Injections (TPRIs) in the context of deterministic authenticated encryption (DAE). First, we propose an efficient generic construction that turns a secure tweakable block cipher (TBC) into an expanding secure TPRI with minimal security loss. Second, we instantiate this generic structure and present TableSpoon, a fixed- length TPRI based on Deoxys-BC, the AES-based tweakable block cipher used in one of the winners of CAESAR. We design and analyze a new TPRI-based DAE scheme that bears similarities to the GCM-SIV mode of operation. Our new mode is highly efficient, parallelizable, and offers $(n+\min(n,t))/2$ bits of security, where n,t denote respectively the input block size and the tweak size of the underlying TPRI. When implemented using TableSpoon, we achieve speeds of 1.20 c/B during the encryption of 64kB messages on the Skylake microarchitecture, which is significantly faster than earlier TBC-based DAE schemes that offer similar security guarantees.

=====================================================================

Speaker: Bizhan Alipourpijani (PhD Student funded by DigiTrust, LORIA) Title: Online Attacks on Picture Owner Privacy

Abstract:
Facebook is the dominant platform for users to interact, share pictures, and stay connected to their friends. Attribute inference attacks are emerging threats to user privacy in social media such as Facebook. We present an online attribute inference attack by leveraging Facebook picture metadata (i) alt-text generated by Facebook to describe picture contents, and (ii) comments containing words, emojis posted by other Facebook users. Specifically, we study the correlation of the picture’s owner with Facebook generated alt-text and comments used by commenters when reacting to the picture. We concentrate on gender attribute, which is highly relevant for targeted advertising or privacy breaking. We explore how to launch an online gender inference attack on any Facebook user by handling online newly discovered vocabulary using the retrofitting process, for enriching a core vocabulary built during offline training. Our experiments show that even when the user hides most public data (e.g., friend list, public attribute, page, group), an attacker can detect user gender with AUC (area under the ROC curve) from 87% to 92%, depending on the picture metadata availability. Moreover, we can detect with high accuracy sequences of words leading to gender disclosure, and accordingly, enable users to derive countermeasures and configure safely their privacy settings.

=====================================================================

Speaker: Robert Künnemann (Research group leader at CISPA) Title: Accountability without bounds!

Abstract: Accountability in protocol design allows us to examine, justify and incentivize trust and provide a basis to act upon attacks that cannot be prevented a priori. We capture accountability as a protocol’s ability to identify the causes of any eventual violation of some security goal and translate it into trace properties that can be automatically verified. More recently, we extended this verification mechanism with support for an unbounded set of participants. Finally, we look at accountability in a setting where protocol parties are truly independent, i.e., they can choose not to follow the protocol without giving control to some designated adversary.

=====================================================================

Speaker: Jannik Dreier (Associate Professor at Université de Lorraine, member of the PESTO team at LORIA)

Title: Automatic Generation of Sources Lemmas in Tamarin: Towards Automatic Proofs of Security Protocols

Abstract: Tamarin is a popular tool dedicated to the formal analysis of security protocols. One major strength of the tool is that it offers an interactive mode, allowing to go beyond what push-button tools can typically handle. Tamarin is, for example, able to verify complex protocols such as TLS, 5G, or RFID protocols. However, one of its drawbacks is its lack of automation. For many simple protocols the user often needs to help Tamarin by writing specific lemmas, called “sources lemmas”, which requires some knowledge of the internal behavior of the tool.

In this paper, we propose a technique to automatically generate sources lemmas in Tamarin. We prove formally that our lemmas indeed hold for arbitrary protocols that make use of cryptographic primitives that can be modelled with a subterm convergent equational theory (modulo associativity and commutativity). We have implemented our approach within Tamarin. Our experiments show that, in most examples of the literature, we are now able to generate suitable sources lemmas automatically, in replacement of the hand-written lemmas. As a direct application, many simple protocols can now be analyzed fully automatically, while they previously required user interaction.