Abstracts
- Speaker: Bill Roscoe
- Title: Generating an unbiassable random oracle within a blockchain using delay encryption
- Abstract: We assume that the agents in a blockchain are potentially self interested parties, most of whom will be “good” (follow mandated protocols) and who all possess reasonably accurate clocks. We cannot, however, demand that all agents deliver all their obligations in a timely manner because of communications issues, and cannot distinguish between a party who deliberately withholds a communication and one whose communication medium goes down. In this context the device of a predetermined group of agents committing a share of a future random value V and decommitting it when V is due is either trivial to undermine or trivial to bias. To overcome this we develop an exact time delay (time lock) encryption method for blockchains and show how it can remove the problems from the random oracle.
- Speaker: Robert Luh
- Title: PenQuest: An adversarial cyber security game for education and threat assessment
- Abstract: The complex interplay of attack techniques and possible countermeasures often makes it difficult to appropriately plan, implement, and evaluate an organization’s defense. In this talk, we introduce PenQuest, a strategy game based on a security meta model that is designed to present a complete view on information system attacks and their mitigation while providing a tool for risk assessment and security education through a wide but flexible range of actors, assets, and actions.
PenQuest simulates attacker & defender behavior as part of a dynamic, imperfect information multiplayer game that derives its ruleset from established information security sources such as MITRE ATT&CK, STIX, and NIST SP 800-53. Attack techniques, vulnerabilities, and mitigating controls are mapped to game elements such as player actions or equipment. We are currently implementing PenQuest as a digital multi-player game, which we are happy to introduce in this talk.
- Speaker: Nicolas Troquard
- Title: Logics of bringing-it-about and some of their applications
- Abstract: We introduce the logics of agency, with a focus on the logics of bringing-it-about. We present a few of their applications for modelling social influence and the use of artefacts.
- Speaker: Lutz Strassburger
- Title: On Combinatorial Proof Identity for First-Order Logic
- Abstract: In this talk I will explore the relationship between combinatorial proofs
for first-order logic and a deep inference proof system for first-order
logic. In particular, I will discuss the decomposition of a proof into a
linear part and a resource management part. Based on this, I will argue
that combinatorial proofs can serve as way to define a universal notion of
proof identity.
This talk is based on a joint work with Dominic Hughes and Jui-Hsuan Wu
(presented at LICS 2021).
- Speaker: Dilian Gurov
- Title: An Abstract Contract Theory for Programs with Procedures
- Abstract: When developing complex software and systems, contracts provide a means for controlling the complexity by dividing the responsibilities among the components of the system in a hierarchical fashion. In specific application areas, dedicated contract theories formalise the notion of contract and the operations on contracts in a manner that supports the development of systems in that area. At the other end, contract meta-theories attempt to provide a systematic view on the various contract theories by axiomatising their desired properties. However, there exists a noticeable gap between the most well-known contract meta-theory, namely the one of Benveniste et al. which focuses on the design of embedded and cyber-physical systems, and the established way of using contracts when developing general software, following Meyer's design-by-contract methodology. At the core of this gap appears to be the notion of procedure: while it is a central unit of composition in software development, the meta-theory does not suggest an obvious way of treating procedures as components.
In this seminar, I will present an abstract contract theory for sequential programming languages that takes procedures as the basic building block. I will show that, on the one hand, the standard method for specification of procedure contracts in Hoare logic, and their procedure-modular verification, can be cast naturally in the framework of our abstract contract theory. On the other hand, I will also show that our contract theory fulfils the axioms of the meta-theory.
- Speaker: David Purser
- Title: Verification of Differential Privacy in Markov chains
- Abstract: Differential privacy is perhaps the most well-known formal privacy guarantee. However, most algorithms are verified as satisfying the property on paper, which can be error prone. We consider the problem of automatically verifying that a program, modelled as a labelled Markov chain, is differentially private. In full generality, the problem is undecidable, but we consider restricted sub-classes in which the problem becomes decidable. I will present joint work with Dmitry Chistikov, Stefan Kiefer and Andrzej Murawski.
- Speaker: Cyprien Delpech de Saint Guilhem
- Title: Recent advances in MPC-inspired zero-knowledge proofs for non-algebraic statements.
- Abstract: While zk-SNARKs and zk-STARKs have received much attention due to their use in blockchain ecosystems; other recent works have focused on improving the concrete efficiency of zero-knowledge proof systems for large and non-algebraic statements, e.g. using circuit representations. This talk will present several such systems for both private-coin and public-coin protocols, leading to recent results for zero-knowledge proofs of RAM programs.
- Speaker: Lucca Hirschi
- Title: Fixing the Achilles Heel of E-Voting: The Bulletin Board
- Abstract: In this talk, we will explore the role of bulletin boards in e-voting and show that previous designs and requirements were not sufficient for key security goals to hold. We present practical attacks based on equivocation against Civitas, Belenios, and Helios and discuss the severity of those attacks in different scenarios. To fix those protocols and future designs, we propose provably minimal bulletin board requirements and a concrete bulletin board protocol achieving them. Our protocol can replace existing bulletin boards, enabling verifiability under much weaker trust assumptions.
This talk is based on a joint work with Lara Schmid and Prof. David Basin (presented at IEEE CSF 2021), as well as on ongoing work with Vincent Laporte.
- Speaker: Emanuele D'Osualdo
- Title: TBA
- Abstract: TBA
- Speaker: Marianna Girlando
- Title: TBA
- Abstract: TBA
Back to SRM presentations.
Contact
For questions and comments contact
Matteo or
Masoud
.
