SRM seminar

SaToSS home
APSIA home

• Related seminars
• SRM
• SRM 2023
• SRM 2022
• SRM 2021
• SRM 2020
• SRM 2019
• SRM 2018
• SRM 2017
• SRM 2016
• SRM 2015
• SRM 2014
• SRM 2013
• SRM 2012
• SRM 2011
• SRM 2010
• SRM 2009
• Seminar Rules

Abstracts

• Speaker: Clément Aubert (Augusta University)
• Title: A gentle introduction to reversible process algebras
• Abstract: Reversible computation gained a lot of traction in recent years thanks to the promise of low-energy, quantum and / or more secure computation. In this talk, I will start by giving a general introduction to the study of reversible process algebras, used to represent and study protocols and interactions between reversible actors. Focusing on reversible CCS (that is, without name-passing ability), I will then give a brief tour of some of the open problems, recent progresses, and connections to other fields.

• Speaker: Boris Skoric (TU Eindhoven)
• Title: Can't Touch This: unconditional tamper evidence from short keys
• Abstract: Storing data on an external server with information-theoretic security, while using a key shorter than the data itself, is impossible. As an alternative, we propose a scheme that achieves information-theoretically secure tamper evidence: The server is able to obtain information about the stored data, but not while staying undetected. Moreover, the client only needs to remember a key whose length is much shorter than the data. We provide a security proof for our scheme, based on an entropic uncertainty relation, similar to QKD proofs. Our scheme works if Alice is able to (reversibly) randomise the message to almost-uniformity with only a short key. By constructing an explicit attack we show that short-key unconditional tamper evidence cannot be achieved without this randomisability. https://arxiv.org/abs/2006.02476

• Speaker: Sebastian Mödersheim (Technical University of Denmark)
• Title: Logic for Privacy in Security Protocols
• Abstract: (alpha,beta)-privacy is an approach to the verification of privacy properties of security protocols. While the de-facto standard is to express privacy as an observational equivalence of two processes, (alpha,beta)-privacy goes a radically different way to formulate privacy a reachability problem, where every state is characterized by two formulae alpha and beta. Here, alpha formalizes all the information that has been intentionally revealed so far, e.g. the result of an election, and that the intruder is allowed to know. In contrast, beta formalizes what the intruder actually has found out by observing messages, performing tests on these messages, and interacting with other agents. In fact, we assume that the intruder knows the protocol and thus can perform a symbolic execution that can be contrasted with the actual observations. A given state violates alpha-beta privacy, if beta implies any privacy-relevant facts that do not follow from alpha already. We give a brief overview of the methods for a decision procedure to check if such a privacy-violating state is reachable within a given number of steps.

• Speaker: Simon Parkin (TU Delft)
• Title: Refining the Blunt Instruments of Cyber-Risk Management
• Abstract: Well-meaning cybersecurity risk owners will deploy controls and countermeasures in an effort to manage the risks they see affecting their services or systems. These controls and countermeasures may produce unintended, negative harms themselves, adversely affecting user behaviour, user inclusion, or the infrastructure itself. Here I will first describe a framework for exploring the potential unintended harms of security and privacy controls [1], informed by a range of case studies. I will then describe subsequent work to explore how existing cyber-risk management approaches can be adapted to be less ‘blunt’ and more precise [2], to preserve legitimate behaviours while preventing malicious behaviours within a managed system. The approaches described here will also be considered from the perspective of trustworthiness in online services, and the security and privacy incentives of different stakeholders interacting within these services.
  [1] Chua et al., “Identifying Unintended Harms of Cybersecurity Countermeasures”, https://discovery.ucl.ac.uk/id/eprint/10088657/
  [2] Parkin & Chua, “A cyber-risk framework for coordination of the prevention and preservation of behaviours”, https://content.iospress.com/articles/journal-of-computer-security/jcs210047
  Bio: Simon is an Assistant Professor in the Cybersecurity group in the Technology, Policy, and Management (TPM) faculty at the Delft University of Technology (TU Delft, Netherlands). His specialization is in human-centred security: usability and perceptions of security-related technologies, security behaviour change, security economics, and decision-making in security technology management, support, and policy. Current research includes: examining how best to position security and remediation support for users of consumer IoT devices; practitioner experiences and decisions in patching of IT systems in complex organizations, and; multi-stakeholder perspectives on the management of employee-facing security in organizations.

• Speaker: Chenxiang Zhang (University of Pisa)
• Title: Elements of Robust Machine Learning
• Abstract: Robust Machine Learning (ML) is critical for the applications in safety-critical domains such as autonomous driving or medical diagnosis. In this seminar, we will focus on the challenges of detecting and generalizing to out-of-distribution data. In other words, robust models should confidently detect dissimilar data from the training distribution, but at the same time generalize to similar data with a slightly shifted distribution. We will introduce two methods to attack these problems: a simple baseline called “deep ensembles”, and a computationally efficient family of models “deterministic uncertainty methods”. Lastly, we will present a few general techniques to improve both the predictive and uncertainty performance. By the end of the seminar, attendees will gain insights into evaluating the reliability of ML models.

• Speaker: Lenore Zuck (University of Illinois, Chicago)
• Title: Accountable Javascript Code Delivery
• Abstract: RFCs (Requests For Comments) are IETF documents that, among other things, describe the Internet’s technical foundations. They have become the official record of the Internet’s design decisions, architecture, and technical standards. In particular, they are considered the official specifications of the Internet’s protocols. The talk explores the benefits of rigorous specifications, and the space between specifications, as provided in RFCs, and rigorous specifications. We will use TCP as a running example and diverge into some examples from recent studies of QUIC.
  Micro CV: Professor at computer science department in University of Illinois Chicago. Before that, at NYU and Yale. Graduated the Weizmann Institute under the supervision of Amir Pnueli. ACM distinguished scientist. Served as a program director at the National Science Foundation, was an (acting) lead program director of the Trustworthy Computing program (currently, SaTC). Areas of research include temporal logic, verification, distributed systems, compiler validation, specification based testing, networking, security, privacy, and ethics.

• Speaker: Rosario Giustolisi (IT University of Copenhagen)
• Title: Last-minute coercion resistance in deniable revoting
• Abstract: Counter-strategies are key components of any coercion-resistant voting scheme, allowing voters to submit votes that represent their own intentions in an environment controlled by a coercer. By deploying a counter-strategy a voter can prevent the coercer from learning if the voter followed the coercer’s instructions or not. Two effective counter-strategies have been proposed in the literature, one based on fake credentials and another on revoting. While fake-credential schemes assume that voters can hide cryptographic keys away from the coercer, revoting-based schemes assume that voters can revote after being coerced.
  In this work, we present a new counter-strategy technique that enables flexible vote updating, that is, a revoting approach that provides protection against coercion even if the adversary is able to coerce a voter at the very last minute of the voting phase. We demonstrate that our technique is effective by implementing it in an Internet-based coercion-resistant voting scheme that allows revoting. To the best of our knowledge, we provide the first technique that enables deniable revoting and that can simultaneously evade last-minute voter coercion.

• Speaker: Ilkan Esiyok (CISPA Helmholtz Center for Information Security)
• Title: Accountable Javascript Code Delivery
• Abstract:The Internet is a major distribution platform for web applications, but there are no effective transparency and audit mechanisms in place for the web. Due to the ephemeral nature of web applications, a client visiting a website has no guarantee that the code it receives today is the same as yesterday, or the same as other visitors receive. Despite advances in web security, it is thus challenging to audit web applications before they are rendered in the browser. We propose Accountable JS, a browser extension and opt-in protocol for accountable delivery of active content on a web page. We prototype our protocol, formally model its security properties with the Tamarin Prover, and evaluate its compatibility and performance impact with case studies including WhatsApp Web, AdSense and Nimiq. Accountability is beginning to be deployed at scale, with Meta’s recent announcement of Code Verify available to all 2 billion WhatsApp users, but there has been little formal analysis of such protocols. We formally model Code Verify using the Tamarin Prover and compare its properties to our Accountable JS protocol. We also compare Code Verify’s and Accountable JS extension's performance impacts on WhatsApp Web.
  Joint work with Pascal Berrang, Katriel Cohn-Gordon, and Robert Künnemann. To appear at NDSS 2023.

• Speaker: Felix Stutz (MPI-SWS Saarbrücken)
• Title: On Implementability of Asynchronous Communication Protocols
• Abstract: Implementing communication protocols is a routine task for distributed software. However, verifying that a protocol is implemented correctly is challenging. The implementability problem, which asks if a (global) protocol can be implemented locally, has been studied from two perspectives. On the one hand, multiparty session types (MSTs) provide a type-theoretic approach which is very efficient but restricts the expressiveness of protocols. On the other hand, high-level message sequence charts (HMSCs) do not impose any restrictions on the protocols, yielding undecidability of the implementability problem for HMSCs. Consequently, model-checking can easily diverge but also suffers from high complexity. Our research aims to find a middle ground between both approaches. In this talk, I will first present an extended MST framework, taking a first step towards a sweet-spot between expressiveness and efficiency. Most notably, it allows a sender to send to multiple receivers as well as a receiver to receive from multiple senders upon branching, making MST verification eligible for common patterns from distributed computing. In the second part, I will elaborate on our decidability result for MST implementability. To show decidability, we exploit our formal encoding from MSTs to HMSCs, generalise results for the latter, and prove that any implementable MST falls into a class of HMSCs with decidable implementability. Last, I will showcase techniques from the HMSC domain that become applicable in the MST setting with these results.
  Based on: - Generalising Projection in Asynchronous Multiparty Session Types | Rupak Majumdar, Madhavan Mukund, Felix Stutz, Damien Zufferey | CONCUR21 | https://arxiv.org/abs/2107.03984
  - Comparing Channel Restrictions of Communicating State Machines, High-level Message Sequence Charts, and Multiparty Session Types | Felix Stutz, Damien Zufferey | GandALF22 | https://arxiv.org/abs/2208.05559
  - Asynchronous Multiparty Session Type Implementability is Decidable - Lessons Learned from Message Sequence Charts | Felix Stutz | To Appear in ECOOP23 | https://arxiv.org/abs/2302.11272

• Speaker: Enka Blanchard (CNRS, Université Polytechnique Hauts-de-France)
• Title: Smörgåsbord of interdisciplinary security
• Abstract:As referenced in the PEBCAK acronym, a significant proportion of security issues (both physical and online) have their sources between the chair and keyboard. Indeed, very few cryptographic systems can resist an "admin/password1" combo. The last 20 years have seen many interesting reflexions on how users and institutions interact with security systems and how these not always rational behaviours have to be integrated at all stages of development. However, some of this research requires familiarity or at least interaction with social sciences. This hurdle means that many results are still poorly known outside of their initial fields, especially in certain countries with strong disciplinary borders (such as France).
  This talk will try to give an introduction to some of these questions by going over two main themes I've explored over the last years : e-voting and authentication. I'll illustrate both with a set of results illustrating some of the varied questions and techniques from usable security. I will finish by quickly going over an analysis we just published on the (lack of) logic of research funding practices and how the methods used go against their stated objectives.

• Speaker: Tobias Käfer (Karlsruher Institute of Technology)
• Title: Knowledge Graphs, Behaviour, and Agents on the Web
• Abstract: Traditionally - and with tremendous deployment nowadays, knowledge graphs are being used to model and manage largely static data using ontologies and in triple stores. This talk covers our research to introduce behaviour to the semantic web stack, with the help of Abstract State Machines, Process Modelling, the Web architecture, and Agents. The talk also contains prototypes we built for some of the discussed approaches.

• Speaker: Christoph Braun (Karlsruher Institute of Technology)
• Title: Authentication Protocols based on Verifiable Credentials on the Web
• Abstract: We examine authentication protocols in the various use cases of the recently emerging Web standards of the W3C Verifiable Credential (VC) data model W3C Decentralised Identifiers (DIDs), and the Solid Protocol. We analyse underlying use cases of VCs and review current implementation guidelines. We model an exemplary authentication protocol based on Verifiable Credentials on the Web. We verify that the protocol is robust against man-in-the-middle attacks: This approach yields us precisely evaluated guidelines for implementing authentication protocols employing the latest standards of VC, DIDs and related proposals. Applying and combining the VC recommendation and related specifications in authentication protocols may seem trivial at first, but preliminary investigations show that existing guidelines are not sufficiently tight to guard against man-in-the-middle attacks.

• Speaker: Naipeng Dong (The University of Queensland)
• Title: Formal and Quantitative Analysis of Blockchain
• Abstract: Blockchain is gaining significant attentions in both industry and academia given its increasingly wider applications such as Web 3 and NFT with the support of smart contract programming. However, most industrial development and academic research have primarily focused on the blockchain applications, but concerns remain on the safety and security of their foundational layers. This talk will discuss our preliminary works on using formal and quantitative analyses of these foundational layers, as well as the challenges and opportunities of this research direction.

Back to SRM presentations.

Contact

For questions and comments contact Jun or Peter .