Logical dynamics in large games
20 November 2019
Professor Jam Ramanujam (The Institute of Mathematical Sciences, India).
Abstract: In two-player games, each player reasons about how the opponent would act at a position and expect herself (the player) to respond, and so on. Such intersubjectivity can be generalised to n-player games, and the logical basis of equilibrium notions is given thus.
However, what if n is large, say 10000? In such games payoffs are associated with strategy distributions rather than profiles. We discuss dynamics in such games and the use of logic to specify player types in these contexts.
Secure data outsourcing
15 November 2019
Associate Professor Alptekin Küpçü (Koc University, Turkey).
Abstract: As many services are moving to the cloud, we are losing control of our own data. This constitutes one of the biggest problems that we face in this decade. In this talk, I will first describe various cloud scenarios and services, including cloud storage and databases, and searching within them. I will briefly present the problems and current solutions to them, highlighting techniques to know to understand and improve current solutions, as well as open problems.
Establishing unlinkability relying on existing verification tools
30 October 2019
Dr Stéphanie Delaune (IRISA, France).
Abstract: Cryptographic protocols aim at securing communications over insecure networks such as the Internet, where dishonest users may listen to communications and interfere with them. For example, passports are no more pure paper documents. Instead, they contain a chip that stores additional information such as pictures and fingerprints of their holder. In order to ensure privacy, these chips include a mechanism, i.e. a cryptographic protocol, that does not let the passport disclose private information to external users. This is just a single example but of course privacy appears in many other contexts such as RFIDs technologies or electronic voting.
Formal methods have been successfully applied to automatically analyze traditional protocols and discover flaws. Privacy-type security properties (e.g. anonymity, unlinkability, ...) are expressed relying on a notion of behavioral equivalence, and are actually more difficult to analyse. We will discuss some recent advances that have been done to analyse automatically equivalence-based security properties, and we will review some issues that remain to be solved in this field. In particular, we will see that existing verification tools, such as ProVerif and Tamarin, are not suitable to analyse unlinkability. Therefore, we have developed a different approach: we design sufficient conditions that can then be effectively checked automatically using existing tools, and allows one to conclude on a number of case studies. This result, first published at S&P in 2016, has been recently extended to deal with stateful protocols. This is a joint work with D. Baelde, L. Hirschi, and S. Moreau.
Supersingular isogeny graphs
9 October 2019
Professor Omran Ahm (Institute for Research in Fundamental Sciences, Iran).
Abstract: The supersingular isogeny graphs are a class of expander graphs which have recently found applications in cryptography. In this talk, first, we explain what they are and then we explain how they have been used to construct cryptographic hash functions and key exchange protocols.
Ring signatures in blockchain
13 August 2019
Dr Tsz Hon Yuen (University of Hong Kong).
Abstract: Ring signature is a signature scheme which provides anonymity to the signer, without using trusted authority. It can be used in privacy-preserving applications such as e-voting and e-cash. Recently, it is used in cryptocurrency Monero to provide anonymity to spenders: the real spender's identity is hidden with respect to N public keys in the system. However, the ring signature used in Monero has signature size O(N), and N=10/20 in practice. Hence the level of anonymity is limited.
A number of researches has been done to reduce the signature size to O(log N). As a result, the ring size of N=2048 or more can be used in practice. It greatly increases the level of anonymity. In our recent work, we show how to construct such efficient ring signature using Bulletproof. We construct the most efficient O(log N)-size ring signature.
Tractable verification of multi-agent systems
29 May 2019
Dr Francesco Belardinelli (Imperial College London, UK).
Abstract: The formal verification of multi-agent systems is a key research area, as MAS are applied to the modelling and design of systems in domains as diverse as transportation, avionics, robotics, and security. Unfortunately, in many set ups of interest the model checking problem is either undecidable or untractable, thus hindering the development of any (efficient) model checking tool.
In this talk I will present two recent contributions on tractable model checking for multi-agent systems. In the first one we show how communication by broadcast can lead to a decidable model checking problem, also in the presence of imperfect information (and perfect memory). In the second contribution, we show that reasoning about a single resource in the temporal logic CTL comes at no extra computational cost. So, under specific assumptions, expressive logics for temporal and strategic reasoning can be applied effectively in the specification and verification of multi-agent systems.
Domain squatting
15 May 2019
Dr Nikolaos Pitropakis (Edinburgh Napier University, UK).
Abstract: Domain squatting is a common adversarial practice where attackers register domain names that are purposefully similar to popular domains. During this presentation we will begin a journey, where we will explore DNS and all of the forms of domain squatting.
Then we will we focus on a specific type of domain squatting called “combosquatting,” in which attackers register domains that combine a popular trademark with one or more phrases (e.g., betterfacebook[.]com, youtube-live[.]com). We will discuss the results of the first large scale, empirical study of combosquatting where more than 468 billion DNS records, collected from passive and active DNS data sources over almost six years were used for the analysis.
Machine learning and cyber security: Friends or foes?
27 February 2019
Matilda Rhode (Cardiff University, UK).
Abstract: Cyber security challenges are constantly evolving. In the short-term malicious actors may tweak individual attacks or malicious software to bypass particular defences. In the longer term the trends in types of attack change whenever a new solution has been widely adopted. Cyber defences are the sticks shaping the malicious landscape but there are also carrots, new opportunities which give good returns relative to the effort of malicious actors. For example the wide adoption of internet of things devices typically introduces a weak point into a network; the increasing reliance on data and digital systems has made ransomware attacks highly lucrative.
Machine learning has been met with scepticism from the security community, as in a number of other domains, but in the last few years has begun to demonstrate its worth in real-world scenarios when compare to traditional rule-based systems. Neural networks in particular have helped to mitigate the problems caused by short term changes to attack techniques.
The wide adoption of machine learning into other domains has introduced new security challenges. Adversarial attacks on computer vision systems as used by self-driving cars and automatic CCTV analysis have created cyber security challenges that did not exists several years ago. Adversarial attacks can also impact machine learning solutions for extant security problems such as malware and intrusion detection. This talk will explore the prominent threats to the security of machine learning cyber defences and how to mitigate them.
Bridging the security gap of NFV/SDN with trusted computing
6 February 2019
Dr Ludovic Jacquin (HP Labs, Bristol).
Biography: Dr Ludovic Jacquin is a Senior Researcher at Hewlett Packard Labs – the research organisation of Hewlett Packard Enterprise – in Bristol, UK. He holds an Applied Mathematics and Computer Science MSc from ENSIMAG (Grenoble, France) and received his PhD in Computer Science from Grenoble University (France) in 2013.
His broader research interest is to develop security mechanisms for computer and network infrastructure, both at the hardware and operating system level. He joined the Security Lab of Hewlett Packard Enterprise in 2014 with a focus on trust and attestation of the network infrastructure in the new paradigm of SDN and their application to related environments such as NFV. During his Ph.D., he mainly worked on the impact of network signalling protocols on security protocols such as IPsec.
Abstract: This talk will present the role of trusted computing and TPMs in SHIELD.
SHIELD is a H2020 Innovation Action project that aims to deliver an open solution for dynamically establishing and deploying virtual Security infrastructures in ISPs and corporate networks. It leverages Trusted Computing technologies to bridge the gap between orchestration tools and the virtual security functions introduced by Network Function Virtualisation; SHIELD also addresses the equivalent gap in networking introduced by Software-Defined Networks between controllers and network elements.
The second part of the talk will focus on some of the future looking research done in the Security Lab of Hewlett Packard Labs.
A treasury system for cryptocurrencies: Enabling better collaborative
23 January 2019
Dr Bingsheng Zhang (University, UK).
Abstract: A treasury system is a community-controlled and decentralized collaborative decision-making mechanism for sustainable funding of blockchain development and maintenance. During each treasury period, project proposals are submitted, discussed, and voted for; top-ranked projects are funded from the treasury.
The Dash governance system is a real-world example of such kind of systems. In this work, we, for the first time, provide a rigorous study of the treasury system. We modelled, designed, and implemented a provably secure treasury system that is compatible with most existing blockchain infrastructures, such as Bitcoin, Ethereum, etc. More specifically, the proposed treasury system supports liquid democracy/delegative voting for better collaborative intelligence. Namely, the stakeholders can either vote directly on the proposed projects or delegate their votes to experts.
Its core component is a distributed universally composable secure end-to-end verifiable voting protocol. The integrity of the treasury voting decisions is guaranteed even when all the voting committee members are corrupted. To further improve efficiency, we proposed the world’s first honest verifier zero-knowledge proof for unit vector encryption with logarithmic size communication.
This partial result may be of independent interest to other cryptographic protocols. A pilot system is implemented in Scala over the Scorex 2.0 framework, and its benchmark results indicate that the proposed system can support tens of thousands of treasury participants with high efficiency. This work is to be published at NDSS 2019.
Rule control of teleo-reactive, multi-tasking, communicating robotic agents
9 January 2019
Professor Keith Clark (Emeritus Professor Imperial College, UK).
Abstract: The robotic agents are programmed in two rule based languages: QuLog and TeleoR. They communicate using a logic based pub/sub and addressed message routing server, Pedro.
QuLog is a flexibly typed multi-threaded relation+function+imperative rule language. Its declarative subset of relation and function defining rules is used for encoding an agent’s dynamic beliefs and static knowledge. Its imperative rules are used for programming an agent’s behaviour. Imperative rules can invoke the relation and function rules, but not vice versa.
TeleoR is an application specific extension of QuLog for programming agents controlling robotic devices. It is a major extension of the T-R language proposed by Nils Nilsson. T-R’s ancestry goes back to the conditional triangular table action plans of the first cognitive robot, Shakey, built and programmed by a team lead by Nilsson at SRI in the late 1960s. Both TeleoR and T-R have sequences of guarded robotic action rules clustered into parameterised procedures:
- Two agents each controlling one mobile robot in co-operative bottle collecting. The agents have a joint goal of together collecting a given number of bottles. They communicate so each agent knows how many bottles both robots have collected, and to avoid the robots colliding with minimal divergence from each robot’s current path. They each stop their robot when the joint total is reached.
- A multi-tasking agent controlling a robotic arm and fairly sharing its use between multiple concurrent construction tasks. Colleagues at UNSW Sydney have ported a slightly more complex two arm controlling version of the agent program to a Baxter robot building towers of letter labeled blocks.
