On information flow and refinement-closure (2008)
Abstract. The question of information flow considers whether a highlevel user of a multi-level security system can pass information to a lowlevel user. One family of information flow properties is...
1 On the Automatic Verification of Non-Standard Measures of Consistency (2008)
Consistency between a process and its specification expressed in CSP is typically presented as a refinement check. Within the traces model consistency is measured by examining only the traces of the...
Counter Abstraction in the CSP/FDR setting Abstract (2008)
In this paper we consider an adaptation of counter abstraction for the CSP/FDR setting. The technique allows us to transform a concurrent system with an unbounded number of agents into a finite-state...
Abstract On timed models and full abstraction (2008)
In this paper we study a denotational model for a discrete-time version of CSP. We give a compositional semantics for the language. The model records refusal information at the end of each time unit;...
A CSP approach to sequential consistency (2007)
In this paper, we show how the process notation of Communicating Sequential Processes (CSP) may be used to describe a lazy caching protocol. We then show that the traces model for CSP can be used to...
How to prevent type flaw attacks on security protocols (2003)
Heather, James A., Lowe, Gavin, Schneider, Steve A.
A type flaw attack on a security protocol is an attack where a field that was originally intended to have one type is subsequently interpreted as having another type. A number of type flaw attacks...
On distributed security transactions that use secure transport protocols (2003)
In this paper we consider techniques for designing and analysing distributed security transactions. We present a layered approach, with a high-level security transaction layer running on top of a...
Using data-independence in the analysis of intrusion detection systems (2003)
Gordon Thomas Rohrmair, Gavin Lowe
Abstract. In a previous paper we showed how to use the process algebra CSP to discover de-synchronisation attacks on intrusion detection systems. However, our analysis was not complete: if we failed...
Using data-independence in the analysis of intrusion detection systems (2003)
Gordon Thomas Rohrmair, Gavin Lowe
Abstract. In a previous paper we showed how to use the process algebra CSP to discover de-synchronisation attacks on intrusion detection systems. However, our analysis was not complete: if we failed...
Using CSP to detect insertion and evasion possibilities within the intrusion detection area (2002)
Gordon Thomas Rohrmair, Gavin Lowe
Abstract. In this paper we will demonstrate how one can model and analyse Intrusion Detection Systems (IDSs) and their environment using the process algebra Communicating Sequential Processes (CSP)...
Analysing protocols subject to guessing attacks (2002)
In this paper we consider guessing attacks upon security protocols, where an intruder guesses one of the values used (typically a poorlychosen password) and then seeks to verify that guess. We...
Quantifying Information Flow (2002)
We extend definitions of information flow so as to quantify the amount of information passed; in other words, we give a formal definition of the capacity of covert channels. Our definition uses the...
Analysing protocols subject to guessing attacks (2002)
In this paper we consider guessing attacks upon security protocols, where an intruder guesses one of the values used (typically a poorly-chosen password) and then seeks to verify that guess. We...
Analysing a Stream Authentication Protocol using Model Checking (2002)
Abstract. In this paper, we consider how one can analyse a stream authentication protocol using model checking techniques. In particular, we will be focusing on the Timed E#cient Stream Loss-tolerant...
Quantifying Information Flow (2002)
In the past, several definitions of information flow based upon process algebras have been presented. Unfortunately, these appear to have all been either too weak---failing to identify certain subtle...
Quantifying Information Flow (2002)
We extend definitions of information flow so as to quantify the amount of information passed; in other words, we give a formal definition of the capacity of covert channels. Our definition uses the...
Quantifying Information Flow (2002)
We extend definitions of information flow so as to quantify the amount of information passed; in other words, we give a formal definition of the capacity of covert channels. Our definition uses the...
2 An example input file 2 2.1 Overview of input file.............................. 3
Analyzing a library of security protocols using Casper and FDR (1999)
Ben Donovan, Paul Norris, Gavin Lowe
In this paper we describe the analysis of a library of fifty security protocols using FDR, a model checker for the process algebra CSP, and Casper, a compiler that produces the CSP descriptions from...
Using CSP to verify sequential consistency (1999)
Summary. This paper shows how the theory of Communicating Sequential Processes (CSP) can be used to establish that a protocol guarantees sequential consistency. The protocol in question is an...
Towards a completeness result for model checking of security protocols (1998)
Model checking approaches to the analysis of security protocols have proved remarkably successful. The basic approach is to produce a model of a small system running the protocol, together with a...
Towards a Completeness Result for Model Checking of Security Protocols (Extended Abstract) (1998)
Model checking approaches to the analysis of security protocols have proved remarkably successful. The basic approach is to produce a model of a small system running the protocol, together with a...
A hierarchy of authentication specifications (1997)
Many security protocols have the aim of authenticating one agent to another. Yet there is no clear consensus in the academic literature about precisely what "authentication" means....
A hierarchy of authentication specifications (1997)
Many security protocols have the aim of authenticating one agent to another. Yet there is no clear consensus in the academic literature about precisely what "authentication " means....
a compiler for the analysis of security protocols (1997)
In recent years, a method for analyzing security protocols using the process algebra CSP [8] and its model checker FDR [24] has been developed. This technique has proved remarkably successful, and...
A Family of Attacks upon Authentication Protocols (1997)
In this paper we present four similar attacks upon well known authentication protocols, and suggest that similar attacks exist for other protocols. Each of these attacks causes an agent B to think...
Using CSP to detect errors in the TMN protocol (1997)
In this paper we use FDR, a model checker for CSP, to detect errors in the TMN protocol [TMN90]. We model the protocol and a very general intruder as CSP processes, and use the model checker to test...
Some New Attacks upon Security Protocols (1996)
Many security protocols have appeared in the literature, with aims such as agreeing upon a cryptographic key, or achieving authentication. However, many of these have been shown to be flawed. In this...
Breaking and Fixing the Needham-Schroeder Public-Key Protocol using FDR (1996)
ABSTRACT In this paper we analyse the well known Needham-Schroeder Public-Key Protocol using FDR, a refinement checker for CSP. We use FDR to discover an attack upon the protocol, which allows an...
Some New Attacks upon Security Protocols (1996)
Many security protocols have appeared in the literature, with aims such as agreeing upon a cryptographic key, or achieving authentication. However, many of these have been shown to be flawed. In this...
An attack on the Needham-Schroeder public-key authentication protocol (1995)
In this paper we present an attack upon the Needham-Schroeder publickey authentication protocol. The attack allows an intruder to impersonate another agent.
Refinement of Complex Systems: a Case Study (1995)
We describe the Temporal Agent Model (TAM) together with its associated refinement calculus. The calculus is based on a wide-spectrum language within which functional and temporal properties can be...
Refinement Of Complex Systems: A Case Study (1995)
Gavin Lowe, Gavin Lowe, Hussein Zedan, Hussein Zedan
We describe the Temporal Agent Model (TAM) together with its associated refinement calculus. The calculus is based on a wide-spectrum language within which functional and temporal properties can be...
Infinite Behaviours In The Temporal Agent Model (1995)
In this paper we extend the Temporal Agent Model [SZJ94] so as to be able to reason about infinite agents. We augment the syntax with an infinite iteration operator, and extend the semantic model so...
Probabilistic and Prioritized Models of Timed CSP (1995)
In this paper we present two languages that are refinements of timed CSP [4]: a probabilistic language, and a fully deterministic language with a notion of priority. In the first part of the paper we...
. We present a graphical calculus, which allows mathematical formulae to be represented and reasoned about using a visual representation. We define how a formula may be represented by a graph, and...
We present a graphical calculus, which allows mathematical formulae to be represented and reasoned about using a visual representation. We define how a formula may be represented by a graph, and...
Scheduling-Oriented Models for Real-Time Systems (1995)
In this paper, we define a formal model for reasoning about resource allocation and scheduling in real-time systems. We extend the model of Scholefield, Zedan and He [3], which models the...
Scheduling-Oriented Models for Real-Time Systems (1994)
In this paper we define models for reasoning about resource allocation and scheduling in real-time systems. We begin by producing a model that allows us to argue about the resource requirements of...
In this paper we consider a simple example of embedded software taken from the aircraft industry [Rol88]. We use the formal models for scheduling analysis developed in [Low94] to specify, design and...
Scheduling-Oriented Models for Real-Time Systems (1994)
In this paper, we define a formal model for reasoning about resource allocation and scheduling in real-time systems. We extend the model in [SZJ94], which models the functionality of agents in the...
Probabilities and priorities in Timed CSP / (1993)
Thesis (D. Phil.)--University of Oxford.
Representing Nondeterministic and Probabilistic Behaviour in Reactive Processes (1993)
. In this paper we investigate ways of modelling communicating processes that display both nondeterministic and probabilistic behaviour. We present an operational model for a probabilistic version of...
Representing Nondeterminism And Probabilistic Behaviour In Reactive Processes (1993)
In this paper we describe a way of modelling communicating processes that display both nondeterministic and probabilistic behaviour. We represent processes by nondeterministic, probabilistic, action...
Some Extensions to the Probabilistic Biased Model of Timed CSP (1992)
In a previous paper [Low92] we presented two languages based upon timed CSP, with associated semantic models. The first language included biased operators in the syntax, which could be used to model...
Specification and Proof in Probabilistic, Prioritized, Timed CSP (1992)
In [Low91] we presented a probabilistic model of timed CSP, which was based upon a deterministic language with prioritized operators, augmented with a probabilistic choice operator. We gave a...
Specification and Proof of Prioritized, Timed CSP Processes (1992)
In a previous paper [Low91] we presented two new languages based upon timed CSP, with associated semantic models. The first language was a completely deterministic language, which included biased...
Prioritized and Probablistic Models of Timed CSP (1991)
In this paper we present two refinements to timed CSP [DS89a]: a probabilistic model, and a fully deterministic model with a notion of priority. In the first part of the paper we describe the...
Relating the Prioritized Model of Timed CSP to the Timed Failures Model (1983)
In a previous paper [Low91] we presented two new models of timed CSP. The first model included biased operators in the syntax, which could be used to model different priorities on actions. The second...