A logic for the compliance budget. Joint work with Gabrielle Anderson and Guy McCusker.

**Abstract**. Security breaches often arise as a result of users' failure to comply
with security policies. Such failures to comply may simply be innocent mistakes. However,
there is evidence that, in some circumstances, users choose not to comply because they
perceive that the security benefit of compliance is outweighed by the cost that is the
impact of compliance on their abilities to complete their operational tasks. That is,
they perceive security compliance as hindering their work. The `compliance budget' is a
concept in information security that describes how the users of an organization's systems
determine the extent to which they comply with the specified security policy. The purpose
of this paper is to initiate a qualitative logical analysis of, and so provide reasoning
tools for, this important concept in security economics for which quantitative analysis is
difficult to establish. We set up a simple temporal logic of preferences, with a
semantics given in terms of histories and sets of preferences, and explain how to use
it to model and reason about the compliance budget. The key ingredients are
preference update, to account for behavioural change in response to policy change,
and an ability to handle uncertainty, to account for the lack of quantitative measures
of the compliance budget.

Manuscript. *Proc. GameSec 2016*, New York City,
November 2016. LNCS 9996:370-381, 2016.

A Substructural Epistemic Resource Logic. Joint work with D. Galmiche and P. Kimmel.

**Abstract**. We present a substructural epistemic logic, based on Boolean BI,
in which the epistemic modalities are parametrized on agents'
local resources. The new modalities can be seen as generalizations
of the usual epistemic modalities. The logic combines Boolean
BI's resource semantics with epistemic agency. We give a labelled
tableaux calculus and establish soundness and completeness with
respect to the resource semantics. We illustrate the use of the logic
by discussing an example of side-channels in access control using
resource tokens.

Manuscript. Revised version
to appear in *Proc. ICLA 2017*, Kanpur, India, January 2017.

An extended version, including all proofs, is available as UCL Computer Science Research Note RN/16/08.

On the adoption of privacy-enhancing technologies. Joint work with Tristan Caulfield and Christos Ioannidis.

**Abstract**. We propose a model, based on the work of Brock and Durlauf, which
looks at how agents make choices between competing technologies, as a framework
for exploring aspects of the economics of the adoption of privacy-enhancing technologies.
In order to formulate a model of decision-making among choices of technologies by
these agents, we consider the following: *context*, the setting in which
and the purpose for which a given technology is used; *requirement*, the
level of privacy that the technology must provide for an agent to be willing to
use the technology in a given context; *belief*, an agent's perception of
the level of privacy provided by a given technology in a given context; and the
*relative value* of privacy, how much an agent cares about privacy in this
context and how willing an agent is to trade off privacy for other attributes.
We introduce these concepts into the model, admitting heterogeneity among agents
in order to capture variations in requirement, belief, and relative value in the
population. We illustrate the model with two examples: the possible effects on the
adoption of iOS devices being caused by the recent Apple--FBI case; and the recent
revelations about the non-deletion of images on the adoption of Snapchat.

Manuscript. *Proc. GameSec 2016*, New York City,
November 2016. LNCS 9996:175-194, 2016.

A substructural modal logic of utility. Joint work with Gabrielle Anderson.

**Abstract**. We introduce a substructural modal logic of utility that can be used to
reason about optimality with respect to properties of states. Our notion of state is quite
general, and is able to represent resource allocation problems in distributed systems.
The underlying logic is a variant of the modal logic of bunched implications, and based
on resource semantics, which is closely related to concurrent separation logic. We
consider a labelled transition semantics and establish conditions under which
Hennessy-Milner soundness and completeness hold. By considering notions of cost,
strategy, and utility, we are able to formulate characterizations of Pareto optimality,
best responses, and Nash equilibrium within resource semantics. We also show that our
logic is able to serve as a logic for a fully featured process algebra and explain the
interaction between utility and the structure of processes.

Manuscript. In press, *Journal of Logic
and Computation*, 2016.

A Logic of Separating Modalities. Joint work with J.-R. Courtault and D. Galmiche.

**Abstract**. We present a logic of separating modalities, LSM, that is
based on Boolean BI. LSM's modalities, which generalize those of S4, combine,
within a quite general relational semantics, BI's resource semantics
with modal accessibility. We provide a range of examples illustrating
their use in a range of examples from computer science. We give a
proof system based on the method of labelled tableaux with countermodel
extraction, establishing its soundness and completeness with respect
to the resource semantics.

*Theoretical Computer Science* 637, 30-58, 2016.
doi: 10.1016/j.tcs.2016.04.040. Manuscript.

Contagion in Cybersecurity Attacks. Joint work with Adrian Baldwin, Iffat Gheyas, Christos Ioannidis, and Julian Williams.

**Abstract**. Systems security is essential for the efficient operation of all
organizations Indeed, most large firms employ a designated `Chief Information Security
Officer' (CISO) to coordinate the operational aspects of the organization's information
security. Part of this role is in planning investment responses to information security
threats against the firms corporate network infrastructure. To this end, we develop and
estimate a vector equation system of threats to ten important IP services, using industry
standard SANS data on threats to various components of a firm's information system over
the period January 2003 to February 2011. Our results reveal strong evidence of contagion
between such attacks, with attacks on ssh and Secure Web Server indicating increased
attack activity on other ports. Security managers who ignore such contagious
inter-relationships may underestimate the underlying risk to their systems' defence of
security attributes, such as sensitivity and criticality, and thus delay appropriate
information security investments.

*Journal of the Operational Research Society*, 2016,
doi: 10.1057/jors.2016.37.
Manuscript.

Ioannidis, C., Pym, D., and Williams, J. (2016) Is Public Co-Ordination of Investment
in Information Security Desirable? *Journal of Information Security* (Special Issue
on Cybersecurity Investments, L. Gordon and M. Loeb, editors), 7, 60-80.
doi: 10.4236/jis.2016.72005.

**Abstract**. This paper provides for the presentation, in an integrated manner, of
a sequence of results addressing the consequences of the presence of an information
steward in an ecosystem under attack and establishes the appropriate defensive investment
responses, thus allowing for a cohesive understanding of the nature of the information
steward in a variety of attack contexts. We determine the level of investment in
information security and attacking intensity when agents react in a non-coordinated
manner and compare them to the case of the system's coordinated response undertaken
under the guidance of a steward. We show that only in the most well-designed institutional
set-up the presence of the well-informed steward provides for an increase of the system's
resilience to attacks. In the case in which both the information available to the steward
and its policy instruments are curtailed, coordinated policy responses yield no additional
benefits to individual agents and in some case they actually compared unfavourably to a
tomistic responses. The system's sustainability does improve in the presence of a steward,
which deters attackers and reduces the numbers and intensity of attacks. In most cases,
the resulting investment expenditure undertaken by the agents in the ecosystem exceeds
its Pareto efficient magnitude.

Intuitionistic layered graph logic. Joint work with Simon Docherty.

**Abstract**. Models of complex systems are widely used in the
physical and social sciences, and the concept of layering, typically
building upon graph-theoretic structure, is a common feature. We
describe an intuitionistic substructural logic that gives an account of
layering. As in bunched systems, the logic includes the usual
intuitionistic connectives, together with a non-commutative,
non-associative conjunction (used to capture layering) and its
associated implications. We give soundness and completeness theorems for
labelled tableaux and Hilbert-type systems with respect to a Kripke
semantics on graphs. To demonstrate the utility of the logic, we show
how to represent a range of systems and security examples, illuminating
the relationship between services/policies and the
infrastructures/architectures to which they are applied.

*Proc. IJCAR 2016*, N. Olivetti and A. Tiwari (editors), Coimbra, Portugal,
June 27-July 2, 2016. LNAI 9706:469-486, 2016.
Manuscript.

Discrete Choice, Social Interaction, and Policy in Encryption Technology Adoption [Short Paper]. Joint work with Tristan Caulfield and Christos Ioannidis.

**Abstract**. We introduce a model for examining the factors that lead to the
adoption of new encryption technologies. Building on the work of Brock and Durlauf,
the model describes how agents make choices, in the presence of social interaction,
between competing technologies given their relative cost, functionality, and
usability. We apply the model to examples about the adoption of encryption in
communication (email and messaging) and storage technologies (self-encrypting
drives) and also consider our model's predictions for the evolution of
technology adoption over time.

To appear: *Proc. Financial Cryptography and Data Security 2016*. LNCS, 2016.
Preprint.

Substructural modal logic for optimal resource allocation. Joint work with Gabrielle Anderson.

**Abstract**. We introduce a substructural modal logic for reasoning about
(optimal) resource allocation in models of distributed systems. The underlying
logic is a variant of the modal logic of bunched implications, and based on
the same resource semantics, which is itself closely related to concurrent
separation logic. By considering notions of cost, strategy, and utility, we
are able to formulate characterizations of Pareto optimality, best responses,
and Nash equilibrium within resource semantics.

Paper 5, *Proc. Strategic Reasoning 2015*, St.
Catharine's College, Oxford, September 21-22, 2015.
Strategic Reasoning 2015.

Hennessy-Milner Completeness in Resource-Process Calculus. Joint work with Gabrielle Anderson and James Brotherston.

**Abstract** We consider the problem of obtaining Hennessy-Milner soundness and
completeness --- the coincidence of logical equivalence and bisimilarity --- in the
setting of transition systems with synchronous concurrent composition. Starting from a
richly expressive modal logic, motivated by resource semantics and distributed systems
modelling, including both additive and multiplicative propositional connectives and also
additive and multiplicative action modalities, as well as certain first-order quantifiers,
we establish sufficient conditions for Hennessy--Milner soundness and completeness to hold.
We develop two examples in detail. First, using the propositional part of the logic, we
consider a calculus of resources and processes, explaining how the semantics may be
refined to give a familiar equational theory. Second, employing a first-order,
arithmetic theory, we consider a calculus with utilities that is able
to express optimality and equilibria in resource allocation.

Technical report, RN/15/05, University College London, 2015: http://www.cs.ucl.ac.uk/fileadmin/UCL-CS/research/Research_Notes/RN- 15- 05.pdf.

Completeness via canonicity for distributive substructural logics: a coalgebraic perspective. Joint work with Fredrik Dahlqvist.

**Abstract**. We prove strong completeness of a range of substructural logics with respect to their relational
semantics by completeness-via-canonicity. Specifically, we use the topological theory of canonical
(in) equations in distributive lattice expansions to show that distributive substructural logics are
strongly complete with respect to their relational semantics. By formalizing the problem in the language
of coalgebraic logics, we develop a modular theory which covers a wide variety of different logics
under a single framework, and lends itself to further extensions.

*Proc 15th Int. Conf. on Relational and Algebraic Methods in
Computer Science (RAMiCS 2015)*, LNCS 9348: 119-135, 2015.

Modelling and Simulating Systems Security Policy. Joint work with Tristan Caulfield.

**Abstract**. Security managers face the challenge of designing security policies that deliver
the objectives required by their organizations. We explain how a rigorous modelling framework and
methodology---grounded in semantically justified mathematical systems modelling, the economics of
decision-making, and simulation---can be used to explore the operational consequences of their
design choices and help security managers to make better decisions. The
methodology is based on constructing executable system models that illustrate
the effects of different policy choices. Models are compositional,
allowing complex systems to be expressed as combinations of smaller, complete
models. They capture the logical and physical structure of systems, the choices
and behaviour of agents within the system, and the security managers'
preferences about outcomes. Utility theory is used to describe the extent to which
security managers' policies deliver their security objectives. Models are
parametrized based on data obtained from observations of real-world
systems that correspond closely to the examples described.

In *Proc SIMUTools 2015*, ACM Digital Library,
SIMUtools 2015.
doi: 10.4108/eai.24-8-2015.2260765.

The julia package used for creating system models may be obtained from GitHub here.

A Calculus and Logic of Bunched Resources and Processes. Joint work with Gabrielle Anderson.

**Abstract**. Mathematical modelling and simulation modelling are fundamental tools of engineering,
science, and social sciences such as economics, and provide decision-support tools in management. Mathematical
models are essentially deployed at all scales, all levels of complexity, and all levels of abstraction. Models are often
required to be executable, as a simulation, on a computer. We present some contributions to the process-theoretic
and logical foundations of discrete-event modelling with resources and processes. Building on previous work
in resource semantics, process calculus, and modal logic, we describe a process calculus with an explicit
representation of resources in which processes and resources co-evolve. The calculus is closely connected to a
substructural modal logic that may be used as a specification language for properties of models. In contrast to
earlier work, we formulate the resource semantics, and its relationship with process calculus, in such a way that
we obtain soundness and completeness of bisimulation with respect to logical equivalence for the naturally
full range of logical connectives and modalities. We give a range of examples of the use of the
process combinators and logical structure to describe system structure and behaviour.

*Theoretical Computer Science* 614:63-96, 2016:
http://www.sciencedirect.com/science/article/pii/S0304397515011214.

Improving Security Policy Decisions with Models. Joint work with Tristan Caulfield.

**Abstract**. Security managers face the challenge of designing security policies that
deliver the objectives required by their organizations. We explain how a rigorous
methodology, grounded in mathematical systems modelling and the economics of
decision-making, can be used to explore the operational consequences of their
design choices and help security managers to make better decisions. The
methodology is based on constructing executable system models that illustrate
the effects of different policy choices. Models are designed to be composed,
allowing complex systems to be expressed as combinations of smaller, complete
models. They capture the logical and physical structure of systems, the choices
and behavior of agents within the system, and the security managers'
preferences about outcomes. Models are parameterized from observations of the
real world and the effectiveness of different security policies is explored
through simulation. Utility theory is used to describe the extent to which
security managers' policies deliver their security objectives.

Preprint. Published version:
*IEEE Security and Privacy*, 13(5), 34-41, September/October 2015.

The julia package used for creating system models may be obtained from GitHub here.

Resilience in Information Stewardship. Joint work with Christos Ioannidis, Julian Williams, and Iffat Gheyas.

**Abstract**. Information security is concerned with protecting the confidentiality,
integrity, and availability of information systems. System managers deploy their resources
with the aim of maintaining target levels of these attributes in the presence
of reactive threats. Information stewardship is the challenge of maintaining the
sustainability and resilience of the security attributes of (complex, interconnected,
multi-agent) information ecosystems. In this paper, we present, in the tradition
public economics, a model of stewardship which addresses directly the question of
resilience. We model attacker-target-steward behaviour in a fully endogenous Nash
equilibrium setting. We analyse the occurrence of externalities across targets and assess
the steward's ability to internalize these externalities under varying
informational assumptions. We apply and simulate this model in the case of a critical
national infrastructure example.

In: WEIS 2014, Penn State University, 23-24 June, 2014: paper, slides.

Compositional Security Modelling: Structure, Economics, and Behaviour. Joint work with Tristan Caulfield and Julian Williams.

**Abstract**. Security managers face the challenge of formulating and implementing policies that deliver their desired system
security postures --- for example, their preferred balance of confidentiality, integrity, and availability --- within budget
(monetary and otherwise). In this paper, we describe a security modelling methodology, grounded in rigorous
mathematical systems modelling and economics, that captures the managers' policies and the behavioural choices of
agents operating within the system. Models are executable, so allowing systematic experimental exploration of the
system-policy co-design space, and compositional, so managing the complexity of large-scale systems.

Proceedings of the Foundations, Tools, and New Concepts in Trusted Computing track of the 2nd International Conference on Human Aspects of Information Security, Privacy and Trust, HCI International 2014, Heraklion, June 2014. LNCS 8533: 233--245, 2014.

Layered Graph Logic as an Assertion Language for Access Control Policy Models. Joint work with Matthew Collinson and Kevin McDonald.

**Abstract**. We describe a uniform logical framework, based on a bunched logic that combines classical additives and very weak multiplicatives,
for reasoning compositionally about access control policy models. We show how our approach takes account of the underlying system architecture,
and so provides a way to identify and reason about how vulnerabilities may arise (and be removed) as a result of the architecture of the system.
We consider, using frame rules, how local properties of access control policies are maintained as the system architecture evolves.

Manuscript. *Journal of Logic and
Computation*, 2015. doi: 10.1093/logcom/exv020. First published online: June 12, 2015.

Trust Domains in system models: algebra, logic, utility, and combinators. Joint work with Gabrielle Anderson.

**Abstract**. Understanding the boundaries of trust is a key aspect of accurately modelling
multi-agent systems with heterogeneous motivating factors. Reasoning about these boundaries in
highly interconnected, information-rich ecosystems is complex, and dependent upon modelling at
the correct level of abstraction. Building on an established mathematical framework, which
incorporates both logical and cost-based descriptions of systems, and a formal characterization
of trust domains in terms of the above, we develop techniques for the combination and substitution
of trust domains.

Manuscript. *Journal of Logic and Computation*, 2015:
doi: 10.1093/logcom/exv030. First published online: June 15, 2015.

Sustainability in Information Stewardship: Time Preferences, Externalities, and Social Co-ordination. Joint work with Christos Ioannidis and Julian Williams.

**Abstract**. The concept of stewardship in environmental economics is an established tool for environmental and natural
resource management and the mitigation of risk from climate change. Similar concepts are well-established
in accounting and management. Despite the ubiquity of the concept of stewardship, there is no generally accepted definition.
We define the information steward as the agent/institution who enhances the system's resilience and
sustainability, by maintaining and extending the life of its nominal operational capacity. Unlike
individual agents who are not able to value systemic losses, the steward, whose function is the
viability of the system as a whole, values such damages that degrade the system at a higher rate by adopting a
lower discount rate. In the presence of deliberate attacks that degrade the information used/kept in the system, individual agents'
defensive expenditure is always lower that the expenditure undertaken under instructions from the information
steward. The ability of the steward to mobilize the totality of agents reduces the number of attackers, increasing
the system's sustainability under a variety of technological considerations. The resulting configuration of defensive
expenditure, although higher than the level that individual agents would have chosen based on their own valuation
of their expected losses, ensures that the overall probability of successful attacks falls, significantly extending the
system's sustainability.

In: WEIS 2013, Georgetown University, Washington DC, 11-12 June, 2103: paper.

Trust Domains: An Algebraic, Logical, and Utility-theoretic Approach. Joint work with Gabrielle Anderson and Matthew Collinson.

**Abstract**. Complex systems of interacting agents are ubiquitous in the highly interconnected, information-rich ecosystems
upon which the world is more-or-less wholly dependent. Within these systems, it is often necessary for an agent,
or a group of agents, such as a business, to establish within a given ecosystem a trusted group, or a region of trust.
Building on an established mathematical systems modelling framework --- based on process algebra, logic, and
stochastic methods --- we give a characterization of such `trust domains' that employs logical assertions of the properties
required for trust and utility-theoretic constraints on the cost of establishing compliance with those properties. We
develop the essential meta-theory and give a range of examples.

Manuscript available here. Presented in the socio-economic track at
TRUST 2013. In: *Trust and Trustworthy Computing*, Michael Huth, N. Asokan, Srdjan Capkun, Ivan
Flechais, Lizzie Coles-Kemp (editors), LNCS 7904:232-249, 2013.

Extended versions of proofs available as University of Aberdeen Computing Science Technical Report TR-ABDN-CS-12-04.

A Proof-theoretic Analysis of the Classical Matrix Method. Joint work with Eike Ritter and Edmund Robinson.

**Abstract**. The matrix method, due to Bibel and Andrews, is a proof procedure designed for automated theorem-proving.
We show that underlying this method is a fully structured combinatorial model of conventional classical proof theory.

Manuscript available here.

*J. Logic Computation* 24 (1): 283-301, 2014. doi: 10.1093/logcom/exs045.
First published online: November 21, 2012
online advance access.

Systematic Decision Making in Security Management: Modelling Password Usage and Support. Joint work with Adam Beautement et al.

**Abstract**. We demonstrate the use of a systematic decision-making methodology to support an informed choice of a password
policy. Our approach uses an executable system model, grounded in empirical data, to compare, using simulations, two different
policy options. The problem is framed economically, with the basis of the comparison being a notion of organizational
utility. We quantify utility in this case by considering breaches of system security, users' productivity, and investment
in support operations. Using our results, we are able to explore trade-offs between these factors and thus determine
the optimal policy configuration given the initial conditions.

In QASA 2012 (International Workshop on Quantitative Aspects in Security Assurance). Affiliated workshop with ESORICS. Presented version available here.

Utility-based Decision-making in Distributed Systems Modelling [Extended Abstract]. Joint work with Gabrielle Anderson and Matthew Collinson.

**Abstract**. We consider a calculus of resources and processes as a basis for modelling
decision-making in multi-agent systems. The calculus represents the regulation
of agents' choices using utility functions that take account of context. Associated with
the calculus is a (Hennessy-Milner-style) context-sensitive modal logic of state. As an application,
we show how a notion of `trust domain' can be defined for multi-agent systems.

Preprint available here. In
*Proc. TARK 2013*, Burkhard C. Schipper (editor), Chennai, 2013. Computing
Research Repository (CoRR): http://arxiv.org/corr/home. ISBN: 978-0-615-74716-3.

Extended versions of proofs available as University of Aberdeen Computing Science Technical Report TR-ABDN-CS-12-04.

A Substructural Logic for Layered Graphs. Joint work Matthew Collinson and Kevin McDonald.

**Abstract**. Complex systems, be they natural or synthetic, are ubiquitous. In particular, complex networks of devices
and services underpin most of society's operations. By their very nature, such systems are difficult to
conceptualize and reason about effectively. The concept of layering is widespread in complex systems,
but has not been considered conceptually. Noting that graphs are a key formalism in the description
of complex systems, we establish a notion of a layered graph. We provide a logical characterization
of this notion of layering using a non-associative, non-commutative substructural, separating logic. We provide
soundness and completeness results for a class of algebraic models that includes layered graphs, which
give a mathematically substantial semantics to this very weak logic. We explain, via examples, applications
in information processing and security.

Pre-publication manuscript here.

*J. Logic Computation* 24 (4):953-988, 2014. doi: 10.1093/logcom/exu002.
First published online: February 18, 2014.

Erratum: *Journal of Logic and Computation*, 2015.
doi: 10.1093/logcom/exv019. First published online: June 9, 2015

A Framework for Modelling Security Architectures in Services Ecosystems. Joint work with Matthew Collinson and Barry Taylor.

**Abstract**. We develop a compositional framework for modelling security and business architectures based
on rigorous underlying mathematical systems modelling technology. We explain the basic architectural
model, which strictly separates declarative specification from operational implementation, and show
architectures can interact by composition, substitution, and stacking. We illustrate these constructions using a
running example based on airport security and an example based on (cloud-based) outsourcing, indicating how
our approach can illustrate how security controls can fail or be circumvented in these cases.
We explain our motivations from mathematical modelling and security economics, and conclude by
indicating how to aim to develop a decision-support technology.

Manuscript available at here. In *Proc*. *ESOCC 2012*.
LNCS: 7592, 64-79, 2012.

Exploring Information Stewardship with the Cloud Ecosystem Model. Joint work with Adrian Baldwin et al.

**Abstract**. The emergence of cloud computing has transformed the way in which enterprise IT is delivered and creates
new challenges around risk management, security strategy, and control over policies and information. For a particular
example, the economies of scale that can be achieved by large cloud service providers are encouraging ecosystems of service
providers in which the marketplace (rather than the consuming enterprises or individuals) determines security standards.
The problem goes beyond core security concerns, since all cloud stakeholders will be relying on others to steward their
information, and so will be concerned with the overall sustainability and resilience of the ecosystem, from both security
and business perspectives. To help cloud consumers and other stakeholders explore the impact of the cloud ecosystem on
their business decisions, we have developed a system that combines systems modelling, simulation, and 3D visualization
techniques. At the heart of this system is a model of the cloud ecosystem, built by combining economic and system
modelling approach. The model uses utility theory as the unifying vocabulary for stakeholders to express their
decision-making. Simulations of the model representing several years of operations are then performed, with various
shocks — such as economic downturns and security attacks — introduced at certain points in time. The visualization
component has been built specifically for this model and consists of interactive 3D graphics that can be
used in any compatible web browser, so allowing stakeholders to interact with and explore the model and simulation
results easily.

To appear, Proc. 2012 International Conference on Modeling, Simulation and Visualization Methods (MSV 2012), 2012 World Congress in Computer Science, Computer Engineering, and Applied Computing. Las Vegas, July 2012. Preprint available here.

A Discipline of Mathematical Systems Modelling. College Publications, 2012. Joint work with Matthew Collinson and Brian Monahan.

**Preface**. The mathematization of the sciences, of engineering, and of economics has been an outstandingly successful intellectual enterprise,
enabling the modern world. As the operations of the world become more and more dependent on highly interconnected, massively complex, networked
systems of computational devices, the need to develop a mathematical understanding of their properties and behaviours is increasingly pressing.

Our approach, described in this monograph, is to combine the compositionality of formal specification --- using techniques from algebra, computation theory, logic, and probability theory --- with the control of level of abstraction afforded by the classical mathematical modelling method.

The first chapter provides a complete high-level view of the approach to systems modelling that is developed in the monograph. It provides both conceptual and philosophical background and introductions to the technical development. The remaining chapters develop the mathematical and computational aspects of our approach. Each chapter develops a specific mathematical or computational component, clearly integrated into the overall development. Examples, including ones based on industrial and commercial applications, are provided throughout. An implementation of a simulation engine (Core Gnosis) for executing models is available for download from HP Labs. Associated with this monograph is a website (http://www.hpl.hp.com/research/systems_security/gnosis.html) from which Core Gnosis may be obtained. This is book is about the conceptual and mathematical foundations of a modelling approach, with indications of how it can, and has been, deployed in practice. We defer to another occasion an account of the pragmatics of the deployment.

Contributor to the ENISA report Economics of Security: Facing the Challenges. Luxembourg: Publications Office of the European Union, 2012. ISBN: 978-92-9204-057-4, doi: 10.2824/23063.

Contagion in Cybersecurity Attacks. Joint work with Adrian Baldwin, Iffat Gheyas, Christos Ioannidis, and Julian Williams.

**Abstract**. We develop and estimate a vector equation system of threats to ten important IP services, using SANS-reported data
over the period January 2003 to February 2011. Our results reveal strong evidence of contagion between such attacks, with
attacks on ssh and Secure Web Server indicating increased attack activity on other ports. Security managers
who ignore such contagious inter-relationships may underestimate the underlying risk to their systems' defence of security
attributes, such as sensitivity and criticality, and thus delay appropriate information security investments.

Proceedings of WEIS 2012, Berlin: paper.

Information Stewardship in the Cloud. Joint work with Simon Shiu.
*IISP Pulse* 7 Winter 2011: 6-8.

Available here.

Enterprise information risk management: Dealing with cloud computing. Joint work with Adrian Baldwin and Simon Shiu. To appear: Privacy and Security for Cloud Computing: Selected Topics, Siani Pearson and George Yee (editors), Springer, Computer Communications and Networks series, 2012.

**Abstract**. Managing information risk is a complex task that must continually adapt to business and technology
changes. We argue that cloud computing presents a more significant step change, and so implies a bigger change for
the enterprise risk and security management lifecycle. Specifically, the economies of scale that large providers
can achieve are creating an ecosystem of service providers in which the marketplace (rather than consuming enterprises)
determines security standards and properties. Moreover, the ability to consume high-level services from different
environments is changing the nature of one-size-fits-all security policies.

Manuscript available here.

The TSB-funded Trust Economics project Final Report.

Information Stewardship in Cloud Ecosystems: Towards Models, Economics, and Delivery. Joint work with Adrian Baldwin, Martin Sadler, and Simon Shiu. Preprint.

Proc. 2011 Third IEEE International Conference on Cloud Computing Technology and Science (CloudCom 2011), IEEE Digital Library, 784--791, 2011. doi: 10.1109/CloudCom.2011.121 Copyright IEEE, 2011.

**Abstract**. We discuss the concept of information stewardship in cloud-based business ecosystems. The constituent
concepts of stewardship --- which we believe will be crucial to the successful development of cloud-based business of all
kinds --- extend those of security to encompass concepts such as values, ethics, resilience, and sustainability:
all familiar from the stewardship of natural resources. Our view is based on rigorous approaches from mathematical
systems modelling and economics, and is informed by concepts from natural resource management and information
assurance.

Fixed Costs, Investment Rigidities, and Risk Aversion in Information Security: A Utility-theoretic Approach. Joint work with Christos Ioannidis and Julian Williams. Proc. WEIS 2011, George Mason University, Fairfax, Virginia, 14-15 June, 2011: WEIS 2011.

Proc. WEIS 2011, George Mason University, Fairfax, Virginia, 14-15 June, 2011.
In *Economics of Security and Privacy III*, Bruce Schneier (editor), Springer 2012. pp. 171--192.

**Abstract**. This paper introduces and demonstrates a simple analytically tractable method of mapping utility
theory to information security problems and in particular optimal timing for vulnerability management.
Our primary focus is on the decision to defer costly deterministic investment, such as the removal of a service or
implementation of a security patch, when the costs associated with future security vulnerabilities are uncertain.
We outline an investment function with fixed and variable costs that imports a nominal rigidity into the investment
decision-making profile. The rigidity introduces a delay in the implementation of security measures, resulting in cyclical
investments in information security. We show how such cycles emerge endogenously from the policy-maker's chosen
trade-offs between system and security attributes.

Available from the WEIS 2011 site at here.

Information Stewardship: Systems Perspective, Systems Solutions. Slides from my Keynote presentation at Information Security Leaders (2011), Edinburgh, February 2011.

Available here.

The Structure and Dynamics of Systems Security Economics. Joint work with Adam Beautement.

**Abstract**. Structured systems security economics provides a conceptual framework, inspired by macroeconomic
models of trade-offs and mathematical systems models, for analysing the structure of security architectures, their policy constraints, and
their interactions with users. In this paper, we explore the dynamics of structured systems security economics
by considering the representation and functionality of Actors in the framework. We show how a simple representation
of Actors' preferences is sufficient to understand the security dynamics of the system and support utility calculations
that inform design and investment decisions. Overall, the framework is intended to facilitate the design and implementation
of trustworthy security systems.

Manuscript available here.

Economics of Information Security and Privacy. Co-editor with Tyler Moore and Christos Ioannidis. Springer New York Dordrecht Heidelberg London, 2010. doi: 10.1007/978-1-4419-6967-5.

Papers from WEIS 2009, the Eighth Workshop on the Economics of Information Security, UCL, June 24-25, 2009.

Available from Amazon.

Security Analytics: Bringing Science to Security Management. Joint work with Simon Shiu.
*IISP Pulse* 4 Summer 2010: 12-13.

Available here.

Information Stewardship in the Cloud: A Model-based Approach. Joint work with Martin Sadler, Simon Shiu, and Marco Casassa Mont. To appear, Proc. CloudComp 2010, Lecture Notes of the Institute for Computer Sciences, Social Informatics and Telecommunications Engineering (LNICST) series, Springer, 2010. Preprint.

**Abstract**. Managing the information stewardship lifecycle is a challenge. In the context of
cloud computing, the stakeholders in cloud ecosystems must also take account of the demands of the
information stewardship lifecycles of other participants in the ecosystem. We describe a modelling
framework --- incorporating tools from mathematical systems modelling, economics,
and policy/user modelling --- suitable for supporting reasoning and decision making in cloud
ecosystems, and so provides a basis for developing model-based service level agreements.

Structured Systems Economics for Security Management. Joint work with Adam Beautement. Proc. WEIS 2010, Harvard University. Paper. Presentation.

**Abstract**. We develop an ontological account of information
security architectures that is inspired by economic models of trade-offs
between confidentiality, integrity, and availability. Our approach clarifies
the nature of the trade-offs by making a clear distinction between declarative and
operational concepts in security. We integrate this approach with a
semantically justified mathematical systems modelling technology, thus providing
a basis for a systematic methodology to support operational decision-making in
information security investments and trade-offs.

Information Stewardship in Cloud Computing. Joint work with Martin Sadler.
*International Journal of Service Science, Management, Engineering,
and Technology* 1(1), 50-67, 2010.
Free sample copy, including this article.

Semantics for Structured Systems Modelling and Simulation. Joint work with
Matthew Collinson and Brian Monahan. *Proc. Simutools 2010*,
ACM Digital Library and EU Digital Library. ISBN: 978-963-9799-87-5.
Preprint.

**Abstract**. Simulation modelling is an important tool for exploring and reasoning
about the dynamics and properties of complex systems, and
many supporting languages are available. Commonly occurring
features of these languages are constructs that capture concepts
such as process, resource, and location. We describe a mathematical
framework that supports a modelling idiom based on these core
concepts, and which also adopts stochastic methods for representing
the environments within which systems exist. We explain how
this framework can be used to give a formal semantics to a simulation
modelling language, Core Gnosis, that includes basic constructs
for process, resource, and location. We include a brief discussion
of a system of logic for reasoning about our models that
is compositional with respect to the structure of models. We believe
that our mathematical analysis of systems in terms of process,
resource, location, and stochastic environment, together with a language
that captures these concepts quite directly, leads to an efficient
and robust modelling framework within which natural mathematical
reasoning about systems is captured in the associated tools.

Decision Support for Systems Security Investment. Joint work with Yolanta
Beresnevichiene and Simon Shiu. *Proc. Business-driven IT Management*
(BDIM) 2010. IEEE Xplore, 2010. Preprint

**Abstract**. Information security managers with fixed budgets must invest
in security measures to mitigate increasingly severe threats whilst
maintaining the alignment of their systems with their organization's
business objectives. The state of the art lacks a systematic methodology
to support security investment decision-making. We describe a
methodology that integrates methods from multi-attribute utility
evaluation and mathematical systems modelling. We illustrate our
approach using a case study of a large organization divesting itself of its
IT support services, delivering useful results to the organization's
security managers. Specifically, by integrating a mathematical model of
system behaviour with an account of the utility of available security
investment strategies, the case study has enabled them to understand
better the trade-offs between the security performance and the
operational consequences of their choices.

Economics of Identity and Access Management: Providing Decision Support for
Investments. Joint work with Marco Casassa Mont, Yolanta
Beresnevichiene, and Simon Shiu. *Proc. Business-driven IT
Management* (BDIM) 2010. IEEE Xplore, 2010. Preprint

**Abstract**. Identity and Access Management (IAM) is a key enabler of
enterprise businesses: it supports automation, security enforcement and
compliance. However, most enterprises struggle with their Identity and Access
Management strategy. Discussions on IAM primarily focus at the IT operational
level, rather than targeting strategic decision makers' issues, at the business
level. Organisations are experiencing an increasing number of internal and
external threats and risks: there is scarcity of resources and budget to
address them all. Decision makers (e.g. CIOs, CISOs) need to prioritise their
choices and motivate their requests for investments. This applies for
investments in IAM vs. other possible security or business investments that
could be made by the organisation. In this context, a range of possible IAM
investment options has an effect on multiple strategic outcomes of interest,
such as assurance, agility, security, compliance, productivity and
empowerment. We have developed a repeatable approach and methodology to help
organisations work through this complex problem space and determine an
appropriate strategy, by providing them with decision support capabilities. The
proposed approach, validated in collaboration with Security & IAM experts,
couples economic modeling, enabling decision makers to explore their
preferences between the different outcomes, with system modeling & simulations
to predict the consequences (likely outcomes) associated with different
investment choices and map them against decision makers' preferences to
identify the most suitable options. We illustrate how this methodology has been
applied in an IAM case study, in a business-driven context with core enterprise
services. This work is in progress. We discuss current results and next steps.

Information Security Trade-offs and Optimal Patching Policies. Joint work with
Christos Ioannidis and Julian Williams.
*European Journal of Operational Research*,
216(2):434-444, 16 January 2012. doi:10.1016/j.ejor.2011.05.050.
Preprint.

**Abstract**.We develop and simulate a model of the deployment of patches
--- which incurs cost --- in the presence of trade-offs between confidentiality
and availability.
The patching of vulnerabilities is divided into regular and irregular events,
for both networks and clients. The computation of the optimal patching policy
requires knowledge of the joint processes of arrivals and intensities, system
architecture, and the type of organization. We have found that different
types of organizations, as characterized by the managers' preferences, exhibit
distinct off-cycle patching profiles that are relatively cost-sensitive, and
that
the frequency of irregular patching depends crucially on the aspect of the
system --- e.g., network or clients --- addressed.

Investments and Trade-offs in the Economics of Information Security. Joint work
with Christos Ioannidis and Julian Williams. *Proc. Financial
Cryptography and Data Security 2009*, LNCS 5628: 148-162, Springer, 2009.
Preprint.

**Abstract**.
We develop and simulate a dynamic model of investment in information
security. The model is based on the recognition that both IT managers
and users appreciate the trade-off between the fundamental
characteristics of information security, namely confidentiality and
availability. The model's parameters can be clustered in a manner that
allows us to categorize and compare the responses to shocks of various
types of organizations. We derive the system's stability conditions
and find that they admit a wide choice of parameters. We examine the system's
responses to the same shock in confidentiality under different parameter
constellations that correspond to various types of organizations. Our
analysis illustrates that the response to investments in information security
will be uniform in neither size nor time evolution.

My Keynote Presentation at the recent ESRC Public Policy Seminar on the Economics of Information Security is summarized in the ESRC Report.

A Logical and Computational Theory of Located Resource. Joint work with Matthew
Collinson and Brian Monahan. *Journal of Logic and Computation*19(b):1207-1244, 2009.
Advance Access published on 22 July, 2009. doi:10.1093/logcom/exp021.
Preprint.
Also available as an HP Labs Technical Report:
HPL-2008-74R1.

**Abstract**. Experience of practical systems modelling suggests that the
key conceptual components of a model of a system are processes, resources, locations, and environment. In
recent work, we have given a process-theoretic account of this view in which resources as well as
processes are first-class citizens. This process calculus, SCRP, captures the
structural aspects of the semantics of the Demos2k modelling tool. Demos2k represents environment
stochastically using a wide range of probability distributions and queue-like data
structures. Associated with SCRP is a (bunched) modal logic, MBI, which combines the usual additive
connectives of Hennessy-Milner logic with their multiplicative counterparts. In this paper, we
complete our conceptual framework by adding to SCRP and MBI an account of a notion of location
that is simple yet sufficiently expressive to capture naturally a wide range of
forms of location, both spatial and logical. We also provide a sketch of an extension of
the Demos2k tool to incorporate this notion of location.

Modelling the Human and Technological Costs and Benefits of USB Memory Stick
Security. Joint work with Adam Beautement et al. Available from
Proc. WEIS 2008.
In *Managing Information Risk and the Economics of Security*. M. Eric
Johnson (editor), Springer, 2009: 141-163.
Preprint.

**Abstract**.
Organizations deploy systems technologies in order to support their
operations and achieve their business objectives. In so doing, they
encounter tensions between the confidentiality, integrity, and
availability of information, and must make investments in information
security measures to address these concerns. We discuss how a
macroeconomics-inspired model, analogous to models of interest rate policy used by
central banks, can be used to understand trade-offs between
investments against threats to confidentiality and availability. We
investigate how such a model might be formulated by constructing a
process model, based on empirically obtained data, of the use of USB
memory sticks by employees of a financial management company.

Some recent HP Labs Technical Reports on topics related to services sciences, systems modelling, mathematical logic, and other topics. Some of these papers have been published elsewhere (conferences, journals, etc.).

- HPL-2006-35: A structural and stochastic modelling philosophy for systems integrity.
- HPL-2006-99: Grand Challenges for Systems and Services Sciences .
- HPL-2006-100: Engineering the polymath in systems and services education.
- HPL-2006-112: Systems and services sciences: a rational and a research agenda.
- HPL-2006-125: Predictive modelling for security operations economics.
- HPL-2007-22: Public Services Innovation through Technology.
- HPL-2007-23: UK Services Innovation Network.
- HPL-2007-89: Assessing the value of investments in network security operations: a systems analytics approach.
- HPL-2007-100: A games model of bunched implications.
- HPL-2007-101: Economic Aspects of a Utility Computing Service.
- HPL-2008-94: Modelling Task Knowledge Structures in Demos 2000.

An Update to Located Demos2k. Joint work with Matthew Collinson and Brian Monahan. Available as an HP Labs Technical Report: HPL-2008-205.

**Abstract**.
We give here a short update concerning Located Demos2k briefly describing the
ability to forget and recall resource links, as reported in an earlier
Technical Report. We also briefly mention our (purely applicative)
implementation in OCaml of a simulator for Located Demos2k. Two appendices contain a
substantial example of Located Demos2k, presented in OCaml terms,
and the execution trace produced by the implementation.

Located Demos2k: A Tool for Executing Processes Relative to Distributed Resources. Joint work with Matthew Collinson and Brian Monahan. Available as an HP Labs Technical Report: HPL-2008-76.

**Abstract**. We describe the background to, and the current state of the
development of, Located Demos2k, an executable modelling language which
reconstructs the Demos2k language starting from an explicit model of
location. The version of Located Demos2k described herein is the first
useful stage in its development, and provides convenient a point of
departure of discussing its further development.

Algebra and Logic for Access Control. Joint work with
Matthew Collinson. *Formal Aspects of Computing*22(2), 83-104, 2010.
Erratum: *Formal Aspects of Computing*22(3-4), 483-484, 2010.
Available as an HP Labs Technical
Report (with erratum incorporated):
HPL-2008-75R1.
The original publication is available at http://www.springerlink.com.

**Abstract**. The access control problem in computer security is
fundamentally concerned
with the ability of system entitites to see, make use of, or alter various
system resources. As such, many access control situations are essentially
problems of concurrency.
We give an account of fundamental situations in access-control in distributed
systems using a resource-based process calculus and a hybrid of Hennessy-Milner
and resource logic.
This yields a consistent account of operational behaviour and logical reasoning
for access control, that includes an analysis of co-signing, roles and
chains-of-trust.

Bunched Polymorphism. Joint work with Matthew Collinson and Edmund
Robinson. *Mathematical Structures in Computer Science* 18(6), 1091-1132,
2008. doi: 10.1017/S0960129508007159.
Preprint.

**Abstract**.
We describe a polymorphic, typed lambda calculus with
substructural features. This calculus extends the
first-order substructural lambda calculus alphalambda
associated with bunched logic. A particular novelty of our new
calculus is the substructural treatment of second-order variables.
This is accomplished through the use of bunches of type variables
in typing contexts. Both additive and multiplicative
forms of polymorphic abstraction are then supported. The
calculus has sensible proof-theoretic properties and a
straightforward categorical semantics using indexed categories.
We produce a model for additive polymorphism with first-order
bunching based on partial equivalence relations. We consider
additive and multiplicative existential quantifiers separately from
the universal quantifiers.

Algebra and Logic for Resource-based Systems Modelling. Joint work with Matthew
Collinson. *Mathematical Structures in Computer Science* 19:959-1027,
2009. doi:10.1017/S0960129509990077. Preprint.

**Abstract**. Mathematical modelling is one of the fundamental tools of science
and engineering. Very often, models are required to be executable, as
a simulation, on a computer. In this paper, we present some
contributions to the process-theoretic and logical foundations of
discrete-event modelling with resources and processes. We present a
process calculus with an explicit representation of resources in which
processes and resources co-evolve. The calculus is closely connected
to a logic that may be used as a specification language for properties
of models. The logic is strong enough to allow requirements that a
system have certain structure; for example, that it is a parallel
composite of subsystems. This work consolidates, extends, and improves
upon aspects of the earlier works. An extended example, consisting of a
semantics for a simple parallel programming language, indicates a
connection with separating logics for concurrency.

Errata

- Page 994 (page 36 in the preprint), Fig. 7: in each of the bottom two clauses,
*R , E ~ R , vS.F*should be*E ~ vS.F*

A Games Model of Bunched Implications. Proc. CSL '07, LNCS 4646: 573-588. Joint work with Guy McCusker.

**Abstract**. A game semantics of the implicational fragment of the
(-*,->)-fragment of the logic of bunched implications, BI, is presented. To
date, categorical models of BI have been restricted to two kinds: functor
category models; and the category Cat itself. The game model is not of this
kind. Rather, it is based on Hyland-Ong-Nickau-style games and embodies a
careful analysis of the notions of resource sharing and separation inherent in
BI. he key to distinguishing between the additive and multiplicative
connectives of BI is a semantic notion of separation. The main result of the
paper is that the model is fully complete: every finite, total strategy in the
model is the denotation of a term of the alphalambda-calculus, the term
language for the fragment of BI under consideration.

Systems Modelling via Resources and Processes: Philosophy, Calculus, Semantics, and Logic. Joint work with Chris Tofts.

Here is a preprint of
*ENTCS* 172, 545-587, 2007. *ENTCS* 172 is entitled 'Computation,
Meaning, and Logic: Articles dedicated to Gordon Plotkin'.

**Abstract**.
We describe a programme of research in resource semantics, concurrency
theory, bunched logic, and stochastic processes, as applied to
mathematical systems modelling. Motivated by a desire for structurally
and semantically rigorous discrete event modelling tools, applicable
to enterprise-scale as well as component-scale systems, we introduce a
new approach to compositional reasoning based on a development of SCCS
with an explicit model of resource. Our calculus models the
co-evolution of resources and processes with synchronization
constrained by the availability of resources. We provide a simple
denotational semantics as a parametrization of Abramsky's synchronization
trees semantics for SCCS. We also provide a logical
characterization, analogous to Hennessy-Milner logic's
characterization of bisimulation in CCS, of bisimulation between
resource processes which is compositional in the concurrent and local
structure of systems. We discuss applications to ideas such as
location and access control.

A Calculus and Logic of Resources and Processes. Joint work with Chris Tofts.

*Formal Aspects of Computing*, 18(4): 495-517, 2006.

Preprint here. The original publication is available at http://www.springerlink.com.

**Abstract**.
Recent advances in logics for reasoning about
resources provide a new approach to compositional reasoning in
interacting systems. We present a calculus of resources and
processes, based on a development of Milner's synchronous calculus of
communication systems, SCCS, that uses an explicit model of
resource. Our calculus models the co-evolution of resources and
processes with synchronization constrained by the availability of
resources. We provide a logical characterization, analogous to
Hennessy-Milner logic's characterization of bisimulation in CCS, of
bisimulation between resource processes which is compositional in the
concurrent and local structure of systems.

Bunching for Regions and Locations. Joint work with Matthew Collinson.

**Abstract**.
There are a number of applied lambda-calculi in which terms and types
are annotated with parameters denoting either locations or locations
in machine memory. Such calculi have been designed with safe
memory-management operations in mind.

It is difficult to construct directly denotational models for existing calculi of this kind. We approach the problem differently, by starting from a class of mathematical models that describe some of the essential semantic properties intended in these calculi. In particular, disjointness conditions between regions (or locations) are implicit in many of the memory-management operations.

Bunched polymorphism provides natural type-theoretic mechanisms for capturing the disjointness conditions in such models. We illustrate this by adding regions to the basic disjointness model of $\alphalambda$, the lambda-calculus associated to the logic of bunched implications. We show how both additive and multiplicative polymorphic quantifiers arise naturally in our models. A locations model is a special case. In order to relate this enterprise back to previous work on memory-management, we provide an example in which the model is refined and used to provide a denotational semantics for a language with explicit allocation and disposal of regions.

In: Proc. MFPS 2006, S. Brookes and M. Mislove (editors),
*Electronic Notes in Theoretical Computer Science*, 2006.

On Bunched Polymorphism (Extended Abstract). Joint work with Matthew Collinson and Edmund Robinson.

**Abstract**.
We describe a polymorphic extension of the substructural lambda
calculus alphalambda associated with the logic of bunched
implications. This extension is particularly novel in that
both variables and type variables are treated substructurally,
being maintained through a system of zoned, bunched contexts.
Polymorphic universal quantifiers are introduced in both additive
and multiplicative forms, and then metatheoretic properties, including
subject-reduction and normalization, are established.
A sound interpretation in a class of indexed category models is defined
and the construction of a generic model is outlined, yielding
completeness.
A concrete realization of the categorical models is given
using pairs of partial equivalence relations on the natural numbers.
Polymorphic existential quantifiers are presented, together with some
metatheory.
Finally, potential applications to closures and memory-management
are discussed.

Proc. CSL 05, *Lecture Notes in Computer Science* 3634, 36-50, 2005.

A games semantics for reductive logic and proof-search. Joint work with Eike Ritter.

**Abstract**. Theorem proving, or algorithmic proof-search, is an
essential enabling technology throughout the computational
sciences. We explain the mathematical basis of proof-search as the
combination of reductive logic together with a control régime. Then
we present a games semantics for reductive logic and show how it may
be used to model two important examples of control, namely
backtracking and uniform proof.

*Proc. ETAPS 05
Workshop on Games for Logic and Programming Languages,
Edinburgh, April, 2005*.

Reductive Logic and Proof-search: Proof Theory, Semantics, and Control. Joint work with Eike Ritter.

*Oxford Logic Guides*, 45, Oxford University Press, 2004.

Errata and Remarks.

*Mathematical Structures in Computer Science* (2007) 17, 957-1027.

**Abstract**. It is well-known that weakening and contraction cause naïve
categorical models of the classical sequent calculus to collapse to
Boolean lattices. In previous work, summarized briefly herein, we
have provided a class of models called classical
categories which is sound and complete and avoids this collapse
by interpreting cut-reduction by a poset-enrichment. Examples of
classical categories include boolean lattices and the category of sets
and relations, where both conjunction and disjunction are modelled by
the set-theoretic product.

In this article, which is self-contained, we present an improved axiomatization of classical categories, together with a deep exploration of their structural theory. Observing that the collapse already happens in the absence of negation, we start with negation-free models called Dummett categories. Examples include, besides the classical categories above, the category of sets and relations, where both conjunction and disjunction are modelled by the disjoint union. We prove that Dummett categories are MIX, and that the partial order can be derived from hom-semilattices which have a straightforward proof-theoretic definition. Moreover, we show that the Geometry-of-Interaction construction can be extended from multiplicative linear logic to classical logic, by applying it to obtain a classical category from a Dummett category.

Along the way, we gain detailed insights into the changes that proofs undergo during cut-elimination in the presence of weakening and contraction.

**Abstract**. It is well-known that weakening and contraction
cause naïve categorical models of the classical sequent
calculus to collapse to Boolean lattices. We introduce sound and
complete models that avoid this collapse by interpreting
cut-reduction by a partial order between morphisms. We provide
concrete examples of such models by applying the
geometry-of-interaction construction to quantaloids with finite
biproducts, and show hoe these models illuminate cut-reduction in
the presence of weakening and contraction. Our models make no
commitment to any translation of classical logic into intuitionistic
logic and distinguish non-deterministic choices of cut-elimination.

The Semantics of BI and Resource Tableaux. Joint work with Didier Galmiche and Daniel Méry at LORIA, Nancy.

**Abstract**. The logic of bunched implications, **BI**, provides a
logical analysis of a basic notion of resource rich enough, for example,
to form the logical basis for `pointer logic' and `separation logic'
semantics for programs which manipulate mutable data structures. We
develop a theory of semantic tableaux for **BI**, so providing an elegant
basis for efficient theorem proving tools for **BI**. It is based on
the use of an algebra of labels for **BI**'s tableaux to solve the
resource-distribution problem, the labels being the elements of
resource models. For **BI** with inconsistency, bottom, the challenge
consists in dealing with **BI**'s Grothendieck topological models within
such a proof-search method, based on labels. We prove soundness and
completeness theorems for a resource tableaux method **TBI** with
respect to this semantics and provide a way to build countermodels
from so-called dependency graphs. Then, from these results, we can
define a new resource semantics of **BI**, based on partially defined
monoids, and prove that this semantics is complete. Such a semantics,
based on partiality, is closely related to the semantics of **BI**'s
(intuitionistic) pointer and separation logics. Returning to the
tableaux calculus, we propose a new version with liberalized rules for
which the countermodels are closely related to the topological Kripke
semantics of **BI**. As consequences of the relationships between
semantics of **BI** and resource tableaux, we prove two strong new
results for propositional **BI**: its decidability and the finite model
property with respect to topological semantics.

**Abstract**. Since its earliest presentations, mathematical logic
has been formulated as a formalization of *deductive* reasoning:
given a collection of hypotheses, a conclusion is derived. However,
the advent of computational logic has emphasized the significance of
*reductive* reasoning: given a putative conclusion, what are
sufficient premisses ? Whilst deductive systems typically have a
well-developed semantics of proofs, reductive systems are typically
well-understood only operationally. Typically, a deductive system can
be read as a corresponding reductive system. The process of
calculating a proof of a given putative conclusion, for which
non-deterministic choices between premisses must be resolved, is
called *proof-search* and is an essential enabling technology
throughout the computational sciences. We suggest that the reductive
view of logic is (at least) as fundamental as the deductive view and
discuss some of the problems which must be addressed in order to
provide a semantics of proof-searches of comparable value to the
corresponding semantics of proofs. Just as the semantics of proofs is
intimately related to the model theory of the underlying logic, so too
should be the semantics of reductions and of proof-search. We discuss
how to solve the problem of providing a semantics for proof-searches
in intuitionistic logic which adequately models both not only the
logical but also, via an embedding of intuitionistic reductive logic
into classical reductive logic, the operational aspects, *i.e.*,
control of proof-search, of the reductive system.

ORDER-ENRICHED CATEGORICAL MODELS OF THE CLASSICAL SEQUENT CALCULUS. Joint work with Carsten Führmann.

**Abstract**. It is well-known that weakening and contraction
cause naïve categorical models of the classical sequent calculus
to collapse to Boolean lattices. Starting from a convenient
formulation of the well-known categorical semantics of linear
classical sequent proofs, we give models of weakening and contraction
that do not collapse. Cut-reduction is interpreted by a partial
order between morphisms. Our models make no commitment to any
translation of classical logic into intuitionistic logic and
distinguish non-deterministic choices of cut-elimination. We show
soundness and completeness via initial models built from proof nets,
and describe models built from sets and relations.

A paper on semantic tableaux for

Errata and remarks applicable to this paper are available here.

A short paper (Extended Abstract) on Bunched Logic Programming is here. It is joint work with a Ph.D. student, Pablo Armelín. It appeared in the proceedings of IJCAR 2001, LNAI 2083, 289-304, 2001. Some notes on a fixed point semantics (a `least Herbrand model') for bunched logic programming are here.

Errata and remarks applicable to this paper are available here.

A preprint of a paper, with James Harland, `Resource-distribution via Boolean constraints', which provides a general, algebraic solution to the problem, in proof-search, of distributing side-formulae between the premisses of multiplicative rules is here.

A short, informal paper, `Notes Towards a Semantics for Proof-search', is here. It is in ENTCS 37 (2001), edited by D. Galmiche and associated with the CADE-17 Workshop, `Type-theoretic Languages: Proof-search and Semantics', 2000. 18 pages.

A preprint, `Possible Worlds and Resources: The Semantics of

A preprint of a paper on the (categorical and proof-theoretic) semantics of classical disjunction, which is in the

A short paper, `Forward and Backward Chaining in Linear Logic', with James Harland and Michael Winikoff, is in ENTCS 37 (2001), edited by D. Galmiche and associated with the CADE-17 Workshop, `Type-theoretic Languages: Proof-search and Semantics', 2000. 16 pages.

I have recently edited (jointly with my colleague Didier Galmiche at LORIA, Nancy, France) a Special Issue of the journal Theoretical Computer Science on `Proof-search in Type-theoretic Languages'. A preprint of the introductory article by Galmiche and myself, which examines a variety of syntactic, semantic and pragmatic issues in the foundations of the theory of proof-search, is here. Small changes may occur before printing.

*Theoretical Computer Science* 232 (2000) 5-53. Erratum: p. 32,
side-condition of Resolution rule, replace index *i* by *k*
and insert `*i* ≤ *k* ≤ *n*,' after the comma.
Erratum also applies to the corresponding occurrence of the Resolution
rule in the preprint (above, p. 26).

A paper on

Erratum: In Proposition 4, `DCC' should be `bicartesian DCC'.

`On Bunched Predicate Logic', appears in LICS '99; a preprint is available here.

A preprint of `Kripke resource models of a dependently-typed, bunched lambda-calculus' is here: It is published as Journal of Logic and Computation 12(6): 1061-1104, 2002. An extended abstract of this paper appears in the LNCS proceedings of CSL'99. (Please note that there is a bad typo in the definition of the class of models: `I isomorphic to 1' should be `I not isomorphic to 1'.) See also Corrections and Remarks, by S. Ishtiaq and D. Pym, Research Report No. RR-00-04, October 2000. ISSN 1470-55559.

An extended abstract on logic programming with bunched implications is available here. It is in ENTCS (17), 24pp., devoted to the CADE-15 Workshop, `Proof-search in Type-theoretic Languages'.

A paper on the intuitionistic force of classical search, which appears in the journal TCS, 232 (2000) 299-333. A preprint is available in postscript format here.

A paper on proof-terms for classical and intuitionistic resolution is in the Journal of Logic and Computation 10(2), 173-207, 2000. A preprint is available in postscript format here.

A paper on a logical framework (RLF) for describing linear and other relevant logics, including the type-assignment system for ML with references, is available in postscript format here. The language of RLF is a type theory with a full linear dependent function space. The paper is in the Journal of Logic and Computation 8(6):809-838, 1998.

David J. Pym