Seminars1718

My research focusses on the formal verification of system and network security protocols like TLS, and mobile phone authentication protocols such as those found in 4G and 5G. We use the “Tamarin Prover” automated verification tool which allows us to formally verify security properties of protocols such as secrecy and authentication. In this talk I will discuss some of the theory behind the Tamarin Prover, some decidability results in the world of security protocol verification (for context), and demonstrate Tamarin’s utility with a real-world case study (which won best paper at ESORICS 2017).
Our case-study considers power grid protocols: most of the world’s power grids are controlled remotely. Their control messages are sent over insecure channels, driving the need for an authentication mechanism. The main communication mechanism for power grids and other utilities is defined by an IEEE standard called DNP3; this includes the Secure Authentication v5 (SAv5) protocol, which aims to ensure that messages are authenticated.
We provide the first security analysis of the complete ‘Secure Authentication v5’ protocol. We formally model and analyse the complex composition of the protocol’s three sub-protocols, considering the full state machine and the possibility of cross-protocol attacks. Our analysis shows that the core DNP3: SAv5 design meets its intended security properties. Notably, we show that a previously reported attack does not apply to the standard; however, our analysis also leads to several concrete recommendations for improving future versions of the standard.

 

We introduce “partial rejection sampling”, to draw samples exactly from a product distribution, conditioned on none of a number of bad events occurring. Our framework builds new connections between the algorithmic Lovasz Local Lemma and some classical sampling algorithms such as the “cycle-popping” algorithm for rooted spanning trees by Wilson. Among other applications, we confirm a conjecture by Gorodezky and Pak (2014), which leads to an approximation algorithm of reachability in bi-directed graphs.
Based on joint work with Mark Jerrum and Jingcheng Liu

Ricci curvature plays a very important role in the study of Riemannian manifolds. In the discrete setting of graphs, there is very active recent research on various types of Ricci curvature notions and their applications. One such notion on graphs is the Ollivier-Ricci curvature. This notion has recently had many applications, ranging from modelling cancer growth to modelling WiFi connections. This stems from this curvature notion being a way to quantify local connectedness.

We study the Ollivier-Ricci curvature of graphs as a function of the chosen idleness. We show that this idleness function is concave and piecewise linear with at most 3 linear parts, with at most 2 linear parts in the case of a regular graph. We then apply our result to show that the idleness function of the Cartesian product of two regular graphs is completely determined by the idleness functions of the factors. I will also present an interactive web applet which has helped in my investigations.

This talk is devoted to the problem of characterizing the family of factorial classes of graphs, i.e., hereditary classes in which the number of n-vertex graphs grows as a factorial type function. First, we will discuss the background and motivation of the problem. Then we will consider a special case of characterizing the family of factorial classes of bipartite graphs. We will present a result showing that the class of P7-free bipartite graphs is factorial. The result completes the description of monogenic factorial classes of bipartite graphs. The proof is based on a decomposition scheme of bipartite graphs, which is of independent interest. Finally, we will discuss some open problems.

Based on joint work with Vadim Lozin.

 

This is about the word problem in Artin groups.

For a group G = < X | R > defined (presented) by finite sets of generators and relations, the word problem is soluble if there is an algorithm which, given a word over X (ie string over X and its set of formal inverses) can decide whether or not w represents the identity element. In the 1950s, Novikov and Boone proved the existence of finitely presented groups with insoluble word problem.

Artin groups form a large and varied class of finitely presented groups (including free groups, free abelian groups, braid groups and much, much more) with many applications. Only some are known to have soluble word problem.

I’ll talk about attempts to solve the word problem in Artin groups, and in particular to find a general solution, that might work for the full spectrum of Artin groups. I’ll survey some background (which will include a definition of Artin groups), then discuss recent work of myself and Derek Holt, and of Patrick Dehornoy and Eddy Godelle.

 

 

We consider job scheduling on multiple cores under the condition that the jobs also share a continuously divisible resource, e.g. bandwidth. Each job comes with a resource requirement and can only be processed at full speed if granted its full resource requirement. The goal is to find a resource assignment that minimizes the makespan.

The focus of the talk is on the assignment of the shared continuous resource to the processors assuming that the job assignment to processors has already been fixed. We present algorithms and complexity results.

In this talk, we explore the maximum matching problem in the data streaming model. A graph streaming algorithm processes the edges of the input graph sequentially one by one while maintaining a memory of sublinear size. Streaming algorithms for matchings have been studied for almost 15 years, and, despite being the most studied graph problem in the streaming model, many natural questions in this area still remain open. The main focus of this talk will be algorithms for random order streams, including a very recent improvement.

On each of n unsteady steps, a drunken gardener drops a seed. Once the flowers have bloomed, what is the minimum length of fencing required to enclose the garden? What is its area? I will describe recent work on the convex hull of planar random walk, concerned in particular with the large-n asymptotics of its perimeter length and area. We provide variance asymptotics and distributional limit theorems. Of the four combinations of the two quantities (perimeter and area) in the two regimes (zero drift or non-zero drift for the steps of the walk), one limit is Gaussian; three are not. This talk is mostly based on joint work with Chang Xu (Strathclyde); I’ll also mention ongoing work with Ostap Hryniv and James McRedmond (Durham).

 

This talk will focus on graph polynomials, which are polynomial valued graph invariants. Arguably, the most important and best studied graph polynomial is the Tutte polynomial. It is important not only because it encodes a large amount of combinatorial information about a graph, but also because of its applications to areas such as statistical physics (as the Ising and Potts models) and knot theory (as the Jones and homfly polynomials).

Because of its importance the Tutte polynomial has been extended to various classes of combinatorial object. For some objects there is more than one definition of a “Tutte polynomial”. For example, there are three different definitions for the Tutte polynomial of graphs in surfaces: M. Las Vergnas’ 1978 polynomial, B. Bolloba‡s and O. Riordan’s 2002 ribbon graph polynomial, and V. Kruskal’s polynomial from 2011. On the other hand, for some objects, such as digraphs, there is no wholly satisfactory definition of a Tutte polynomial. Why is this? Why are there three different Tutte polynomials of graphs in surfaces? Which can claim to be the Tutte polynomial of a graph in a surface? More generally, what does it mean to be the Tutte polynomial of a class of combinatorial objects? In this talk I will describe a way to canonically construct Tutte polynomials of combinatorial objects, and, using this framework, will offer answers to these questions.

Multi-layer networks occur widely in natural and social systems. I’ll outline details of a few of these, including the sheep and cattle contact networks in Britain. Motivated by a desire to compute efficiently on such networks, I’ll talk about the problem of counting the number of occurrences of (small) subgraphs or motifs in multi-layer graphs in which each layer of the graph has useful structural properties. Focussing on the parameterised complexity of motif-counting problems, I’ll outline conditions on the layers of a network that yield fixed-parameter tractable algorithms for motif-counting in the overall network, and discuss the results of a few experiments on the Scottish cattle-trading network.

(joint work with Kitty Meeks)

Matrices and matrix products play a crucial role in a representation and analysis of various computational processes. However, many simply formulated and elementary problems for matrices are inherently difficult to solve even in dimension two, and most of these problems become undecidable in general starting from dimension three or four. Let us given a finite set of square matrices (known as a generator) which is forming a multiplicative semigroup S. The classical computational problems for matrix semigroups are:

• Membership (Decide whether a given matrix M belong to a semigroup S) and two special cases such as: Identity (i.e. if M is the identity matrix) and Mortality (i.e. if M is the zero matrix) problems
• Vector reachability (Decide for a given vectors u and v whether exist a matrix M in S such that Mu=v)
• Scalar reachability (Decide for a given vectors u, v and a scalar L whether exist a matrix M in S such that uMv=L)
• Freeness (Decide whether every matrix product in S is unique, i.e. whether it is a code) and some variants of the freeness such as finite freeness problem, the recurrent matrix problem, the unique factorizability problem, vector freeness problem, vector ambiguity problems, etc.

Recently, we proposed a number of new approaches of translating numerical problems of 2×2 integer matrices into variety of combinatorial and computational problems on words and automata over group alphabet. Studying their transformations as specific rewriting systems have led to a few results on decidability and complexity for several subclasses. In this talk I will give a wider view on the number of challenging computational problems related to matrix systems, then I will present new results on the matrix problems for the special linear group and will talk on a number of long standing open problems in the filed.

 

In this talk, I will show how to construct a matrix M with nonnegative rational entries and with the following properties. The matrix has a factorization M = W H into matrices W and H with nonnegative entries such that the shared dimension of W and H is 5, but every such factorization needs to have irrational entries in W and H. This answers a question by Cohen and Rothblum (1993): nonnegative ranks of matrices over the reals and over the rationals are different functions.

Joint work with Stefan Kiefer, Ines Marusic, Mahsa Shirmohammadi, and James Worrell.

Despite the unprecedented advancement achieved by deep learning as a machine learning approach there remain fundamental theoretical questions that have not been rigorously addressed, for example why dropout works, or what co-variate shifting is. In this talk I will highlight some of these challenges and raise open questions that will potentially stimulate future work with significant contribution to the understanding of how and why deep learning works.