Macquarie University
01whole.pdf (1.03 MB)

Game semantics for non-deterministic security

Download (1.03 MB)
posted on 2022-11-03, 01:02 authored by Chris Chen

The Shadow Semantics [47, 48, 50] models secure refinement, i.e. preservation of privacy under adversarial inference attacks. Previous work has given a structural (affirmative) account of secure refinement and its primitives, with some progress towards a testing (refutational) account. At the same time, (mutable-state) programs in the Shadow Se- mantics can be modelled readily as functions, but lack ‘healthiness conditions’ [11, 53] to characterise the underlying properties of information flow. Our contributions are twofold. First, we provide a testing (refutational) account of secure refinement as a game semantics for a certain adversarial game. In so doing we develop and characterise the ‘predicates’ first proposed in [47]. This game semantics provides an interpretation of the Shadow Semantics in terms of a security threat model. Its structure hints at connections to the quantitative analogue, qif [4]. Second, we give an order-theoretic account of the Shadow Semantics, adapting a recently developed framework from category theory [27, 32]. The Shadow Semantics’s main primitives are shown to arise from an adjunction on a certain ‘lax’ category. This account gives an alternative ‘first-principles’ derivation of the Shadow Semantics, and hints at future foundational work in the category theory of inference attacks.


Table of Contents

1. Introduction -- 2. Preliminaries and notation -- 3. Orders and refinement -- 4. The Shadow Semantics -- 5. Lattices and P+-algebras -- 6. Attacks and predicates -- 7. Shadow semantics – game model -- 8. Healthiness -- 9. Hyper-shadows and categorical duality -- 10. Significance and further work -- Bibliography


A thesis submitted to Macquarie University for the degree of Master of Research

Awarding Institution

Macquarie University

Degree Type

Thesis MRes


Thesis (MRes), Macquarie University, Faculty of Science and Engineering, Department of Computing, 2022

Department, Centre or School

Department of Computing

Year of Award


Principal Supervisor

Annabelle McIver

Additional Supervisor 1

Richard Garner


Copyright: The Author Copyright disclaimer:




65 pages

Usage metrics

    Macquarie University Theses