We systematically scrutinise all the facets of privacy in the 5G delegated-authentication procedure called AKMA (Authentication and Key Management for Applications based on 3GPP credentials in the 5G Systems). We define, in general terms, a privacy-threat model and privacy requirements for this protocol. Using these definitions, we find numerous privacy failings in the AKMA protocol. We propose a patch, called AKMAp, which imposes minimal changes on AKMA, yet it attains all our privacy requirements. We also formalise and analyse all of this in terms of formal privacy-verification in the Dolev-Yao model; to this end, we use the Tamarin prover to systematically carried out our formal analyses of AKMA and AKMAp.

In an anonymous credential system, users collect credentials from issuers, and can use their credentials to generate privacy-preserving identity proofs that can be shown to third-party verifiers. Since the introduction of anonymous credentials by Chaum in 1985, there has been promising advances with respect to system design, security analysis and real-world implementations of anonymous credential systems.In this paper, we examine Hyperledger AnonCreds, an anonymous credential system that was introduced in 2017 and is currently undergoing specification. Despite being implemented in deployment-ready identity system platforms, there is no formal security analysis of the Hyperledger AnonCreds protocol. We rectify this, presenting syntax and a security model for, and a first security analysis of, the Hyperledger AnonCreds protocol. In particular, we demonstrate that Hyperledger AnonCreds is correct, and satisfies notions of unforgeability and anonymity. We conclude with a discussion on the implications of our findings, highlighting the importance of rigorous specification efforts to support security evaluation of real-world cryptographic protocols.

Adversarial Patch Attacks (APAs) induce prediction errors by inserting carefully crafted regions into images. This paper presents the first defence against APAs for deep networks that perform semantic segmentation of scenes. We show that a conditional generator can be trained to produce patches on demand targeting specific classes and achieving superior performance versus conventional pixel-optimised patch attacks. We then leverage this generator along with the segmentation network as part of a generative adversarial network, which trains the model to ignore the adversarial patches produced by the generator, while simultaneously training the generator to produce updated patches to attack the fine-tuned network. We show that our process confers strong protection against adversarial patches, and that this protection generalises to traditional pixel-optimised adversarial patches.

Online voting for independent elections is generally supported by trusted election providers. Typically these providers do not offer any way in which a voter can verify their vote, and hence the providers are trusted with ballot privacy and in ensuring correctness. Despite the desire to offer online voting for political elections, this lack of transparency and verifiability is often seen as a significant barrier to the large-scale adoption of online elections. Adding verifiability to an online election increases transparency and integrity, as well as allowing voters to verify that the vote they cast has been recorded correctly and included in the tally. However, replacing existing online systems with those that provide verifiable voting requires new algorithms and code to be deployed, and this presents a significant business risk to commercial election providers, as well as the societal risk for official elections selecting for public office. In this paper we present the first step in an incremental approach which minimises the business risk but demonstrates the advantages of verifiability, by developing an implementation of key elements of a Selene-based verifiability layer and adding it to an operational online voting system. Selene is a verifiable voting protocol that publishes votes in plaintext alongside a voter's tracker. These trackers enable voters to confirm that their votes have been captured correctly by the system, such that the election provider does not know which tracker has been allocated to which voter. This results in a system where even a “dishonest but cautious” election authority running the system cannot be sure of changing the result in an undetectable way, and hence gives stronger guarantees on the integrity of the election than were previously present. We explore the challenges presented by adding a verifiability layer to an operational system. The system was used in two initial trials conducted within real contested elections. We conclude by outlining the further steps in the road-map towards the deployment of a fully trustworthy online voting system.

In today’s world, critical infrastructure is often controlled by computing systems. This introduces new risks for cyber attacks, which can compromise the security and disrupt the functionality of these systems. It is therefore necessary to build such systems with strong guarantees of resiliency against cyber attacks. One way to achieve this level of assurance is using formal verification, which provides proofs of system compliance with desired cyber security properties. The use of Formal Methods (FM) in aspects of cyber security and safety-critical systems are reviewed in this article. We split FM into the three main classes: theorem proving, model checking, and lightweight FM. To allow the different uses of FM to be compared, we define a common set of terms. We further develop categories based on the type of computing system FM are applied in. Solutions in each class and category are presented, discussed, compared, and summarised. We describe historical highlights and developments and present a state-of-the-art review in the area of FM in cyber security. This review is presented from the point of view of FM practitioners and researchers, commenting on the trends in each of the classes and categories. This is achieved by considering all types of FM, several types of security and safety-critical systems, and by structuring the taxonomy accordingly. The article hence provides a comprehensive overview of FM and techniques available to system designers of security-critical systems, simplifying the process of choosing the right tool for the task. The article concludes by summarising the discussion of the review, focusing on best practices, challenges, general future trends, and directions of research within this field.

Users accessing services are often required to provide personal information, for example, age, profession and location, in order to satisfy access polices. This personal information is evident in the application of e-ticketing where discounted access is granted to visitor attractions or transport services if users satisfy policies related to their age or disability or other defined over attributes. We propose a privacy-preserving electronic ticket scheme using attribute-based credentials to protect users' privacy. The benefit of our scheme is that the attributes of a user are certified by a trusted third party so that the scheme can provide assurances to a seller that a user's attributes are valid. The scheme makes the following contributions: (1) users can buy different tickets from ticket sellers without releasing their exact attributes; (2) two tickets of the same user cannot be linked; (3) a ticket cannot be transferred to another user; (4) a ticket cannot be double spent. The novelty of our scheme is to enable users to convince ticket sellers that their attributes satisfy the ticket policies and buy discounted tickets anonymously. This is a step towards identifying an e-ticketing scheme that captures user privacy requirements in transport services. The security of our scheme is proved and reduced to a well-known complexity assumption. The scheme is also implemented and its performance is empirically evaluated.

This paper discusses an approach for incremental change to an online voting system, introducing a verifiability layer based on the Selene protocol to a trusted-third-party-based system, resulting in a fully verifiable and transparent e-voting system. The paper also describes how to use Distributed Ledger Technology as a component of the implementation of Selene to manage the verifiability data in a distributed way for resilience and trust.

Abstract This work presents our approach to formally model the Swiftaid system design, a digital platform that enables donors to automatically add Gift Aid to donations made via card payments. Following principles of Behaviour-Driven Development, we use Gherkin to capture requirements specified in legislation, specifically the UK Charity (Gift Aid Declarations) Regulations 2016. The Gherkin scenarios provide a basis for subsequent formal modelling and analysis using Event-B, Rodin and ProB. Interactive model simulations assist communication between domain experts, software architects and other stakeholders during requirements capture and system design, enabling the emergent system behaviour to be validated. Our approach was employed within the development of the real Swiftaid product, launched by Streeva in February 2019. Our analysis helped conclude that there was not a strong enough business case for one of the features, whichwas shown to provide nominal user convenience at the expense of increased complexity. This work provides a case study in allying formal and agile software development to enable rapid development of robust software.

An anonymous single sign-on (ASSO) scheme allows users to access multiple services anonymously using one credential. We propose a new ASSO scheme, where users can access services anonymously through the use of anonymous credentials and unlinkably through the provision of designated verifiers. Notably, verifiers cannot link a user's service requests even if they collude. The novelty is that when a designated verifier is unavailable, a central authority can authorize new verifiers to authenticate the user on behalf of the original verifier. Furthermore, a central verifier can also be authorized to de-anonymize users and trace their service requests. We formalize the scheme along with a security proof and provide an empirical evaluation of its performance. This scheme can be applied to smart ticketing where minimizing the collection of personal information of users is increasingly important to transport organizations due to privacy regulations such as general data protection regulations (GDPRs).

Direct Anonymous Attestation (DAA) is a cryptographic scheme that provides Trusted Platform Module TPM-backed anonymous credentials. We develop Tamarin modelling of the ECC-based version of the protocol as it is standardised and provide the first mechanised analysis of this standard. Our analysis confirms that the scheme is secure when all TPMs are assumed honest, but reveals a break in the protocol's expected authentication and secrecy properties for all TPMs even if only one is compromised. We propose and formally verify a minimal fix to the standard. In addition to developing the first formal analysis of ECC-DAA, the paper contributes to the growing body of work demonstrating the use of formal tools in supporting standardisation processes for cryptographic protocols.

Abstract In this paper we present a new way of reconciling Event-B refinement with linear temporal logic (LTL) properties. In particular, the results presented in this paper allow properties to be established for abstract system models, and identify conditions to ensure that the properties (suitably translated) continue to hold as those models are developed through refinement. There are several novel elements to this achievement: (1) we identify conditions that allow LTL properties to be mapped across refinement chains; (2) we provide translations of LTL predicates to reflect the introduction through refinement of new events and the renaming and splitting of existing events; (3) we do this for an extended version of LTL particularly suited to Event-B, including state predicates and enabledness of events, which can be model-checked at the abstract level. Our results are more general than any previous work in this area, covering liveness in the context of anticipated events, and relaxing constraints between adjacent refinement levels. The approach is illustrated with a case study. This enables designers to develop event based models and to consider their execution patterns so that liveness and fairness properties can be verified for Event-B systems.

Near Field Communication (NFC) is a Radio Frequency (RF) technology that allows data to be exchanged between devices that are in close proximity. An NFC-based mobile coupon (M-coupon) is a coupon that is retrieved by the user from a source such as a newspaper or a smart poster and redeemed afterwards. The M-coupon is a cryptographically secured electronic message with some value stored on user’s mobile. We develop a formal framework for security analysis of NFC mobile coupons protocols using formal methods ( CasperFDR ). The framework aims to check whether NFC M-coupon protocols address their security requirements. The paper starts with a formal definition of the NFC M-coupon requirements in which can be applied to a variety of protocols. Then, we apply the framework to a quadratic residue -based NFC M-coupon protocol proposed in the literature. The analysis shows an attack against User Authentication property. An additional contribution is that we model the protocol with a challenge of modelling the quadratic residue theorem (QR). We propose two ways of abstracting QR in the model with the pros and cons of both methods. We show how to overcome some limitations of CasperFDR, the protocol analysis tool used, that prevent us from modelling the protocol in a natural way. Moreover, we discuss an interesting observation regarding how found attacks can be affected by a divided long message in CasperFDR.

The Prêt à Voter cryptographic voting system was designed to be flexible and to offer voters a familiar and easy voting experience. In this article, we present our development of the Prêt à Voter design to a practical implementation used in a real state election in November 2014, called vVote. As well as solving practical engineering challenges, we have also had to tailor the system to the idiosyncrasies of elections in the Australian state of Victoria and the requirements of the Victorian Electoral Commission. This article includes general background, user experience, and details of the cryptographic protocols and human processes. We explain the problems, present solutions, then analyze their security properties and explain how they tie in to other design decisions.

The Secure Web Bulletin Board (WBB) is a key component of verifiable election systems. However, there is very little in the literature on their specification, design and implementation, and there are no formally analysed designs. The WBB is used in the context of election verification to publish evidence of voting and tallying that voters and officials can check, and where challenges can be launched in the event of malfeasance. In practice, the election authority has responsibility for implementing the web bulletin board correctly and reliably, and will wish to ensure that it behaves correctly even in the presence of failures and attacks. To ensure robustness, an implementation will typically use a number of peers to be able to provide a correct service even when some peers go down or behave dishonestly. In this paper we propose a new protocol to implement such a Web Bulletin Board, motivated by the needs of the vVote verifiable voting system. Using a distributed algorithm increases the complexity of the protocol and requires careful reasoning in order to establish correctness. Here we use the Event-B modelling and refinement approach to establish correctness of the peered design against an idealised specification of the bulletin board behaviour. In particular we have shown that for n peers, a threshold of t > 2n/3 peers behaving correctly is sufficient to ensure correct behaviour of the bulletin board distributed design. The algorithm also behaves correctly even if honest or dishonest peers temporarily drop out of the protocol and then return. The verification approach also establishes that the protocols used within the bulletin board do not interfere with each other. This is the first time a peered secure web bulletin board suite of protocols has been formally verified.

No abstract available.

Abstract Most security protocols appearing in the literature make use of cryptographic primitives that assume that the participants have access to some sort of computational device. However, there are times when there is need for a security mechanism to evaluate some result without leaking sensitive information, but computational devices are unavailable. We discuss here various protocols for solving cryptographic problems using everyday objects: coins, dice, cards, and envelopes.

Abstract We present formal definitions of anonymity properties for voting protocols using the process algebra CSP. We analyse a number of anonymity definitions, and give formal definitions for strong and weak anonymity, highlighting the difference between these definitions. We show that the strong anonymity definition is too strong for practical purposes; the weak anonymity definition, however, turns out to be ideal for analysing voting systems. Two case studies are presented to demonstrate the usefulness of the formal definitions: a conventional voting system, and Prêt à Voter, a paper-based, voter-verifiable scheme. In each case, we give a CSP model of the system, and analyse it against our anonymity definitions by specification checks using the Failures-Divergences Refinement (FDR2) model checker. We give a detailed discussion on the results from the analysis, emphasizing the assumptions that we made in our model as well as the challenges in modelling electronic voting systems using CSP.

Abstract Event-B provides a flexible framework for stepwise system development via refinement. The framework supports steps for (a) refining events (one-by-one), (b) splitting events (one-by-many), and (c) introducing new events. In each of the steps events can be indicated as convergent (to be made internal) or anticipated (treatment deferred to a later refinement step). All such steps are accompanied with precise proof obligations. However, no behavioural semantics has been provided to validate the proof obligations, and no formal justification has previously been given for the application of these rules in a refinement chain. Behavioural semantics expresses a clear relationship between the first and last machines in a refinement chain. The framework we present provides a coherent justification for Abrial’s approach to refinement in Event-B, and its generalisation to interface extension: adding events to the interface. In this paper, we give a behavioural semantics for Event-B refinement, with a treatment for the first time of splitting events and of anticipated events, adding to the well-understood treatment of convergent events. To this end, we define a CSP semantics for Event-B and show how the different forms of Event-B refinement can be captured as CSP refinement. It turns out that the appropriate CSP refinement relationship is influenced by the particular Event-B development strategy taken. We present two such strategies, one allowing, the other disallowing interface extensions.

Social Networks were created to allow users to maintain circles of friends and acquaintances. Over time, they have come to be used to share data objects such as pictures between friends. There have been several approaches to formalize social networks in order to specify complicated access control policies for such objects. These approaches have involved a combination of existing logic with custom languages, with new operators being introduced when more complex policies needed to be expressed. In this paper we demonstrate that set theoretic notation provides a convenient syntax for specifying a social network and the associated access control policies. We demonstrate that our notation enables us to extend the range of policies that can be articulated. We also demonstrate that our notation is simpler and more concise than existing approaches.

Abstract The design and implementation of critical controllers benefit from development in a formal method such as the B‐Method. However, B does not support direct specification of executions, but this is a requirement in controller design. The aim here is to develop a set of annotations so that they can be used by a B design engineer to capture execution requirements while creating the B model. The annotations, once shown to be consistent with the B machine, can be used independently to assess the correctness of the proposed CSP controllers. CSP||B is an alternative formal method integration that can be used to develop critical controllers with both state and event behaviour. The advantage of using annotations is that the execution requirements can be captured and shown to be consistent with the state during operation development, and that a control loop invariant to establish correctness does not have to be independently developed. Handel‐C is used on route to hardware synthesis as it supports the implementation of concurrency and the manipulation of state. Annotations are again used to guide the translation of the B and control annotations into Handel‐C. This work has three main aims. First, we introduce a set of annotations to describe control directives to permit controller development in B. The annotations capture execution requirements. They give rise to proof obligations that when discharged prove that the annotations are consistent with the machine they are written in, and therefore will not cause the machine to diverge. Second, we prove that CSP controllers that are consistent with the annotations will preserve the non‐divergence property established between the machine and the annotations. Third, we show how annotation refinement is possible, and show a range of mappings from annotated B and consistent controllers to Handel‐C. The development of mappings demonstrates the feasibility of automatic translation of annotated B to Handel‐C. Copyright © 2010 John Wiley & Sons, Ltd.

Abstract In this paper, we present a formal model and analysis of the Advanced Microcontroller Bus Architecture (AMBA) Advanced High‐performance Bus (AHB). The model is given in CSP ∥ B—an integration of the process algebra CSP and the state‐based formalism B. We describe the theory behind the integration of CSP and B, and present the model in this theory. Analysis is performed using the model‐checker ProB. The contribution of this paper may be summarized as follows: presentation of a formal model of the AMBA AHB protocol such that it may be used for analysis of co‐design systems incorporating the bus, an evaluation of the integration of CSP and B in the production of such a model, and a demonstration and evaluation of ProB in performing this analysis. Copyright © 2009 John Wiley & Sons, Ltd.

¿¿¿¿¿¿Pre¿t a¿ Voter provides a practical approach to end-to-end verifiable elections with a simple, familiar voter-experience. It assures a high degree of transparency while preserving secrecy of the ballot. Assurance arises from the auditability of the election itself, rather than the need to place trust in the system components. The original idea has undergone several revisions and enhancements since its inception in 2004, driven by the identification of threats, the availability of improved cryptographic primitives, and the desire to make the scheme as flexible as possible. This paper presents the key elements of the approach and describes the evolution of the design and their suitability in various contexts. We also describe the voter experience, and the security properties that the schemes provide.

Summary form only given. In this paper, we show a combination of the process algebra CSP and the state-based formalism B, combined into a single notation called CSPparB (pronounced CSP parallel B) being used in the formal development of reconfigurable hardware, implemented in Handel-C. The use of CSPparB and associated fools is demonstrated using a significant, realistic application. This paper is the first recorded use of CSPparB in hardware development although it has been previously used for software. The contribution of this paper may be summarised as follows: demonstration of formal CSPparB development, guided by engineering intuition and domain knowledge; evidence that CSPparB forms a feasible technology upon which to build high assurance hardware systems; examples of proof techniques and tool usage for CSPparB in giving these high levels of assurance. Development is top-down and piece-wise: refinement is from an abstract sequential specification info a highly concurrent implementation. Justification of refinement steps employs the use of control loop invariants, which are used to show the consistency of the interaction of the CSP and the B components. In introducing concurrency, additional requirements appear which could be met by software, dedicated hardware components, or by custom hardware on an FPGA. The piece-wise nature of the development allow for this choice to be postponed while other components are implemented - possibly in different technologies. The choice of where concurrency may be introduced in order to meet timing requirements, whilst still attaining reasonable area usage is guided by knowledge of the application domain and the target FPGA platform. Safety and functional properties of the abstract specification are automatically verified; theoretical results concerning refinement guarantee that these hold for the implementation. Proof obligations are discharged using the CSP model-checker FDR and the theorem prover B-Toolkit. The central conclusion of this paper is that CSPparB forms the basis of a valid technology for the exploration and development of high assurance hardware and software systems. Further research is to investigate co-design, understand how a design calculus may be incorporated, and how further automatic tool support may be provided in discharging CLI proofs

Abstract The introduction of probabilistic behaviour into the B-method is a recent development. In addition to allowing probabilistic behaviour to be modelled, the relationship between expected values of the machine state can be expressed and verified. This paper explores the application of probabilistic B to a simple case study: tracking the volume of liquid held in a tank by measuring the flow of liquid into it. The flow can change as time progresses, and sensors are used to measure the flow with some degree of accuracy and reliability, modelled as non-deterministic and probabilistic behaviour respectively. At the specification level, the analysis is concerned with the expectation clause in the probabilistic B machine and its consistency with machine operations. At the refinement level, refinement and equivalence laws on probabilistic GSL are used to establish that a particular design of sensors delivers the required level of reliability.

A number of key establishment protocols claim the property of forward secrecy, where the compromise of a long-term key does not result in the compromise of previously computed session-keys. We describe how such protocols can be modelled using the process algebra CSP and explain why the well-known rank function approach is incapable of proving their correctness. This shortcoming motivates us to propose a generalised proof technique based on the novel concept of a temporal rank function. We apply this approach to two examples: a protocol due to Boyd and the Cliques (A-GDH.2) group key agreement protocol.

Abstract Recent work on combining CSP and B has provided ways of describing systems comprised of components described in both B (to express requirements on state) and CSP (to express interactive and controller behaviour). This approach is driven by the desire to exploit existing tool support for both CSP and B, and by the need for compositional proof techniques. This paper is concerned with the theory underpinning the approach, and proves a number of results for the development and verification of systems described using a combination of CSP and B. In particular, new results are obtained for the use of the hiding operator, which is essential for abstraction. The paper provides theorems which enable results obtained (possibly with tools) on the CSP part of the description to be lifted to the combination. Also, a better understanding of the interaction between CSP controllers and B machines in terms of non-discriminating and open behaviour on channels is introduced, and applied to the deadlock-freedom theorem. The results are illustrated with a toy lift controller running example.

Schneider's work on rank functions [IEEE TSE 24(9) (1998)] provides a formal approach to verification of certain properties of a security protocol. However, he illustrates the approach only with a protocol running on a small network; and no help is given with the somewhat hit-and-miss process of finding the rank function that underpins the central theorem. In this paper, we develop the theory to allow for an arbitrarily large network, and give a clearly defined decision procedure by which one may either construct a rank function, proving correctness of the protocol, or show that no rank function exists. We briefly discuss the implications of the absence of a rank function, and the open question of completeness of the rank function theorem.

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 have appeared in the academic literature. In this paper we prove that type flaw attacks can be prevent ed using a simple technique of tagging each field with some information indicating its intended type.

Various formulations of non-interference have been proposed to try to characterise the absence of information flows in system or network. There is still no consensus in the information security community as to which of these accurately captures our intuition of the notion of secrecy. We argue that non-interference is closely related to the characterisation of process equivalence. What constitutes process equivalence is itself a fundamental question in computer science with several distinct definitions proposed in the literature. We illustrate how several of the definitions of non-interference mirror notions of process equivalence. Casting these security concepts in a process algebraic framework clarifies, for example, the role of non-determinism and allows results to be carried over regarding composition and the completeness of unwinding rules. We also discuss some natural generalisations of the approach.

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 have appeared in the academic literature. In this paper we prove that type flaw attacks can be prevented using a simple technique of tagging each field with some information indicating its intended type.

Schneider's (1998) work on rank functions provides a formal approach to verification of certain properties of a security protocol. However, he illustrates the approach only with a protocol running on a small network; and no help is given with the somewhat hit-and-miss process of finding the rank function which underpins the central theorem. We develop the theory to allow for an arbitrarily large network, and give a clearly defined decision procedure by which one may either construct a rank function, proving correctness of the protocol, or show that no rank function exists. We discuss the implications of the absence of a rank function, and the open question of completeness of the rank function theorem.

Abstract. Restricted views of process behaviour result in a form of abstraction which is useful in the construction of specifications involving fault-tolerance and atomicity. This paper presents an operational characterisation of abstraction for refusable and non-refusable events in terms of testing. This view is a generalisation of standard notions of testing, and is given a new denotational characterisation encapsulated within the CSP denotational semantics. It informs, reinforces and extends the traditional denotational approach to abstraction.

The information security community has long debated the exact definition of the term "security". Even if we focus on the more modest notion of confidentiality the precise definition remains controversial. In their seminal paper, Goguen and Meseguer (1982) took an important step towards a formalisation of the notion of absence of information flow with the concept of non-interference. This too was found to have problems and limitations, particularly when applied to systems displaying non-determinism which led to a proliferation of refinements of this notion and there is still no consensus as to which of these is "correct". We show that this central concept in information security is closely related to a central concept of computer science: that of the equivalence of systems. The notion of non-interference depends ultimately on our notion of process equivalence. However what constitutes the equivalence of two processes is itself a deep and controversial question in computer science with a number of distinct definitions proposed in the literature. We illustrate how several of the leading candidates for a definition of non-interference mirror notions of system equivalence. Casting these security concepts in a process algebraic framework clarifies the relationship between them and allows many results to be carried over regarding, for example, composition and unwinding. We also outline some generalisations of non-interference to handle partial and conditional information flows.

The paper applies the theory of communicating sequential processes (CSP) to the modelling and analysis of a non-repudiation protocol. Non-repudiation protocols differ from authentication and key-exchange protocols in that the participants require protection from each other, rather than from an external hostile agent. This means that the kinds of properties that are required of such a protocol, and the way it needs to be modelled to enable analysis, are different to the standard approaches taken to the more widely studied class of protocols and properties. A non-repudiation protocol proposed by Zhou and Gollmann (1996) is analysed within this framework, and this highlights some novel considerations that are required for this kind of protocol.

This paper presents a general approach for analysis and verification of authentication properties using the theory of Communicating Sequential Processes (CSP). The paper aims to develop a specific theory appropriate to the analysis of authentication protocols, built on top of the general CSP semantic framework. This approach aims to combine the ability to express such protocols in a natural and precise way with the ability to reason formally about the properties they exhibit. The theory is illustrated by an examination of the Needham-Schroeder (1978) public key protocol. The protocol is first examined with respect to a single run and then more generally with respect to multiple concurrent runs.

The paper presents a general approach for analysis and verification of authentication properties in the language of communicating sequential processes (CSP). It is illustrated by an examination of the Needham-Schroeder public key protocol (R. Needham and M. Schroeder, 1978). The contribution of the article is to develop a specific theory appropriate to the analysis of authentication protocols, built on top of the general CSP semantic framework. This approach aims to combine the ability to express such protocols in a natural and precise way with the facility to reason formally about the properties they exhibit.

Security properties such as confidentiality and authenticity may be considered in terms of the flow of messages within a network. To the extent that this characterisation is justified, the use of a process algebra such as Communicating Sequential Processes (CSP) seems appropriate to describe and analyse them. This paper explores ways in which security properties may be described as CSP specifications, how security mechanisms may be captured, and how particular protocols designed to provide these properties may be analysed within the CSP framework. The paper is concerned with the theoretical basis for such analysis. A sketch verification of a simple example is carried out as an illustration.

Abstract The theory of timed Communicating Sequential Processes is a mathematical approach to the design and analysis of timed distributed systems. This paper extends the language of timed CSP to include a general treatment of recursion. A semantics for mutual recursion is introduced, together with a sufficient condition for the necessary fixpoint to be unique. The resulting language has the familiar unwinding property of process algebra, and exhibits a number of useful algebraic identities. A theory of recursion induction is formulated, and a simple example is presented to illustrate its use.