Chris Hankin

TCS Journal 2006 Journal Article

A framework for security analysis of mobile wireless networks

• Sebastian Nanz
• Chris Hankin

We present a framework for specification and security analysis of communication protocols for mobile wireless networks. This setting introduces new challenges which are not being addressed by classical protocol analysis techniques. The main complication stems from the fact that the actions of intermediate nodes and their connectivity can no longer be abstracted into a single unstructured adversarial environment as they form an inherent part of the system's security. In order to model this scenario faithfully, we present a broadcast calculus which makes a clear distinction between the protocol processes and the network's connectivity graph, which may change independently from protocol actions. We identify a property characterising an important aspect of security in this setting and express it using behavioural equivalences of the calculus. We complement this approach with a control flow analysis which enables us to automatically check this property on a given network and attacker specification.

TCS Journal 2005 Journal Article

Measuring the confinement of probabilistic systems

• Alessandra Di Pierro
• Chris Hankin
• Herbert Wiklicky

In this paper we lay the semantic basis for a quantitative security analysis of probabilistic systems by introducing notions of approximate confinement based on various process equivalences. We re-cast the operational semantics classically expressed via probabilistic transition systems (PTS) in terms of linear operators and we present a technique for defining approximate semantics as probabilistic abstract interpretations of the PTS semantics. An operator norm is then used to quantify this approximation. This provides a quantitative measure ɛ of the indistinguishability of two processes and therefore of their confinement. In this security setting a statistical interpretation is then given of the quantity ɛ which relates it to the number of tests needed to breach the security of the system.

TCS Journal 1998 Journal Article

Refining multiset transformers

• Chris Hankin
• Daniel Le Métayer
• David Sands

Gamma is a minimal language based on local multiset rewriting with an elegant chemical reaction metaphor. The virtues of this paradigm in terms of systematic program construction and design of parallel programs have been argued in previous papers. Gamma can also be seen as a notation for coordinating independent programs in a larger application. In this paper, we study a notion of refinement for programs involving parallel and sequential composition operators, and derive a number of programming laws. The calculus thus obtained is applied in the development of a generic “pipelining” transformation, which enables certain sequential compositions to be refined into parallel compositions.

TCS Journal 1998 Journal Article

Theoretical aspects of coordination languages

• Roberto Gorrieri
• Chris Hankin

TCS Journal 1988 Journal Article

A safe approach to parallel combinator reduction

• Chris Hankin
• Geoffrey Burn
• Simon Peyton Jones

In this paper we present the results of two pieces of work which, when combined, allow us to take a program text in a functional language and produce a parallel implementation of that program. We present techniques for discovering sources of parallelism in a program at compile time, and then show how this parallelism is naturally mapped into a parallel combinator set that we will define. To discover sources of parallelism in a program, we use abstract interpretation. Abstract interpretation is a compile-time technique which is used to gain information about a program that may then be used to optimise the execution of the program. A particular use of abstract interpretation is in strictness analysis of functional programs. In a language that has lazy semantics, the main potential for parallelism arises in the evaluation of operands of strict operators. A function is strict in an argument if its value is undefined whenever the argument is undefined. If we can use strictness analysis to detect which arguments a function is strict, we then know that these arguments can be safely evaluated in parallel because this will not affect the lazy semantics. Having identified the sources of parallelism at compile-time it is necessary to communicate these to the run-time system. In the second part of the paper we use an extended set of combinators, including some parallel combinators that achieve this purpose.