BRICS

Basic Research in Computer Science

Logics for The Applied π Calculus

Michael David Pedersen BRICS Report Series RS-06-19 ISSN 0909-0878 December 2006 BRICS RS-06-19 M. D. Pedersen: Logics for The Applied π Calculus Copyright \begin{matrix}c \\ ◯ \end{matrix} 2006, Michael David Pedersen.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus IT-parken, Aabogade 34 DK–8200 Aarhus N Denmark

Telephone: +45 8942 9300
Telefax: +45 8942 5601
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/06/19/

Logics for The Applied π Calculus

♢

Master’s thesis

Michael David Pedersen

June 12, 2006

(Revised August 7, 2006)

♢

Aalborg University

Department of Computer Science · Fredrik Bajers Vej 7E DK-9210 Aalborg Ø

Preface

This BRICS report was originally a master’s thesis documenting work in the specialisation year at the Department of Computer Science, Aalborg University, and is based on a project proposal by Hans Hüttel. The thesis strengthens and goes beyond the work presented in the DAT5 project entitled A Logic of Frames in the Applied π Calculus.

Familiarity with process calculi (e.g. CCS, the π calculus and associated modal logics) corresponding to the level given in the DAT4 course Semantics and Verification and the DAT6 course Semantics and Verification 2 is assumed. Mathematics skills corresponding to bachelor level computer science, including an understanding of basic set theory, equivalence relations, definition and proof by induction, will be of advantage.

Michael David Pedersen, December 18, 2006.

Summary

The Applied π calculus by Abadi and Fournet is a uniform and generic extension of the π calculus for which particular primitives such as tuples and cryptographic functions can be defined and used on a per-application basis. This is in contrast to the basic π calculus in which the only type of messages that can be communicated are atomic names. The key idea in Applied π is to integrate arbitrary terms into the calculus and its semantics based on a function signature, and to base equality between terms on an equational theory instead of syntactic equality on names.

Processes in Applied π also differ from standard π calculus processes by integrating the notion of active substitutions in the process expression itself. An active substitution is a binding of a term to a variable which intuitively represents a message sent by a process. The frame of a process can then be thought of as the substitution arising by combining all active substitutions embedded in the process expression, and is hence a representation of environment knowledge. Indistinguishability of two frames can be expressed in terms of a binary relation, ≈_{s}, called static equivalence. Roughly speaking, two frames are statically equivalent if an environment cannot distinguish the frames by testing for equality between any pair of terms constructed from variables in the frames.

Frames and static equivalence play a central role in labelled bisimilarity (which coincides with observational equivalence) of processes in Applied π: two processes are bisimilar if they can simulate each others actions and if their frames are statically equivalent, i.e. if the processes can be distinguished neither on their dynamic behaviour nor on their static characteristics.

The main objective of this report is a logic for the Applied π calculus which characterises labelled bisimilarity. The motivation is similar to that of Applied π itself, namely generality: the logic can be adapted to a particular application simply by defining a suitable function signature and equational theory. Since labelled bisimilarity contains a condition on static equivalence on frames, the first step towards a logic for Applied π is a logic for frames which characterises static equivalence. A logic for frames in turn relies on a definition of static equivalence which does not contain a universal quantification over arbitrary terms.

The first major contribution of this report is an strong version of static equivalence, ≈_{ss}, in which frames may be distinguished by testing on reduction of terms in addition to equality. Strong static equivalence is particularly useful because a refined definition, ≈′_{ss}, can be given which does not depend on universal quantification over arbitrary terms. The refined definition is based on the notion of ecores – an extension and generalisation of the cores used by Boreale et al. in the Spi calculus – which intuitively are the minimal terms deducible from a frame which are relevant for deciding static equivalence. We then show that ≈_{ss} and ≈′_{ss} coincide under certain general conditions (namely in independent convergent subterm theories). The refined definition is used as a basis for a logic of frames and to show that this logic characterises strong static equivalence. A further refinement, ≈′′_{ss}, which is also shown to be equivalent to ≈_{ss}, is given and used as a basis for characteristic formulae in the logic for frames. Finally we show that strong static equivalence coincides with the standard static equivalence (≈_{s}) under certain conditions. These conditions are for example satisfied by theories of symmetric key encryption and by theories of public key encryption if public keys are assumed to always be known.

The second major contribution of this report is a first order logic for frames, LF, which characterises strong static equivalence and which is amenable to construction of characteristic formulae. LF includes atomic propositions which facilitate direct reasoning about the terms in a frame. The logic also includes first order quantification, intuitively over the set of terms which can be deduced from the frame by an environment, hence facilitating indirect reasoning about environment knowledge.

The third and final major contribution of this report is a modal logic, LA, for Applied π which characterises labelled bisimilarity on processes. LA is obtained by adding suitable Hennessy-Milner style modalities to LF. Consequently the logic can be used to reason both about the dynamic behaviour and static characteristics of processes. Finally, we demonstrate how LA can be applied to capture a well known attack on the Needham-Schroeder Public Key Protocol.

Resumé

Anvendt π-kalkylen af Abadi and Fournet er en ensartet og generel udvidelse af π-kalkylen, hvor primitiver såsom lister og kryptografiske funktioner kan defineres alt efter den ønskede anvendelse af kalkylen. Dette er i modsætning til π-kalkylen, hvor det kun er muligt at kommunikere atomare navne. Idéen i Anvendt π er at integrere vilkårlige termer i kalkylen og dennes semantik baseret på en funktionssignatur, og basere lighed mellem termer på en ligningsteori i stedet for syntaktisk lighed mellem navne.

Processer i Anvendt π afviger også fra almindelige π-kalkyleprocesser ved at integrere begrebet aktive substitutioner i selve syntaksen for processer. En aktiv substitution er en binding af en term til en variabel, som intuitivt set repræsenterer en besked sendt af processen. Rammen af en proces kan da betragtes som den substitution man opnår ved at samle alle aktive substitutioner fra processen, og er dermed en repræsentation af omgivelsernes viden. Observerbar lighed på to rammer kan udtrykkes i en binær relation kaldet statisk ækvivalens. Groft set er to rammer statisk ækvivalente, hvis de ikke kan skelnes af omgivelserne ved at teste lighed mellem vilkårlige par af termer konstrueret fra variabler i rammerne.

Rammer og statisk ækvivalens spiller en vigtig rolle i mærket bisimulering mellem processer i Anvendt π (som også sammenfalder med observerbar lighed mellem processer): To processer er bisimuleringsækvivalente, hvis de kan simulere hinandens handlinger, og deres rammer er statisk ækvivalente, dvs. hvis processerne hverken kan skelnes på deres dynamiske adfærd eller statiske egenskaber.

Det primære mål med denne rapport er en logic for Anvendt π som karakteriserer mærket bisimulering. Motivationen er, tilsvarende Anvendt π, generalitet: Logikken kan tilpasses bestemte anvendelsesområder ved simpelthen at definere en passende funktionssignatur og ligningsteori. Eftersom mærket bisimulering indeholder en betingelse om statisk ækvivalens af rammer, er det første skridt mod en logik for Anvendt π en logik for rammer, som karakteriserer statisk ækvivalens. En logic for rammer må endvidere bero på en definition af statisk ækvivalens som ikke indeholder universel kvantificering over vilkårlige termer.

Det første væsentlige bidrag i denne rapport er en stærk udgave af statisk ækvivalens, ≈_{ss}, hvor rammer kan skelnes på test a mulige termreduktioner såvel som på lighed mellem termer. Stærk statisk ækvivalens er specielt brugbar, fordi en forfinet definition, ≈′_{ss}, kan udledes, som ikke beror på universel kvantificering over vilkårlige termer. Den forfinede definition er baseret på ecores – en udvidelse og generalisering af cores som anvendt af Boreale et al. på Spi-kalkylen – som intuitivt set er de minimale termer, der kan udledes fra en ramme, og som spiller en rolle i statisk ækvivalens. Vi viser at ≈_{ss} og ≈′_{ss} sammenfalder under bestemte generelle antagelser (nemlig i uafhængige konvergerende undertermsteorier). Den forfinede definition bruges som grundlag for en rammelogik og til at vise, at denne logic karakteriserer stærk statisk ækvivalens. En yderligere forfining, ≈′′_{ss}, som vi også viser sammenfalder med ≈_{ss}, bliver brugt som grundlag for at udlede karakteristiske formler i rammelogikken. Endelig viser vi at stærk statisk ækvivalens sammenfalder med standardudgaven (≈_{s}) under bestemte betingelser. Disse betingelser er for eksempel opfyldt af teorier med symmetrisk kryptering, og af teorier med offentlig-nøglekryptering hvor offentlige nøgler altid er kendt af alle parter.

Det andet væsentlige bidrag i denne rapport er en førsteordens rammelogic, LF, som karakteriseser stærk statisk ækvivalens, og som giver anledning til konstruktion af karakteristiske formler. LF indeholder atomare udsagn, der muliggør direkte ræsonnementer om termerne i en ramme. Logikken indeholder også førsteordens kvantificering, intuitivt set over mængden af termer, som omgivelserne kan udlede fra en ramme, hvilket muliggør indirekte ræsonnementer om omgivelsernes viden.

Det tredje og sidste væsentlige bidrag i denne rapport er en modallogik, LA, for Anvendt π som karakteriserer mærket bisimulering mellem processer. LA er en udvidelse af LF med passende Hennessy-Milner-modaliteter. Dermed opnås en logic, som kan ræsonnere om den dynamiske adfærd, såvel som de statiske egenskaber, af processer. Endelig demonstrerer vi, hvordan LA kan anvendes til at udtrykke et velkendt angreb på Needham-Schroeder Public Key protokollen.

Contents

1 Introduction 1 1.1 Brief History . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.2 The Applied π Calculus . . . . . . . . . . . . . . . . . . . . . . . 2 1.3 Static Equivalence . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.4 Process Logics . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.5 Objectives and Contributions . . . . . . . . . . . . . . . . . . . . 4 1.6 Outline of the Report . . . . . . . . . . . . . . . . . . . . . . . . 6

2 Preliminaries 7 2.1 Syntax of Applied π . . . . . . . . . . . . . . . . . . . . . . . . . 7 2.2 Semantics of Applied π . . . . . . . . . . . . . . . . . . . . . . . . 10 2.3 Equivalences in Applied π . . . . . . . . . . . . . . . . . . . . . . 18 2.4 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23

3 A Refined Definition of Strong Static Equivalence 25 3.1 Previous Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 3.2 Initial Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 3.3 The Refined Definition . . . . . . . . . . . . . . . . . . . . . . . . 37 3.4 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 3.5 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42

4 Results On The Refined Definition 45 4.1 ≈′_{ss} implies ≈_{ss} . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 4.2 ≈_{ss} implies ≈′_{ss} . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 4.3 Conditions under which ≈_{s} and ≈_{ss} Coincide . . . . . . . . . . . 56 4.4 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62

5 A Logic for Frames 63 5.1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63 5.2 Syntax and Semantics . . . . . . . . . . . . . . . . . . . . . . . . 67 5.3 Characterisation . . . . . . . . . . . . . . . . . . . . . . . . . . . 69 5.4 Characteristic Formulae . . . . . . . . . . . . . . . . . . . . . . . 73 5.5 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82

\underline{CONTENTS}

6 A Logic for Applied π 83 6.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83 6.2 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84 6.3 Match and Matching Input Modality . . . . . . . . . . . . . . . . 85 6.4 Characterisation . . . . . . . . . . . . . . . . . . . . . . . . . . . 88 6.5 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91

7 An Application to the Needham-Schroeder Public Key Protocol 93 7.1 The Needham-Schroeder Public Key Protocol . . . . . . . . . . . 93 7.2 The Specification . . . . . . . . . . . . . . . . . . . . . . . . . . . 95 7.3 Logical Properties . . . . . . . . . . . . . . . . . . . . . . . . . . 100 7.4 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104

8 Conclusion 105 8.1 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105 8.2 Future Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 106

Chapter 1

Introduction

As computer and software systems play increasingly important roles in society, they are also trusted with more and more safety-critical tasks. Classical examples include monitoring of nuclear reactors and automated metro trains which operate without drivers. Clearly the correct operation of such software systems is of utmost importance. Correctness and security is also a concern in the financial world where transactions are performed online, and in everyday email-communication where sensitive data may be transmitted over the Internet. Hence there is an increasing interest in formal methods for modelling software systems and verifying that they work as intended.

Recent years have seen the advent of ubiquitous computing: the integration of small and unobtrusive computing devices into our environment and every day life. For example modern cars have embedded computers which monitor and report on various functions, wrist clocks may contain computers with calendars notifying of scheduled events, and tiny computers with environmental sensors (“motes”) can be deployed to form wireless networks which monitor e.g. seismic activity. This raises enormous scientific challenges in ensuring that complex ubiquitous computer networks function correctly and safely. Indeed, “Science for Global Ubiquitous Computing” is the title of one of the seven Grand Challenges for Computer Research [16] proposed for the upcoming decades.

1.1 Brief History

CHAPTER 1. INTRODUCTION

Process calculi form the basis of a large range of formal methods, and was founded by Robin Milner in his 1980 publication on the Calculus of Communicating Systems (CCS) [21]. CCS enables software systems and communication protocols to be modelled abstractly as processes which can synchronise on channel names and which can then be reasoned about in the calculus. This later developed into the π calculus [22] with the novelty of allowing private channel names (i.e. with restricted scope) and allowing communication of channel names themselves (based on the notion of scope extension), resulting in a vast increase of expressive power. It then became possible to model concepts such as access control and mobility.

The π calculus has sparked a large body of further research resulting in a number of extensions to the calculus, e.g. the Polyadic π calculus [25, Section 3.3] which allows communication of tuples of names instead of just singleton names. Another such extension is Abadi and Gordon’s Spi calculus [5] which adds cryptographic primitives, thus enabling reasoning about cryptographic protocols.

1.2 The Applied π Calculus

In a 2001 publication [4], Abadi and Fournet presented the Applied π calculus, a uniform and generic extension of the π calculus for which particular primitives such as tuples and cryptographic functions can be defined and used on a per-application basis. This is in contrast to the basic π calculus in which the only type of messages that can be communicated are atomic names. The key idea in Applied π is to integrate arbitrary terms into the calculus and its semantics based on a function signature, and to base equality between terms on an equational theory.

The function signature specifies the set of function symbols which can be used to iteratively form terms over names, and the equational theory, =_{E}, is an equivalence relation which defines when two terms are equal. As an example, the signature may contain two binary function symbols enc and dec which can be used for symmetric encryption and decryption, respectively. This signature gives rise to terms on the form enc(b, k^{+}), which intuitively represents the name b encrypted with the public key k^{+}. The associated equational theory should define the relationship between encryption and decryption, in which case the equality dec(enc(b, k^{+}), k^{−}) =_{E} b would hold (where k^{−} is the corresponding private key of k^{+}).

Processes in Applied π also differ from standard π calculus processes by integrating the notion of active substitutions, which intuitively capture the history of messages sent by a process in the process expression itself. Take as an example the following Applied π process:

P = (νk)\overline{a}⟨enc(b, k^{+})⟩.\overline{a}⟨k^{−}⟩.P′

Here the name k is fresh, indicating that it is a the seed for a public-private key pair unknown to the environment. P performs two outputs on channel a: first the name b encrypted with public key k^{+}, and then the corresponding private key k^{−}. The semantics of Applied π prescribes that P reduces to the process

(νk)({^{enc(b,k^{+})}/_{x_{1}}}|{^{k^{−}}/_{x_{2}}}|P′)

The sub-processes {^{enc(b,k^{+})}/_{x_{1}}} and {^{k^{−}}/_{x_{2}}} are active substitutions which represent the messages sent by P, and hence the information made available to the environment. Informally, the frame φ(P) of the process P can then be thought 1.3. STATIC EQUIVALENCE

of as the substitution arising by combining all active substitutions embedded in the process while preserving the restriction on k:

φ(P) = (νk){^{enc(b,k^{+})}/_{x_{1}}, ^{k^{−}}/_{x_{2}}}

In this way φ(P) is a representation of the terms known by the environment as a result of intercepting P ’s output activities on unsecured communication channels.

Applied π can be used to model protocols by defining a signature and equational theory appropriate to a given protocol. An example of existing work to this end is [1] in which Abadi et al. reason about guessing attacks. Furthermore, automated analysis of models can be carried using Blanchet’s tool ProVerif [8]. ProVerif has been employed by Kremer and Ryan in [19] to analyse security protocol models in Applied π for known-pair and chosen-text attacks (relying on weaknesses in block chaining modes), and in [18] to analyse an electronic voting protocol.

1.3 Static Equivalence

Indistinguishability of two frames can be expressed in terms of a binary relation called static equivalence. Intuitively two frames are statically equivalent if an environment cannot distinguish the frames by testing for equality between any pair of terms which are based on the frames. Take as an example the following frames:

φ_{1} = (νk, b){^{enc(b,k^{+})}/_{x_{1}}, ^{k^{−}}/_{x_{2}}, ^{b}/_{x_{3}}}
φ_{2} = (νk, b){^{enc(enc(b,b^{+}),k^{+})}/_{x_{1}}, ^{k^{−}}/_{x_{2}}, ^{enc(b,b^{+})}/_{x_{3}}}
φ_{3} = (νk, b){^{enc(enc(b,k^{+}),k^{+})}/_{x_{1}}, ^{k^{−}}/_{x_{2}}, ^{b}/_{x_{3}}}

Then φ_{1} and φ_{2} are statically equivalent; the intuition is that the equality dec(x_{1}, x_{2}) =_{E} x_{3} holds in both frames – because dec(enc(b, k^{+}), k^{−}) =_{E} b and dec(enc(enc(b, b^{+}), k^{+}), k^{−}) =_{E} enc(b, b^{+}) – and any other equality over terms built from variables and non-bound names which holds in one frame also holds in the other. In particular, the private key b^{−} is now known in φ_{2} and therefore the environment cannot decrypt x_{1} twice and use the result to distinguish the two frames. On the other hand, the frames φ_{1} and φ_{3} are not statically equivalent, because the equality dec(dec(x_{1}, x_{2}), x_{2}) =_{E} x_{3} holds in φ_{3} but not in φ_{1} (nor in φ_{2}).

The claim that φ_{1} and φ_{2} are statically equivalent is a bold one, because we may have overlooked some equality which holds in one frame but not in the other. In fact one may question whether static equivalence is even decidable. The answer is positive for certain equational theories and negative for others; these issues has been investigated by Abadi and Cortier in [2, 3] and by Borgström in [10]. The notions of frames and static equivalence also feature in the work by Boreale et al.[9] in which proof techniques for the Spi calculus are developed, although frames are not an explicit part of the process syntax in the Spi calculus. We shall return to this work in Chapter 3.

Static equivalence is interesting in its own right as a formal definition of indistinguishability of environment knowledge, but it also a useful notion for defining bisimilarity. Roughly speaking, two processes are bisimilar if they can simulate each other’s actions and if their frames are statically equivalent; i.e. if the processes can be distinguished neither on their dynamic behaviour nor on their static characteristics.

1.4 Process Logics

Verification of a software system using a process calculus typically involves three steps. First, an abstract model of the software system is expressed as a model process P_{m} which captures the essential behaviour of the system. Second, the idealised behaviour, which the system designer expects the system to exhibit, is expressed as the specification process P_{s}. Third, it is shown that P_{m} and P_{s} are equivalent according to a suitable notion of bisimulation equivalence.

An alternative, or complementary, way of verifying software systems is to model the system in a process calculi and then express correctness properties as formulae of a modal logic for the relevant process calculi, e.g. the Hennessy-Milner Logic (HML) for CCS [15] and for the π calculus [23], or the Spi calculus logic in [13]. Here the modalities are used to reason about possible or necessary actions. Another classical example is the BAN logic [11] which has been widely used for verification of authentication protocols, and here the modality is on belief (although this logic is not based explicitly on a process calculus). Generally, a process logic has the advantage that correctness properties may be expressed more directly and clearly as a formula than as a specification process, and a logical approach provides a different perspective on the verification problem.

A common result for process logics is that they characterise a suitable notion of bisimulation equivalence between processes, i.e. that that two processes are equivalent exactly if they satisfy the same set of formulae. Hence if a specification process satisfies some correctness property and the model process does not, then the model and specification are not bisimilar.

1.5 Objectives and Contributions

The main objective of the work documented in this report is a logic for the Applied π calculus. This logic would have the same appeal as the Applied π calculus itself has in the first place, namely generality, in that a logic for Applied π may capture other logics (such as the Spi logics) as a special case. We design the logic for Applied π in three stages, each of which provide a significant contribution to the theoretical development of Applied π.

The first contribution of this report is a stronger definition of static equivalence (henceforth referred to as strong static equivalence) in which frames may 1.5. OBJECTIVES AND CONTRIBUTIONS

be distinguished by testing on reduction of terms in addition to equality. We argue that strong static equivalence is meaningful in applications; for example, in contrast to the standard definition, strong static equivalence distinguishes the following two frames:

φ =^{Δ} (νa, c, k){^{enc(a,k^{+})}/_{x_{1}}, ^{k^{−}}/_{x_{2}}}

φ′ =^{Δ} (νa, c, k){^{enc(a,k^{+})}/_{x_{1}}, ^{c^{−}}/_{x_{2}}}

Here we have that dec(x_{1}, x_{2}) is reducible in the first frame but not in the second. There is no distinguishing equality, so the frames are statically equivalent according to the standard definition. However we also show that there are theories in which strong static equivalence coincides with the standard static equivalence; these include theories with symmetric key encryption and theories with public key encryption in which public keys are always known.

In addition to being meaningful in applications, strong static equivalence is useful because a refined definition can be given (inspired by the notion of cores in [9]) which does not rely on universal quantification over arbitrary terms and which places explicit conditions on certain syntactic equalities and reductions.

This leads us to the second contribution of this report, namely a first order logic for frames in Applied π which characterises strong static equivalence. The logic is designed based on the refined definition of strong static equivalence, which also gives a direct approach to construction of characteristic formulae for frames (a characteristic formula for frame φ is a finite formula which is satisfied by exactly those frames that are strong statically equivalent to φ). Characteristic formulae can be useful in theoretical developments but they also demonstrate that the logic is highly expressive, since a single formulae can capture all the essential properties (with respect to strong static equivalence) of a frame. Indeed the strong version of static equivalence is devised exactly with characteristic formulae in mind.

The logic of frames includes atomic propositions for asserting equality, reduction and syntactic equality between terms, and also includes first order quantification, intuitively over the set of terms which can be deduced from the frame by an environment. Hence a formula may be given to assert that e.g. there exists a term y (known by the environment) such that x_{1} can be decrypted with y to obtain x_{2}

The third and final contribution of this report is a modal logic for Applied π which characterises a bisimulation equivalence on processes. This logic is obtained by adding suitable Hennessy-Milner style modalities to the logic of frames, allowing assertions such as process P can perform an input of an encrypted term M_{1} followed by some output, after which the decryption key for the term M_{1} is known by the environment

1.6 Outline of the Report

The report is structured as follows. In Chapter 2 we introduce the Applied π calculus in greater detail along with other necessary preliminaries, including a high-level definition of strong static equivalence. Chapter 3 gives a refined definition of strong static equivalence which is a necessary basis for characteristic formulae, and Chapter 4 gives a proof that the refined definition coincides with the standard definition under certain conditions. Chapter 5 presents a firstoder logic for frames after the discussing underlying considerations, and shows that the logic characterises static equivalence under certain conditions. The chapter ends with a construction of characteristic formulae. In Chapter 6 the logic of frames is extended to a logic for Applied π and it is shown that the logic characterises bisimilarity. An application of the logic to the analysis of the Needham-Schroeder Public Key Protocol is then given in Chapter 7. The report is concluded in Chapter 8 along with pointers to future work.

Preliminaries

In this chapter we introduce the Applied π calculus based on [4]. Section 1 presents the syntax with emphasis on how arbitrary terms are represented in the calculus. Section 2 presents the semantics with emphasis on equality between terms and the underlying notion of term rewrite systems. Section 3 presents some important equivalence relations, including two notions of static equivalence which will feature extensively throughout the report.

2.1 Syntax of Applied π

One of the novelties of Applied π over the Pi calculus is that arbitrary terms can be passed over channels and tested for equality. We thus start by defining terms, and then proceed to define the syntax of two kinds of processes which feature in the calculus.

2.1.1 Terms

We define terms following the treatment in [7, Section 3.1]. Terms are constructed by applying function symbols to names, and the available function symbols may vary on a per application basis. The signature Σ is a set of available functions symbols where each f ∈ Σ is associated with a natural number k, which is the arity of f. Functions of arity 0 are called constant symbols. We denote the set of function symbols in Σ with arity k by Σ^{(k)}.

Let N be the set of names, ranged over by a, b, c, …, k, let X be the set of variables, ranged over by x, y, z and let U be the set N ∪ X, ranged over by u. Then the set of terms in the signature, T (Σ, U), is defined inductively as follows

• U ⊆ T (Σ, U)

• for all k ≥ 0:

f(M_{1}, …, M_{k}) ∈ T (Σ, U) if f ∈ Σ^{(k)} and M_{1}, …, M_{k} ∈ T (Σ, U)

CHAPTER 2. PRELIMINARIES

The set of names, respectively variables, occurring in a term M ∈ T (Σ, U) will be denoted by n(M), respectively v(M), and we will use the abbreviation n(M_{1}, M_{2}) to denote n(M_{1}) ∪ n(M_{2}).

Often we will be interested in identifying substrings at certain positions of a term M ∈ T (Σ, U). The set of positions in M, pos(M), is a set of strings over the alphabet of positive integers and is defined inductively as

• If M ∈ U, then pos(M) =^{Δ} {ϵ} where ϵ denotes the empty string.

• If M = f(M_{1}, …, M_{k}) for some f ∈ Σ^{(k)} then

pos(M) =^{Δ} {ϵ} ∪ ⋃_{i=1}^{k}{iw | w ∈ pos(M_{i})}

We say that a position w′ is a prefix of a position w if there exists w′′ such that w = w′w′′. The subterm of M at position w is denoted by M|_{w} and is defined inductively on the length of w as follows:

M|_{ϵ} =^{Δ} M
f(M_{1}, …, M_{k})|_{iw} =^{Δ} M_{i}|_{w}

Finally, we define the set of subterms of M as

st(M) =^{Δ} {M|_{w} | w ∈ pos(M)}

2.1.2 Plain Processes

We now proceed to the syntax of processes in the Applied π calculus. A process can either be a plain processes or an extended processes. Plain processes are similar to processes in the Pi calculus except that arbitrary terms may be sent along channels:

A, B, C ::= 0 | A|B |!A | (νn)A | if M_{1} = M_{2} then A else B | u(x).A | \overline{u}⟨M⟩.A

The set of plain processes is denoted by A. The informal meaning of each process construct is explained briefly below.

1. 0 is the null process which cannot do anything.

2. A|B is parallel composition in which A and B execute concurrently.

3. !A is replication, the intuition being that an unlimited number of copies of A are executed in parallel.

4. (νn)A is name restriction, meaning that the name n is private, or “fresh”, in A, and thus can only be used in A.

2.1. SYNTAX OF APPLIED π

5. if M_{1} = M_{2} then A else B is a process which behaves as A if M_{1} = M_{2} and as B otherwise. The equality is more general than syntactic equality, which will be clear when the semantics is presented in the next section.

6. u(x).A is message input. A term M can be input on the channel u and bound to the variable x, whereafter the process behaves as A with x substituted for M.

7. \overline{u}⟨M⟩.A is message output. A term M is output on the channel u, where after the process continues as A.

2.1.3 Extended Processes

Extended processes are plain processes extended with the notion of active substitutions, which play an essential role in Applied π. In general, a substitution is a total function σ : X → T (Σ, U) which maps variables to terms [7, Section 3.1]. Following standard conventions, we shall use xσ to denote the substitution σ applied to x and we let dom(σ) and im(σ) denote the domain and the image of σ, respectively. We define the extended substitution σ{^{M}/_{y}} as

xσ\{^{M}/_{y}\} = \begin{cases}M & if y = x \\ xσ & if y ≠ x \end{cases}

The extension σσ_{2} is obtained by iteratively extending σ with each element of σ_{2} in the obvious way.

We write ∅ for the substitution σ with dom(σ) = ∅ and we shall generally use the notation {^{M_{1}}/_{x_{1}}, …, ^{M_{k}}/_{x_{k}}} to define the substitution σ where σ(x_{i}) = M_{i} (for 1 ≤ i ≤ k) and σ(y) = y for all y ∈ X − {x_{1}, …, x_{k}}. When the number of variables in the substitution is insignificant we shall use the notation {^{M_{i}}/_{x_{i}}}_{i∈I} where I denotes some sequence, and in general we shall use the notation (x)_{i∈I} to denote the sequence (x_{1}, …, x_{k}) for some k. A substitution can be extended to a mapping σ̂ : T (Σ, U) → T (Σ, U) where σ̂(M) is the term resulting from replacing all x ∈ v(M) with xσ. A similar extension can be made to processes, giving a substitution ˆ σ̂ : P → P where ˆ σ̂(P) is the process resulting by replacing each term M in P for σ̂(M). In the following we shall use substitutions and their extensions interchangeably. We shall also assume that any substitution σ is cycle-free in the sense that none of the variables in the domain of σ occur in terms in the image of σ.

A grammar for extended processes can now be given:

P, Q, R ::= A | P |Q | (νn)P | (νv)P | {^{M}/_{x}}

The set of extended processes is denoted by P; note that A ⊂ P. Considered as a process, the active substitution {^{M}/_{x}} may “attack” any other process it is put in parallel with and apply the substitution to this process. Hence the parallel composition {^{M}/_{x}}|P is intuitively equivalent to the process P {^{M}/_{x}}.

Processes can be protected against substitution by using variable restriction, so e.g. the substitution {^{M}/_{x}} will have no effect on the process (νx)P.

Note that active substitutions in general cannot be under input/output guards, cannot be part of a conditional, and cannot be replicated. Several active substitutions can be put in parallel, in which case we write {^{M_{1}}/_{x_{1}}}| … |{^{M_{k}}/_{x_{k}}} = {^{M_{1}}/_{x_{1}}, …, ^{M_{k}}/_{x_{k}}}. When multiple names are under restriction, we shall write (νn_{1}, …, n_{k})P instead of (νn_{1}), …, (νn_{1})P, and we shall write (νñ)P when the particular names under restriction are unimportant.

The set of free names, fn(P), of an extended process is defined as follows:

fn(0) = ∅
fn(P |Q) = fn(P) ∪ fn(Q)
fn(!P) = fn(P)
fn((νn)P) = fn(P) − {n}
fn(if M_{1} = M_{2} then P else Q) = n(M_{1}) ∪ n(M_{2}) ∪ fn(P) ∪ fn(Q)
fn(a(x).P) = {a} ∪ fn(P)
fn(\overline{a}⟨M⟩.P) = \{a\} ∪ n(M) ∪ fn(P)
fn({^{M}/_{x}}) = n(M)

The set of bound names, bn(P), of an extended process is defined as follows:

bn(0) = ∅
bn(P |Q) = bn(P) ∪ bn(Q)
bn(!P) = bn(P)
bn((νn)P) = bn(P) ∪ {n}
bn(if M_{1} = M_{2} then P else Q) = bn(P) ∪ bn(Q)
bn(a(x).P) = bn(P)
bn(\overline{a}⟨M⟩.P) = bn(P)
bn({^{M}/_{x}}) = ∅

The free variables fv(P) and the bound variables bv(P) are defined similarly. The set of names of an extended process is defined as n(P) = fn(P) ∪ bn(P).

In this report we shall mainly be interested in extended processes, so henceforth we refer to these simply as processes.

2.2 Semantics of Applied π

2.2. SEMANTICS OF APPLIED π

Having defined the syntax in the previous section, we now proceed by giving meaning to the syntactical constructs in Applied π. We start by considering how equality between terms can be defined on a per application basis, which relies on the notion of an equational theory. We then define structural equivalence, which is the foundation of the reduction relation and the labelled operational semantics which are subsequently introduced.

2.2.1 Rewrite Systems and The Equational Theory

Test on equality between terms is a central feature of the conditional process construct. In order to define the semantics for conditionals, a definition of equality must therefore be given. This in turn relies on the notion of term rewrite systems (TRS) to which we now give a brief introduction, following the treatment in [7].

Term rewrite systems are used to specify how terms can be evaluated step by step. First, a rewrite rule r is on the form L >_{r} R where L, R ∈ T (Σ, X) and v(R) ⊆ v(L). L will be referred to as the left hand side (LHS) or the redex, and R as the right hand side (RHS) or the reduct. The function symbol occurring as the outermost function symbol of the redex will be referred to as the destructor function.

A term rewrite system R is then a set of rewrite rules. We say that a term M_{1} is less general than, or an instance of, a term M_{2} if there exists a unifying substitution θ such that M_{1} = M_{2}θ. A term M_{1} reduces primitively to M_{2} using some rule L >_{r} R, written M_{1} >_{r} M_{2}, if M_{1} = Lθ and M_{2} = Rθ for some substitution θ. More generally though, we are interested in the rewrite relation > induced by the rewrite system. We then define M_{1} > M_{2} if and only if some subterm M_{1}|_{w} is an instance of L with some unifying substitution θ and M_{2} = M_{1}{^{Rθ}/_{M_{1}|_{w}}}, and we say that M_{1} rewrites (or reduces) to M_{2}.

Example 2.2.1. Consider a rewrite system R over the signature Σ consisting of a binary function symbol for pair construction, [·, ·], and the unary function symbols fst(·) and snd(·) for projection of first and second coordinates of a pair, respectively. R can be defined from the following two rewrite rules:

fst([z_{1}, z_{2}]) >_{r_{1}} z_{1}
snd([z_{1}, z_{2}]) >_{r_{2}} z_{2}

We then have that e.g. fst([snd([a, b]), c]) >_{r_{1}} snd([a, b]) as an example of a primitive rewrite. We also have that fst([snd([a, b]), c]) > fst([b, c]) > b and fst([snd([a, b]), c]) > snd([a, b]) > b

Here are some important notions concerning rewrite systems:

• We denote by >^{∗} the reflexive and transitive closure of the relation > and by <>^{∗} the symmetric, reflexive and transitive closure of >.

• A term M_{1} is reducible if there exists a term M_{2} s.t. M_{1} > M_{2}. M_{1} is in normal form (or irreducible) if it is not reducible.

• A term M_{2} is a normal form of M_{1} if M_{1} >^{∗} M_{2} and M_{2} is in normal form. If M_{1} has a unique normal form, this is denoted by M_{1} ↓.

• A TRS is called confluent if whenever M_{1} >^{∗} M_{2} and M_{1} >^{∗} M_{3} there exists an M_{4} such M_{2} >^{∗} M_{4} and M_{3} >^{∗} M_{4}.

• A TRS is called terminating if there is no infinite chain M_{1} > M_{2} > M_{3} . . ..

• A TRS is called normalising if every term has a normal form.

• A TRS is called convergent if it is both confluent and terminating.

Note that terminating implies normalising, although the converse does not necessarity hold.

Having introduced the basics of term rewrite systems we can now give a definition of equality between terms.

Definition 1 (Equational Theory). An equational theory =_{E}, generated from a TRS R, is an equivalence relation on T (Σ, U) which satisfies the following rules:

(Rewrite)  \overline{M_{1} =_{E} M_{2}} if (M_{1} >_{r} M_{2}) ∈ R
(Reflexivity)  \overline{M =_{E} M}
(Symmetry)  \frac{M_{2} =_{E} M_{1}}{M_{1} =_{E} M_{2}}
(Transitivity) \frac{M_{1} =_{E} M_{3} M_{3} =_{E} M_{2}}{M_{1} =_{E} M_{2}}
(Function)  \frac{M_{1} =_{E} M′_{1}, …, M_{k} =_{E} M′_{k}}{f(M_{1}, …, M_{k}) =_{E} f(M′_{1}, …, M′_{k})} where f ∈ Σ^{(k)}
(Substitution) \frac{M_{1} =_{E} M_{2}}{M_{1}θ =_{E} M_{2}θ} for all substitutions θ

It is shown in [7, Theorem 3.1.12] that the equational theory =_{E} generated from R coincides with the reflexive, symmetric and transitive closure of the rewrite relation, i.e. M_{1} =_{E} M_{2} ⇔ M_{1} <>^{∗} M_{2}. This gives us a degree of freedom in later proofs, for as we shall discover, the definition in terms of an equational theory is not always convenient to work with. Another important result, which we shall use extensively in this report, says that M_{1} =_{E} M_{2} ⇔ M_{1} ↓= M_{2} ↓ for confluent and normalising rewrite systems [7, Theorem 2.1.9]

Example 2.2.2. As an example of an equational theory, we now define the theory E_{sym} of symmetric key encryption, pairing, and hash functions. When doing so, we must define a signature by specifying function symbols and their associated arities, and we must define the rewrite system used for generating the equational theory.

Theory E_{sym} .

Signature: enc(·, ·), dec(·, ·), [·, ·], fst(·), snd(·),f(·).

Rewrite System:

dec(enc(z_{1}, z_{2}), z_{2}) >_{r_{1}} z_{1}
fst([z_{1}, z_{2}]) >_{r_{2}} z_{1}
snd([z_{1}, z_{2}]) >_{r_{3}} z_{2}

The hash property of the function f, i.e. that f is one-way and collision-free, is reflected by the lack of axioms involving f. Example terms in this theory are enc(a, k), dec(enc(a, k), k) and enc([f(a), [b, c]], k). Here are some example equalities in E_{sym}:

dec(enc(a, k), k) =_{E} a
dec(enc([f(a), [b, c]], k), k) =_{E} [f(a), [b, c]]
fst(dec(enc([f(a), [b, c]], k), k)) =_{E} f(a)

Example 2.2.3. In public key encryption schemes a public key k^{+}, typically known to any participating principal, can be used to encrypt messages, but only a corresponding private key k^{−}, known only by a single principal, can be used for decryption. The idea behind public key encryption can be expressed in the following equational theory, where we again have pairing and hash functions:

Theory E_{pub} .

Signature: enc(·, ·), dec(·, ·), ·^{+}, ·^{−}, [·, ·], fst(·), snd(·),f(·).

Rewrite System:

dec(enc(z_{1}, z_{2}^{+}), z_{2}^{−}) >_{r_{1}} z_{1}
fst([z_{1}, z_{2}]) >_{r_{2}} z_{1}
snd([z_{1}, z_{2}]) >_{r_{3}} z_{2}

We have the following equalities:

dec(enc(a, k^{+}), k^{−}) =_{E} a but
dec(enc(a, k^{+}), k^{+}) ≠_{E} a

Example 2.2.4. The theories introduced in the two previous examples are fairly simple. When demonstrating concepts and results later in the report we need to take more complex rewrite rules into account. Hence we now define an extended version of the public-key theory in which two keys are used for both encryption and decryption.

Theory E_{pub2} .

Signature: enc(·, ·), dec(·, ·), ·^{+}, ·^{−}, [·, ·], fst(·), snd(·),f(·).

Rewrite System:

dec(enc(z_{1}, f(z_{2}^{+}, z_{3}^{+})), f(z_{2}^{−}, z_{3}^{−})) >_{r_{1}} z_{1}
fst([z_{1}, z_{2}]) >_{r_{2}} z_{1}
snd([z_{1}, z_{2}]) >_{r_{3}} z_{2}

In this report we shall restrict our attention to a certain class of equational theories known as convergent subterm theories (the following definition is adapted from [2, Definition 1]):

Definition 2 (Convergent Subterm Theories). An equational theory is a convergent subterm theory if it is generated from a convergent TRS R = ⋃_{i=1}^{n}{L_{i} >_{r_{i}} R_{i}} where each R_{i} is a proper subterm of L_{i}.

It follows from the subterm condition (i.e. that R_{i} is a proper subterm of L_{i}) that the rewrite system generating convergent subterm rewrite system is also terminating and hence normalising. Since convergence implies confluence, the aforementioned result that M_{1} =_{E} M_{2} ⇔ M_{1} ↓= M_{2} ↓ holds for the theories which we consider in this report.

Recall that a destructor function is a function symbol which occurs as the outermost function symbol in the redex of some rewrite rule (e.g. dec(·, ·), fst(·), snd(·) etc.). We shall make one additional assumption about the theories which we consider, namely that rewrite rules are independent in the sense that they only contain destructor functions as the outermost function symbol; i.e. we disregard rewrite rules such as

dec(enc(fst(z_{1}, z_{2}), z_{3}), z_{3}) > z_{1}

which intuitively says that only encrypted first components of pairs can be decrypted. This assumption is not very strong though, for the vast majority of theories with rules on the above form are not convergent. Take for example the following terms in the theory arising from the above rule:

M_{1} = dec(enc(fst([a, b]), k), k)
M_{2} = dec(enc(a, k), k)
M_{3} = a

Then M_{1} >^{∗} M_{2} and M_{1} >^{∗} M_{3} but there is no M_{4} such that M_{2} >^{∗} M_{4} and M_{3} >^{∗} M_{4}, i.e. confluence and hence convergence fails. An example of a rewrite system which is convergent and in which destructor functions occur internally in a redex is given in [1] (where it is used to model the property that decryption keys cannot be guessed):

dec(enc(z_{1}, z_{2}), z_{2}) >_{r_{1}} z_{1}
enc(dec(z_{1}, z_{2}), z_{2}) >_{r_{2}} z_{1}

For consider the following term:

M_{1} = enc(dec(enc(a, k), k), k)

Then M_{1} can be reduced using both rule r_{1} and r_{2}, but the resulting reduct is always the same (namely enc(a, k)), indicating that the rewrite system is convergent. However, disregarding this type of rules does not result in a great loss of generality.

2.2.2 Structural Equivalence

Semantics for Applied π is based on a structural equivalence relation on processes. Here an evaluation context is a process with a hole which is not under a replication, a conditional, an input, or an output. Structural equivalence ≡ is then defined as the smallest equivalence relation on P which is closed under α-conversion on names and variables, under application of evaluation context, and which satisfies the following:

Par-0  P ≡ P |0
Par-A  P |(Q|R) ≡ (P |Q)|R
Par-C  P |Q ≡ Q|P
Repl  !P ≡ P |!P
New-0  (νn)0 ≡ 0
New-C  (νu)(νv)P ≡ (νv)(νu)P
New-Par  P |(νu)Q ≡ (νu)(P |Q) if u ∉ fn(P) ∪ fv(P)
Alias  (νx){^{M}/_{x}} ≡ 0
Subst  {^{M}/_{x}}|P ≡ {^{M}/_{x}}|P {^{M}/_{x}}
Rewrite  {^{M_{1}}/_{x}} ≡ {^{M_{2}}/_{x}} when M_{1} =_{E} M_{2}

Note that ≡ is not a congruence because of the limitations on the type of contexts which may be applied (in effect, only closure under parallel composition and under restriction is required). Note also that the first 7 rules are standard, as given in e.g. [25, Section 2.2], except that there is no scope extrusion for conditionals.

The last three rules give meaning to active substitutions. Alias says that an active substitution with its variable under restriction cannot do anything and, together with Par-0, how an arbitrary active substitution can be introduced. Subst formalises the intuition given in the previous subsection that an active substitution may apply its substitution to any process it runs in parallel with, and the Rewrite rule relates structural equivalence and equivalence in the underlying equational theory.

2.2.3 Internal Reduction

An internal reduction relation →, which explains how processes behave, can now be defined based on structural equivalence. In the following, C[P] denotes the evaluation context C[−] applied to the process P:

Comm  \overline{a}⟨x⟩.P |a(x).Q → P |Q
Then  \frac{M_{1} =_{E} M_{2}}{if M_{1} = M_{2} then P else Q → P}
Else  \frac{M_{1} ≠_{E} M_{2}}{if M_{1} = M_{2} then P else Q → Q}
Ctx  \frac{P → Q}{C[P] → C[Q]}
Struct  \frac{P ≡ P′, P → Q, Q ≡ Q′}{P′ → Q′}

Note how equality in the equational theory plays an essential role in the rules involving conditionals. As usual, →^{∗} is the transitive closure of →. The Comm rule appears concerning at a first glance: only variables (and not terms) can be output, and the output seems to disappear in the reduced process. This simplicity of communication in the reduction semantics relies on active substitutions and structural equivalence to work as we shall see in the following example.

Example 2.2.5. We assume the theory E_{sym} of symmetric encryption and pairing introduced in Example 2.2.2. The following reduction then illustrates the communication mechanism for the case of a pair, as well as the reduction semantics for conditionals.

\overline{a}⟨[M, s]⟩ | a(x).if snd(x) = s then \overline{b}⟨fst(x)⟩
≡\overline{a}⟨[M, s]⟩ | (νx)\{^{[M,s]}/_{x}\} | a(x).if snd(x) = s then \overline{b}⟨fst(x)⟩
≡(νx)(\overline{a}⟨[M, s]⟩ | \{^{[M,s]}/_{x}\} | a(x).if snd(x) = s then \overline{b}⟨fst(x)⟩)
≡(νx)(\overline{a}⟨x⟩ | \{^{[M,s]}/_{x}\} | a(x).if snd(x) = s then \overline{b}⟨fst(x)⟩)
→(νx)(if snd(x) = s then \overline{b}⟨fst(x)⟩ | \{^{[M,s]}/_{x}\})
≡(νx)(if snd([M, s]) = s then \overline{b}⟨fst([M, s])⟩ | \{^{[M,s]}/_{x}\})
→(νx)(\overline{b}⟨fst ([M,s])⟩ | \{^{[M,s]}/_{x}\})
≡\overline{b}⟨fst ([M,s])⟩

2.2.4 Labelled Operational Semantics

The labelled operational semantics extends the reduction relation from the previous subsection by explicitly labelling reductions with actions. This allows reasoning about processes which interact with their environment, and is also the basis of a bisimulation relation on processes which we shall introduce later. The relation which shall be defined is on the form P ⟶^{α} P′ where the label α is either an input a(M) or an output \overline{a}⟨u⟩. The bound output label (νu)\overline{a}⟨u⟩ will be used to reflect that the name or variable u is under restriction. The following rules, together with the reduction rules from the previous section, define the labelled operational semantics relation P ⟶^{α} P′.

In  a(x).A ⟶^{a(M)} A{^{M}/_{x}}
Out-Atom  \overline{a}⟨u⟩.A ⟶^{\overline{a}⟨u⟩} A
Open-Atom  \frac{P ⟶^{\overline{a}⟨u⟩} P′ u ≠ a}{(νu)P ⟶^{(νu)\overline{a}⟨u⟩} P′}

Scope  \frac{P ⟶^{α} P′ u does not occur in α}{(νu)P ⟶^{α} (νu)P′}

Par  \frac{P ⟶^{α} P′ bv(α) ∩ fv(Q) = bn(α) ∩ fn(Q) = ∅}{P |Q ⟶^{α} P′|Q}

Struct  \frac{P ≡ Q Q ⟶^{α} Q′ Q′ ≡ P′}{P ⟶^{α} P′}

Note that this in an early semantics, i.e. input actions take immediate effect.

Example 2.2.6. Here is an example of a process which communicates with the environment in the labelled semantics, again assuming the theory E_{sym} from Example 2.2.2:

(νk)\overline{a}⟨enc(M, k)⟩.\overline{a}⟨k⟩.a(z).if z = M then \overline{c}⟨o⟩
≡⟶^{(νx)\overline{a}⟨x⟩}(νk)(\{^{enc(M,k)}/_{x}\}|\overline{a}⟨k⟩.a(z)if z = M then \overline{c}⟨o⟩)
≡⟶^{(νy)\overline{a}⟨y⟩}(νk)(\{^{enc(M,k)}/_{x}\}|\{^{k}/_{y}\}|a(z).if z = M then \overline{c}⟨o⟩)
⟶^{a(dec(x,y))}(νk)(\{^{enc(M,k)}/_{x}\}|\{^{k}/_{y}\}|if dec(x, y) = M then \overline{c}⟨o⟩)
→(νk)(\{^{enc(M,k)}/_{x}\}|\{^{k}/_{y}\}|if dec(enc(M, k), k) = M then \overline{c}⟨o⟩)
→(νk)(\{^{enc(M,k)}/_{x}\}|\{^{k}/_{y}\}|\overline{c}⟨o⟩)

The structural equivalence in the first two steps is used to introduce an active substitution with a variable under restriction – this restriction then dissappears in the subsequent bound output.

2.3 Equivalences in Applied π

In this section four notions of equivalence on processes are introduced, namely observational equivalence, two kinds of static equivalence, and labelled bisimilarity.

2.3.1 Observational Equivalence

The first equivalence we define on extended processes is observational equivalence. For this purpose we say that a process P has a barb on channel a, written P ⇓ a, if P →^{∗} C[\overline{a}⟨M⟩.P′] for some evaluation context C[−].

Definition 3 (Observational Equivalence). Observational equivalence, ≈, is the largest symmetric relation R on closed extended processes with the same domain such that P RQ implies:

1. if P ⇓ a, then Q ⇓ a.

2. if P →^{∗} P′ then Q →^{∗} Q′ and P′RQ′ for some Q′.

3. C[P]RC[Q] for all evaluation contexts C[−].

Observational equivalence corresponds to the open barbed bisimilarity studied in [26] by Sangiorgi and Walker. They also show that this bisimilarity does not coincide with the barbed congruence in [25, Section 7.2], where closure under application of evaluation contexts is separated from the bisimulation conditions.

The definition of observational equivalence suffers from a universal quantification over all contexts. Later we shall give an equivalence based on the labelled operational semantics which does not have this problem. It depends on the notion of static equivalence which is the subject of the next subsection.

2.3.2 Static Equivalence

We now arrive at two notions which will receive considerable attention in the rest of this report, namely that of frames and that of static equivalence. Frames, ranged over by φ, are limited forms of extended processes built only from name restriction and active substitutions, and are on the form

φ = (νñ){^{M_{1}}/_{x_{1}}} | ⋯ | {^{M_{k}}/_{x_{k}}}

where for technical convenience we assume that each M_{i} is irreducible. Note that this is slightly different from the definition of frames in [4] where restrictions may occur interleaved with active substitutions, terms need not be irreducible and variables may be private in addition to names. A frame can be considered a substitution in which names may be private and can therefore be applied to variables in the usual way. We shall often use the short hand notation φ = (νñ){^{M_{i}}/_{x_{i}}}_{i∈I} or φ = (νñ)σ (where σ is a substitution) instead of writing out the sequence of active substitutions, and we shall write (ν∗)σ for the closed frame where all occurring names are private.

2.3. EQUIVALENCES IN APPLIED π

Any extended process P can be mapped to its associated frame, intuitively by deleting all plain processes, extending all restrictions to the outer level and normalising terms in active substitution.

Definition 4. We define the frame of an extended process A inductively as follows:

φ(P) =^{Δ} (ν∅)∅  if P is a plain process
φ({^{M}/_{x}}) =^{Δ} {^{M↓}/_{x}}
φ((νn)P) =^{Δ} (νñn)σ  where φ(P) = (νñ)σ
φ((νx)P) =^{Δ} (νñ)σσ  where φ(P) = (νñ)σ
φ(P_{1} | P_{2}) =^{Δ} (νñ_{1}ñ_{2})σ_{1}σ_{2}  where φ(P_{1}) = (νñ_{1})σ_{1}
and φ(P_{2}) = (νñ_{2})σ_{2}
and ñ_{1} ∩ n(σ_{2}) = ñ_{2} ∩ n(σ_{2}) = ∅

In the last case α-conversion may be necessary to ensure that ñ_{1} ∩ n(σ_{2}) = ñ_{2} ∩ n(σ_{2}) = ∅. The case for private variables states that active substitutions containing private variables must be applied to obtain frames which only contain private names.

As the example reduction in the previous section showed, each output action performed by a process extends the active substitution. Hence, at any given time, the frame of an extended process P represents the messages communicated by P and thereby also the “static” knowledge available to the environment. This gives rise to an equivalence relation ≈_{s} on frames called static equivalence where, intuitively, two frames are statically equivalent if the environment cannot distinguish them, e.g if two frames represent the same knowledge.

The only way the environment can deduce information from a frame is by testing for equality between terms of the frame. This is captured in the following definition.

Definition 5 (Equality in frames). Two terms M_{1} and M_{2} are equal in frame φ, written (M_{1} = M_{2})φ if and only if n(M_{1}, M_{2})∩bn(φ) = ∅ and M_{1}φ =_{E} M_{2}φ.

Note the condition that n(M_{1}, M_{2})∩bn(φ) = ∅, which is necessary for scope extension to work. To see this, take the frame φ = (νa){^{[a,b]}/_{x}} in the theory E_{1}. An environment may check that snd(x) = b holds in φ as follows:

if snd(x) = b then P_{Y ES} else P_{NO}|(νa){^{[a,b]}/_{x}}
→(νa)(if snd(x) = b then P_{Y ES} else P_{NO}|{^{[a,b]}/_{x}})
→(νa)(if snd([a, b]) = b then P_{Y ES} else P_{NO}|{^{[a,b]}/_{x}})
→(νa)(P_{Y ES}|{^{[a,b]}/_{x}})

Step 2 in this reduction relies on extending the scope of a, which is only possible because a is not free in the terms tested in the conditional. Hence the equality fst(x) = a should not hold in φ, since the scope of the name a cannot be extended to any conditional process in which a is free.

We are now ready to give the all-important definition of static equivalence between frames.

Definition 6 (Static equivalence). Two frames φ and φ′ are statically equivalent, written φ ≈_{s} φ′, if and only if dom(φ) = dom(φ′) and

(M_{1} = M_{2})φ ⇔ (M_{1} = M_{2})φ′ for all terms M_{1} and M_{2}

Furthermore, we say that two processes P and Q are statically equivalent, written P ≈_{s} Q, if and only if φ(P) ≈_{s} φ(Q).

Example 2.3.1. We revisit the example frames from the introduction:

φ_{1} = (νk, b){^{enc(b,k^{+})}/_{x_{1}}, ^{k^{−}}/_{x_{2}}, ^{b}/_{x_{3}}}
φ_{2} = (νk, b){^{enc(enc(b,b^{+}),k^{+})}/_{x_{1}}, ^{k^{−}}/_{x_{2}}, ^{enc(b,b^{+})}/_{x_{3}}}
φ_{3} = (νk, b){^{enc(enc(b,k^{+}),k^{+})}/_{x_{1}}, ^{k^{−}}/_{x_{2}}, ^{b}/_{x_{3}}}

Then φ_{1} ≈_{s} φ_{2} while φ_{1} ≉_{s} φ_{3}, the relevant equality being dec(x_{1}, x_{2}) =_{E} x_{3}. This holds in φ_{1} because dec(enc(b, k^{+}), k^{−}) =_{E} b, and it holds in φ_{2} because dec(enc(enc(b, b^{+}), k^{+}), k^{−}) =_{E} enc(b, b^{+}). However, it does not hold in φ_{3} because dec(enc(enc(b, k^{+}), k^{+}), k^{−}) ≠_{E} b.

One could consider defining static equivalence in a more direct manner as follows: φ ≈_{s} φ′ iff dom(φ) = dom(φ′) and for every pair of terms M_{1}, M_{2} with v(M_{1}, M_{2}) ⊆ v(φ) and n(M_{1}, M_{2}) ∩ (bn(φ) ∪ bn(φ′)) = ∅ it holds that M_{1}φ =_{E} M_{2}φ ⇔ M_{1}φ′ =_{E} M_{2}φ′. Indeed this is done in e.g. [10], but it is not equivalent to the definition we have given here. For with our definition it holds for any two frames φ and φ′ that bn(φ) ≠ bn(φ′) ⇒ φ ≉_{s} φ′. For suppose that a ∈ bn(φ) − bn(φ′) (where − is the set difference operator). Then the equality a =_{E} a holds in φ but not in φ′.

The universal quantification over terms in the definition of static equivalence poses problems for practical application. Abadi and Cortier show in [2] that static equivalence is not decidable in general, but they also show that it is decidable for convergent subterm theories as defined in Definition 2. In [3] they give decidability results for a bigger class of theories.

2.3.3 Labelled Bisimilarity

Labelled bisimilarity avoids the universal quantification over contexts which haunts observational equivalence and instead relies on static equivalence.

Definition 7 (Labelled bisimilarity). (≈_{l}) is the largest symmetric relation R such that P RQ implies:

1. P ≈_{s} P′;

2. if P →^{∗} P′ then Q →^{∗} Q′ and P′RQ′ for some Q′;

3. if P ⟶^{α} P′ and fv(α) ⊆ dom(P) and bn(α) ∩ fn(Q) = ∅ then Q →^{∗}⟶^{α}→^{∗} Q′ and P′RQ′ for some Q′.

It is shown in [4, Theorem 1] that observational equivalence and labelled bisimilarity coincide.

2.3.4 Strong Static Equivalence

A notion of static equivalence has now been defined with the intuition that statically equivalent frames should be indistinguishable by observer processes which are able to test for equality between terms in frames. However, one could question whether equality is the only relevant predicate to test for when deciding static equivalence. Consider the following example frames for motivation:

φ =^{Δ} (νa, c, k){^{enc(a,k^{+})}/_{x_{1}}, ^{k^{−}}/_{x_{2}}}

φ′ =^{Δ} (νa, c, k){^{enc(a,k^{+})}/_{x_{1}}, ^{c^{−}}/_{x_{2}}}

The first frame contains an encrypted name and the corresponding private key which can be used for decryption. The second frame contains the same encrypted name but does not contain the corresponding private key for decryption. Now it turns out that φ ≈_{s} φ′. The only relevant attempt at constructing a distinguishing equality is as follows:

x_{1} =_{E} enc(dec(x_{1}, x_{2}), k^{+})

but this equality does not hold in either frame since k ∈ bn(φ) and k ∈ bn(φ′).

The fact that φ ≈_{s} φ′ might be slightly surprising. For we then get that the following Applied π processes are bisimilar:

P =^{Δ} (νa, c, k)(\overline{b}⟨enc(a, k^{+})⟩.\overline{b}⟨k^{−}⟩

P′ =^{Δ} (νa, c, k)(\overline{b}⟨enc(a, k^{+})⟩.\overline{b}⟨c^{−}⟩

Hence a process which sends an encrypted term and subsequently reveals its private decryption key is bisimilar to a (more sound) process which sends an encrypted term but does not leak the corresponding private decryption key! Is this sensible? Well, the intuition that no observer process can distinguish P and P′ is intact, since an observer will be able to decrypt the encrypted term from P but will never be in a position to look at the contents (i.e. test for equality) since the name a is private. An observer who tests equality on a would hence not be able to communicate with P since scope extrusion to the observer fails.

Implementations of cryptographic functions (e.g. the OpenSSL library [27]) typically don’t provide means of testing whether decryption with a given decryption key is successful or not. However, in many applications it is assumed that such information is available, e.g. by appending a publicly known token to the clear text before encryption; it can then be checked if the decryption output also contains this token.

In other applications including e.g. pairing and lists, strongly typed programming languages such as Java will throw runtime exceptions if e.g. the fst projection function is applied to an object M which is not a pair. More specifically, if such object M is received over a network socket, a typecast to the pair type will fail. Hence a principal will be able to detect whether fst(M) is reducible or not.

So reductions (which can also be viewed as computation steps) are most often observable in practical applications: it would be feasible for a process to be able to test if a decryption succeeds or not, even though it may not be able to look at the decrypted term. And it would be feasible for a process to test if application of a projection function to a pair succeeds or not. This motivates us to extend the Applied π syntax with an additional test on reductions thus:

P, Q, R ::= ... | if M >^{k} then P else Q

Intuitively such test succeeds if M can rewrite in k steps to some M′. The definition of internal reduction, →, can then be extended accordingly:

Then-2  \frac{∃M′.M >^{k} M′}{if M >^{k} then P else Q → P}
Else-2  \frac{¬∃M′.M >^{k} M′}{if M >^{k} then P else Q → Q}

Note that a test of the form M_{1} > M_{2} is not strong enough for our purpose. For this test would not be able to distinguish the frames φ and φ′ with public-key encrypted terms above. The reason is that M_{2} cannot be the private name a, for scope extrusion to an observer making this test would fail.

Before defining a stronger version of static equivalence in which rewrites are observable, we first define the notion of rewrite in frame along the same lines as equality in frames.

Definition 8 (Rewrite in frames). Say that a term M can rewrite in k steps in frame φ, written (M >^{k})φ, if and only if n(M) ∩ bn(φ) = ∅ and there exists a term M′ such that Mφ >^{k} M′.

Definition 9 (Strong static equivalence). Two frames φ and φ′ are strong statically equivalent, written φ ≈_{ss} φ′, if and only if dom(φ) = dom(φ′) and:

1. (M_{1} =_{E} M_{2})φ ⇔ (M_{1} =_{E} M_{2})φ′ for all terms M_{1} and M_{2}.

2. (M >^{k})φ ⇔ (M >^{k})φ′ for all terms M.

Furthermore, we say that two extended processes P and Q are strong statically equivalent, written P ≈_{ss} Q, if and only if φ(P) ≈_{ss} φ(Q).

\underline{2.4. SUMMARY}

It is immediate that ≈_{ss} implies ≈_{s}. The example given in the start of this subsection demonstrated that ≈_{ss} does not generally imply ≈_{s}, so the additional test on rewrites increases the distinguishing power of processes. However we shall later pin down a class of equational theories in which also ≈_{s} implies ≈_{ss}, i.e. in which the two definitions coincide. To give a preliminary example of this result, take the symmetric-key counterpart of the frames given earlier:

φ_{2} =^{Δ} (νa, c, k){^{enc(a,k)}/_{x_{1}}, ^{k}/_{x_{2}}}
φ′_{2} =^{Δ} (νa, c, k){^{enc(a,k)}/_{x_{1}}, ^{c}/_{x_{2}}}

Then φ_{2} ≉_{s} φ′_{2} because the following equality distinguishes the two frames:

x_{1} =_{E} enc(dec(x_{1}, x_{2}), x_{2})

Clearly also φ_{2} ≉_{ss} φ′_{2} because dec(x_{1}, x_{2}) >^{1} holds in φ but not in φ′.

2.4 Summary

In this chapter we have introduced syntax and semantics for the Applied π calculus, a uniform and generic extension of the π calculus for which particular primitives such as tuples and cryptographic functions can be defined and used on a per-application basis. The key idea is to integrate arbitrary terms into the calculus and its semantics based on a function signature, and to base equality between terms on an equational theory instead of syntactic equality on names.

We have seen how a frame is obtained by extracting all active substitutions of a process, and we have defined an indistinguishability relation ≈_{s} on frames called static equivalence. Roughly speaking, two frames are statically equivalent if an environment cannot distinguish the frames by testing for equality between any pair of terms constructed from variables in the frames. Furthermore, we have defined a stronger static equivalence, ≈_{ss}, in which term reductions are observable in addition to equality between terms.

Frames and static equivalence play a central role in labelled bisimilarity (which coincides with observational equivalence) of processes in Applied π: two processes are bisimilar if they can simulate each others actions and if their frames are statically equivalent, i.e. if the processes can be distinguished neither on their dynamic behaviour nor on their static characteristics.

A Refined Definition of Strong Static Equivalence

We now set out to find refined definition of strong static equivalence which provides a suitable basis for a logic for frames and is amenable to construction of characteristic formulae. First we consider some previous work to this end in Section 1 and pay particular attention to work by Boreale et al. on characteristic formulae for frames in the Spi calculus. Section 2 continues with a number of preliminary definitions. These are then used in the refined definition of strong static equivalence given in Section 3. Section 4 demonstrates the refined definition with a number of examples designed to strengthen our belief that the standard and refined definitions of strong static equivalence coincide.

3.1 Previous Work

As mentioned earlier, Abadi and Cortier have shown that static equivalence is decidable for the class of independent convergent subterm theories which was introduced in Subsection 2.2.1 [2, 3]. Therefore one would expect that they at some stage construct a finite set of equalities which is sufficient for deciding static equivalence. This is indeed the case; to decide static equivalence between two frames φ and φ′, they associate a finite set of equalities Eq(φ) and Eq(φ′) with each frame such that φ ≈_{s} φ′ if and only if the two frames satisfy the equalities from each other’s set. Hence an alternative definition of static equivalence which does not contain an universal quantification over terms can be made based on this approach. Unfortunately this definition would not serve as a sufficient basis for characteristic formulae. For a characteristic formula must be defined based on a single frame, whereas the above approach defines equivalence based on two specific frames.

CHAPTER 3. A REFINED DEFINITION OF STRONG STATIC …

Since static equivalence is known to be undecidable for certain theories even when (equational) equality between terms is decidable [2], there are theories in which characteristic formulae do not exists or are not computable (assuming that satisfaction is decidable for the logic in question). For decidability of static equivalence reduces to computing characteristic formulae and deciding satisfaction: to decide if φ ≈_{s} φ′, compute the characteristic formula C_{φ} of φ and check if C_{φ} ⊨ φ′. Hence we focus our efforts on independent convergent subterm theories in which static equivalence is known to be decidable. Although decidability in itself does not guarantee existence of characteristic formulae, we shall learn that characteristic formulae with respect to strong static equivalence can indeed be constructed in convergent subterm theories.

In [9] the problem of finding an alternative, tractable definition of static equivalence is attacked for the particular case of (a variant of) the Spi calculus with symmetric key encryption. This definition does yield a construction of characteristic formulae, the key idea being that of a core. We will give the intuition of this idea by an example, and in the next section we formalise and generalise the relevant notions in the hope of getting similar results for a wider class of equational theories not restricted to symmetric encryption. Consider the following two frames:

φ = (νa, c, k){^{enc(enc(a,c),k)}/_{x_{1}}, ^{k}/_{x_{2}}, ^{enc(a,c)}/_{x_{3}}}
φ′ = (νa, c, k){^{enc(a,k))}/_{x_{1}}, ^{k}/_{x_{2}}, ^{a}/_{x_{3}}}

Let M_{i} = x_{i}φ and M′_{i} = x_{i}φ′. Then the core core(x_{i}, φ) of x_{i} in φ is, intuitively, the largest subterm of M_{i} which cannot be further decomposed using the information available in φ. In the above example we can apply the decryption function to M_{1} = enc(enc(a, c), k) with the key k available through x_{2} and get dec(enc(enc(a, c), k), k) =_{E} enc(a, c). Hence M_{1} is not a core. But the subterm N_{1} = enc(a, c) is a core, because we cannot apply any decryption function to reveal a since the key c is not available in the frame. The other cores in φ and φ′ can be derived similarly and are summarised below, where for brevity we define define N_{i} = core(x_{i}, φ) and N′_{i} = core(x_{i}, φ′):

N_{1} = enc(a, c)  N′_{1} = a
N_{2} = k  N′_{2} = k
N_{3} = enc(a, c)  N′_{3} = a

Observe that φ ≈_{s} φ′; two interesting equalities which both frames satisfy are enc(x_{3}, x_{2}) =_{E} x_{1} (by reflexivity) and dec(x_{1}, x_{2}) = x_{3} (by axiom). There are two key reasons why these equalities hold in both frames:

1. Two cores in φ are equal exactly when the corresponding cores in φ′ are equal. Specifically, N_{1} = N_{3} and N′_{1} = N′_{3}

2. Corresponding terms M_{i} and M′_{i} are equal up to cores, in the sense that M_{i} and M′_{i} are composed from exactly the same functions applied to their respective cores. Specifically, M_{1} = enc(N_{3}, N_{2}) and M′_{1} = enc(N′_{3}, N′_{2})

3.1. PREVIOUS WORK

The alternative, tractable definition of static equivalence given in [9] for frames in the Spi calculus with symmetric key encryption is essentially based on the two observations above.

We will use these ideas as a basis for devising a general refined definition of strong static equivalence which coincides with the standard definition of strong static equivalence in any independent convergent subterm theory (i.e. not just in symmetric key encryption theories). A straight forward generalisation presents a number of challenges though, many of which become apparent simply by moving from symmetric key encryption to public key encryption with pairs and hash functions. Take for example the counterparts of the above frames with public key encryption, pairing and hash functions in the theory E_{pub}:

φ_{2} = (νa, c, k){^{enc([a,enc(b,c^{+})],k^{+})}/_{x_{1}}, ^{k^{−}}/_{x_{2}}, ^{enc(b,c)}/_{x_{3}}}
φ′_{2} = (νa, c, k){^{enc([a,b],f(k)^{+})}/_{x_{1}}, ^{f(k)^{−}}/_{x_{2}}, ^{b}/_{x_{3}}}

Now how should one define e.g. core(x_{1}, φ_{2})? The intuition is that the core is the smallest term that can be revealed from x_{1}, but both a and enc(b, c^{+}) satisfy this intuition. Hence it would seem that a term can now have several cores. And what about subterms such as the public key k^{+} in M_{1} – should this be considered a core of x_{1}? Probably not, since it cannot be revealed from x_{1}. Hence we would intuitively expect to obtain the following cores of the two frames:

N_{1} = a  N′_{1} = a
N_{2} = enc(b, c^{+})  N′_{2} = b
N_{3} = k^{−}  N′_{3} = f(k)^{−}
N_{4} = enc(b, c^{+})  N′_{3} = b

Lets investigate how the idea with equality between cores and equality of terms up to cores works in our new setting.

1. Equality between cores. The equalities N_{2} = N_{4} and N′_{2} = N′_{4} do hold as expected. However, important information is lost if we only consider equality between cores. There is for instance no syntactic equality relating the public and private keys. Hence the fact that snd(dec(x_{1}, x_{2})) =_{E} x_{3} does not follow by syntactic equality between keys as it would in the symmetric key case.

2. Equality up to cores. We would like to express that e.g.

M_{1} = enc([a, enc(b, c^{+})], k^{+}) and M′_{1} = enc([a, b], f(k)^{+}) can be written as the same context over cores. This gives rise to a dilemma about how to define the notion of a context. Since k^{+} is not a core, we would have to include the private name k in the context and write M_{1} = enc([N_{1}, N_{2}], k^{+}), i.e. obtaining the context enc([y_{1}, y_{2}], k^{+}). But this context will not work for M′_{1} because the encryption key in this term is f(k)^{+}: M′_{1} ≠ enc([N′_{1}, N′_{2}], k^{+}). So it would not appear that the two terms can be written as the same context over cores.

In order to overcome these problems and in order to make our terminology precise, a number of preliminary definitions – including that of a context, revelation from terms and cores – will be given in the next section.

3.2 Initial Definitions

In this section we give some preliminary definitions which are needed in the refined strong static equivalence. We start by making precise the notion of contexts. We then define revelation, a binary relation which expresses when a term can reveal one of its subterms (e.g. by decryption with an appropriate key). Revelation is a central ingredient in the analysis of a frame, which intuitively is the set of all terms that can be revealed from the frame. Finally the analysis leads to a general definition of cores in Applied π.

As we demonstrated in the last section, the standard notion of cores is insufficient. Therefore we extend our notion of cores to include more terms from the analysis, and we coin these ecores (for extended cores). We end the section with a discussion of correlated variables and partitioning contexts, notions which are required in order to bound the number of contexts considered in the refined definition of strong static equivalence.

3.2.1 Contexts

We start with a definition of contexts.

Definition 10 (Contexts). A general context C^{N} [x_{1}, …, x_{k}] is a term where N is a set of names, v(C^{N} [x_{1}, …, x_{k}]) = {x_{1}, …, x_{k}} and n(C^{N} [x_{1}, …, x_{k}]) ⊆ N. The instantiation C^{N} [M_{1}, …, M_{k}] is the term C^{N} [x_{1}, …, x_{k}]{^{M_{1}}/_{x_{1}}, …, ^{M_{k}}/_{x_{k}}}. A context which is just a variable or a name is called a trivial context. In this report we will only consider two special cases, namely contexts C^{∅}[x̃] (i.e. with no names) and contexts C^{{⊥}}[x̃] which may contain only a distinguished wild card name ⊥. We shall use the short hand C[x̃] for the former and C^{⊥}[x̃] for the latter.

We shall take the liberty of writing C^{N} [x̃] instead of C^{N} [x_{1}, …, x_{k}] when the indices on variables are irrelevant or understood. We shall assume that the sequence ỹ binds to its enclosing context, so if e.g. two contexts C_{1}[ỹ] and C_{2}[ỹ] are under consideration, it is not necessarily the case that v(C_{1}[ỹ]) = v(C_{2}[ỹ]).

3.2.2 Revelation

3.2. INITIAL DEFINITIONS

We now formalise the general idea that a term can reveal one of its subterms, e.g. that a pair can reveal its first and second components because it can be submitted to the first and second projection functions. The first definition expresses which superterm a reduct can be said to originate from, and we call the appropriate superterm the revelator.

Definition 11 (Revelator). Let L >_{r} R be a rewrite rule and let w be the position of R in L, i.e. L|_{w} = R. Suppose that M_{1} >_{r} M_{2}, i.e. M_{1} rewrites primitively to M_{2} using rewrite rule r. We then say that M_{1}|_{w′} is a revelator of the reduction, and we write M_{1} >_{r}^{M_{1}|_{w′}} M_{2}, if w′ is a prefix of w, i.e. if there is a position w′′ such that w = w′w′′.

Example 3.2.1. Consider the term M = enc(a, k^{+}) in the public-key theory E_{pub}. The following reductions then hold:

dec(M, k^{−}) > a
fst([k^{+}, M]) > k^{+}

Here M is a revelator of the first reduction, and hence a can be revealed from M by using the appropriate private key. However, M is not a revelator of the second reduction; this corresponds to the intution that the public key cannot be extracted from a cipher text.

Definition 12 (Destructor context). Let L[z̃] >_{r} R[z̃] be a rewrite rule and let D[x, x̃] be a context which is unifiable with L[z̃]. Let w be the position of the variable x, i.e. D[x, x̃]|_{w} = x. Then D[x, x̃] is a destructor context if L[z̃]|_{w} is a revelator.

Using the notions of revelator and destructor contexts, the revelation M ≻_{S} M′ can now be defined. Informally, this asserts that M′ is a reduct of some term constructed by applying functions to M with arguments from the set S.

Definition 13 (Revelation Relation). Let S be a set of terms. The revelation, ≻_{S}, is a binary relation over terms where we define M ≻_{S} M|_{w} if and only if there is a destructor context D[x, x̃] and terms T̃ ⊆ S such that D[M, T̃] >_{r}^{M} M|_{w}.

It follows from this definition that revelation is based on the rewrite rules of a given TRS. Henceforth we shall always assume that any TRS we consider is equipped with a revelation relation.

Example 3.2.2. Take the set S = {enc([b, enc(c, k_{2}^{+})], k_{1}^{+}), [d, k_{1}^{−}]} as an example (in the theory E_{pub}). Then we have that:

[d, k_{1}^{−}] ≻_{S} d
[d, k_{1}^{−}] ≻_{S} k_{1}^{−}
enc([b, enc(c, k_{2}^{+})], k_{1}^{+}) ⊁_{S} [b, enc(c, k_{2}^{+})]

The last revelation does not hold since k_{1}^{−} is not directly available in the set S and hence cannot be used for revelation in single rewrite-step.

3.2.3 Analysis

Next we define the analysis A(M, S) of a term M with respect to a set of terms S. A(M, S) is intuitively the set of terms that M can reveal by repeated revelation from the terms in S. A term may reveal multiple subterms, some of which may be identical, and it will be important for the later development that each instance is represented in the analysis. It will also be important that analysis terms can be ordered by position in their parents, and therefore this information is recorded in the analysis. More precisely, we then get that the analysis A(M, S) is a set of pairs (M|_{w}, w) where M|_{w} is a term revealed from M. Here is the formal definition:

Definition 14 (Term analysis). Let S be a set of terms and let M ∈ S. Then the analysis of M with respect to S is defined inductively as follows:

A^{0}(M, S) = {(M, ϵ)}
A^{i+1}(M, S) = A^{i}(M, S) ∪ {(M|_{w}, w)|∃N ∈ A^{i}(M, S) s.t. N ≻_{⋃_{T ∈S} A^{i}(T,S)} M|_{w}}
A(M, S) = ⋃_{i∈ω} A^{i}(S)

We further define A(M, φ) =^{Δ} A(M, im(φ) ∪ fn(φ)) for frames φ.

In many situations the positions included in the analysis are irrelevant and we shall instead consider the term analysis multiset A^{∗}(M, S) defined as

A^{∗}(M, S) = {M|_{w} | (M|_{w}, w) ∈ A(M, S)}

Since our point of view will always be apparent from the context, we shall not distinguish between A(M, S) and A^{∗}(M, S) in the future.

Example 3.2.3. Let S be the set of terms from the previous example (in the theory E_{pub}). Then

A([d, k_{1}^{−}], S) ={[d, k_{1}^{−}], d, k_{1}^{−}}
A(enc([b, enc(c, k_{2}^{+})], k_{1}^{+}), S) ={enc([b, enc(c, k_{2}^{+})], k_{1}^{+}), [b, enc(c, k_{2}^{+})], b,
enc(c, k_{2}^{+})}

Note that enc(c, k_{2}^{+}) is part of the second analysis because the decryption key k_{1}^{−} is available in the first analysis. However, c is not in the second analysis because the key k_{2}^{−} is unknown.

Sometimes we shall be interested in the combined analysis of an entire set of terms. This set analysis is defined as follows:

Definition 15 (Set analysis). Let S be a set of terms. Then the analysis of S is defined as A(S) = ⋃_{M∈S} A(M, S).

Example 3.2.4. Continuing the example with the set S from above (in the theory E_{pub}), we get that

A(S) = {enc([b, enc(c, k_{2}^{+})], k_{1}^{+}), [d, k_{1}^{−}], d, k_{1}^{−},
[b, enc(c, k_{2}^{+})], b, enc(c, k_{2}^{+})]}

There are of course alternative ways of defining analysis. One could be to give an inductive definition of set analysis and then define term analysis from this. However the analysis of a term M in φ cannot be defined simply as

A(M, S) = {M′ | M′ ∈ st(M) ∧ M′ ∈ A(S)}

since there may be a subterm of M which is not accessible by revelation from M but which can nevertheless be revealed from some other term in S, so a more involved definition would be necessary. Another alternative would be to define analysis as the fixed point of a suitable function, but this is largely a matter of taste.

3.2.4 Cores and Ecores

We are now equipped to give a general definition of cores in the Applied π calculus. This is a first step towards defining the terms which are essentially sufficient for deciding strong static equivalence between two frames.

Definition 16 (Core). The cores of term a M with respect to the set S is the maximum set of terms (M|_{w}, w) from A(M, S) where M|_{w} is ≻-irreducible:

cores(M, S) = {(M|_{w}, w) | (M|_{w}, w) ∈ A(M, S) ∧ M|_{w} ⊁_{A(S)}}

If (N, w) ∈ cores(M, S) we call N a core. The cores of a term M in a frame φ is defined as cores(M, φ) = cores(M, im(φ) ∪ fn(φ)). If x ∈ dom(φ) then cores(x, φ) = cores(xφ, φ). Finally, we define the cores of a frame φ = (νñ){^{M_{i}}/_{x_{i}}}_{i∈I} as

cores(φ) = ⋃_{i∈I}{(M_{i}|_{w}, w, i) | (M_{i}|_{w}, w) ∈ cores(M_{i}, φ)} ∪ {(n, , ) | n ∈ fn(φ)}

We will mainly be interested in cores of frames which are defined as sets of triples, again for the purpose of ordering – i.e. we will order cores in a frame by the index of their parent term and by their position in the parent term. We have also defined the cores of a frame to include all free names in the frame (the place holder for index and position simply indicates that these values are irrelevant for free names). The reason is that free names are important when deciding static equivalence. Take e.g. the frame φ = {^{f(a)}/_{x_{1}}} where a is a free name; then the environment can test that a = f(a) holds in φ, so a should be considered a core in φ. Another motivation for including free names in the core set of a frame is that any frame with free names n_{1}, …, n_{k} is statically equivalent to a closed frame (i.e. with no free names) but where each n_{1}, …, n_{k} is published as a term of the frame.

As with the analysis we often take the liberty of ignoring the position information and consider cores as multisets of terms instead of pairs or triples. In these cases it always holds that cores(M, S) is a subset of A(M, S) and that each M|_{w} ∈ cores(M, S) is a subterm of M (per definition of revelation).

Example 3.2.5. Take the frame φ = (νk_{1}, b, c){^{enc([b,enc(c,k_{2}^{+})],k_{1}^{+})}/_{x_{1}}, ^{[d,k_{1}^{−}]}/_{x_{2}}} which is based on the set S from the previous examples (again in the theory E_{pub}). Then

cores(enc([b, enc(c, k_{2}^{+})], k_{1}^{+}), S) = {b, enc(c, k_{2}^{+})}
cores([d, k_{1}^{−}], S) = {d, k_{1}^{−}}
cores(x_{1}, φ) = {b, c}
cores(x_{2}, φ) = {d, k_{1}^{−}}
cores(φ) = {b, c, d, k_{1}^{−}, d, k_{2}}

We have that c ∈ cores(x_{1}, φ) because the name k_{2} is free. The key k_{2}^{−} is therefore known and can be used in the revelation of c from enc(c, k_{2}). Note also that d is included twice in the last example. This is because we are working with multisets: d is both revealed from [d, k_{1}^{−}] and is free in φ. For the same reason the free name k_{2} is also included in the last example.

The motivation for introducing cores is that these are essentially the terms which matter when deciding static equivalence between two frames φ and φ′: two terms M_{i} ∈ im(φ) and M′_{i} ∈ im(φ′) must be equal up to cores, and whenever two cores N_{i}, N_{j} in φ are related in a certain way (such as by equality or rewrite relations) then the corresponding cores N′_{i}, N′_{j} in φ′ must also be related in the same way.

But the basic definition of cores is insufficient for capturing this intuition. Take for instance the following simple frame:

φ =^{Δ} (νk){^{enc([a,b],k^{+})}/_{x_{1}}, ^{k^{−}}/_{x_{2}}}

Then cores(x_{1}, φ) = {a, b}, but k^{+} is not a core. First of all this means that M = enc(a, k^{+}) cannot be written as a context over cores (since a context cannot contain the private name k). Second, disregarding k^{+} altogether results in a loss of information – the fact that the equality dec(M, k^{−}) =_{E} [a, b] holds is lost. The term k^{+} is inaccessible in the sense that it cannot be deduced by revelation (it is not in the analysis) but still plays an essential role in deciding static equivalence. Or put differently, if we were to replace k^{+} with some other arbitrary term, this would change the analysis of φ.Let us make precise the notion of inaccessible terms.

Definition 17 (Inaccessible Terms). Let φ be any frame and let M ∈ im(φ). A sub-term M|_{w} is inaccessible in M if each of the following conditions hold:

1. M|_{w} ∉ A(φ).

2. for all N ∈ cores(φ) and M^{∗} ∈ st(M|_{w}) it holds that M^{∗} ∉ st(N).

We have argued that basic cores as defined above are insufficient in the presence of inaccessible terms – the inaccessible terms should somehow be taken into account when deciding static equivalence. Inaccessible terms must still have a different status than cores though, for they cannot be “dug out” and used in new settings since they are not part of the analysis; they are stuck in their parent terms. So in addition to cores, we should also take appropriate analysis terms, which contain inaccessible terms, into account. This prompts us to define extended cores thus:

Definition 18 (Extended cores). A term M|_{w} ∈ A(M, S) is a extended core, or ecore, with respect to the set S if either

1. (M|_{w}, w) ∈ core(M, S).

2. There is no context C[x_{1}, …, x_{k}] and no terms M_{1}, …, M_{k} ∈ A(S) such that M|_{w} = C[M_{1}, …, M_{k}].

The set of extended cores of M with respect to S is denoted by ecore(M, S), and as for cores we define ecores(M, φ) = ecores(M, im(φ)∪fn(φ)) and ecores(x, φ) = ecores(xφ, φ). Finally, we define the ecores of a frame φ = (νñ){^{M_{i}}/_{x_{i}}}_{i∈I} as

ecores(φ) = ⋃_{i∈I}{(M_{i}|_{w}, w, i) | (M_{i}|_{w}, w) ∈ ecores(M_{i}, φ)}∪{(n, , ) | n ∈ fn(φ)}

Again we often disregard the position information in ecores. Note that if a term M does not have any inaccessible subterms then ecores(M, φ) = cores(M, φ). Let us consider some examples.

Example 3.2.6. Take the frame φ =^{Δ} (ν∗){^{[enc(a,k_{1}^{+}),enc(b,k_{2}^{+})]}/_{x_{1}}, ^{k_{1}^{−}}/_{x_{2}}} in

the theory E_{pub}. Then

cores(x_{1}, φ) = {a, enc(b, k_{2}^{+})}
ecores(x_{1}, φ) = {enc(a, k_{1}^{+}), enc(b, k_{2}^{+}), a}

Note how each term in im(φ) can now be written as a context over ecores, and how the inaccessible terms are included in ecores while still located in their parent terms. Another way of putting it is that the analysis can be reconstructed from extended cores by applying appropriate function symbols!

Example 3.2.7. Take the frame φ =^{Δ} (ν∗){^{enc(enc(a,k^{+}),k^{+})}/_{x_{1}}, ^{k^{−}}/_{x_{2}}} in the theory E_{pub}. Then

cores(x_{1}, φ) = {a}
ecores(x_{1}, φ) = {enc(enc(a, k^{+}), k^{+}), enc(a, k^{+}), a}

Note that, in this particular example, ecores(x_{1}, φ) = A(x_{1}, φ). Also note that ecores may have other ecores as subterms, which is not the case for standard cores.

In contrast to cores as defined in the Spi calculus, ecores(x, φ) in our new definition is a set, which is natural when considering theories with e.g. pairing. But in the following development it will be necessary to impose a linear ordering on ecores for the purpose of comparing cores with the same index in different frames, which is exactly why we have gone through the trouble of including position information in the definition of ecores.

To define a linear ordering on ecores, first let < be the standard less-than ordering on integers and let ≪ be the standard lexiographic ordering relation on positions (i.e. w_{1} ≪ w_{2} iff w_{1} is lexiographically less than w_{2}). Assume also an arbitrary but fixed ordering ≪≪ on names. An ordering on ecores can then be defined as follows.

Definition 19 (Ordering of ecores). Let φ = (νñ){^{M_{i}}/_{x_{i}}}_{i∈I} be any frame and let (N_{1}, w_{1}, i_{1}), (N_{2}, w_{2}, i_{2}) ∈ ecores(φ). Define N_{1} ≪ N_{2} iff either of the following hold:

1. i_{1} < i_{2}.

2. i_{1} = i_{2} and w_{1} ≪ w_{2}

3. w_{2} = i_{2} = and w_{1} ≠ and i_{1} ≠

4. w_{1} = i_{1} = w_{2} = i_{2} = and N_{1} ≪≪ N_{2}

Informally, order between parent terms has highest priority, position within identical terms has second priority, and ordering on (free) names has third priority.

From now on we will consider ecores as sequences (ordered by ≪) expressed using the notation ecores(φ) = N_{1}, …, N_{k}, or ecores(φ) = (N)_{i∈J}, but will still take the liberty of using set-theoretic notions such as membership. The specifics in the definition of ≪ will play no further role; it has been given above in order to demonstrate that an ordering is indeed possible and well-defined.

3.2.5 Correlated Variables

In the refined definition of strong static equivalence to be given in the next section, we shall consider not only appropriate relationships (such as equality and rewrites) between cores, but also relationships between contexts over cores. In order to limit the complexity of this refined definition and subsequently give a construction of finite characteristic formula, it is crucial that we only consider a restricted class of contexts. To that end we start by defining the notion of correlation between positions and variables in a context.

Definition 20 (Correlated positions and variables). Let L[z̃] > R[z̃] be a rewrite rule and let C[ỹ] be a context which is unifiable with L[z̃]. Let w_{i} and w_{j} be two positions in C[ỹ] and let w′_{i} and w′_{j} be the longest prefixes of w_{i}, respectively w_{j}, such that the position w′_{i}, respectively w′_{j}, exists in L[z̃]. We then say that w_{i} and w_{j} are strongly correlated, written w_{i} ⇄ w_{j}, if v(C[z̃]|_{w′_{i}})∩ v(C[z̃]|_{w′_{j}}) ≠ ∅. If z ∈ v(C[z̃]|_{w′_{i}}) ∩ v(C[z̃]|_{w′_{j}}) we further say that w_{i} and w_{j} are correlated through z and write w_{i} ⇄_{z} w_{j}.

Strong correlation is a reflexive and symmetric binary relation. Define weak correlation, ⇌, to be the transitive closure of strong correlation and say that w_{i}, w_{j} are weakly correlated if w_{i} ⇌ w_{j}.

For each pair of variables y_{i}, y_{j} ∈ v(C[ỹ]) let w̃_{i} and w̃_{j} be the positions of y_{i} and y_{j} in C[ỹ], respectively (there will be multiple positions if a variable has multiple occurrences). We then say that y_{i} and y_{j} are strongly (respectively weakly) correlated if every w_{i} ∈ w̃_{i} is strongly (respectively weakly) correlated to every w_{j} ∈ w̃_{j}.

Correlation is always relative to both a context and a rewrite rule. The definition may seem a little technical at first, but it really just pins down the natural idea that correlated variables are the ones which depend on each other in rewrites. Let us consider an example.

Example 3.2.8. Consider the following extended public key rewrite rule from the theory E_{pub2} (introduced first in Example 2.2.4):

dec(enc(z_{1}, f(z_{2}^{+}, z_{3}^{+})), f(z_{2}^{−}, z_{3}^{−})) > z_{1}

and the context

dec(enc(y_{1}, y_{2}), f(y_{3}, y_{4}^{−}))

Then y_{1} is neither strongly nor weakly correlated to any other variables. y_{3} and y_{4} are strongly correlated to y_{2} but not to each other. They are however weakly correlated to each other. Suppose now that the instance dec(enc(N_{1}, N_{2}), f(N_{3}, N_{4}^{−})), where N_{1}, …, N_{4} are some cores, is an instance of the LHS of the above rewrite rule and hence is reducible. The fact that y_{1} is not correlated to any other variables means that we can substitute N_{1} for any other term N′_{1} and the the rewrite will still be possible. If instead we substitute N_{2} for some N′_{2} the rewrite may no longer be possible, since correlation between y_{2} and the other variables dictates a syntactic constraints on N_{2} in relation to the other cores (for instance N_{2} must contain N_{3} and N_{4} as subterms).

The last example demonstrated how rewrites intuitively depend only on the instantiation of correlated variables. The notion of correlation can therefore be used to define the type of contexts which are relevant for the upcoming refined definition of static equivalence. The contexts which we are interested in for this purpose are the simplest contexts (in a certain precise sense) in which all variable positions are correlated; this intuition is formalised in the following definition of partitioning contexts.

Definition 21 (Partitioning Contexts). A context C^{⊥}[ỹ] is a partitioning context if it is unifiable with the LHS of some rewrite rule L[z̃] > R[z̃] and all of the following hold:

1. y_{i} ⇌ y_{j} for all y_{i}, y_{j} ∈ v(C^{⊥}[ỹ]).

2. C^{⊥}[ỹ]|_{w} = ⊥ implies L[z̃]|_{w} = z for all w and some z ∈ v(L[z̃]).

3. w ⇌̸ w_{i} for all positions w and w_{i} where C^{⊥}[ỹ]|_{w} = ⊥ and C^{⊥}[ỹ]|_{w_{i}} = y_{i} for some y_{i} ∈ v(C^{⊥}[ỹ]).

The first condition says that all variables in the context must be weakly correlated. The second condition says that all occurrences of ⊥ must unify trivially with a variable in the rewrite rule. And the third condition says that no variables are correlated to any occurrence of ⊥; this is a way of expressing that the context is maximal in the sense that it cannot be extended with further variables.

Example 3.2.9. Consider again the extended public key rewrite rule from E_{pub2}:

dec(enc(z_{1}, f(z_{2}^{+}, z_{3}^{+})), f(z_{2}^{−}, z_{3}^{−})) > z_{1}

Then the following are examples of contexts which can easily verified to be partitioning:

• dec(enc(y_{1}, ⊥^{+}, ⊥^{+})), f(⊥^{−}, ⊥^{−})).

• dec(enc(⊥, y_{1}), f(y_{2}, y_{3}^{−})).

• dec(enc(⊥, f(⊥^{+}, y_{1}^{+})), f(⊥^{−}, f(y_{2})^{−})).

The following are examples of contexts which are not partitioning:

• dec(enc(y_{1}, y_{2}), f(y_{3}, y_{4}^{−})) is not partitioning because y_{1} is not strongly correlated to any of the other variables (so condition 1 fails).

• dec(enc(f(⊥), f(y_{1}^{+}, ⊥^{+})), f(y_{2}, ⊥^{−})) is not partitioning because the first position of ⊥ does not match the position of z_{1} (so condition 2 fails).

• dec(enc(⊥, f(⊥^{+}, ⊥^{+})), f(y_{2}, ⊥^{−})) is not partitioning because there is a related context with more correlated variables which is partitioning, e.g. dec(enc(⊥, f(y_{1}, ⊥^{+})), f(y_{2}^{−}, ⊥^{−})) (so condition 3 fails).

The term partitioning context is chosen because correlation is an equivalence relation and hence partitions variables into equivalence classes; all variables in a partitioning context are then in the same equivalence class. Moreover, each equivalence class gives rise to a generated partitioning context, as defined next.

Definition 22 (Generated Partitioning Contexts). Let C[ỹ] be some context which unifies with the LHS of some rewrite rule L[z̃] >_{r} R[z̃] and let ỹ_{1}, …, ỹ_{k} be the partition of ỹ under ⇌.

Then each equivalence class ỹ_{i} generates a (unique) partitioning context C_{i}^{⊥}[ỹ_{i}] defined as follows:

1. C_{i}^{⊥}[ỹ_{i}] is a partitioning context with respect to the rewrite rule r.

3.3. THE REFINED DEFINITION

2. If C^{⊥}[ỹ]|_{w} = y then C_{i}^{⊥}[ỹ_{i}]|_{w} = y for all y ∈ ỹ_{i} and for all positions w.

Example 3.2.10. Take again the rewrite rule extended public key rewrite rule from E_{pub2}

dec(enc(z_{1}, f(z_{2}^{+}, z_{3}^{+})), f(z_{2}^{−}, z_{3}^{−})) >_{r} z_{1}

and consider the following context which unifies with the LHS of this rule:

dec(enc(y_{1}, y_{2}), f(y_{3}, y_{4}^{−}))

As we saw in an earlier example there are two variable equivalence classes, ỹ_{1} = {y_{1}} and ỹ_{2} = {y_{2}, y_{3}, y_{4}}. They generate the following two partitioning contexts:

C_{1}^{⊥}[ỹ_{1}] = dec(enc(y_{1}, f(⊥^{+}, ⊥^{+})), f(⊥^{−}, ⊥^{−}))
C_{2}^{⊥}[ỹ_{2}] = dec(enc(⊥, y_{2}), f(y_{3}, y_{4}^{−}))

In words, if L[z̃] >_{r} R[z̃] is a rewrite rule and the context C[ỹ] unifies with L[z̃], then the partitioning context generated from the equivalence class ỹ_{i} is obtained by preserving the part of C[ỹ] which contains ỹ_{i} and simplifying the rest with ⊥ to match L[z̃]. So intuitively, any generated partitioning context will also unify with L[z̃]. Furthermore, if C[Ñ] (i.e. the context instantiated with cores) unifies with L[z̃], then so will the instance C_{i}[Ñ] of every genererating partitioning context. This observation will play a key role in the proofs to be given later in the report.

3.3 The Refined Definition

In this section a refined definition of strong static equivalence which is amenable to the construction of characteristic formulae will be given based on the notions introduced in the last section.

First recall from Subsection 2.2.1 that a term M_{1} is less general than a term M_{2} if there is some substitution θ such that M_{1} = M_{2}θ; if this is the case, we write M_{1} ⊏ M_{2} in the following. Similarly, we say that M_{1} is more general than M_{2}, written M_{1} ⊐ M_{2}, if there exists some substitution θ such that M_{2} = M_{1}θ. Finally, we shall write M_{1}□M_{2} to mean that M_{1} and M_{2} are unifiable but neither is more or less general than the other, i.e. there exists a unifying substitution θ such that M_{1}θ = M_{2}θ, M_{1} ⊐̸ M_{2} and M_{1} ⊏̸ M_{2}.

We shall mainly be interested in asserting generality on contexts in relation to the LHS of some rewrite rule. For this purpose we also define ⊏, ⊐ and □ as unary relation symbols, and write e.g. C[ỹ]□ if there exists a rewrite rule L[z̃] >_{r} R[z̃] in the relevant TRS such that C[ỹ]□L[z̃] (and similarly for ⊏ and ⊐). With these notions we are now ready to state the refined definition of strong static equivalence.

Definition 23 (Refined Strong Static Equivalence). Let φ ≡ (νñ){^{M_{i}}/_{x_{i}}}_{i∈I} and φ′ ≡ (νñ){^{M′_{i}}/_{x_{i}}}_{i∈I} be two frames with ecores(φ) = (N)_{j∈J}, ecores(φ′) = (N′)_{j∈J}. Then φ and φ′ are strong statically equivalent, written φ ≈′_{ss} φ′, if dom(φ) = dom(φ′) and each of the following conditions hold:

1. For each i ∈ I there is some context C[ỹ] such that

• M_{i} = C[Ñ]

• M′_{i} = C[Ñ′]

2. For any context C[ỹ] and for all j ∈ J it holds that

C[Ñ] = N_{j} ⇔ C[Ñ′] = N′_{j}

3. For any partitioning context C_{1}^{⊥}[ỹ] where C_{1}^{⊥}[ỹ] ⊐ or C^{⊥}[ỹ]□ it holds for all C_{2}^{⊥}[ỹ] that

C_{1}^{⊥}[Ñ] >_{r} C_{2}^{⊥}[Ñ] ⇔ C_{1}^{⊥}[Ñ′] >_{r} C_{2}^{⊥}[Ñ′]

Condition 1 requires that each M_{i} ∈ im(φ) and M′_{i} ∈ im(φ′) are equal up to ecores. For this to be well defined, there must be at least one context C[ỹ] such that M_{i} = C[Ñ], i.e. all terms in a frame can be written as a context over ecores. This fact is established in the following easy lemma; indeed a slightly stronger result is proven, namely that any analysis term can be written as a context over ecores.

Lemma 1. Let φ be any frame with ecores(φ) = (N)_{j∈J}. Then for any M ∈ A(φ) there exists a context C[ỹ] such that M = C[Ñ].

Proof. By induction in the height of the parse tree of M.

Basis. Then M = a for some name a. If a ∈ bn(φ) then a = N_{j} for some ecore N_{j} since a can only be included in the analysis by revelation and a cannot be further reduced by revelation. Hence the context is the trivial context C_{i}[ỹ] = y_{j}. If a ∈ fn(φ) then a is per definition an ecore, so again the context is the trivial context.

Step. If M is an ecore, i.e. M = N_{j} for some j ∈ J, then the context is the trivial context C_{i}[ỹ] = y_{j}. Otherwise it follows from the definition of ecores that there must be some context C[x_{1}, …, x_{k}] and terms M_{1}, …, M_{k} ∈ A(φ) such that M = C[M_{1}, …, M_{k}]. Applying the induction hypothesis to each M_{i} we get that M_{i} = C_{i}[Ñ] for some context C_{i}[ỹ] and Ñ ⊆ ecores(φ). Hence M = C[C_{1}[Ñ], …, C_{2}[Ñ]] which concludes the proof.

This lemma, together with condition 2, gives that condition 1 in fact holds for all contexts.

3.4. EXAMPLES

One may fear that this refined definition ≈′_{ss} is no better than ≈_{ss}, since conditions 2 and 3 contain universal quantifications over contexts. When constructing characteristic formulae for a frame φ it is necessary to express both which equalities from condition 2 on the form C[Ñ] = N_{j} do hold, but also which do not hold. The key point here is that there are only finitely many equalities on the form C[Ñ] = N_{j} which do hold since there are only a finite number of cores each of finite size. We will see in the next chapter how an appropriate semantics for quantifiers in our first-order logic of frames will allow us to give a finite formulae expressing all the negative equalities.

A similar concern arises in condition 3. There are only finitely many partitioning contexts which are more general than the LHS of some rewrite rule, but there are infinitely many contexts which are unifiable with, but neither less general than nor more general than, the LHS of some rewrite rule. Take for example the public key rewrite rule; then the following infinite sequence of partitioning contexts satisfy this:

dec(enc(⊥, y_{1}), y_{2}),
dec(enc(⊥, y_{1}^{+}), y_{2}),
dec(enc(⊥, f(y_{1})^{+}), y_{2}),
dec(enc(⊥, f(f(y_{1}))^{+}), y_{2}),
…

The key point is that because the contexts are partitioning contexts and because there are only finitely many many cores, there are a finite number of instantiations which are reducible. Quantification in the logic will then allow us to give finite formulae expressing all the instantiations which are not reducible.

If we had also included in condition 3 contexts which are less general than the LHS of some rewrite rule, then the situation would be different. For there would be infinitely many instantiations of this kind of context which are reducible as well as infinitely many instantiations which are not reducible. Luckily these contexts need not be taken into account explicitly in the definition, for as we shall see later a rewrite condition for this kind of context follows from condition 2.

3.4 Examples

The conditions in ≈′_{ss} have been carefully devised with the aim that ≈′_{ss} and ≈_{ss} should coincide. That this is indeed the case is not trivially obvious. The next section develops a proof of coincidence between the two definitions, but first we proceed in this section with some motivating examples which shed some light onto the workings of the refined definition and gives us confidence in its sanity. The examples will be based on the theories of symmetric key encryption E_{sym}, public key encryption E_{pub} and extended public key encryption E_{pub2} which were introduced in Chapter 2. Whenever we consider two frames φ and φ′ we will let N_{i} range over ecores(φ) and N′_{i} range over ecores(φ′).

Example 3.4.1. Consider the following frames in the theory E_{sym}:

φ = (νa, k, c){^{enc(enc(a,k),c)}/_{x_{1}}, ^{c}/_{x_{2}}}
φ′ = (νa, k, c){^{enc(enc(enc(a,k),k),c)}/_{x_{1}}, ^{c}/_{x_{2}}}

These are clearly strong statically equivalent, and indeed all the conditions of ≈′_{ss} are satisfied. The ecores are as follows:

N_{1} = enc(a, k)  N′_{1} = enc(enc(a, k), k)
N_{2} = c  N′_{2} = c

This illustrates the intuition that the two frames are equal up to ecores (i.e. condition 1 holds) and that ecores cannot be distinguished by testing syntactic equality or by testing reductions.

Example 3.4.2. Consider the following frames, again in the theory E_{sym}, which are identical to the frames from the last example except an unknown key k in φ′ has been replaced by a known key c:

φ = (νa, c, k){^{enc(enc(a,k),c)}/_{x_{1}}, ^{c}/_{x_{2}}}
φ′ = (νa, c, k){^{enc(enc(enc(a,k),c),c)}/_{x_{1}}, ^{c}/_{x_{2}}}

This change results in the two frames not being strong statically equivalent because the equality

x_{1} =_{E} enc(dec(dec(x_{1}, x_{2}), x_{2}), x_{2})

holds in φ′ but not in φ. The ecores of the two frames are

N_{1} = enc(a, k)  N′_{1} = enc(a, k)
N_{2} = c  N′_{2} = c

Condition 1 of ≈′_{ss} then captures the difference between the two frames because the first term from φ can only be written as enc(N_{1}, N_{2}) while the first term from φ′ can only be written as enc(enc(N_{1}, N_{2}), N_{2}), and the relevant contexts are thus not the same. Note however that the cores in the two frames are exactly the same (namely a and c), so φ and φ′ could not have been distinguished using only condition 2 and 3 in ≈′_{ss}. Hence condition 1 is strictly necessary.

Example 3.4.3. Consider the following frames in the theory E_{pub}, which are similar to the frames from the previous example except that they use public key encryption instead of symmetric key encryption:

φ = (νa, c, k){^{enc(enc(a,k^{+}),c^{+})}/_{x_{1}}, ^{c^{−}}/_{x_{2}}}
φ′ = (νa, c, k){^{enc(enc(enc(a,k^{+}),c^{+}),c^{+})}/_{x_{1}}, ^{c^{−}}/_{x_{2}}}

This time the two frames should not be strong statically equivalent because the term

dec(dec(x_{1}, x_{2}), x_{2})

can reduce in two steps in φ′ but only in one step in φ. The public key k^{+} is not in the analysis of the above frames, so the ecores are given as follows:

N_{1} = enc(enc(a, k^{+}), c^{+})  N′_{1} = enc(enc(enc(a, k^{+}), c^{+}), c^{+})
N_{2} = enc(a, k^{+})  N′_{2} = enc(enc(a, k^{+}), c^{+})
N′_{3} = enc(a, k^{+})
N_{4} = c^{−}  N′_{4} = c^{−}

(note that N_{3} does not exist in φ). The two frames are then distinguished by condition 3 which fails because dec(N′_{2}, N′_{4}) > N′_{3}, while this does not hold for the corresponding cores from φ. Note that the context employed in this reduction is valid for use in condition 3 of ≈′_{ss} (it is partitioning and less general than the LHS of the decryption rule).

Note also that condition 1 in ≈′_{ss} cannot be used to distinguish the two frames as it could in the previous example. For the empty trivial context C[ỹ] = y_{1} satisfies condition 1: M_{1} = N_{1} and M′_{1} = N′_{1}.

This example thus illustrates the crucial role of extended cores and their contained inaccessible terms: if k^{+} were not retained in an ecore then no rewrite could distinguish φ and φ′.

Example 3.4.4. Consider the following very simple frames (in any theory with hash functions f(·) and g(·)) where the name a is free:

φ = {^{f(a)}/_{x}}
φ′ = {^{g(a)}/_{x}}

These frames are not strong statically equivalent because the equality f(a) = x holds in φ but not in φ′. An environment can test this equality because the name a is free.

Recall now that we have defined free names to be ecores and hence we have that

N_{1} = f(a)  N′_{1} = g(a)
N_{2} = a  N′_{2} = a

and condition 2 can now be used to distinguish the two frames since f(N_{2}) = N_{1} holds but f(N′_{2}) = N′_{1} does not.

This example hence illustrates the necessity of condition 2 and that taking contexts into account is indeed necessary. If condition 2 were weakened to require only that two cores N_{i} and N_{j} are equal if and only if N′_{i} and N′_{j} are equal (as in [9]), frames involving hash functions akin to φ and φ′ would not be distinguished. This would have wide implications for any theories which may exhibit hash-like behaviour, such as public key encryption would do in cases where a public key is known but the corresponding private key is not.

Example 3.4.5. Consider the following frames (in a theory with pairing, e.g. E_{sym}):

φ = (νa, b){^{[a,b]}/_{x_{1}}, ^{[a,b]}/_{x_{2}}}
φ′ = (νa, b){^{[a,b]}/_{x_{1}}, ^{[b,a]}/_{x_{2}}}

These are not strong statically equivalent because fst(x_{1}) =_{E} fst(x_{2}) holds in φ but not in φ′. Again this is captured by the the second condition of ≈′_{ss}; we have that

N_{1} = a  N′_{1} = a
N_{2} = b  N′_{2} = b
N_{3} = a  N′_{3} = b
N_{4} = b  N′_{4} = a

so N_{1} = N_{3} but N′_{1} ≠ N′_{3}. Hence, here the relevant context is just the trivial context y_{1} instantiated to the core N_{1}. It follows that condition 2 also requires, as a special case, that whenever two cores in φ are equal, the corresponding cores in φ′ must also be equal. This example also serves to illustrate than an ordering on cores is indeed necessary.

Example 3.4.6. Consider the following frames in a theory with hash functions f(·) and g(·):

φ = (νa, b){^{f(a)}/_{x_{1}}, ^{g(b)}/_{x_{2}}}
φ′ = (νa, b){^{a}/_{x_{1}}, ^{b}/_{x_{2}}}

These are clearly strong statically equivalent, and it is easy to see that all conditions of ≈′_{ss} hold. Suppose however that we are working in a theory with the rewrite rule

f(z_{1}) + g(z_{2}) >_{r} f(z_{1})

In that case φ ≉_{s} φ′ since the equality x_{1} + x_{2} =_{E} x_{1} holds in φ but not in φ′. This example serves to illustrate the need for condition 3 which captures this equality, and without which the two frames would be strong statically equivalent according to the new definition.

3.5 Summary

We have given a refined version of strong static equivalence which goes some of the way towards a construction of characteristic formulae, although the refined definition still relies on quantification over a certain type of contexts (namely partitioning contexts).

In support of the refined definition, we have introduced a number of concepts: revelation is a binary relation which expresses when a term can reveal one of its subterms (e.g. by decryption with an appropriate key); the analysis of a frame is is the set of terms obtained by repeated revelation from the frame; cores are the terms from the analysis which are minimal under revelation; ecores are an extension of cores with additional information indispensable for deciding strong static equivalence; correlated variables and partitioning contexts are required to bound the number of contexts considered in the refined definition of strong static equivalence.

Finally, a number of examples have been given which have strengthened our belief in the refined definition of strong static equivalence.

Results On The Refined Definition

The refined definition of strong static equivalence, ≈′_{ss}, presented in the previous chapter has been devised with the intention that it should coincide with ≈_{ss}. In this chapter we prove that this indeed is the case. Section 1 shows one direction, namely that ≈′_{ss} implies ≈_{ss} (or more precisely that ≈′_{ss}⊆≈_{ss}), while Section 2 shows the other direction that ≈_{ss} implies ≈′_{ss} (≈_{ss}⊆≈′_{ss}).

We have already seen that ≈_{ss} and ≈_{s} do not coincide in general. But in theories in which inaccessible terms do not exist, including symmetric key theories and public key theories where public keys are always known, they do coincide. We show this result in Section 3.

4.1 ≈′_{ss} implies ≈_{ss}

The main theorem of this section states that ≈′_{ss} implies ≈_{ss}. In order to prove this result a number of preliminary lemmas are required. One of the key lemmas states that if φ ≈′_{ss} φ then it holds for any contexts C_{1}[ỹ] and C_{2}[ỹ] that

C_{1}[Ñ] =_{E} C_{2}[Ñ] ⇔ C_{1}[Ñ′] =_{E} C_{2}[Ñ′]

The proof of this in turn relies on a lemma stating that rewrites are preserved by substitution of cores:

C_{1}[Ñ] > C_{2}[Ñ] ⇔ C_{1}[Ñ′] > C_{2}[Ñ′]

and a lemma stating that syntactic equality is preserved by substitution of cores:

C_{1}[Ñ] = C_{2}[Ñ] ⇔ C_{1}[Ñ′] = C_{2}[Ñ′]

We start by attacking the latter result, which is expressed formally in the following lemma.

CHAPTER 4. RESULTS ON THE REFINED DEFINITION

Figure 4.1: Illustration of the two cases and the terms involved.

C_{1}[− − −\overbrace{− − \underbrace{∗ ∗ ∗ ∗ ∗} −−_{discrepancy at w}}^{C_{1}[Ñ′]|_{w′} =N′_{j}} − −−] ≠ C_{2}[− − −\overbrace{− − \underbrace{∗ ∗ ∗ ∗ ∗} −−_{discrepancy at w}}^{C_{2}[Ñ′]|_{w′} =C[Ñ′]} − −−]

(a) The first case.

C_{1}[− − −\overbrace{− − \underbrace{∗ ∗ ∗ ∗ ∗} −−_{discrepancy at w}}^{C_{1}[Ñ′]|_{w′} =N′_{j}} − −−] ≠ C_{2}[−\overbrace{− − \overbrace{− − \underbrace{∗ ∗ ∗ ∗ ∗} −−_{discrepancy at w}}^{C_{2}[Ñ′]|_{w′} ∈st(N′_{i})}−}^{C_{2}[Ñ′]|_{w′′} =N′_{i}}−]

(b) The second case.

Lemma 2. Let φ and φ′ be two frames with φ ≈′_{ss} φ′, ecores(φ) = (N)_{j∈J} and ecores(φ′) = (N′)_{j∈J}. It then holds for any contexts C_{1}[ỹ] and C_{2}[ỹ] that

C_{1}[Ñ] = C_{2}[Ñ] ⇔ C_{1}[Ñ′] = C_{2}[Ñ′]

Proof. We show the direction from left to right; the converse is symmetric. Suppose that C_{1}[Ñ] = C_{2}[Ñ] and suppose for a contradiction that C_{1}[Ñ′] ≠ C_{2}[Ñ′]. Then the two contexts must differ at some position, so let w be a position of greatest length such that C_{1}[Ñ′]|_{w} ≠ C_{2}[Ñ′]|_{w}. Now there must be a prefix w′ of w and an ecore N′_{j} such that either C_{1}[Ñ′]|_{w′} = N′_{j} or C_{2}[Ñ′]|_{w′} = N′_{j}; for otherwise C_{1}[Ñ] ≠ C_{2}[Ñ], contrary to assumption. Suppose the former without loss of generality, i.e. N′_{j} is an ecore in the first context which captures the discrepancy between the LHS and the RHS. There are now two cases to consider – each is illustrated in Figure 4.1 and covered below.

1. There is some context C[ỹ] such that C_{2}[ỹ]|_{w′} = C[ỹ]. Since C_{1}[Ñ′]|_{w′} ≠ C_{2}[Ñ′]|_{w′} per choice of w′ we then have that N′_{j} ≠ C[Ñ′]. Condition 2 in the definition of ≈′_{ss} gives that also N_{j} ≠ C[Ñ], i.e. C_{1}[Ñ]|_{w′} ≠ C_{2}[Ñ]|_{w′}. Hence C_{1}[Ñ] ≠ C_{2}[Ñ], giving the desired contradiction.

2. The position w′ does not exist in C_{2}[ỹ], i.e. C_{2}[Ñ′]|_{w′} is a subterm of some core N′_{i} in C_{2}[Ñ′]. Then there is some prefix w′′ of w and context C[ỹ] such that N′_{i} = C_{2}[Ñ′]|_{w′′}. Also, there is some context C_{1}^{∗}[ỹ] such that C_{1}[Ñ′]|_{w′′} = C_{1}^{∗}[Ñ′]. We have that C_{1}[Ñ′]|_{w′′} ≠ C_{2}[Ñ′]|_{w′′} and hence that C_{1}^{∗}[Ñ′] ≠ N′_{i}. The contradiction is then obtained in the same manner as for case 1.

Next we turn our attention to showing that arbitrary rewrites are preserved by substitution of ecores. This is accomplished in three steps:

\underline{4.1. ≈′_{SS} IMPLIES ≈_{SS}}

1. Show that primitive rewrites on any partitioning context is preserved by substitution of ecores. Condition 3 in ≈′_{ss} gives that this result holds for any partitioning contexts which are not more specific than the LHS of some rewrite rule. We rely on condition 2 to show that substitution of ecores also works for partitioning contexts which are more specific than the LHS of some rewrite rule.

2. Show that primitive rewrites on any context (i.e. not necessarily partitioning) are preserved by substitution of ecores. For this we rely on the notion of generated partitioning contexts.

3. Show that any rewrites (i.e. not necessarily primitive) on any context are preserved by substitution of ecores.

Each of the three steps is covered by a separate lemma.

Lemma 3. Let φ and φ′ be two frames with φ ≈′_{ss} φ′, ecores(φ) = (N)_{j∈J} and ecores(φ′) = (N′)_{j∈J}. It then holds for any partitioning context C_{1}^{⊥}[ỹ] and any context C_{2}^{⊥}[ỹ] that:

C_{1}^{⊥}[Ñ] >_{r} C_{2}^{⊥}[Ñ] ⇔ C_{1}^{⊥}[Ñ′] >_{r} C_{2}^{⊥}[Ñ′]

Proof. We show the direction from left to right; the converse is symmetric. Suppose that C_{1}^{⊥}[Ñ] >_{r} C_{2}^{⊥}[Ñ] by virtue of rule r : L[z̃] >_{r} R[z̃]. If C_{1}^{⊥}[Ñ] ⊐ L[z̃] or C_{1}^{⊥}[Ñ]□L[z̃] the result follows immediately from condition 3 in ≈′_{ss}, so suppose that C_{1}^{⊥}[Ñ] ⊏ L[z̃]

Per definition of primitive rewrites and the assumption that C_{1}^{⊥}[ỹ] is less general than L[z̃], there exists a substitution θ = {^{T_{i}}/_{z_{i}}}_{i∈I} such that C_{1}^{⊥}[Ñ] = L[z̃]θ and C_{2}^{⊥}[Ñ] = R[z̃]θ. It must be shown that there is some substitution θ′ such that C_{1}^{⊥}[Ñ′] = L[z̃]θ′ and C_{2}^{⊥}[Ñ′] = R[z̃]θ′. Say that there are k occurrences of z_{i} in L[z̃]. Then since each position w_{j} of an occurrence of z_{i} (i.e. with L[z̃]|_{w_{j}} = z_{i}) also exists in C_{1}^{⊥}[ỹ], the subterm C_{1}^{⊥}[Ñ]|_{w_{j}} is in fact a context over ecores. Hence we have that

T_{i} = C_{1}^{⊥}[Ñ]|_{w_{1}} =, …, = C_{1}^{⊥}[Ñ]|_{w_{k}}

and it follows by Lemma 2 that also

T′_{i} = C_{1}^{⊥}[Ñ′]|_{w_{1}} =, …, = C_{1}^{⊥}[Ñ′]|_{w_{k}}

Hence C_{1}^{⊥}[Ñ′] and C_{2}^{⊥}[Ñ′] are instances of L[z̃] and R[z̃] respectively, with unifying substitution θ′ = {^{T′_{i}}/_{z_{i}}}_{i∈I}.

Lemma 4. Let φ and φ′ be two frames with φ ≈′_{ss} φ′, ecores(φ) = (N)_{j∈J} and ecores(φ′) = (N′)_{j∈J}. It then holds for any contexts C_{1}[ỹ] and C_{2}[ỹ] that

C_{1}[Ñ] >_{r} C_{2}[Ñ] ⇔ C_{1}[Ñ′] >_{r} C_{2}[Ñ′]

Proof. We show the direction from left to right; the converse is symmetric. Suppose that C_{1}[Ñ] >_{r} C_{2}[Ñ] by virtue of some rewrite rule L[z̃] >_{r} R[z̃], i.e. C_{1}[Ñ] is an instance of L[z̃]. This also means that C_{1}[ỹ] and L[z̃] are unifiable with some unifying substitution θ = {^{T_{a}}/_{z_{a}}}_{a∈A}{^{S_{b}}/_{y_{b}}}_{b∈B}. C_{1}[Ñ] satisfies the constraints in θ in the sense that if e.g. θ = {^{f(y_{1})}/_{y_{2}}} then it must hold that N_{2} = f(N_{1}). In general, the substitution θ can be viewed as a set of constraints which must be satisfied in order for any instance of C_{1}[ỹ] to be reducible.

Let ỹ_{1}, …, ỹ_{k} be the partition into equivalence classes of ỹ with respect to ⇌. The key observation is that whenever C_{1}[Ñ] is an instance of L[z̃] it also holds for every generated partitioning context C_{i}^{⊥}[ỹ_{i}] that C_{i}^{⊥}[Ñ_{i}] is an instance of L[z̃]. To see this, let θ_{i} be the unifying substitution for C_{i}^{⊥}[ỹ] and L[ỹ] (a such exists per definition of partitioning contexts). Suppose for a contradiction that C_{i}^{⊥}[Ñ] does not satisfy the constraints in θ_{i}. Any variable z ∈ z̃ which does not join correlated variables unifies trivially with some ⊥ per construction of partitioning contexts. So the only constraint which can fail is a constraint on some of the ecores in C_{i}^{⊥}[Ñ]. But these constraints are inherited from θ and hence also fail for C_{1}[Ñ]. This contradicts the assumption that C_{1}[Ñ] is an instance of L[˜].

Now suppose for a contradiction that that C_{1}[Ñ′] ≯_{r} C_{2}[Ñ′], i.e. some constraints in θ fail for this instantiation. Then there must be a generated partitioning context C_{i}^{⊥}[ỹ] such that C_{i}^{⊥}[Ñ′] fails some of the same constraints in θ, i.e. C_{i}^{⊥}[Ñ′] ≯_{r}. By Lemma 3 it also holds that C_{i}^{⊥}[Ñ] ≯_{r}, contrary to the observation above.

We conclude that also C_{1}[Ñ′] >_{r} C_{2}[Ñ′] as desired.

Lemma 5. Let φ and φ′ be two frames with φ ≈′_{ss} φ′, ecores(φ) = (N)_{j∈J} and ecores(φ′) = (N′)_{j∈J}. It then holds for any contexts C_{1}[ỹ] and C_{2}[ỹ] that

C_{1}[Ñ] > C_{2}[Ñ] ⇔ C_{1}[Ñ′] > C_{2}[Ñ′]

Proof. We show the direction from the left to right; the converse follows by symmetry. So suppose that C_{1}[Ñ] > C_{2}[Ñ]. Per definition of the rewrite relation, there is some subterm C_{1}[Ñ]|_{w} which matches the redex of a rewrite rule r and therefore rewrites primitively: C_{1}[Ñ]|_{w} >_{r} C_{1}[Ñ]|_{w_{2}} (note that the redex must also be a context over ecores since we are working in subterm theories). Then C_{2}[Ñ] = C_{1}[Ñ]{^{C_{1}[Ñ]|_{w_{2}}}/_{C_{1}[Ñ]|_{w}}}. By Lemma 4 C_{1}[Ñ′]|_{w} >_{r} C_{1}[Ñ′]|_{w_{2}} and by Lemma 2 also C_{2}[Ñ′] = C_{1}[Ñ′]{^{C_{1}[Ñ′]|_{w_{2}}}/_{C_{1}[Ñ′]|_{w}}}. We then conclude, per definition of the reduction relation, that C_{1}[Ñ′] > C_{2}[Ñ′].

We are now ready to state the main lemma of this section, namely that equality is preserved by substitution of ecores from statically equivalent frames.

Lemma 6. Let φ and φ′ be two frames with φ ≈′_{ss} φ′, ecores(φ) = (N)_{j∈J} and ecores(φ′) = (N′)_{j∈J}. It then holds for any contexts C_{1}[ỹ] and C_{2}[ỹ] that

C_{1}[Ñ] =_{E} C_{2}[Ñ] ⇔ C_{1}[Ñ′] =_{E} C_{2}[Ñ′]

Proof. We show the implication from left to right (the converse then follows by symmetry), so suppose that C_{1}[Ñ] =_{E} C_{2}[Ñ]. Since the relation =_{E} coincides with <>^{∗} (the reflexive, symmetric and transitive closure of the rewrite relation), we also have that C_{1}[Ñ] <>^{∗} C_{2}[Ñ]. Since we are working with convergent theories there is a C_{3}[Ñ] = C_{1}[Ñ] ↓= C_{2}[Ñ] ↓. Hence it holds that C_{1}[Ñ] >^{k_{1}} C_{3}[Ñ] and C_{2}[Ñ] >^{k_{2}} C_{3}[Ñ] for some k_{1}, k_{2} ∈ ℕ. We will show that these reduction sequences are preserved by substitution of ecores from φ′, i.e. that also C_{1}[Ñ′] >^{k_{1}} C_{3}[Ñ′] and C_{2}[Ñ′] >^{k_{2}} C_{3}[Ñ′].

We give a proof of the first case by induction in k_{1}. Basis (k_{1} = 0). Then we have that C_{1}[Ñ] = C_{3}[Ñ], and it follows by Lemma 2 that also C_{1}[Ñ′] = C_{3}[Ñ′]. Step (assume for k_{1}, prove for k_{1} + 1). In this case we have that C_{1}[Ñ] > M >^{k_{1}} C_{3}[Ñ] for some M. The crucial point is that M can be written as a context over ecores since it is a subterm of a context over ecores, i.e. M = C_{4}[Ñ] for some C_{4}[ỹ]. So we have that C_{1}[Ñ] > C_{4}[Ñ] >^{k_{1}} C_{3}[Ñ]. By Lemma 5 it also holds that C_{1}[Ñ′] > C_{4}[Ñ′]. The induction hypothesis gives that C_{4}[Ñ′] >^{k_{1}} C_{3}[Ñ′]. Hence C_{1}[Ñ′] >^{k_{1}+1} C_{3}[Ñ′] as desired.

The proof that C_{2}[Ñ′] >^{k_{2}} C_{3}[Ñ′] is identical. It follows immediately that C_{1}[Ñ′] ↓= C_{2}[Ñ′] ↓ and by assumption of convergent subterm theories that C_{1}[Ñ′] <>^{∗} C_{2}[Ñ′]. Hence also C_{1}[Ñ′] =_{E} C_{2}[Ñ′], which concludes the proof.

The above proof relies crucially on confluence for working on >^{∗} instead of on <>^{∗}. It would be impossible to carry out the induction on reduction sequences on the form C_{1}[Ñ] <>^{∗} C_{2}[Ñ]. For suppose the first step in this sequence is C_{1}[Ñ] < M <>^{∗} C_{2}[Ñ]. Then it would not necessarily be possible to write M as a context over ecores; for example we might have that a < fst[a, b] <>^{∗} snd[b, a] where b is private in φ and where fst[a, b] therefore cannot be written as any context over ecores. Consequently neither Lemma 2 nor the induction hypothesis can be applied.

One might also attempt to give an alternative proof directly from the definition of =_{E}; this would go by induction in the height of the proof tree of the equality C_{1}[Ñ] =_{E} C_{2}[Ñ]. However this approach presents some difficulties. First of all, there is a universal quantification over substitutions in the Substitution rule. This can be overcome by replacing the Substitution and the Rewrite rule with the following new rule:

(Primitive Rewrite)\overline{M_{1} =_{E} M_{2}} if M_{1} >_{r} M_{2}

It is easy to prove that the equational theory induced based on this new rule is the same as the theory induced by the standard definition. Intuitively, instead of instantiating variables at arbitrary positions in the proof of an equality, the variable could just as well have been instantiated at time of introduction.

However one problem with an induction in the height of the proof tree of C_{1}[Ñ] =_{E} C_{2}[Ñ] remains, namely the transitivity case. The premises would give that C_{1}[Ñ] =_{E} M and M =_{E} C_{2}[Ñ], but it is not necessarily possible to write M as a context over ecores and thus the induction hypothesis does not apply. There does not seem to be any easy solution to this problem, so a direct proof on =_{E} fails for this lemma.

We now arrive at the main result of this section:

Theorem 1. ≈′_{ss} implies ≈_{ss}.

Proof. Let φ ≡ (νñ){^{M_{i}}/_{x_{i}}}_{i∈I} and φ′ ≡ (νñ){^{M′_{i}}/_{x_{i}}}_{i∈I} be two frames with φ ≈′_{ss} φ′ and let ecores(φ) = (N)_{j∈J} and ecores(φ′) = (N′)_{j∈J}. We must show that the two conditions in ≈_{ss} both hold.

Condition 1 Let M_{1} and M_{2} be any two terms. We must show that (M_{1} =_{E} M_{2})φ ⇔ (M_{1} =_{E} M_{2})φ′; we show the implication from left to right, as the converse is symmetric. So suppose that (M_{1} =_{E} M_{2})φ, i.e. n(M_{1}, M_{2})∩bn(φ) = ∅ and M_{1}φ =_{E} M_{2}φ. This means that M_{1} and M_{2} are in fact context over variables from φ and some free names ñ, so we reason as follows:

M_{1}φ =_{E} M_{2}φ
C_{M_{1}}[x_{a_{1}}, …, x_{a_{s}}, ñ]φ =_{E} C_{M_{2}}[x_{b_{1}}, ⋯, x_{b_{t}}, ñ]φ  ⇕
C_{M_{1}}[x_{a_{1}}φ, …, x_{a_{s}}φ, ñ] =_{E} C_{M_{2}}[x_{b_{1}}φ, ⋯, x_{b_{t}}φ, ñ]  ⇕
C_{M_{1}}[M_{a_{1}}, …, M_{a_{s}}, ñ] =_{E} C_{M_{2}}[M_{b_{1}}, …, M_{b_{t}}, ñ]

Condition 1 in the definition of ≈′_{ss} says that each M ∈ im(φ) can be written as a context over ecores, and since each free name in φ is also an ecore we have that ñ = Ñ and hence:

C_{M_{1}}[C_{a_{1}}[Ñ], …, C_{a_{s}}[Ñ], Ñ] =_{E} C_{M_{2}}[C_{b_{1}}[Ñ], ⋯, C_{b_{t}}[Ñ], Ñ]

Next apply Lemma 6:

C_{M_{1}}[C_{a_{1}}[Ñ′], …, C_{a_{s}}[Ñ′], Ñ′] =_{E} C_{M_{2}}[C_{b_{1}}[Ñ′], ⋯, C_{b_{t}}[Ñ′], Ñ′]

By condition 1 of ≈′_{ss} again, each context C_{a_{i}}[Ñ′] is syntactically equal to the corresponding term M′_{a_{i}} ∈ im(φ′). We also have that ecores which represent free names are identical in the two frames. Hence:

C_{M_{1}}[M′_{a_{1}}, …, M′_{a_{s}}, ñ] =_{E} C_{M_{2}}[M′_{b_{1}}, …, M′_{b_{t}}, ñ]
C_{M_{1}}[x_{a_{1}}φ′, …, x_{a_{s}}φ′, ñ] =_{E} C_{M_{2}}[x_{b_{1}}φ′, ⋯, x_{b_{t}}φ′, ñ]  ⇕
M_{1}φ′ =_{E} M_{2}φ′

Finally, since bn(φ) = bn(φ′) we get that (M_{1} =_{E} M_{2})φ′ as desired, concluding the proof of condition 1 in ≈_{ss}.

\underline{4.2. ≈_{SS} IMPLIES ≈′_{SS}}

Condition 2. Let M be any term. We must show that (M >_{φ}^{k}) ⇔ (M >_{φ′}^{k}); we do the implication from left to right as the converse follows by symmetry. So suppose that (M >_{φ}^{k}), i.e. n(M) ∩ bn(φ) = ∅ and there is some M^{k} such that Mφ >^{k} M^{k}. In other words, there is a sequence of rewrites Mφ > M^{1} > ⋯ > M^{k}. As in the proof of condition 1 it follows by the condition on names that M is in fact a context over terms from φ and free names, and we reason as follows:

Mφ = C_{M}[x_{a_{1}}, ⋯, x_{a_{s}}, ñ]φ
= C_{M}[x_{a_{1}}φ, ⋯, x_{a_{s}}φ, ñ]
= C_{M}[M_{a_{1}}, ⋯, M_{a_{s}}, ñ]
= C_{M}[C_{a_{1}}[Ñ], ⋯, C_{a_{s}}[Ñ], Ñ]

Again the last step follows from condition 1 in the definition of ≈′_{ss}, which says that each M ∈ im(φ) can be written as a context over ecores.

Since we are working in subterm theories, each of the reducts M^{i} are subterms of Mφ and hence can also be written as a context over ecores and free names. We then have the following sequence of rewrites:

C_{M}[C_{a_{1}}[Ñ], ⋯, C_{a_{s}}[Ñ], Ñ] > C_{1}[Ñ] > ⋯ > C_{k}[Ñ]

and by Lemma 5 the corresponding rewrites on ecores in φ′ also hold:

C_{M}[C_{a_{1}}[Ñ′], ⋯, C_{a_{s}}[Ñ′], Ñ′] > C_{1}[Ñ′] > ⋯ > C_{k}[Ñ′]

By condition 1 of ≈′_{ss} again, each context C_{a_{i}}[Ñ′] is syntactically equal to the corresponding term M′_{a_{i}} ∈ im(φ′), and the free names are the same in the two frames:

C_{M}[M′_{a_{1}}, ⋯, M′_{a_{s}}, ñ] > C_{1}[Ñ′] > ⋯ > C_{k}[Ñ′]
C_{M}[x_{a_{1}}, ⋯, x_{a_{s}}, ñ]φ′ > C_{1}[Ñ′] > ⋯ > C_{k}[Ñ′]  ⇕
Mφ′ > C_{1}[Ñ′] > ⋯ > C_{k}[Ñ′]

Hence (M >_{φ′}^{k}) as desired.

4.2 ≈_{ss} implies ≈′_{ss}

The main theorem of this section states that ≈_{ss} implies ≈′_{ss}. In order to prove this result a number of preliminary lemmas are again required. One of the key lemmas states that if φ ≈_{ss} φ′ then for each N_{j} ∈ ecores(φ) there is a context R[x̃] over terms from im(φ) such that R[M̃] >^{k} N_{j} and R[M̃′] >^{k} N′_{j}. The context R[M̃] is coined the recipe of N_{j} since in records the details of how the ecore N_{j} is revealed from terms in φ.

To make these ideas precise we start by giving a definition of recipes.

Definition 24 (Analysis recipe). Let φ be any frame and let M|_{w} ∈ A(M, φ) for some M ∈ im(φ). The analysis recipe R[x̃] for M|_{w} is a context which is defined inductively on the analysis level i as follows:

• M|_{w} ∈ A^{0}(M_{i}, φ). Then M|_{w} = M and we define R[x̃] to be the trivial context x where M = xφ.

• M|_{w} ∈ A^{i+1}(M_{i}, φ). If also M|_{w} ∈ A^{i}(M_{i}, φ) then the analysis recipe is identical to the analysis recipe from level i. Otherwise, per definition of analysis, there is some M|_{w_{2}} ∈ A^{i}(M, φ) such that M|_{w_{2}} ≻_{⋃_{M∈S} A^{i}(M,S)}> M|_{w} (where S = im(φ) ∪ fn(φ)), which per definition of revelation means that there are L_{1}, …, L_{k} each in A^{i}(M, φ) for some M ∈ im(φ), and a destructor context D[x, x_{1}, …, x_{k}], such that D[M|_{w_{2}}, L_{1}, …, L_{k}] > M|_{w}. Choose D^{∗}[x, x_{1}, …, x_{k}] to be any such context for which all subterms are irreducible, i.e. only a primitive reduction is possible (such context will always exist!). Let R[x̃] be the analysis recipe for M|_{w_{2}} and let R_{j}[x̃] be the analysis recipe for each L_{j} (these recipes are well-defined because M|_{w_{2}} and the L_{j}s are in A^{i}(M_{i}, φ)). Then D^{∗}[R[x̃], R_{1}[x̃], …, R_{k}[x̃]] is defined to be the analysis recipe for M|_{w}.

Analysis recipes are not necessarily unique since there may be two analysis terms which are syntactically equal and hence both can be used for revelation in the analysis. But this will not be important for our purpose. The next lemma states that corresponding analysis terms from statically equivalent frames have the same analysis recipes.

Lemma 7. Let φ ≡ (νñ){^{M_{i}}/_{x_{i}}}_{i∈I}, φ′ ≡ (νñ′){^{M′_{i}}/_{x_{i}}}_{i∈I} with φ ≈_{ss} φ′. If R[x̃] is an analysis recipe for M_{i}|_{w} ∈ A(M_{i}, φ) then it is also an analysis recipe for M′_{i}|_{w} ∈ A(M′_{i}, φ′) and there is a k ∈ ℕ such that

R[M̃] >^{k} M_{i}|_{w} ≯
R[M̃′] >^{k} M′_{i}|_{w} ≯

Proof. By induction in the definition of analysis recipes.

Basis (M_{i}|_{w} ∈ A^{0}(M_{i}, φ)). Trivial.

Step (M_{i}|_{w} ∈ A^{i+1}(M_{i}, φ)). Per definition of analysis there is some M_{i}|_{w_{2}} ∈ A^{i}(M_{i}, φ) such that M_{i}|_{w_{2}} ≻_{⋃_{T ∈S} A^{i}(T,S)}> M_{i}|_{w} (where S = im(φ) ∪ fn(φ)), which per definition of revelation means that there are L_{1}, …, L_{s} each in A^{i}(M, φ) for some M ∈ im(φ), and a destructor context D[x, x_{1}, …, x_{s}], such that D[M_{i}|_{w_{2}}, L_{1}, …, L_{s}] >^{M_{i}|_{w_{2}}} M_{i}|_{w}.

Let R[x̃] be the analysis recipe for M_{i}|_{w_{2}} and let R_{j}[x̃] be the analysis recipe for each L_{j}. Then D[R[x̃], R_{1}[x̃], …, R_{s}[x̃]] is per definition an analysis recipe for M_{i}|_{w}.

Per induction hypothesis there is a k ∈ ℕ such that R[M̃] >^{k} M_{i}|_{w_{2}} and R[M̃′] >^{k} M′|_{w_{2}}. Similarly there is a k_{j} ∈ ℕ such that R_{j}[M̃] >^{k_{j}} L_{j} and R_{j}[M̃′] >^{k_{j}} L′_{j} for each j. Hence we get that

D[R[M̃], R_{1}[M̃], …, R_{s}[M̃]] >^{l} D[M_{i}|_{w_{2}}, L_{1}, …, L_{s}]
D[R[M̃′], R_{1}[M̃′], …, R_{s}[M̃′]] >^{l} D[M′_{i}|_{w_{2}}, L′_{1}, …, L′_{s}]

where l = k +k_{1} +⋯+k_{s}. Per definition of analysis recipes, exactly one further rewrite is possible for the former context D[M_{i}|_{w_{2}}, L_{1}, …, L_{s}], namely the primitive rewrite. By condition 2 in ≈_{ss}, exactly one rewrite is also possible for the latter context D[M′_{i}|_{w_{2}}, L′_{1}, …, L′_{s}], and per definition of analysis recipes this must be also be a primitive rewrite. Since M_{i}|_{w_{2}} and M′_{i}|_{w_{2}} are the revelators for the respective reductions and the reduct in the first case is M_{i}|_{w}, the reduct for the second case must correspondingly be M_{i}|_{w}.

Finally, the induction hypothesis gives that R[x̃′] is also the analysis recipe for M′|_{w_{2}} and R_{j}[M̃′] is the analysis recipe for M′_{j} for each j. Hence the context

D[R[x̃], R_{1}[x̃], …, R_{s}[x̃]]

is per definition also the analysis recipe for M′_{i}|_{w}. This concludes the proof.

The above result could be re-phrased in terms of “revelation bisimulation”; informally, any two corresponding analysis terms from statically equivalent frames can exhibit the same revelations and the revealed terms are bisimilar (i.e. corresponding revelated terms can exhibit the same further revelations). We will not pursue this direction further since it is not necessary for our purposes, but the idea of revelation bisimulation does yield some insight into the nature of static equivalence.

The next lemma is an immediate corollary of Lemma 7:

Lemma 8. Let φ and φ′ be two frames with φ ≈_{ss} φ′, ecores(φ) = (N)_{j∈J} and ecores(φ) = (N′)_{j∈J}. Then for any contexts C_{1}[ỹ] and C_{2}[ỹ] it holds that

C_{1}[Ñ] =_{E} C_{2}[Ñ] ⇔ C_{1}[Ñ′] =_{E} C_{2}[Ñ′]

Next we give two important results on the kind of contexts C^{⊥}[ỹ] considered in condition 3 of ≈′_{ss}. Informally, the first lemma says that every variable in C^{⊥}[ỹ] is strongly correlated to at least one variable at a position which exists in the relevant rewrite rule. This is used in the proof of the second lemma, which says that only primitive rewrites on C^{⊥}[Ñ] are possible.

Lemma 9. Let φ and φ′ be two frames with φ ≈_{ss} φ′, ecores(φ) = (N)_{j∈J} and ecores(φ) = (N′)_{j∈J}. Let C_{1}[ỹ] be any partitioning context with C_{1}[ỹ] ⊐ L[z̃] or C_{1}[ỹ]□L[z̃] for some rewrite rule L[z̃] >_{r} R[z̃]. Then any variable position w in C[ỹ] (i.e. a position such that C[ỹ]|_{w} is a variable) is strongly correlated to some variable position w′ which exists in L[z̃].

Proof. Let w be any position in C[ỹ]. There are two cases to consider.

1. w is weakly correlated to all other positions w′ in C[ỹ] only through a single variable z in v(L[z̃]), i.e. w ⇄_{z}^{k} w′ for some natural number k. Hence also w ⇄ w′, i.e. w and w′ are also strongly correlated. By the assumption that C_{1}[ỹ] ⊐ L[z̃] or C_{1}[ỹ]□L[z̃], at least one of the positions w′ exist in L[z̃], which concludes the first case.

2. w is weakly correlated to some w′ through at least two variables z_{1} and z_{2} in v(L[z̃]). In this case we have for some w′′ that w ⇄_{z_{1}}^{k} w′′ ⇄_{z_{2}} w′. Again this implies that w ⇄ w′. Since w′′ correlates through both z_{1} and z_{2} this position must exist in L[z̃], which concludes the second case.

Lemma 10. Let φ be any frame with ecores(φ) = (N)_{j∈J}. It then holds for any partitioning context C_{1}^{⊥}[ỹ] with C_{1}^{⊥}[ỹ] ⊐ or C_{1}^{⊥}[ỹ]□ and any context C_{2}^{⊥}[ỹ] that

C_{1}^{⊥}[Ñ] > C_{2}^{⊥}[Ñ] ⇔ C_{1}^{⊥}[Ñ] >_{r} C_{2}^{⊥}[Ñ]

Proof. Let L[z̃] >_{r} R[z̃] be the rewrite rule such that C_{1}[ỹ] ⊐ L[z̃] or C_{1}[ỹ]□L[z̃]. The direction from right to left is immediate from the definition of the rewrite relation. For the converse first observe that any subterm C_{1}[Ñ]|_{w} at a position w which exists in L[z̃] is irreducible by the assumption of independent rewrite systems (i.e. no destructor functions occur internally in rewrite rules). Consequently any possible internal reduction must be at position w which exist in C_{1}[ỹ] but not in L[z̃]. But by Lemma 9 the position w is strongly correlated to a position w′ which exists in L[z̃]. Therefore C_{1}[Ñ]|_{w} must be a subterm of some ecore and is hence irreducible.

We are now ready to show that ≈_{ss} implies condition 3 in ≈′_{ss}.

Lemma 11. Let φ ≡ (νñ){^{M_{i}}/_{x_{i}}}_{i∈I}, φ′ ≡ (νñ′){^{M′_{i}}/_{x_{i}}}_{i∈I}, ecores(φ) = (N)_{j∈J}, ecores(φ) = (N′)_{j∈J} and φ ≈_{ss} φ′. Let C_{1}^{⊥}[ỹ] be a partitioning context with C_{1}^{⊥}[ỹ] ⊐ or C_{1}[ỹ]□. It then holds for any context C_{2}^{⊥}[ỹ] that

C_{1}^{⊥}[Ñ] >_{r} C_{2}^{⊥}[Ñ] ⇔ C_{1}^{⊥}[Ñ′] >_{r} C_{2}^{⊥}[Ñ′]

Proof. We show the direction from left to right; the converse is symmetric. Suppose that the rewrite C_{1}^{⊥}[Ñ] >_{r} C_{2}^{⊥}[Ñ] is possible by virtue of some rule L[z̃] >_{r} R[z̃]. We then have that C_{1}^{⊥}[Ñ] =_{E} C_{2}^{⊥}[Ñ] and by Lemma 8 also C_{1}^{⊥}[Ñ′] =_{E} C_{2}^{⊥}[Ñ′]. The challenge is to show that the equality is in fact a primitive rewrite, which is not immediately apparent. For it may be that the equality is concluded by transitivity, i.e. multiple reduction steps are necessary. Such multiple rewrites may also be possible in C_{1}[Ñ] even though they are not necessary for establishing the equality, so we cannot use this to give a proof by contradiction. We must take another approach.

Each ecore N_{j} and N′_{j} is an analysis term so by Lemma 7 there is an analysis recipe R_{j}[x̃] such that R_{j}[M̃] >^{k_{j}} N_{j} and R_{j}[M̃′] >^{k_{j}} N′_{j}. As in the proof of Lemma 7 we get that there is a context C^{⊥}[x̃] such that C^{⊥}[M̃] >^{l} C_{1}^{⊥}[Ñ] and C^{⊥}[M̃′] >^{l} C_{1}^{⊥}[Ñ′]. C_{2}^{⊥}[Ñ] is irreducible by Lemma 10, so C^{⊥}[M̃] normalises in l + 1 reduction steps. By condition 2 in ≈_{ss} exactly one further rewrite is possible for C^{⊥}[Ñ′], for otherwise C^{⊥}[M̃′] would have a different number of reductions than C^{⊥}[M̃]. Finally we have by Lemma 10 that this must be a primitive rewrite.

Technically one must require in the above argument that the reduction C^{⊥}[M̃] >^{l} C_{1}^{⊥}[Ñ] in l steps is maximal, i.e. that there is no longer reduction sequence yielding the same reduct. Any maximal reduction must be a bottom-up reduction in the sense that subterms are always reduced first. It follows that any maximal reduction of C^{⊥}[M̃] must be through C_{1}^{⊥}[Ñ] and correspondingly that any maximal reduction of C^{⊥}[M̃′] must be through C_{1}^{⊥}[Ñ′], which is necessary for the soundness of the proof.

The next lemma states that ≈_{ss} implies condition 2 in ≈′_{ss}.

Lemma 12. Let φ ≡ (νñ){^{M_{i}}/_{x_{i}}}_{i∈I}, φ′ ≡ (νñ′){^{M′_{i}}/_{x_{i}}}_{i∈I}, ecores(φ) = (N)_{j∈J}, ecores(φ) = (N′)_{j∈J} and φ ≈_{ss} φ′. It then holds for any context C[ỹ] and any j ∈ J that

C[Ñ] = N_{j} ⇔ C[Ñ′] = N′_{j}

Proof. Suppose that C[N_{1}, …, N_{s}] = N_{j}. Each N_{i} has a recipe R_{i}[x̃], i.e. R_{i}[M̃] >^{k_{i}} N_{i} where k_{i} maximal. Hence

C[R_{1}[M̃], …, R_{s}[M̃]] =_{E} R_{j}[M̃]

and by condition 1 in ≈_{ss} also

C[R_{1}[M̃′], …, R_{s}[M̃′]] =_{E} R_{j}[M̃′]

By Lemma 7 the recipe for each N′_{i} is R_{i}[x̃], so R_{i}[M̃′] >^{k_{i}} N_{i} where k_{i} maximal and we have that

C[N′_{1}, …, N′_{k}] =_{E} N′_{j}

The right hand side, N′_{j}, is irreducible since it is an ecore. We then propose a Claim: The left hand side is also irreducible. Given this claim, the equality is syntactic by confluence, which concludes the proof.

Proof of claim. Suppose for a contradiction that the left hand side, C[N′_{1}, …, N′_{s}], is not irreducible, i.e. we have for some M′ that:

C[R_{1}[M̃′], …, R_{s}[M̃′]] >^{l} C[N′_{1}, …, N′_{k}] > M′

where l = k_{1} + … k_{s} is maximal. Condition 2 in ≈_{ss} then gives that also

C[R_{1}[M̃], …, R_{s}[M̃]] >^{l} C[N_{1}, …, N_{k}] > M

for some M, contradicting that C[N_{1}, …, N_{k}] is syntactically equal to an ecore (and hence irreducible).

Finally we arrive at the main result of this section.

Theorem 2. ≈_{ss} implies ≈′_{ss} Proof. Let φ ≡ (νñ){^{M_{i}}/_{x_{i}}}_{i∈I}, φ′ ≡ (νñ′){^{M′_{i}}/_{x_{i}}}_{i∈I}, ecores(φ) = (N)_{j∈J}, ecores(φ) = (N′)_{j∈J} and φ ≈_{ss} φ′. We must show that conditions 1, 2 and 3 in ≈′_{ss} hold.

Condition 1. By Lemma 1 any M_{i} ∈ im(φ) can be written as a context over ecores, i.e. at least one context C_{i}[ỹ] exists such that M_{i} = C_{i}[Ñ]. Then it must also hold that M′_{i} = C_{i}[Ñ′]; for otherwise there would be ecores N_{j} and N′_{j} in M_{i} and M′_{i} respectively such that N_{j} and N′_{j} do not have the same analysis recipes, contradicting Lemma 7.

Condition 2. This is Lemma 12.

Condition 3. This is Lemma 11.

4.3 Conditions under which ≈_{s} and ≈_{ss} Coincide

In Chapter 2 we demonstrated that ≈_{s} and ≈_{ss} do not generally coincide and gave the following counter-example in the theory of public key encryption:

φ =^{Δ} (νa, c, k){^{enc(a,k^{+})}/_{x_{1}}, ^{k^{−}}/_{x_{2}}}

φ′ =^{Δ} (νa, c, k){^{enc(a,k^{+})}/_{x_{1}}, ^{c^{−}}/_{x_{2}}}

It is easy to verify that φ ≈_{s} φ′ while φ ≉_{ss} φ′. Hence allowing tests on reductions as well as tests on equality increases the distinguishing power of an observer process. However, there are theories where tests on reductions do not yield increased distinguishing power. Take for example the symmetric-key counterpart of the above frames:

φ_{2} =^{Δ} (νa, c, k){^{enc(a,k)}/_{x_{1}}, ^{k}/_{x_{2}}}
φ′_{2} =^{Δ} (νa, c, k){^{enc(a,k)}/_{x_{1}}, ^{c}/_{x_{2}}}

We still have that φ_{2} ≉_{ss} φ′_{2} because dec(M_{1}, M_{2}) > while dec(M′_{1}, M′_{2}) ≯, so condition 2 in ≈_{ss} fails. But suddenly we also have that φ_{2} ≉_{s} φ′_{2} because the following equality holds in φ_{2} but not in φ′_{2}:

x_{1} =_{E} enc(dec(x_{1}, x_{2}), x_{2})

Hence in this case the standard static equivalence agrees with the strong version. The reason for this is intuitively that, for the above equality to hold in φ_{2}, a reduction on dec(M_{1}, M_{2}) is forced. For if no reduction is possible, and since M_{1} is irreducible, we would have by confluence that

M_{1} = enc(dec(M_{1}, M_{2}), M_{2})

This syntactic equality is impossible since M_{1} cannot be a proper subterm of itself.

4.3. CONDITIONS UNDER WHICH ≈_{S} AND ≈_{SS} COINCIDE

The question now is in which situations a reduction can be forced by an appropriate equality as in the example above – and thus where condition 2 in ≈_{ss} is superfluous. The equality in the above example can be constructed because the term enc(a, k) in φ_{2} can be written as a non-trivial context over other analysis terms. In contrast it was not possible to write enc(a, k^{+}) in φ as a nontrivial context over analysis terms since k^{+} is not in the analysis (we have that enc(a, k^{+}) is an ecore but not a core).

More generally, any analysis term L which is not an ecore can be written as a non-trivial context over other analysis terms exactly when cores(φ) = ecores(φ). For otherwise L would per definition be an ecore, which is impossible since ecores are per assumption cores (and L was assumed not to be a core).

We now have the intuition to give a formal proof of the main result in this section, namely that ≈_{ss} implies ≈′_{ss} whenever cores(φ) = ecores(φ). We start with a preliminary lemma, namely the counterpart of Lemma 7 which says that corresponding terms from statically equivalent frames have the same analysis recipes. We cannot rely on the original proof of this lemma since it assumed ≈_{ss} and relied on condition 2. Hence we employ the idea set forth in the above example that equalities can force rewrites.

Lemma 13 (cf. Lemma 7). Let φ ≡ (νñ){^{M_{i}}/_{x_{i}}}_{i∈I}, φ′ ≡ (νñ′){^{M′_{i}}/_{x_{i}}}_{i∈I} with φ ≈_{s} φ′ and suppose that cores(φ) = ecores(φ). If R[x̃] is an analysis recipe for M_{i}|_{w} ∈ A(M_{i}, φ) then it is also an analysis recipe for M′_{i}|_{w} ∈ A(M′_{i}, φ′) and there is a k ∈ ℕ such that

R[M̃] >^{k} M_{i}|_{w} ≯
R[M̃′] >^{k} M′_{i}|_{w} ≯

Proof. By induction in the definition of analysis recipes.

Basis (M_{i}|_{w} ∈ A^{0}(M_{i}, φ)). Trivial.

Step (M_{i}|_{w} ∈ A^{i+1}(M_{i}, φ)). We shall benefit from some notational short hands: for any tuple L̃ ⊆ A(φ) where L̃ = L_{1}, …, L_{s} and R_{1}[x̃], …, R_{s}[x̃] are the respective analysis recipes, we let R̃_{L}[x̃] =^{Δ} R_{1}[x̃], …, R_{s}[x̃].

Now per definition of analysis there is some M_{i}|_{w_{2}} ∈ A^{i}(M_{i}, φ) such that M_{i}|_{w_{2}} ≻_{⋃_{M∈S} A^{i}(M,S)} M_{i}|_{w} (where S = im(φ) ∪ fn(φ)), which per definition of revelation means that there are terms L_{1}, …, L_{s} ⊆ ⋃_{M∈S} A^{i}(M, S) and a destructor context D[x, x_{1}, …,] such that D[M_{i}|_{w_{2}}, L̃] >^{M_{i}|_{w_{2}}} M_{i}|_{w}. Let R[x̃] be the analysis recipe for M_{i}|_{w_{2}} and let R̃_{L}[x̃] be the tuple of analysis recipes for L̃ as defined above. Then D[R[x̃], R̃_{L}[x̃]] is per definition an analysis recipe for M_{i}|_{w}.

Per induction hypothesis there is a k such that R[M̃] >^{k} M_{i}|_{w_{2}} and R[M̃′] >^{k} M′|_{w_{2}}. Similarly there is a k_{j} such that R_{j}[M̃] >^{k_{j}} L_{j} and R_{j}[M̃′] >^{k_{j}} L′_{j} for each R_{j}[x̃] in R̃_{L}[x̃]. Hence we get that

D[R[M̃], R̃_{L}[M̃] >^{l} D[M_{i}|_{w_{2}}, L̃]
D[R[M̃′], R̃_{L}[M̃′]] >^{l} D[M′_{i}|_{w_{2}}, L̃′]

where l = k +k_{1} +⋯+k_{s}. Per definition of analysis recipes, exactly one further rewrite is possible for the former context D[M_{i}|_{w_{2}}, L̃], namely the primitive rewrite:

D[M_{i}|_{w_{2}}, L̃] >_{r} M_{i}|_{w}

The challenge is now to show that a reduction is possible on the latter context, D[M′_{i}|_{w_{2}}, L̃′]. In the proof of Lemma 7 we simply relied on condition 2 in ≈_{ss}, but now this condition is not available because we are assuming the weaker static equivalence, ≈_{s}. So a more cunning approach is called for.

The assumption that cores(φ) = ecores(φ) is the key here. We then get that any analysis term L which is not a core is syntactically equal to a non-trivial context over other analysis terms. For otherwise L would per definition be an ecore which is impossible since ecores are now cores (and L was assumed not to be a core). Hence for some terms T̃ ⊆ A(φ) we can write

M_{i}|_{w_{2}} = C[M_{i}|_{w}, T̃]

Each T_{j} ∈ T̃ has some analysis recipe R_{j}[x̃], i.e. R_{j}[M̃] > T_{j}; strictly speaking this should be shown in a separate induction, since the induction hypothesis does not necessarily apply to T_{j}, but the result should come as no surprise. Noting that

D[M_{i}|_{w_{2}}, L̃] =_{E} M_{i}|_{w}

and using that any analysis term is equal to the instantiation of its analysis recipe, we reason as follows:

M_{i}|_{w_{2}} = C[M_{i}|_{w}, T̃]
M_{i}|_{w_{2}} =_{E} C[D[M_{i}|_{w_{2}}, L̃], T̃]  ⇕
R[M̃] =_{E} C[D[R[M̃], R̃_{L}[M̃]], R̃_{T} [M̃]]  ⇕
(R[x̃] =_{E} C[D[R[x̃], R̃_{L}[x̃]], R̃_{T} [x̃]])φ

Per definition of ≈_{s} we may continue thus:

(R[x̃] =_{E} C[D[R[x̃], R̃_{L}[x̃]], R̃_{T} [x̃]])φ′
R[M̃′] =_{E} C[D[R[M̃′], R̃_{L}[M̃′]], R̃_{T} [M̃′]]  ⇕
M′_{i}|_{w_{2}} =_{E} C[D[M′_{i}|_{w_{2}}, L̃′], T̃′]

The last step follows from the induction hypothesis: since R[x̃] is the analysis recipe for M_{i}|_{w_{2}} ∈ A^{i}(M_{i}, φ) we have that R[M̃] >^{k} M_{i}|_{w_{2}} and R[M̃′] >^{k} M′_{i}|_{w_{2}}. The tuples L̃′ and T̃′ simply contain the normalised recipes from R̃_{L}[M̃′] and R̃_{T} [M̃′], respectively. Since these recipes are not for analysis terms in level i, the induction hypothesis does not apply to these. Hence we do not know that each L′_{j} ∈ L̃′ corresponds to the analysis term L_{j} ∈ L̃, and indeed we do not even know that L′_{j} is an analysis term. However this is unimportant – all that matters for our purpose is that each L′_{j} is irreducible.

From the last equality we deduce that D[M′_{i}|_{w_{2}}, L̃′] must be reducible. For suppose not towards a contradiction. The LHS of the last equality is irreducible because it is a subterm of M_{i} and we assume each M_{i} ∈ im(φ) to be irreducible. Therefore, by confluence the normal form of the RHS is syntactically equal to M_{i}|_{w_{2}}. But this is impossible since the normal form of the RHS then contains M_{i}|_{w_{2}} as a proper subterm.

Per definition of analysis recipes, only one reduction is possible on D[M_{i}|_{w_{2}}, L̃′], and since M_{i}|_{w_{2}} is the revelator it must hold that

D[M_{i}|_{w_{2}}, L̃′] >_{r} M_{i}|_{w}

and we conclude as desired that

D[R[M̃], R̃_{L}[M̃] >^{l} D[M_{i}|_{w_{2}}, L̃] > M_{i}|_{w}
D[R[M̃′], R̃_{L}[M̃′]] >^{l} D[M′_{i}|_{w_{2}}, L̃′] > M′_{i}|_{w}

Finally, the induction hypothesis gives that R[x̃] is also the analysis recipe for M|_{w_{2}} and R_{j}[x̃] is the analysis recipe for L_{j} for each L_{j} ∈ L̃. Hence the context

D[R[x̃], R̃_{L}[x̃]]

is per definition also the analysis recipe for M′_{i}|_{w}. This concludes the proof.

Lemma 14 (cf. Lemma 8). Let φ and φ′ be two frames with φ ≈_{s} φ′ and suppose that cores(φ) = ecores(φ). Then it holds for any contexts C_{1}[ỹ] and C_{2}[ỹ] that

C_{1}[Ñ] =_{E} C_{2}[Ñ] ⇔ C_{1}[Ñ′] =_{E} C_{2}[Ñ′]

Proof. This is a corollary of Lemma 13.

Lemma 15. Let φ and φ′ be two frames with φ ≈_{s} φ′ and suppose that cores(φ) = ecores(φ). Then it holds for any contexts C_{1}[ỹ] and C_{2}[ỹ] where C_{1}[ỹ] ⊐ or C_{1}[ỹ]□ that

C_{1}[Ñ] >_{r} C_{2}[Ñ] ⇔ C_{1}[Ñ′] >_{r} C_{2}[Ñ′]

Proof. We show the direction from left to right; the converse is symmetric. So suppose that

C_{1}[Ñ] >_{r} C_{2}[Ñ]

We must show that this rewrite is preserved when substituting cores from φ′. Since the rewrite is primitive C_{1}[ỹ] unifies with the LHS of some rewrite rule, i.e. there is a destructor context D[x, x̃] and some other context C[ỹ] such that

C_{1}[Ñ] = D[C[Ñ], Ñ] > C_{2}[Ñ]

where C[Ñ] is the revelator. Since we are working with subterm theories, C_{2}[Ñ] is a subterm of C[Ñ]. We now employ the same trick as in the proof Lemma 13: the assumption that cores(φ) = ecores(φ) gives us that any analysis term which is not itself a core can be written as a non-trivial context over cores. Therefore there is some context C_{3}[x, x̃] such that

C[Ñ] = C_{3}[C_{2}[Ñ], Ñ]
C[Ñ] =_{E} C_{3}[D[C[Ñ], Ñ], Ñ]  ⇕
C[Ñ′] =_{E} C_{3}[D[C[Ñ′], Ñ′], Ñ′]

The last step followed by Lemma 14. As before we conclude that D[C[Ñ′], Ñ′] must be primitively reducible, although this time we call upon Lemma 10 to get that the LHS C[Ñ′] is irreducible (this lemma applies because we have assumed that C_{1}[ỹ] ⊐ or C_{1}[ỹ]□). Since C[Ñ′] is the revelator we then conclude as desired that

C_{1}[Ñ′] = D[C[Ñ′], Ñ′] >_{r} C_{2}[Ñ′]

Theorem 3. If ecores(φ) = cores(φ) then φ ≈_{ss} φ′ ⇔ φ ≈_{s} φ′.

Proof. The direction from left to right is immediate from the definitions of ≈_{ss} and ≈_{s}.

For the other direction it must be shown that, under the given assumptions, condition 2 in ≈_{ss} is a consequence of condition 1 – i.e. we must show that

(M >^{k})φ ⇔ (M >^{k})φ′

for all terms M and all k ∈ ℕ.

First observe that any two corresponding terms M_{i} ∈ im(φ) and M′_{i} ∈ im(φ′) can be written as the same context over cores. For otherwise there would be cores N_{j} ∈ ecores(M_{i}, φ) and N′_{j} ∈ ecores(M′_{i}, φ′) which do not have the same analysis recipe, contradicting Lemma 13.

So suppose that (M >^{k})φ and let ecores(φ) = (N)_{j∈J} and ecores(φ′) = (N′)_{j∈J}. Then n(M) ∩ bn(φ) = ∅ and Mφ >^{k}. Since every free name in φ is an ecore, we have for some context C_{1}[ỹ] that

Mφ = C_{1}[Ñ]
Mφ′ = C_{1}[Ñ′]

The proof now proceeds by induction in k in order to show that C_{1}[Ñ] >^{k}⇒ C_{1}[Ñ′] >^{k}.

Basis (k = 0). This is trivial (use reflexivity).

Step (assume for k, prove for k + 1). We then have that

C_{1}[Ñ] > C_{2}[Ñ] >^{k}

for some C_{2}[ỹ]. Per definition of the rewrite relation there is some subterm C_{1}[Ñ]|_{w_{1}} of C_{1}[Ñ] which rewrites primitively, i.e.

C_{1}[Ñ]|_{w} >_{r} C_{2}^{∗}[Ñ]|_{w_{2}}

Apply Lemma 15 to get that also

C_{1}[Ñ′]|_{w_{1}} >_{r} C_{2}[Ñ′]|_{w_{2}}

As in the proof of Lemma 5 we then get that

C_{1}[Ñ′] > C_{2}[Ñ′]

Since C_{2}[Ñ] >^{k} it follows by the induction hypothesis that also C_{2}[Ñ′] >^{k}. Hence we have that

Mφ′ = C_{1}[Ñ′] >^{k+1}

which per definition means that (M >^{k})φ′.

Theorem 3 above can be rephrased to state that ≈_{ss} and ≈_{s} coincide in any theory where inaccessible terms are impossible. For if there are no inaccessible terms then any analysis term which is not an ecore can be written as contexts over other analysis terms, so it follows per definition of ecores that ecores(φ) = cores(φ).

The condition that no inaccessible terms are possible is easy to check from the definition of a given equational theory. Take for example any analysis term term enc(M_{1}, M_{2}) in the theory of symmetric key encryption. If enc(M_{1}, M_{2}) is not an ecore then neither M_{1} nor M_{2} can be inaccessible. For M_{1} is revealed from enc(M_{1}, M_{2}) and hence is in the analysis. And in order for this to be possible, the symmetric key M_{2} must also be in the analysis. Hence any frame φ in a symmetric key theory satisfies that ecores(φ) = cores(φ) and so by Theorem 3 ≈_{ss} and ≈_{s} coincide.

In contrast, a term enc(M_{1}, M_{2}) in a public key theory might have the public key M_{2} inaccessible. For it may be that enc(M_{1}, M_{2}) can be decrypted even though M_{2} is not in the analysis; all that is required is for the corresponding private key to be in the analysis.

However, we can make the assumption that any public key is always known by the environment, i.e. any public key will always be in the analysis of a frame. Indeed, this is one of the main attractions of public-key cryptography: a principal may publish its public key for use by any interested parties. Under this assumption we do have that no inaccessible terms are possible, and hence that ≈_{ss} and ≈_{s} coincide. On the other hand, this assumption is not valid for public-key signatures where we would have the following rewrite rule – the only difference from the public-key decryption rule is that the order of public and private keys has been swapped:

dec(enc(z_{1}, z_{2}^{−}), z_{2}^{+}) >_{r} z_{1}

For here we would have to assume that the private key is always known to an environment, which obviously is not sound.

4.4 Summary

In this chapter we have shown two important results, namely that ≈_{ss} and ≈′_{ss} coincide and that ≈_{s} and ≈_{ss} coincide for frames where cores(φ) = ecores(φ) – or, more generally, in theories with no inaccessible terms. These include theories with symmetric key encryption and theories with public key encryption, under the assumption that public keys are always known to the environment.

A Logic for Frames

This chapter sets out to design a logic for frames which characterises strong static equivalence and which is amenable to construction of characteristic formulae. The refined definition of strong static equivalence, ≈′_{ss}, presented in Chapter 3 was derived exactly with this purpose in mind, so we will base our developments on ≈′_{ss} instead of ≈_{ss} whenever convenient. We established in Chapter 4 that the two definitions of strong static equivalence coincide, so the results in this section apply to both ≈′_{ss} and ≈_{ss}.

The resulting first order logic for frames can be used to reason directly about the terms in the frames using propositions for equality, syntactic equality and reductions. Quantification ranges over the synthesis of the frame, which intuitively is the set of terms that an environment can deduce by constructing new terms from the ecores of the frame. Quantification thus allows indirect reasoning about the knowledge of an environment, and assertions such as there exists a term y (known by the environment) such that x_{1} can be decrypted with y to obtain x_{2} can be made.

Section 1 gives an informal discussion of possible constructs for inclusion in the logic and Section 2 formalises the resulting syntax and semantics. In Section 3 it is shown that the logic characterises strong static equivalence; the proof of this result relies on lemmas from Chapter 4. Finally section 4 shows how characteristic formulae can be constructed. The construction is based on a further refinement of strong static equivalence which does not exhibit the problems of universal quantification over contexts which were still present in ≈′_{ss}.

5.1 Motivation

CHAPTER 5. A LOGIC FOR FRAMES

This section presents some examples and informal ideas on which the syntax and semantics for the logic for frames are based. The objective is to answer the question of which kind of assertions one would like to express about frames. We base our discussion on applications in cryptographic protocols but will still maintain a certain level of generality. Simplicity of the logic will have high priority for the sake of subsequent theoretical developments.

A key objective is to develop a logic which characterises strong static equivalence, i.e. whenever two frames are statically equivalent they should satisfy the same set of formulae. Another aim is to make characteristic formulae possible, i.e. for every frame φ there should exist a formula C_{φ} s.t. φ ≈′_{ss} φ′ if and only if φ′ ⊨ C_{φ} for all frames φ′. A starting point for achieving this is to include the operators featuring in the definition of ≈′_{ss} in the logic.

We start by considering ideas for the basic propositional equational logic in the first subsection and then continue with a discussion of a first order logic (i.e. a logic with quantification over terms) in the second subsection.

5.1.1 Propositional Equational Logic

A formula in propositional logic is generally built from atomic propositions p_{i}, logical connectives (such as ∨, ¬, ∧, → and ↔), together with suitable bracketing; an example formula could thus be (p_{1} ∨ p_{2}) ∧ ¬p_{3}. In ordinary propositional logic, the atomic propositions are boolean variables whose truth values must be assigned by a valuation function in order to decide the truth of any given formula. So an atomic proposition (and hence a formula) is true with respect to some valuation. In the case of a logic for frames, the truth of an atomic proposition (and hence of a formula) should be relative to a frame, and (some of) the atomic propositions will be equalities, giving rise to an equational logic. In the following we will loosely write φ ⊨ A when the formula A is true in the frame φ; the precise definition of this satisfaction relation will be given in the next section.

First we must decide what kind of atomic propositions are meaningful and useful for reasoning about frames. We base our discussion on two statically equivalent frames in the public key theory E_{pub}:

φ = (νa, b, c){^{enc(c^{−},k^{+})}/_{x_{1}}, ^{enc(b,c^{+})}/_{x_{2}}, ^{b}/_{x_{3}}}
φ′ = (νa, b, c){^{enc(f(c)^{−},k^{+})}/_{x_{1}}, ^{enc(f(b),f(c)^{+})}/_{x_{2}}, ^{f(b)}/_{x_{3}}}

Equality of Terms in Frames

Equality between terms in frames immediately comes to mind as a possible atomic proposition. For example one would expect that the equality proposition dec(x_{2}, dec(x_{1}, k^{−})) =_{E} x_{3} holds in the frame φ, written φ ⊨ dec(x_{2}, dec(x_{1}, k^{−})) =_{E} x_{3}. On the other hand, the proposition dec(x_{1}, k^{−}) =_{E} c^{−} should not be true in φ since c is private. If it were true the logic would not characterise static equivalence since the proposition is certainly not true in φ′. Hence a meaningful semantics for the equality proposition is captured precisely in the definition of equality of terms in frames (Definition 5), i.e. φ ⊨ M_{1} =_{E} M_{2} if and only if (M_{1} =_{E} M_{2})φ.

As a bonus feature, the formula a =_{E} a can be used to check that the name a is free in a frame, since the only reason why this formula may not hold in a 5.1. MOTIVATION

frame φ is that a ∈ bn(φ).

The equality proposition together with negation would be sufficient to characterise the weak version of static equivalence. However it does not yield much insight into the nature of a frame and is therefore uninteresting in itself. Furthermore, it would not suffice for constructing characteristic formulae, so we shall need to consider additional atomic propositions.

Reduction

Reduction propositions on the form dec(x_{2}, dec(x_{1}, k^{−})) > x_{3} will be required in characteristic formulae in order to express condition 3 in the definition of ≈′_{ss}. Intuitively this proposition would be true in φ and φ′ (although technically the reduction requires two steps). The intended meaning is that φ ⊨ M_{1} > M_{2} if and only if M_{1}φ > M_{2}φ. For the same reason as with equality, we must require that n(M_{1}, M_{2}) ∩ bn(φ) = ∅.

Reduction propositions may not appear useful at a first glance because of our inability to express that e.g. dec(x_{1}, k^{+}) > c^{−} (where c is private). But in combination with existential quantification (to be considered in the next subsection), the reduction proposition will give rise to significant expressive power.

Syntactic equality

Propositions with syntactic equality between terms on the form M_{1} = M_{2} is necessary to express condition 1 and 2 in the definition of ≈′_{ss} in a characteristic formulae. The intended meaning of such propositions is, not surprisingly, that φ ⊨ M_{1} = M_{2} if and only if M_{1}φ = M_{2}φ, and again we must require that n(M_{1}, M_{2}) ∩ bn(φ) = ∅.

Other candidates

Ecores form another essential ingredient in the definition of ≈′_{ss}, and hence one might considering including in the logic a proposition core(x, M) stating that the term M is an ecore in x. With a naive interpretation of the core proposition, we would have that for example core(x_{3}, b) is true in the frame φ. However it would not be true in φ′ (where the ecore of x_{3} is f(b)) so the resulting logic would fail to characterise static equivalence. It turns out that an appropriate ecore proposition can be expressed using existential quantification and the reduction proposition, so we do not need to explicitly include it in our logic.

As another idea for atomic propositions, recall that a frame represents messages sent by some process on a public channel, and hence represents the knowledge of an environment. It would therefore be nice to directly assert that the environment can deduce a given term, i.e. that the term c^{−} can be deduced from φ (namely by decrypting x_{1} with k^{−} since k is a free name). But c^{−} cannot be deduced from φ′ – f(c^{−}) can be deduced, but f is a one-way hash function. It follows that a deduction proposition would not characterise static equivalence and hence we do not include it in the logic. However, we shall see how to obtain similar expressiveness using first order quantification in the next subsection.

5.1.2 First-order Logic

Adding the quantifier ∃ yields a much more interesting logic with a resulting increase in expressiveness. It is however not obvious how the semantics for this quantifier should be defined; in particular, the domain over which a quantification ranges is of much significance. The intuition is that a frame φ should satisfy a formula ∃xA (where A is another formula with the variable x free) if there is some term M such that φ satisfies A{^{M}/_{x}}. A slightly nicer way of expressing this is that φ{^{M}/_{x}} must satisfy A. The question is now which domain we allow the term M to be drawn from.

A first idea may be to let quantification range over arbitrary terms. However this would result in characterisation failing; for example, φ′ defined in the previous subsection would satisfy ∃x(x_{3} = f(x)) (choose x = b) while φ clearly would not. The problem is intuitively that the quantified variable is bound to a term occurring on sub-core level in the frame; this is problematic since subterms of cores do not have any effect on static equivalence.

The solution is to let quantification range over the set of terms which can already be deduced from the frame. For example, the terms f(b), f(f(b)) and f(enc(f(b), k)) can be deduced from φ′ but b cannot (we formally define deduction in terms of a synthesis from ecores in the next section).

Existential quantification together with the atomic propositions can now be used to express many interesting properties about frames. For example we may express that the core b in ecores(x_{2}, φ) has analysis recipe dec(x_{2}, dec(x_{1}, k^{−})) as follows:

∃y_{1}∃y_{2}(dec(x_{2}, dec(x_{1}, k^{−})) > y_{1} ∧ y_{1} > y_{2} ∧ ¬∃y_{3}(y_{2} > y_{3}))

because this formula is satisfied exactly if the term in question is the analysis recipe for the core b. Notice how the formula is satisfied by both φ and φ′. We shall rely on this idea when expressing ecores in the construction of characteristic formulae later in this chapter.

Existential quantification can also be used to express that x_{2} can be decrypted using some private key known to the environment:

∃y_{1}∃y_{2}(dec(x_{2}, y_{1}) > y_{2})

Again this formulae is true in both φ and φ′ (for the former choose y_{1} = c^{−} and y_{2} = b, and for the latter choose y_{1} = f(c)^{−} and y_{2} = f(b)). Alternatively we can also use syntactic equality to express that the encrypted term in x_{1} is known to the environment thus:

∃y(x_{1} = enc(y, k^{+}))

5.2. SYNTAX AND SEMANTICS

5.2 Syntax and Semantics

Formal syntax and semantics for the logic of frames will now be given. Having discussed the motivation in the last section, we will be brief.

5.2.1 Syntax

The syntax for the chosen first order logic for frames, LF, is defined as follows, where the M_{i} range over terms and x ranges over variables:

A ::=M_{1} =_{E} M_{2} | M_{1} > M_{2} | M_{1} = M_{2} | A_{1} ∨ A_{2}
|¬A_{1} | (A_{1}) | ∃x(A_{1})

The full set of logical connectives is defined from ¬,∨ and ∃ in the usual way:

A_{1} ∧ A_{2} =^{Δ} ¬(¬A_{1} ∨ ¬A_{2})
A_{1} → A_{2} =^{Δ} A_{2} ∨ ¬A_{1}
A_{1} ↔ A_{2} =^{Δ} A_{1} → A_{2} ∧ A_{2} → A_{1}
∀x(A_{1}) =^{Δ} ¬∃x(¬A_{1})
true =^{Δ} x =_{E} x
false =^{Δ} ¬true

We assume that propositional connectives associate from the left i.e. A_{1}∨A_{2}∧A_{3} is interpreted as (A_{1} ∨A_{2})∧A_{3}, but parenthesis can always be used to explicitly override this. When there is no ambiguity we may omit parenthesis in existential quantification (and write e.g. ∃y_{1}∃y_{2}M_{1} = M_{2}). Free and bound variables in formulae are defined as expected, i.e. quantification is the only binder.

Example 5.2.1. The following is an example of a formula generated from the chosen grammar:

∃y_{1}∃y_{2}(dec(x_{2}, y_{1}) > y_{2} ∧ ¬∃y_{3}∃y_{4}(dec(y_{2}, y_{3}) > y_{4}))

This expresses that x_{2} can be decrypted using some known key and that the resulting term cannot be further decrypted.

5.2.2 Semantics

Common for all three atomic propositions is the requirement that terms do not contain private names. Therefore we start by defining the notions of reduction in frames and syntactic equality in frames along the same line as equality in frames.

Definition 25 (Reduction in frame). M_{1} reduces to M_{2} in φ, written (M_{1} > M_{2})φ, if and only if n(M_{1}, M_{2}) ∩ bn(φ) = ∅ and M_{1}φ > M_{2}φ.

Definition 26 (Syntactic equality in frame). M_{1} is syntactically equal to M_{2} in φ, written (M_{1} = M_{2})φ, if and only if n(M_{1}, M_{2}) ∩ bn(φ) = ∅ and M_{1}φ = M_{2}φ.

We can now define the satisfaction relation ⊨ for the propositional logic:

φ ⊨ M_{1} =_{E} M_{2}  =^{Δ} (M_{1} =_{E} M_{2})φ
φ ⊨ M_{1} > M_{2}  =^{Δ} (M_{1} > M_{2})φ
φ ⊨ M_{1} = M_{2}  =^{Δ} (M_{1} = M_{2})φ
φ ⊨ A_{1} ∨ A_{2}  =^{Δ} φ ⊨ A_{1} or φ ⊨ A_{2}
φ ⊨ ¬A  =^{Δ} φ ⊭ A

As discussed in the previous section, quantification should be restricted to the universe of terms which the environment can deduce from a given frame. Intuitively these are the terms which can be constructed by applying function symbols to terms from the ecores of the frame.

Definition 27 (Frame synthesis). The set of terms deducible from a frame φ is called the synthesis of φ and is defined inductively as follows:

S^{0}(φ) =^{Δ} ecores(φ)
S^{i+1}(φ) =^{Δ} S^{i} ∪ {f(T_{1}, …, T_{k}) | f ∈ Σ^{(k)} and T_{1}, …, T_{k} ∈ S^{i}(φ)}

It follows that the synthesis is infinite while the analysis and ecores are finite. Since any analysis term can be written as a context over ecores, the containment hierarchy between the three sets is

ecores(φ) ⊆ A(φ) ⊂ S(φ)

Note that the synthesis can alternatively be defined as the set of all contexts over ecores.

Our definition of synthesis is similar to that of deduction from frames by Abadi et al. in [2, Section 2.3], but there are two differences: first, deduction includes terms with arbitrary fresh names (i.e. non-private names which do not occur in the frame). Second, deduction also includes terms M with arbitrary bound names, as long as bound names in M ↓ occur only as subterms of analysis terms. For example, the term M = fst([a, b]) can be deduced from a frame where b is private and not in the analysis, but M would not be in the synthesis of such frame. The differences between deduction and synthesis are not significant for our purpose though; we adopt synthesis for technical convenience since any synthesis term per definition can be written as a primitive context over ecores. Also there does not seem to be any reason why terms with fresh names should be of interest in quantification.

The definition of satisfaction can now be completed with the case for existentially quantified formulae:

φ ⊨ ∃x(A_{1}) =^{Δ} φ{^{M}/_{x}} ⊨ A_{1} for some term M ∈ S(φ)

5.3. CHARACTERISATION

Observe how bindings of quantified variables are represented in a natural way by extending the frame with an additional substitution. In cases where x ∈ dom(φ) we assume alpha-conversion of x to some x′ ∉ dom(φ), since otherwise a quantification may overwrite existing terms in φ.

5.3 Characterisation

In this section we show that LF characterises ≈_{ss} and hence ≈′_{ss}. In order to do this, we need a result which says that two strong statically equivalent frames φ and φ′ can be extended with appropriate terms M and M′ while maintaining strong static equivalence. This will be expressed in the following two extension lemmas

Lemma 16 (Extension Lemma 1). Let φ = (νñ){^{M_{i}}/_{x_{i}}}_{i∈I} and φ′ = (νñ){^{M′_{i}}/_{x_{i}}}_{i∈I} be two frames with φ ≈_{ss} φ′, and let ecores(φ) = (N)_{j∈J} and ecores(φ′) = (N′)_{j∈J}. Then for any j ∈ J it holds that

φ{^{N_{j}}/_{x_{s}}} ≈_{ss} φ′{^{N′_{j}}/_{x_{s}}}

(where s is any index with s ∉ I).

Proof. It must be shown that both conditions of ≈_{ss} hold for the extended frames. For this we rely on Lemma 7 which says that N_{j} and N′_{j} have the same analysis recipes.

Condition 1. Suppose that (M_{1} =_{E} M_{2})φ{^{N_{j}}/_{y}}, i.e. n(M_{1}, M_{2})∩bn(φ{^{N_{j}}/_{y}}) = ∅ and M_{1}φ{^{N_{j}}/_{y}} =_{E} M_{2}φ{^{N_{j}}/_{y}}. If x_{s} ∉ v(M_{1}, M_{2}) we are done, so suppose that x_{s} ∈ v(M_{1}, M_{2}). Suppose further for notational convenience and without loss of generality that both x_{s} ∈ v(M_{1}) and x_{s} ∈ v(M_{2}). M_{1} and M_{2} are in fact contexts, so we reason as follows:

M_{1}φ{^{N_{j}}/_{y}}) =_{E} M_{2}φ{^{N_{j}}/_{y}}
C_{1}[x̃, x_{s}]φ{^{N_{j}}/_{x_{s}}} =_{E} C_{2}[x̃, x_{s}]φ{^{N_{j}}/_{x_{s}}}  ⇕
C_{1}[M̃, N_{j}] =_{E} C_{2}[M̃, N_{j}]

Now let R[x̃] be the analysis recipe for N_{j}. By Lemma 7 on p. 52, R[M̃] >^{k} N_{j} and hence also R[M̃] =_{E} N_{j}. Using that φ ≈_{ss} φ′ and condition 1 of ≈_{ss} we continue thus:

C_{1}[M̃, R[M̃]] =_{E} C_{2}[M̃, R[M̃]]
(C_{1}[x̃, R[x̃]] =_{E} C_{2}[x̃, R[x̃]])φ  ⇕
(C_{1}[x̃, R[x̃]] =_{E} C_{2}[x̃, R[x̃]])φ′  ⇕
C_{1}[M̃′, R[M̃′]] =_{E} C_{2}[M̃′, R[M̃′]]

By Lemma 7 again, R[x̃] is also the analysis recipe for N′_{j} and R[M̃] >^{k} N′_{j}. The proof of condition 1 can then be completed thus:

C_{1}[M̃′, N′_{j}] =_{E} C_{2}[M̃′, N′_{j}]
(C_{1}[x̃, x_{s}] =_{E} C_{2}[x̃, x_{s}])φ′{^{N′_{j}}/_{x_{s}}}  ⇕
(M_{1} =_{E} M_{2})φ′{^{N′_{j}}/_{x_{s}}}

Condition 2. This is somewhat similar to the proof of condition 1. If we again have that R[M̃] >^{k} N_{j} we use that φ ≈_{ss} φ′, and condition 2 in ≈_{ss} then allows us to reason as follows

(M >^{c})φ{^{N_{j}}/_{x_{s}}}
(C[x̃, x_{s}] >^{c})φ{^{N_{j}}/_{x_{s}}}  ⇕
C[M̃, N_{j}] >^{c}  ⇕
C[M̃, R[M̃]] >^{c+k}  ⇕
(C[x̃, R[x̃]] >^{c+k})φ  ⇕
(C[x̃, R[x̃]] >^{c+k})φ′  ⇕
C[M̃′, R[M̃′]] >^{c+k}  ⇕
C[M̃′, N′_{j}]] >^{c}  ⇕
(C[x̃, x_{s}] >^{c})φ′{^{N′_{j}}/_{x_{s}}}

In contrast to the proof of condition 1, the above line of reasoning relies crucially on Lemma 7 saying that R[M̃] >^{k} N_{j} and R[M̃′] >^{k} N′_{j}, i.e. that the recipe instances reduce in exactly the same number of steps to the respective cores.

Lemma 17 (Extension Lemma 2). Let φ = (νñ){^{M_{i}}/_{x_{i}}}_{i∈I} and φ′ = (νñ){^{M′_{i}}/_{x_{i}}}_{i∈I} be two frames with φ ≈_{ss} φ′, and let ecores(φ) = (N)_{j∈J} and ecores(φ′) = (N′)_{j∈J}. Then for any C[ỹ] it holds that

φ{^{C[Ñ]}/_{x_{s}}} ≈_{ss} φ′{^{C[Ñ′]}/_{x_{s}}}

(where s is any index with s ∉ I).

Proof. It must be shown that both conditions of ≈_{ss} hold for the extended frames. We just show condition 1 as condition 2 is similar.

Condition 1. Suppose that (M_{1} =_{E} M_{2})φ{^{C[Ñ]}/_{y}}), i.e. n(M_{1}, M_{2}) ∩ bn(φ{^{C[Ñ]}/_{y}}) = ∅ and M_{1}φ{^{C[Ñ]}/_{y}} =_{E} M_{2}φ{^{C[Ñ]}/_{y}}. If x_{s} ∉ v(M_{1}, M_{2}) we are done, so suppose that x_{s} ∈ n(M_{1}, M_{2}). Suppose further for notational convenience and without loss of generality that both x_{s} ∈ v(M_{1}) and x_{s} ∈ v(M_{2}).

First apply Lemma 16 iteratively to φ ≈_{ss} φ′ to get that

φ{^{N_{j}}/_{y_{j}}}_{j∈J} ≈_{ss} φ′{^{N′_{j}}/_{y_{j}}}_{j∈J}

We then use this to reason as follows.

C_{1}[x̃, y]φ{^{C[Ñ]}/_{y}} =_{E} C_{2}[x̃, y]φ{^{C[Ñ]}/_{y}}
C_{1}[M̃, C[Ñ]] =_{E} C_{2}[M̃, C[Ñ]]  ⇕
C_{1}[x̃, C[ỹ]]φ{^{N_{j}}/_{y_{j}}}_{j∈J} =_{E} C_{2}[x̃, C[ỹ]]φ{^{N_{j}}/_{y_{j}}}_{j∈J}  ⇕
C_{1}[x̃, C[ỹ]]φ′{^{N′_{j}}/_{y_{j}}}_{j∈J} =_{E} C_{2}[x̃, C[ỹ]]φ′{^{N′_{j}}/_{y_{j}}}_{j∈J}  ⇕
C_{1}[M̃′, C[Ñ′]] =_{E} C_{2}[M̃′, C[Ñ′]]  ⇕
C_{1}[x̃, y]φ′{^{C[Ñ′]}/_{y}} =_{E} C_{2}[x̃, y]φ′{^{C[Ñ′]}/_{y}}  ⇕
M_{1}φ′{^{C[Ñ′]}/_{y}} =_{E} M_{2}φ′{^{C[Ñ′]}/_{y}}

Technically we could also have given a direct proof of Lemma 17 above, but the presentation and notation would have been more involved. Note that static equivalence is not preserved by extension with arbitrary terms – take for example the following two frames in the theory E_{pub} (where we only use hash functions):

φ =^{Δ} (νa){^{f(a)}/_{x_{1}}}
φ′ =^{Δ} (νa){^{a}/_{x_{1}}}

Then φ ≈_{ss} φ′. But φ{^{f(a)}/_{x_{2}}} ≉_{ss} φ′{^{f(a)}/_{x_{2}}} because the equality x_{1} =_{E} x_{2} holds in the extended φ but not in the extended φ′. So even though all the equalities which hold in the original frames also hold in the extended frames, there may be new equalities which hold in only one of the extended frames. Hence it is essential that the two frames are extended with the same context over their respective cores.

With the second extension lemma in our toolbox we now arrive at the main result of this section, namely that the logic LF characterises ≈_{ss}. For stating the characterisation theorem we find it convenient to introduce the notion of a logical theory:

Definition 28. The logical theory of frame φ in the logic LF is the class of formulae in LF which are true in φ:

Th_{LF}(φ) =^{Δ} {A ∈ LF | φ ⊨ A}

Theorem 4 (LF characterises ≈_{ss}). φ ≈_{ss} φ′ ⇔ Th_{LF}(φ) = Th_{LF}(φ′).

Proof. Let φ ≡ (νñ){^{M_{i}}/_{x_{i}}}_{i∈I} and φ′ ≡ (νñ){^{M′_{i}}/_{x_{i}}}_{i∈I} be any frames with ecores(φ) = (N)_{j∈J} and ecores(φ′) = (N′)_{j∈J}. There are two directions to prove.

(⇐) Suppose that Th_{LF}(φ) = Th_{LF}(φ′), i.e. (φ ⊨ A ⇔ φ′ ⊨ A) for all formulae A ∈ LF. In particular this holds for the class of formulae M_{1} =_{E} M_{2}, i.e. (φ ⊨ M_{1} =_{E} M_{2} ⇔ φ′ ⊨ M_{1} =_{E} M_{2}). Per definition of satisfaction, (M_{1} =_{E} M_{2})φ ⇔ (M_{1} =_{E} M_{2})φ′, which proves condition 1.

Condition 2 in ≈_{ss} states that (M >^{k})φ ⇔ (M >^{k})φ′; we show the direction from left to right (the converse is symmetric). So suppose that (M >^{k})φ, which per definition of rewrites in frames means that n(M)∩bn(φ) = ∅ and M >^{k} M^{k} for some M^{k}. Expanding on the transitive closure relation, there are terms M^{1}, …, M^{k−1} such that M > M^{1} > ⋯ > M^{k−1} > M^{k}. Each of these terms are clearly in S(φ), so it holds that:

φ ⊨ ∃y_{1}∃y_{2} … ∃y_{k}(M > y_{1} ∧ y_{1} > y_{2} ∧ ⋯ ∧ y_{k−1} > y_{k})

and per assumption also

φ′ ⊨ ∃y_{1}∃y_{2} … ∃y_{k}(M > y_{1} ∧ y_{1} > y_{2} ∧ ⋯ ∧ y_{k−1} > y_{k})

which per definition of satisfaction means that there are terms M^{1}, …, M^{k} ∈ S(φ′) such that M > M^{1} > ⋯ > M^{k−1} > M^{k}. Hence (M >^{k})φ′.

(⇒) Suppose that φ ≈_{ss} φ′. We show by structural induction on formula A that (φ ⊨ A ⇒ φ′ ⊨ A) holds for all formulae A; the proof of the converse is identical.

Basis Case: A = (M_{1} =_{E} M_{2}). Per definition of satisfaction, (M_{1} =_{E} M_{2})φ. Per assumption of static equivalence also (M_{1} =_{E} M_{2})φ′, which again per definition of satisfaction means that φ′ ⊨ M_{1} =_{E} M_{2}.

Case: A = (M_{1} > M_{2}). Per definition of satisfaction, M_{1}φ > M_{2}φ and n(M_{1}, M_{2}) ∩ bn(φ) = ∅. We then have that M_{1} and M_{2} are in fact contexts over variables and free names ñ, and as in the proof of Theorem 1 we get that

C_{M_{1}}[M_{a_{1}}, … M_{a_{s}}, ñ] > C_{M_{2}}[M_{b_{1}}, … M_{b_{s}}, ñ]

Since ≈_{ss} implies ≈′_{ss}, we can rely on the definition of ≈′_{ss} and the results from Subsection 4.1. Condition 1 in ≈′_{ss} gives that each M ∈ im(φ) can be written as a context over ecores, and since any free name is also an ecore we have that

C_{M_{1}}[C_{a_{1}}[Ñ], … C_{a_{s}}[Ñ], Ñ] > C_{M_{2}}[C_{b_{1}}[Ñ], … C_{b_{s}}[Ñ], Ñ]

Applying Lemma 5 (p. 48) gives:

C_{M_{1}}[C_{a_{1}}[Ñ′], … C_{a_{s}}[Ñ′], Ñ] > C_{M_{2}}[C_{b_{1}}[Ñ′], … C_{b_{s}}[Ñ′], Ñ]

By condition 1 of ≈′_{ss} again, each context C_{a_{i}}[Ñ] is syntactically equal to the corresponding term M′_{a_{1}} ∈ im(φ′), and since φ and φ′ have the same free names we get

C_{M_{1}}[M′_{a_{1}}, … M′_{a_{s}}, ñ] > C_{M_{2}}[M′_{b_{1}}, … M′_{b_{s}}, ñ]

Hence M_{1}φ′ > M_{2}φ′, which for the terms M_{1} and M_{2} is equivalent to (M_{1} > M_{2})φ′.

5.4. CHARACTERISTIC FORMULAE

Case: A = (M_{1} = M_{2}). Per definition of satisfaction, M_{1}φ = M_{2}φ and n(M_{1}, M_{2}) ∩ bn(φ) = ∅. An argument similar to the proof above applies, except that we call on Lemma 2 (p. 46) instead of Lemma 5. This gives that M_{1}φ′ = M_{2}φ′, i.e. φ′ ⊨ M_{1} = M_{2}.

Step Case: A = ¬A_{1}. By the induction hypothesis and the assumption φ ≈_{ss} φ′ we have that (φ ⊨ A_{1}) ⇔ (φ′ ⊨ A_{1}), which is equivalent to (φ ⊭ A_{1}) ⇔ (φ′ ⊭ A_{1}). This per definition of satisfaction implies that (φ ⊨ ¬A_{1}) ⇔ (φ′ ⊨ ¬A_{1}).

Case: A = A_{1} ∨ A_{2}. By the induction hypothesis we have that (φ ⊨ A_{i}) ⇔ (φ′ ⊨ A_{i}) for i = 1, 2. There are three sub-cases to consider: 1) φ and φ′ both satisfy A_{1} and A_{2} and hence both satisfy A_{1} ∨ A_{2}. 2) Neither φ nor φ′ satisfy A_{1} and A_{2} and hence neither satisfy A_{1} ∨ A_{2}. 3) φ and φ′ both satisfy exactly one of A_{1} and A_{2} and hence they both satisfy A_{1} ∨ A_{2}. Hence (φ ⊨ A_{1} ∨ A_{2}) ⇔ (φ′ ⊨ A_{1} ∨ A_{2})

Case: A = ∃xA_{1}. Per definition of satisfaction, φ ⊨ ∃x(A_{1}) means that φ{^{M}/_{x}} ⊨ A_{1} for some M ∈ S(φ). Any synthesis term can be written as a context over ecores, i.e. M = C[Ñ] for some context C[ỹ]. Let M′ = C[Ñ′]. The second extension lemma (Lemma 17) then says that a φ{^{M}/_{x}} ≈_{ss} φ′{^{M′}/_{x}}. Applying the induction hypothesis to this gives that also φ′{^{M′}/_{x}} ⊨ A_{1}. Now any context over cores is a synthesis term, so per definition of satisfaction we get that φ′ ⊨ ∃xA_{1}.

We have now shown that the first order logic LF characterises ≈_{ss} (and hence also ≈′_{ss}). One may ask if the propositional logic alone, without existential quantification, would also characterise ≈_{ss}. The answer is probably no. For existential quantification was used in the above proof to show condition 2 of ≈_{ss}. Condition 2 states, as a special case, that whenever a term M_{i} ∈ im(φ) can reveal a subterm M_{i}|_{w} then the corresponding term M′_{i} ∈ im(φ′) can reveal the corresponding subterm M′_{i}|_{w}. Hence condition 2 indirectly involves analysis terms. But the basic propositions in LF cannot be used to reason about arbitrary analysis terms because they cannot include terms with private names. Hence it would seem that existential quantification over the synthesis (and hence also over the analysis) is strictly necessary for characterisation.

5.4 Characteristic Formulae

We have now given syntax and semantics for a logic of frames and shown that it characterises ≈′_{ss}. The development of ≈′_{ss}, and the choice of atomic propositions for the logic, has been guided by our desire to find characteristic formulae for frames. But ≈′_{ss} is still too high-level to yield a direct encoding into characteristic formula. The problem has been pointed out earlier, namely that condition 2 and 3 in ≈′_{ss} involve infinitely many contexts. In the first subsection we therefore set out to give a further refinement of strong static equivalence which does not exhibit this problem. In subsections 2 and 3, encodings of revelation and ecores into the logic are given. Subsection 4 gives an encoding of each of the conditions in the further refined definition of strong static equivalence, and subsection 5 collects the efforts to give a unified construction of characteristic formula.

5.4.1 A Further Refinement of Strong Static Equivalence

Recall from Section 3.3 that condition 2 in the definition of ≈′_{ss} generally involves infinitely many partitioning contexts which are unifiable with, but neither more general than or less general than, the LHS of some rewrite rule. We gave an example with the public key rewrite rule which gives rise to the following infinite sequence of partitioning contexts:

dec(enc(⊥, y_{1}), y_{2}),
dec(enc(⊥, y_{1}^{+}), y_{2}),
dec(enc(⊥, f(y_{1})^{+}), y_{2}),
dec(enc(⊥, f(f(y_{1}))^{+}), y_{2}),
…

A characteristic formula must capture all the instantiations of partitioning contexts which are not reducible, e.g. that

dec(enc(⊥, N_{1}), N_{2}) ≯,
dec(enc(⊥, N_{1}^{+}), N_{2}) ≯,
dec(enc(⊥, f(N_{1})^{+}), N_{2}) ≯,
dec(enc(⊥, f(f(N_{1}))^{+}), N_{2}) ≯,
…

But expressing this directly in the logic would give rise to infinite conjunction. Instead we just choose the first of the contexts and use existential quantification to express that

¬∃y^{∗}.dec(enc(⊥, y^{∗}), N_{2}) >

This works because existential quantification ranges over the synthesis of a frame and because every synthesis term can be written as a context over cores. The chosen context is what we refer to as a minimised context, the definition of which is given next.

Definition 29 (Minimised Contexts). A minimised context C[ỹ, ỹ^{∗}] is a context with C[ỹ, ỹ^{∗}] ⊐ such that every superterm of y^{∗} ∈ ỹ^{∗} contains ⊥ or some y ∈ ỹ; formally, whenever C[ỹ]|_{w} = y^{∗} ∈ ỹ^{∗} it holds for every proper prefix w′ of w that st(C[ỹ]|_{w′}) ∩ ({⊥} ∪ ỹ) ≠ ∅.

ỹ^{∗} is a distinguished set of variables, referred to as the minimised variables, which are intended to be bound to synthesis terms rather than ecores.

Since minimised contexts are per definition more general than some rewrite rule, there are only finitely many of them. This enables us to give a further refinement of strong static equivalence using existential quantification and involving only finitely many contexts in the rewrite conditions. The problem with infinitely many contexts in condition 2 of ≈′_{ss} is resolved in a similar (but more straight forward) manner.

Definition 30 (Further Refined Strong Static Equivalence). Let φ ≡ (νñ){^{M_{i}}/_{x_{i}}}_{i∈I} and φ′ ≡ (νñ){^{M′_{i}}/_{x_{i}}}_{i∈I} be two frames with ecores(φ) = (N)_{j∈J}, ecores(φ′) = (N′)_{j∈J}. Then define φ ≈′′_{ss} φ′ iff dom(φ) = dom(φ′) and for each i ∈ I the following conditions hold:

1 For some context C[ỹ] it holds that

• M_{i} = C[Ñ]
• M′_{i} = C[Ñ′]

2a For all i, j ∈ J it holds that

N_{i} = N_{j} ⇔ N′_{i} = N′_{j}

2b For all contexts C[ỹ] and for all j ∈ J it holds that

C[Ñ] = N_{j} ⇒ C[Ñ′] = N′_{j}

2c If there there is no context C[ỹ] and j ∈ J s.t. C[Ñ] = N_{j}, then it must hold for all f(x_{1}, …, x_{k}) ∈ Σ^{(k)} that:

¬∃M_{1}, …, M_{k} ∈ S(φ′).f(M_{1}, …, M_{k}) = N′_{j}

3a For any partitioning context C_{1}^{⊥}[ỹ] where C_{1}^{⊥}[ỹ] ⊐ it holds for all C_{2}^{⊥}[ỹ] that

C_{1}^{⊥}[Ñ] > C_{2}^{⊥}[Ñ] ⇔ C_{1}^{⊥}[Ñ′] > C_{2}^{⊥}[Ñ′]

3b For any partitioning context C_{1}^{⊥}[ỹ] where C_{1}^{⊥}[ỹ]□ it holds for all C_{2}^{⊥}[ỹ] that

C_{1}[Ñ] > C_{2}[Ñ] ⇒ C_{1}[Ñ′] > C_{2}[Ñ′]

3c For any minimised partitioning context C_{1}^{⊥}[ỹ, ỹ^{∗}] where C_{1}^{⊥}[ỹ, ỹ^{∗}]□ it holds for all C_{2}^{⊥}[ỹ] that

¬∃T_{1}, …, T_{k} ∈ S(φ).C_{1}[Ñ, T_{1}, …, T_{k}] >_{r} C_{2}[Ñ] ⇒

¬∃T′_{1}, …, T′_{k} ∈ S(φ′).C_{1}[Ñ′, T′_{1}, …, T′_{k}] >_{r} C_{2}[Ñ′]

Lemma 18. ≈′_{ss} and ≈′′_{ss} coincide.

Proof. In other words, we must show for all frames that φ ≈′_{ss} φ′ ⇔ φ ≈′′_{ss} φ′. So there are two directions to prove; we start with the easiest one.

(⇒). Suppose that φ ≈′_{ss} φ′. We must show that all conditions in ≈′′_{ss} are satisfied.

Condition 1. This is the same as condition 1 in ≈′_{ss}.

Conditions 2a and 2b. These are both special cases of condition 2 in ≈′_{ss} (to get condition 2a just choose C[Ñ] to be the trivial context y_{j}).

Condition 2c. Suppose for a contradiction that condition 2c fails, i.e. there is no context C[ỹ] and j ∈ J such that C[Ñ] = N_{j}, but there is some function symbol f(x_{1}, …, x_{k}) ∈ Σ^{(k)} and some terms T′_{1}, …, T′_{k} ∈ S(φ′) such that f(T′_{1}, …, T′_{k}) = N′_{j}. Per definition of synthesis, each T′_{i} can be written as a context over cores, i.e. T′_{i} = C_{i}[Ñ′]. This gives that f(C_{1}[Ñ′], …, C_{k}[Ñ′]) = N′_{j}. By condition 2 in the definition of ≈′_{ss} it also holds that f(C_{1}[Ñ], …, C_{k}[Ñ]) = N_{j}, which contradicts the assumption that no such context exists.

Conditions 3a and 3b. These are both special cases of condition 3 in ≈′′_{ss} Condition 3c. We show the contraposition of condition 3c (the idea is

similar to that employed for condition 2c). So suppose that there are terms T′_{1}, …, T′_{k} ∈ S(φ′) such that C_{1}[Ñ′, T′_{1}, …, T′_{k}] > C_{2}[Ñ′]. Per definition of synthesis, each T′_{i} can be written as a context over cores, i.e. T′_{i} = C_{T_{i}}[Ñ′]. This gives that C_{1}[Ñ′, C_{T_{1}}[Ñ′], …, C_{T_{k}}[Ñ′]] > C_{2}[Ñ′_{j}]. By condition 2 in the definition of ≈′_{ss} it also holds that C_{1}[Ñ, C_{T_{1}}[Ñ], …, C_{T_{k}}[Ñ]] > C_{2}[Ñ]. Hence there are T_{1}, …, T_{k} ∈ S(φ) such that C_{1}[Ñ, T_{1}, …, T_{k}] > C_{2}[Ñ] (namely T_{i} = C_{T_{i}}[Ñ]).

(⇐). Suppose that φ ≈′′_{ss} φ′. We must show that all three conditions in ≈′_{ss} are satisfied.

Condition 1. This is the same as condition 1 in ≈′′_{ss}.

Condition 2. It must be shown that C[Ñ] = N_{j} ⇔ C[Ñ′] = N′_{j}. The direction from left to right is immediate from condition 2b. For the other direction we assume C[Ñ′] = N′_{j} and show that also C[Ñ] = N_{j}. This goes by induction in the height h of the parse tree of the term N′_{j}.

Basis (h = 0). Then N′ is a name and we get that C[ỹ] is the trivial context y_{j} for some j. The result then follows from condition 2a.

Step (assume for h, prove for h + 1). If C[ỹ] is the trivial context, i.e. C[ỹ] = y_{i} for some i, we have that N′_{i} = N′_{j} and the result follows immediately from condition 2a.

Otherwise we assume for notational simplicity that C[Ñ′] = f(C_{2}[Ñ′]) = N′_{j} for some context C_{2}[ỹ], i.e. the unary function symbol f is the outer-most function symbol of N′_{j} (the generalisation is straight forward). We first show that

f(C_{3}[Ñ]) = N_{j} for some context C_{3}[ỹ]

i.e. that f is also the outer-most function symbol of N_{j}. To see this observe that there must be some context C_{4}[ỹ] such that C_{4}[Ñ] = N_{j}. For otherwise condition 2d gives that there is no function symbol f(x_{1}, …, x_{k}) ∈ Σ^{(k)} and no terms T_{1}, …, T_{k} ∈ S(φ′) such that f(T_{1}, …, T_{k}) = N′_{j}. But this is impossible because each core N′ is in S(φ) and C[Ñ′] = N′_{j}. Now condition 2c gives that also C_{4}[Ñ′] = N′_{j}, and hence C_{4}[Ñ′] = f(C_{2}[Ñ′]). So we conclude that C_{4}[Ñ] = f(C_{3}[Ñ]) = N_{j} for some context C_{3}[Ñ].

Next we show that

C_{3}[Ñ] = C_{2}[Ñ]

It follows from f(C_{3}[Ñ]) = N_{j} and condition 2b that also f(C_{3}[Ñ′]) = N′_{j}. We also have that f(C_{2}[Ñ′]) = N′_{j}, so it must hold that C_{3}[Ñ′] = C_{2}[Ñ′]. The induction hypothesis gives that condition 2 in the definition of ≈′_{ss} holds for cores with parse trees of height h or less, and thus Lemma 2 (p. 46) applies for terms with parse trees of height h or less. Hence the lemma applies to the present equality, and we may conclude that C_{3}[Ñ] = C_{2}[Ñ]. This in turn establishes that C[Ñ] = N_{j}, which completes the inductive proof of condition 2.

Condition 3. We must show that C_{1}[Ñ] >_{r} C_{2}[Ñ] ⇔ C_{1}[Ñ′] >_{r} C_{2}[Ñ′]. The direction from left to right is immediate from 3b. For the other direction suppose that C_{1}[Ñ′] >_{r} C_{2}[Ñ′]. In order to keep the notation simple, we just show this result for a specific rewrite rule and a specific context. We choose a rewrite rule which is sufficiently complex to exhibit the essence of the proof, namely the extended public key encryption rule in E_{pub2}– it should be clear as we proceed that the arguments can be lifted to the general case:

Rewrite rule: dec(enc(z_{1}, f(z_{2}^{+}, z_{3}^{+})), f(z_{2}^{−}, z_{3}^{−}) >_{r} z_{1}
Context C_{1}[Ñ′] =dec(enc(⊥, y_{1}), f(g(y_{2})^{−}, y_{3})

Now, in this example we would have that

dec(enc(⊥, N′_{1}), f(g(N′_{2})^{−}, N′_{3}) > ⊥

and hence there is a T′ ∈ S(φ′) (namely T′ = g(N′_{2})^{−}) such that

dec(enc(⊥, N′_{1}), f(T′, N′_{3}) > ⊥

The relevant context, namely

dec(enc(⊥, y_{1}), f(y_{2}^{∗}, y_{3})

is a minimised context and hence condition 3c applies. From contraposition of 3c it follows that there is a T ∈ S(φ) such that

dec(enc(⊥, N_{1}), f(T, N_{3}) > ⊥

Since any synthesis term can be written as a context over cores, there is a context C[ỹ] such that T = C[Ñ], i.e.

dec(enc(⊥, N_{1}), f(C[Ñ], N_{3}) > ⊥

By condition 3b it also holds that

dec(enc(⊥, N′_{1}), f(C[Ñ′], N′_{3}) > ⊥

This implies that C[Ñ′] = g(N′_{2})^{−} because y_{2}^{∗} is strongly correlated to y_{1} (in general, Lemma 9 on p. 53 gives that minimised variables will always be strongly correlated to some variable akin to y_{1}). Hence also C[Ñ] = g(N_{2})^{−} by Lemma 2 (p. 46). This concludes the proof, since we now get that

dec(enc(⊥, N_{1}), f(g(N_{2})^{−}, N_{3}) > ⊥

5.4.2 Encoding Revelation

Recall that we defined M ≻_{A(φ)} M|_{w} to express that there are terms T_{1}, …, T_{k} ∈ A(φ) and a destructor context D[y, y_{1}, …, y_{k}] such that D[M, T_{1}, …, T_{k}] >_{r}^{M} M|_{w}. Observe that there are always infinitely many potential destructor contexts which can be used for a given revelation, again because it always holds that D[y, y_{1}, …, y_{k}]□. In the theory of public key encryption, the following is an example of an infinite sequence of destructor context:

dec(y_{1}, y_{2})
dec(y_{1}, y_{2}^{+})
dec(y_{1}, f(y_{2})^{+})
dec(y_{1}, f(f(y_{2}))^{+})
…

As in the previous subsection we rely on minimised contexts to avoid infinite conjunctions. The key observation is the following: whenever a revelation from M is possible by D[M, T̃] > M|_{w} where T̃ ⊆ A(φ), the same revelation is also possible using some minimised context D^{∗}[y, ỹ^{∗}] and terms from the synthesis, i.e. D^{∗}[M, T̃^{∗}] > M|_{w} where T̃^{∗} ⊂ S(φ). This is an immediate consequence of the definition of minimised contexts and the fact that any context over analysis terms is a synthesis term. We illustrate this fact with an example.

Example 5.4.1. Consider a frame φ and a term M = enc(a, k^{+}) in the usual public key theory E_{pub} and suppose that T = k ∈ A(φ).Then M_{1} ≻_{A(φ)} a because the rewrite dec(M, T^{+}) > a is possible. The relevant context, namely dec(y_{1}, y_{2}^{−}), can be minimised to obtain dec(y_{1}, y_{2}^{∗}). The term T^{∗} = k^{−} is in the synthesis of φ (because k is in the analysis), and we get the reduction dec(M, T^{∗}) > a. So the revelation of a from M is possible using the minimised context and synthesis terms instead of analysis terms.

Since there finitely many minimised contexts, the following set is finite:

S_{destruct} = {D[y, ỹ^{∗}] | D[y, ỹ^{∗}] is a minimised destructor context} We are now in a position to encode the revelation relation in our logic:

M ≻ T =^{Δ} ⋁_{D[y,y_{1}^{∗},...,y_{k}^{∗}]∈S_{destruct}} ∃y_{1}^{∗} … ∃y_{k}^{∗}(D[M, y_{1}^{∗}, …, y_{k}^{∗}] > T)

5.4.3 Encoding Ecores

Let φ ≡ (νñ){^{M_{i}}/_{x_{i}}}_{i∈I} be any frame, let ecores(φ) = N_{1}, …, N_{s}, let R_{j}[x̃] be the analysis recipe for each N_{j} and let k_{j} ∈ ℕ be such that R_{j}[M̃] >^{k_{j}} N_{j}. For each ecore N_{j} we can construct a formula ψ_{ecore−j}(y) with a free variable y which says that y is the ecore N_{j}:

ψ_{ecore−j}(y) =^{Δ} ∃y_{1} … ∃y_{k_{j}}(R_{j}[x̃] > y_{1} ∧ y_{2} > y_{3} ∧ ⋯ ∧ y_{k_{j}−1} > y)∧

[¬∃y_{2}(y ≻ y_{2})∨

⋀_{f(y_{1},...,y_{s})∈Σ^{(s)}} ∀y_{1}, …, y_{s}¬(y = f(y_{1}, …, y_{s}))]

The first part of this formula says that the recipe instance for N_{j} must reduce to y in exactly k_{j} steps. The second part is a disjunction which expresses that either y is a pure core (the first disjunct) or y is an extended core (the second disjunct).

The characteristic formulae must first of all bind each ecore N_{j} to some variable y_{j}. No ”let” construct is available in the logic, but existential quantification can serve a similar purpose (this is sound since every core is a synthesis term). Below is given the first step in the construction of a characteristic formula for φ. The sub-formula C′_{φ} encodes each of the conditions in ≈′′_{ss} and will be defined in the subsequent sections.

C_{φ} = ∃y_{1} … ∃y_{k}(ψ_{ecore−1}(y_{1}) ∧ ⋯ ∧ ψ_{ecore−k}(y_{k}) ∧ C′_{φ})

5.4.4 Encoding The Conditions

Let φ ≡ (νñ){^{M_{i}}/_{x_{i}}}_{i∈I} and let ecores(φ) = N_{1}, …, N_{s}. We continue the construction of the characteristic formula C_{φ} for φ by encoding each of the conditions in ≈′′_{ss} into a formulae ψ_{cond}, each of which will feature as a conjunct in C′_{φ}. The encodings will refer to the ecores bound to the variables ỹ above.

Condition 1

Each M_{i} can be written as a context over ecores – let C_{i}[ỹ] be any such context. Condition 1 in ≈′′_{ss} is then expressed in the following formulae:

ψ_{cond−1} =^{Δ} ⋀_{i∈I} x_{i} = C_{i}[ỹ]

Condition 2a Define the sets

S_{2a} =^{Δ} {(i, j) | N_{i} = N_{j}}

S̄_{2a} =^{Δ} {(i, j) | N_{i} ≠ N_{j}}

The following formula encodes condition 2a:

ψ_{cond−2a} =^{Δ} ⋀_{(i,j)∈S_{2a}} y_{i} = y_{j} ∧ ⋀_{(i,j)∈S̄_{2a}} y_{i} ≠ y_{j}

Condition 2b Define the set

S_{2b} =^{Δ} {(C[ỹ], j) | C[Ñ] = N_{j}}

The following formula encodes condition 2b:

ψ_{cond−2b} =^{Δ} ⋀_{(C[ỹ],j)∈S_{2b}} C[ỹ] = y_{j}

Condition 2c Define the set

S_{2c} =^{Δ} {j | there is no context C[ỹ] such that C[Ñ] = N_{j}}

The following formula encodes condition 2c:

ψ_{cond−2c} =^{Δ} ⋀_{j∈S_{2c}} ⋀_{f(z_{1},...,z_{k})∈Σ^{k}} ∀z_{1} … ∀z_{k}(¬f(z_{1}, …, z_{k}) = y_{j})

Condition 3a Define the sets

S_{3a} =^{Δ} {(C_{1}^{⊥}[ỹ], C_{2}^{⊥}[ỹ]) | C_{1}[ỹ] is partitioning ∧ C_{1}^{⊥}[Ñ] ⊐ ∧C_{1}^{⊥}[Ñ] > C_{2}^{⊥}[Ñ]}

S̄_{3a} =^{Δ} {(C_{1}^{⊥}[ỹ], C_{2}^{⊥}[ỹ]) | C_{1}[ỹ] is partitioning ∧ C_{1}^{⊥}[Ñ] ⊐ ∧C_{1}^{⊥}[Ñ] ≯ C_{2}^{⊥}[Ñ]}

The following formula encodes condition 3a:

ψ_{cond−3a} =^{Δ} ⋀_{(C_{1}^{⊥}[ỹ],C_{2}^{⊥}[ỹ])∈S_{3a}} C_{1}^{⊥}[ỹ] > C_{2}^{⊥}[ỹ] ∧ ⋀_{(C_{1}^{⊥}[ỹ],C_{2}^{⊥}[ỹ])∈S̄_{3a}} ¬C_{1}^{⊥}[ỹ] > C_{2}^{⊥}[ỹ]

Condition 3b

Define the set

S_{3b} =^{Δ} {(C_{1}^{⊥}[ỹ], C_{2}^{⊥}[ỹ]) | C_{1}[ỹ] is partitioning ∧ C_{1}^{⊥}[Ñ]□ ∧ C_{1}^{⊥}[Ñ] > C_{2}^{⊥}[Ñ]}

The following formula encodes condition 3b:

ψ_{cond−3b} =^{Δ} ⋀_{(C_{1}^{⊥}[ỹ],C_{2}^{⊥}[ỹ])∈S_{3b}} C_{1}^{⊥}[ỹ] > C_{2}^{⊥}[ỹ]

Condition 3c

Define the set

S_{3c} =^{Δ} {C_{1}^{⊥}[ỹ, z_{1}, …, z_{t}] | C_{1}^{⊥}[ỹ, z_{1}, …, z_{t}] is a minimised partitioning context ∧

¬∃T_{1}, …, T_{k} ∈ S(φ).C_{1}[Ñ, T_{1}, …, T_{k}] >}

The following formula encodes condition 3c:

ψ_{cond−3c} =^{Δ} ⋀_{C_{1}^{⊥}[ỹ,z_{1},...,z_{t}]∈S_{3c}} ∀z_{1} … ∀z_{k}∀z(¬C_{1}^{⊥}[ỹ, z_{1}, …, z_{k}] > z)

5.4.5 Putting it Together

The construction of a characteristic formula C_{φ} was started in Subsection 5.4.3 and Subsection 5.4.4 gave an encoding of the conditions in ≈′′_{ss}, each of which should feature as a conjunct in C_{φ}. All that remains now is to put it all together.

Definition 31 (Characteristic Formula). Let φ ≡ (νñ){^{M_{i}}/_{x_{i}}}_{i∈I} be any frame, let ecores(φ) = N_{1}, …, N_{s}, let R_{j}[x̃] be the analysis recipe for each N_{j} and let k_{j} ∈ ℕ be such that R_{j}[M̃] >^{k_{j}} N_{j}. We now rely on the constructions in the previous subsections to give a definition of the characteristic formula for φ, C_{φ}:

C_{φ} =^{Δ} ∃y_{1} … ∃y_{k}(
ψ_{ecore−1}(y_{1}) ∧ ⋯ ∧ ψ_{ecore−k}(y_{k})∧
ψ_{cond−1}∧
ψ_{cond−2a} ∧ ψ_{cond−2b} ∧ ψ_{cond−2c}
ψ_{cond−3a} ∧ ψ_{cond−3b} ∧ ψ_{cond−3c})

Theorem 5. For any frames φ and φ′ with dom(φ) = dom(φ′) it holds that

φ ≈_{ss} φ′ ⇔ φ′ ⊨ C_{φ}

Proof. It is clear from the construction of C_{φ} that

φ ≈′′_{ss} φ′ ⇔ φ′ ⊨ C_{φ}

By Lemma 18, ≈′′_{ss} and ≈′_{ss} coincide, and by Theorem 1 and Theorem 2, ≈′_{ss} and ≈_{ss} coincide.

5.5 Summary

We have given a first order logic for frames, LF, with atomic propositions for asserting equality, syntactic equality and reductions, which enable direct reasoning about the terms contained in a frame. Quantification ranges over the synthesis of a frame which intuitively is the set of terms that can be constructed by applying function symbols to ecores. Quantification hence enables indirect reasoning about the knowledge represented by a frame, which is essential for expressing e.g. that there is some term y_{1} (known to the environment) that can be used to decrypt x_{1} and obtain some analysis term y_{2}.

It has been shown that LF characterises strong static equivalence. Furthermore, we have given a construction of characteristic formulae. This construction relies on a further refinement of strong static equivalence which does not involve any universal quantification over contexts. The existence of characteristic formulae is an important result which shows the expressive power of the logic: LF is sufficiently powerful to describe all the essential features of a frame (with respect to static equivalence) in a single finite formula.

A Logic for Applied π

In the previous chapter a logic for frames was developed. It was shown that the logic characterises static equivalence on frames and a construction of characteristic formulae was given. In this chapter we build upon the logic for frames and extend it with Hennessy-Milner modalities, yielding a logic for Applied π processes which characterises labelled bisimilarity. The resulting logic can be used to reason about the dynamic behaviour of a process as well as the static knowledge represented by the frame of the process, allowing assertions such as process P can perform an input of an encrypted term M_{1} followed by some output, after which the decryption key for the term M_{1} is known by the environment to be expressed.

Section 1 presents the syntax of the Applied π logic and Section 2 gives the semantics in terms of a satisfaction relation. The choice of syntax and semantics is to some extent predetermined by our intention for the logic to characterise labelled bisimilarity, so we will be brief with the presentation. Section 3 discusses two additional logical construct which can be defined from the basic logic, namely match and the matching input modality. Finally section 4 contains a proof that the logic characterises labelled bisimilarity; this relies on the results from the previous chapter which say that the underlying logic of frames characterises strong static equivalence.

6.1 Syntax

The definition of labelled bisimilarity between processes includes conditions on internal reduction, output transitions, bound output transitions and input transitions. The syntax of the logic LA for Applied π must therefore include modalities for each of these transitions in addition to the propositional connectives and the constructs from the logic of frames:

CHAPTER 6. A LOGIC FOR APPLIED π

A ::=M_{1} =_{E} M_{2} | M_{1} > M_{2} | M_{1} = M_{2} | ∃x(A_{1})
|¬A_{1} | A_{1} ∨ A_{2} | (A_{1})
|⟨τ⟩A_{1}
|⟨ā⟩A_{1}
|⟨νā⟩A_{1}
|⟨a(u)⟩A_{1}

For example, the modal formula ⟨a(x)⟩A_{1} expresses that a process can do an input on channel a, bound to the variable x, after which the process satisfies A_{1}. The full range of propositional and first order connectives can be defined in the same manner as for LF. Similarly, the dual modalities (necessity) can be defined as usual; for example the dual modality of ⟨τ⟩ is defined thus:

[τ]A_{1} =^{Δ} ¬⟨τ⟩¬A_{1}

Note that constructs from the logic of frames may be freely mixed with the modalities. This opens up the possibility to reason about environment knowledge over time. Take for example the following formula:

∃x_{1}(⟨ā⟩⟨a(y)⟩∃x_{2}(dec(y, x_{1}) > x_{2}))

This formula expresses that a decryption key x_{1} for the term which is input at some later stage is known up front; more specifically, it says that there is a known decryption key x_{1} such that, after outputting some arbitrary term and inputting y, y can be decrypted with x_{1} to obtain some x_{2}. A bigger example will be given in the next chapter where the logic is applied to reasoning about a security protocol.

6.2 Semantics

Semantics for the modalities is guided by our intention for LA to characterise labelled bisimilarity. Since this is a weak bisimilarity, the modalities must also be weak, i.e. input and output actions may be preceded and followed by any number of internal actions. Let ⊨_{LF} be the satisfaction relation for LF. The satisfaction relation for LA can then be defined as follows:

6.3. MATCH AND MATCHING INPUT MODALITY

P ⊨ M_{1} =_{E} M_{2}  =^{Δ} φ(P) ⊨_{LF} M_{1} =_{E} M_{2}
P ⊨ M_{1} = M_{2}  =^{Δ} φ(P) ⊨_{LF} M_{1} = M_{2}
P ⊨ M_{1} > M_{2}  =^{Δ} φ(P) ⊨_{LF} M_{1} > M_{2}
P ⊨ ∃x(A_{1})  =^{Δ} there exists M ∈ S(φ(P)) s.t. (P | {^{M}/_{x}}) ⊨ A_{1}
P ⊨ ¬A_{1}  =^{Δ} P ⊭ A_{1}
P ⊨ A_{1} ∨ A_{2}  =^{Δ} P ⊨ A_{1} or P ⊨ A_{2}
P ⊨ (A_{1})  =^{Δ} P ⊨ A_{1}
P ⊨ ⟨τ⟩A_{1}  =^{Δ} there exists P′ s.t. P ⟶^{τ}^{∗} P′ and P′ ⊨ A_{1}
P ⊨ ⟨ā⟩A_{1}  =^{Δ} there exists u, P′ s.t. P ⟶^{τ}^{∗}⟶^{\overline{a}⟨u⟩}⟶^{τ}^{∗} P′ and P′ ⊨ A_{1}
P ⊨ ⟨νā⟩A_{1}  =^{Δ} there exists u, P′ s.t. P ⟶^{τ}^{∗}⟶^{(νu)\overline{a}⟨u⟩}⟶^{τ}^{∗} P′ and P′ ⊨ A_{1}
P ⊨ ⟨a(x)⟩A_{1}  =^{Δ} there exists M, P′ s.t. P ⟶^{τ}^{∗}⟶^{a(M)}⟶^{τ}^{∗} P′ and P′ ⊨ A_{1}{^{M}/_{x}}

6.3 Match and Matching Input Modality

Syntax and semantics for the Applied π logic have now been given. In this section we consider two additional operators which are not part of the basic logic. The first is match ([M_{1} =_{E} M_{2}]A) which asserts that whenever the match predicate holds, the formula A must be true. The second is the matching input modality (⟨a(^{M}/_{x})⟩A) which requires that M be input on a; this is in contrast to the modality ⟨a(x)⟩A where any term can be input on a.

We discover that a naive adoption of the match operator from the π calculus logics [23] and the Spi logics [13] yields a logic which does not characterise labelled bisimilarity. A weaker match operator can however be defined from the equality predicate in the underlying frames logic, and this is also the key to defining the matching input modality from the existing input modality.

6.3.1 The Problem with Match

As in the π calculus, Applied π includes the process construct

if M_{1} =_{E} M_{2} then P else Q

for testing equivalence between two terms and, based on the outcome, continuing either as process P or Q. One might therefore expect that a match operator [M_{1} =_{E} M_{2}]A must be included in the logic in order for the logic to characterise labelled bisimilarity. Since tests on arbitrary terms (possibly containing private names) is allowed in the calculus, one might further expect that the match operator in the logic can take arbitrary terms and that satisfaction could then be defined as follows:

P ⊨ [M_{1} =_{E} M_{2}]A =^{Δ} if M_{1}φ =_{E} M_{2}φ then P ⊨ A

Note how this definition does not rely on equality in frames (i.e. we just require that M_{1}φ =_{E} M_{2}φ instead of (M_{1} =_{E} M_{2})φ), reflecting the intuition that an equality may hold even when M_{1} and M_{2} contain private names as in the conditional process construct. As we shall see in the next chapter, this definition of the match operator would be useful in applications. However, the resulting logic would not characterise labelled bisimilarity. To illustrate this fact consider the following two processes which are vacuously labelled bisimilar because they are statically equivalent and have no dynamic behaviour:

P =^{Δ} (νk)({^{k}/_{x}})
Q =^{Δ} (νk)({^{f(k)}/_{x}})

Take the match formula A =^{Δ} ¬[x =_{E} k]false which expresses that x =_{E} k. Then P ⊨ A while Q ⊭ A, which serves to show that a logic with arbitrary match does not characterise labelled bisimilarity. The reason is, intuitively, that even though processes have the power to test for this kind of equalities, they might not do so – and hence their behaviour may be independent of the outcome of the test.

The Spi logic includes a match predicate similar to the one above, and an example similar to the one above suggests that the Spi logic does not characterise the relevant bisimulation. Hence it would seem that the Spi characterisation theorem [13, Theorem 1 p. 8] does not hold; the proof of this theorem, given in [14], does not resolve the doubt since the case for match is omitted.

What is needed is a weaker test operator which cannot be used to distinguish statically equivalent processes, and the natural choice is to define the match operator in terms of equality in frames:

P ⊨ [M_{1} =_{E} M_{2}]A =^{Δ} if (M_{1} =_{E} M_{2})φ then P ⊨ A

However this operator is redundant since the test proposition M_{1} =_{E} M_{2} is already part of the logic. We can then use this together with the propositional connectives to give an equivalent definition of the above weaker version of the match operator, thus:

P ⊨ [M_{1} =_{E} M_{2}]A =^{Δ} (M_{1} =_{E} M_{2} → A)

Similar test operators can be defined for syntactic equality and for reductions.

6.3.2 Matching Input Modality

The basic input modality ⟨a(x)⟩A asserts that a process can afford a transition labelled a(M) for some term M to a derivative which satisfies A{^{M}/_{x}}. We also wish to consider a stronger matching input modality, ⟨a(^{M}/_{x})⟩A, which asserts that a process can afford the transitions labelled a(M) for exactly the term M, to a derivative which satisfies A{^{M}/_{x}}. Matching input modality is strictly necessary to prove that the logic characterises labelled bisimilarity in the next section. Satisfaction can be defined as follows:

P ⊨ ⟨a(^{M}/_{x})⟩A =^{Δ} there exists P′ s.t. P ⟶^{τ}^{∗}⟶^{a(M)}⟶^{τ}^{∗} P′ and P′ ⊨ A{^{M}/_{x}}

As with the match operator, it turns out that the matching input modality is redundant; it can be defined from the standard input modality together with syntactic equality, thus:

⟨a(^{M}/_{x})⟩A =^{Δ} ⟨a(x)⟩(x = M ∧ A)

Informally, this definition says that a process satisfies ⟨a(^{M}/_{x})⟩A if it can input some term bound to variable x and if this term is syntactically equal to M. This seems sensible; however there is a catch, for the semantics for x = M is defined in terms of syntactic equality in frames, i.e. a process P satisfies x = M if and only if (x = M)φ(P). For this to be true, it must first of all hold that n(M) ∩ bn(φ(P)) = ∅. The following lemma establishes that this is indeed the case for any input M, and it follows immediately that the above definition of the matching input modality in terms of the standard input modality and syntactic equality captures the intended meaning.

Lemma 19. For any transition P ⟶^{a(M)} P′ where M occurs free (i.e. with no names under restriction) in some sub-process of P′ it holds that n(M) ⊆ fn(φ(P′)).

Proof. By transition induction, i.e. induction in the height of the derivation

tree of P ⟶^{a(M)} P′ with case distinction on the last rule applied.

Case: transition concluded by In . Then P = a(x).P′ and by definition of (extended) processes no active substitution can occur within the scope of an input. Hence φ(P′) = (ν∅)∅ so contains no private names, and the result holds vacuously.

Case: transition concluded by Scope . Then P = (νn)Q, Q ⟶^{a(M)} Q′ and P′ = (νn)Q′. The induction hypothesis gives that n(M) ∩ bn(φ(Q′)) = ∅ and the side condition in the Scope rule gives that n does not occur in M. Since the frame of P is just the frame of Q with an additional restriction on n, we have that also n(M) ∩ bn(φ(Q′)) = ∅ and hence that n(M) ⊆ fn(φ(Q′))

Case: transition concluded by Par . Then we have that P = Q | Q′,

Q ⟶^{a(M)} Q′′ and P′ = Q′′ | Q′. Now recall how to obtain the frame of P′: first obtain φ(Q′′) = ñ_{1}σ_{1} and φ(Q′) = ñ_{2}σ_{2} such that ñ_{1} ∩ n(σ_{2}) = ñ_{2} ∩ n(σ_{1}) = ∅ by α-converting as necessary. By induction hypothesis n(M) ∩ ñ_{1} = ∅. Per assumption we also have that n(M) ⊆ n(Q′′) and therefore n(M) ∩ ñ_{2} = ∅. Hence n(M) ∩ (ñ_{1} ∪ ñ_{2}) = ∅ giving that n(M) ∩ bn(φ(P′)) = ∅. Since M does occur in P′ we conclude that n(M) ⊆ fn(φ(P′)).

Case: transition concluded by Struct . Then P ≡ Q, Q ⟶^{a(M)} Q′ and Q′ ≡ P′. Since M occurs free in a subcomponent of P it follows by inspection of the rules for structural congruence that M also occurs free as a subcomponent of Q. By induction hypothesis n(M) ⊆ fn(φ(Q′)), and again by inspection of rules for structural congruence it holds that n(M) ⊆ fn(φ(P′)).

Note that it does not necessarily hold that the names of an input are free in the derived process. Here is an example:

P =^{Δ} (νk)(\{^{k}/_{x}\}) | a(y).\overline{b}⟨y⟩.0

Then P affords the input transition P ⟶^{a(k)} P′ where

P′ = (νk)(\{^{k}/_{x}\}) | \overline{b}⟨k⟩.0

and hence k ∈ bn(P′). However, the frame of the derivative P′ above is obtained by α-converting the bound k thus:

φ(P′) = (νc)(\{^{c}/_{x}\} | \overline{b}⟨k⟩.0)

and then we have that k ∉ bn(φ(P′)). Hence it is strictly necessary to speak only about the frame of the derived process in Lemma 19.

We have now introduced the matching input modality and shown how this can be defined from the basic input modality and equality. As a final remark we note that a matching output modality ⟨\overline{a}⟨M⟩⟩ would result in a logic which does not characterise labelled bisimilarity. Because for P and Q to be labelled bisimilar, the output condition requires only that whenever P can perform an output action \overline{a}⟨x⟩, then Q can also perform this output action – there is no requirement for x to be bound to the same term in the two processes.

6.4 Characterisation

In this section we show the expected result that LA characterises labelled bisimilarity. Existential quantification can now have any formulae in its scope (and not just LF formulae), so we must start by proving a new extension lemma saying that labelled bisimilarity between processes is preserved by extension with certain active substitutions.

Lemma 20 (Process extension lemma). Let P and Q be two processes with P ≈_{l} Q. Let ecores(φ(P)) = (N)_{j∈J} and ecores(φ(P)) = (N′)_{j∈J}. Then for any context C[ỹ] and any variable x fresh in P and Q it holds that

P | {^{C[Ñ]}/_{x}} ≈_{l} Q | {^{C[Ñ′]}/_{x}}

Proof. Suppose that P ≈_{l} Q. By condition 1 of labelled bisimilarity we have that φ(P) ≈_{ss} φ(Q). By the second extension lemma for frames (Lemma 17) it also holds that

φ(P){^{C[Ñ]}/_{x}} ≈_{ss} φ(Q){^{C[Ñ′]}/_{x}}

which is equivalent to

φ(P | {^{C[Ñ]}/_{x}}) ≈_{ss} φ(Q | {^{C[Ñ′]}/_{x}})

This establishes condition 1 of labelled bisimilarity for the extended processes.

For the other two conditions it suffices to show that P can perform exactly the same actions as the extended process P | {^{C[Ñ]}/_{x}}. This amounts to showing that any action which P can perform can also be performed by the extended process, and conversely that any action that the extended process can perform can also be performed by P.

Suppose that P can perform some action. If the action is an internal reduction then the extended process can perform the same action since internal reduction is closed by application of evaluation contexts. If P can perform a labelled action, the Par rule gives that the extended process can perform the same action (here we use that the variable x does not occur anywhere in P, so the premise of the rule is satisfied).

For the converse suppose that the extended process can perform some action. If the action is an internal reduction, this can only be done by process P since active substitutions have neither match or communication capabilities. Note that a reduction using the Then or Else rules is independent of the active substitution since the variable x per assumption does not occur in the match predicate. If the extended process can perform a labelled action, then this action can only be concluded using the Par rule where the process P performs the same action.

We are now ready to show the main characterisation result. The proof is fairly standard and follows the structure in e.g. [23, Proof of Theorem 1, p. 24]. As is common for this kind of characterisation theorem we assume that processes are image finite: it must hold for any process P that the set {P′ | P ⟶^{α} P′} is finite. In the parts of the proof concerning the frame logic we rely on the above extension lemma together with the results from the previous chapter saying that the logic of frames characterises strong static equivalence.

Theorem 6. For image-finite processes, LA characterises labelled bisimilarity (based on strong static equivalence):

P ≈_{l} Q ⇔ Th_{LA}(P) = Th_{LA}(Q)

Proof. There are two directions to show.

(⇒) Suppose that P ≈_{l} Q and P ⊨ A. We show by structural induction in A that also Q ⊨ A. We only show the base cases, the step for existential quantification, and the step for the input modalities; the remaining cases are similar or standard.

Basis.

Case: A = M_{1} ∘ M_{2} where ∘ is either =_{E}, = or >. Per definition of satisfaction, φ(P) ⊨_{LF} M_{1} ∘ M_{2}. From the assumption that P ≈_{l} Q and condition 1 of labelled bisimilarity, we have that φ(P) ≈_{ss} φ(Q). By Theorem 4 also φ(Q) ⊨_{LF} M_{1} ∘ M_{2}, i.e. Q ⊨ M_{1} ∘ M_{2}.

Step.

Case: A = ∃x(A_{1}). Per definition of satisfaction there is a M ∈ S(φ(P)) such that (P | {^{M}/_{x}}) ⊨ A_{1}. We then proceed as in the corresponding case in the proof of Theorem 4. Any synthesis term can be written as a context over cores, i.e. M = C[Ñ] for some context C[ỹ]. From the assumption that P ≈_{l} Q and the extension lemma for processes (Lemma 20), we have that also P | {^{M}/_{x}} ≈_{l} Q | {^{M′}/_{x}} where M′ = C[Ñ′]. Therefore the induction hypothesis gives that Q | {^{M′}/_{x}} ⊨ A_{1}, and since M′ ∈ S(φ(Q)) we conclude from the definition of satisfaction that Q ⊨ ∃x(A_{1}).

Case: A = ⟨a(x)⟩A_{1}. Per definition of satisfaction there exists a term M, and processes P′,P′′ and P′′′ such that

P ⟶^{τ}^{∗} P′ ⟶^{a(M)} P′′ ⟶^{τ}^{∗} P′′′ and P′′′ ⊨ A_{1}{^{M}/_{x}}

From the assumption that P ≈_{l} Q and by inductively using condition 2 in the definition of labelled bisimilarity, there is a process Q′ such that Q ⟶^{τ}^{∗} Q′ and

P′ ≈_{l} Q′. By condition 3 there is a process Q′′ such that Q′ ⟶^{a(M)} Q′′ with P′′ ≈_{l} Q′′. Using condition 2 inductively again we conclude that there is a process Q′′′ such that

Q ⟶^{τ}^{∗} Q′ ⟶^{a(M)} Q′′ ⟶^{τ}^{∗} Q′′′

where P′′′ ≈_{l} Q′′′. The induction hypothesis gives that Q′′′ ⊨ A_{1}{^{M}/_{x}}, and hence we conclude from the definition of satisfaction that Q ⊨ ⟨a(x)⟩A_{1}.

(⇐) For the other direction suppose that Th_{LA}(P) = Th_{LA}(Q), i.e. P and Q satisfy the same formulae. We must show that P and Q are related by some labelled bisimulation. Define the relation L where P LQ if and only if Th_{LA}(P) = Th_{LA}(Q). Then clearly P LQ; we show that L is a labelled bisimulation, i.e. that it satisfies the three conditions in the definition of ≈_{l}.

P and Q satisfy the same formulae, and in particular they satisfy the same frame formulae. It follows by Theorem 4 that φ(P) ≈_{ss} φ(Q) which establishes condition 1 in the definition of labelled bisimilarity.

Next we show condition 3 for the case where α = a(M). So suppose that

P ⟶^{a(M)} P′ and let (Q)_{i∈I} be an enumeration of the set {Q′ | Q ⟶^{a(M)} Q′}. Suppose for a contradiction that Q cannot simulate P, i.e. that (P′, Q_{i}) ∉ L for all i ∈ I. Then P′ and Q_{i} do not satisfy the same formulae (this follows by contraposition of the direction proven above), i.e. for each i ∈ I there is a formulae A_{i} ∈ Th_{LA}(P′) − Th_{LA}(Q_{i}). Per assumption of image-finiteness the enumeration (Q)_{i∈I} is finite, so the formula A = ⟨a(^{M}/_{x})⟩ ⋀_{i∈I} A_{i} is well defined (if I = ∅ we define ⋀_{i∈I} A_{i} to be true). Then by construction A ∈ Th_{LA}(P) − Th_{LA}(Q), contradicting that P ≈_{l} Q.

The proofs for the other labels in condition 3, and the proof for condition 2, are similar.

Note how the input modality ⟨a(^{M}/_{x})⟩, which was defined from ⟨a(x)⟩ and equality, plays an essential role in the proof of the input case in condition 3. For if we only had ⟨a(x)⟩ available we could conclude only that Q can match P ’s transition with some input on a, but not necessarily with an input of M on a; this would not be strong enough to prove bisimilarity.

6.5 Summary

We have extended the logic of frames with four modalities, namely an internal action modality, two output modalities and an input modality. An additional input matching input modality has been introduced and shown to be definable from the basic logic. We have also argued that a generic match operator (where private names may occur in terms) would result in the logic not characterising labelled bisimilarity, but a weaker match operator can be defined from the equality proposition inherited from the frame logic.

The result is a logic LA for Applied π which characterises labelled bisimilarity. The logic allows intermixing frame formulae from LF (including existential quantification) with modalities, which opens up the possibility of reasoning about knowledge over time.

An Application to the Needham-Schroeder Public Key Protocol

In this chapter we demonstrate how the logic for Applied π, based on the logic of frames, can be used to reason about a security protocol. The Needham-Schroeder Public Key Protocol [24] has been chosen for this purpose because its specification in Applied π is fairly simple and because it affords a well known attack [20] which can be expressed in the logic.

We start by explaining the Needham-Schroeder Public Key Protocol and a known attack in Section 1, after which we present an Applied π specification of the protocol in Section 2. In Section 3 we show how to express security properties in the logic, including a property which captures the attack on the protocol.

7.1 The Needham-Schroeder Public Key Protocol

The basic Needham-Schroeder Public Key Protocol is presented in the first subsection followed by an explanation of the attack in the second subsection.

7.1.1 The Protocol

The Needham-Schroeder Public Key Protocol can be used to authenticate two principals A and B to each other using public key cryptography, where we let A^{+} and B^{+} denote the public keys of A and B respectively. The protocol also employs nonces N_{a} and N_{b} which are random messages, generated by A and B respectively, intended to be used only in a single run of the protocol.

CHAPTER 7. AN APPLICATION TO THE NEEDHAM- …

The complete Needham-Schroeder Public Key Protocol includes steps for obtaining public keys from a trusted key server. For simplicity we omit these steps and assume that the public keys are already available to the participating principals; following [20], the core protocol can then be described informally thus:

Message 1 A → B : A, B, {N_{a}, A}_{B^{+}}
Message 2 B → A : B, A, {N_{a}, N_{b}}_{A^{+}}
Message 3 A → B : A, B, {N_{b}}_{B^{+}}

Principal A initiates the protocol by sending a message to B in step 1. The first two parts of the message simply express the fact that A wishes to establish a session with B. The third part of the message contains the nonce N_{a} and the identity A encrypted under B’s public key. Upon receiving this message, B uses its private key for decryption and obtains the nonce N_{a}. B then returns this nonce, together with a freshly generated nonce N_{b}, encrypted under A’s public key. When A receives this message, A believes that the message must originate from B because only B would be able to decrypt the contents of the first message to obtain the nonce N_{a}. Hence A happily returns the nonce N_{b} to B, again encrypted with B’s public key, in the belief that the nonce is a shared secret between the two principals. Similarly, B believes that the messages originated from A and that N_{b} is their shared secret, since only A should be able to decrypt the second message.

Following the three steps outlined above, A and B could proceed to generate a secret symmetric encryption key from the nonce N_{b}, which could be used for encryption in the remainder of the session. Symmetric key cryptography offers the advantage of speed compared to public key cryptography, so after the initial authentication using public keys, symmetric keys are employed in many practical applications such as the Secure Shell (ssh) program.

7.1.2 An Attack

An attack on the protocol which compromises the secrecy of the nonce N_{b} (and potentially subsequent symmetric encryption keys) is revealed in [20]. This is a classical example of how formal methods can be applied to reveal weaknesses in a protocol which for many years was believed to be secure. The attack involves an intruder I acting as a “man in the middle”: If A initiates a session with I, I can establish a new session with B impersonating A. B will then believe that it is carrying out a session with A instead of I. Hence the attack involves interleaving two runs of the protocol; we denote these two runs by α and β and write e.g. α.2 to refer to step two in run α. We also write I(A) to indicate that I is impersonating A. The attack on the protocol can then be described as follows:

7.2. THE SPECIFICATION

Message α.1  A → I : A, I, {N_{a}, A}_{I^{+}}
Message β.1  I(A) → B : A, B, {N_{a}, A}_{B^{+}}
Message β.2  B → I(A) : B, A, {N_{a}, N_{b}}_{A^{+}}
Message α.2  I → A : I, A, {N_{a}, N_{b}}_{A^{+}}
Message α.3  A → I : A, I, {N_{b}}_{I^{+}}
Message β.3  I(A) → B : A, B, {N_{b}}_{B^{+}}

In step β.2 the intruder receives the nonce N_{b}, but it is encrypted under A’s public key and hence I cannot decrypt it. Instead the intruder uses A as an oracle by replaying this message in α.2, and in message α.3 I receives the nonce N_{b} encrypted under I’s own public key; it can thus use its private key to obtain N_{b}. Note that B still believes that it has successfully carried out the authentication session with A and that N_{b} is a shared secret between A and B.

The protocol can be fixed simply by including the identity of the responder B in the encrypted part of message 2. A can then test if the message in step 3 originates from the expected principal.

7.2 The Specification

In this section we model the Needham-Schroeder Public Key Protocol in Applied π. We start in Subsection 1 by outlining some general assumptions, known as the Dolev-Yao Model. In Subsection 2 we present the equational theory used in the specification, which is based on public key encryption and lists. Subsection 3 discusses how to represent public keys in the specification and how these are used as process identifiers. Subsection 4 introduces some notational short hand which is useful in the specification, namely agent identifiers and outputguarded nondeterministic choice. Finally the complete specification is presented in Subsection 5, and we conclude with a transition trace leading to the attack in Subsection 6.

7.2.1 The Dolev-Yao Model

Applications of formal methods to security protocol often rely on what is known as the Dolev-Yao model [12]. The Dolev-Yao model is based on the following two assumptions:

• An intruder has complete knowledge of and access to communication channels in the sense that he/she can send arbitrary messages, can intercept any message, and modify it any way he/she sees fit.

• Cryptographic functions are perfect: decryption is only possible with the appropriate decryption key.

In Applied π the first assumption is realised through the labelled semantics and active substitutions: any output will result in a new active substitution which contributes to the frame of the process, and the frame is thus a representation of the environment knowledge which is a available to an attacker. The environment (or attacker) may compose any message by analysing and synthesising the frame of a process and send the message back to the process using labelled input.

The second assumption is realised through the algebraic specification of cryptographic functions by rewrite rules generating an equational theory. In a theory with symmetric key encryption, the equality dec(enc(x_{1}, x_{2}), x_{3}) =_{E} a holds if and only if x_{2} = x_{3}.

7.2.2 The Equational Theory

From the informal presentation of the protocol it is clear that an equational theory with public key encryption is required. We also need means of sending multiple terms in one message, and for this purpose an equational theory with lists is convenient. Hence we arrive at the following definition:

Definition 32. The signature and equational theory used for the subsequent specification is defined below.

Theory E_{NS} .

Signature: enc(·, ·), dec(·, ·), ·^{+}, ·^{−},cons(·, ·),head(·),tail(·), NIL.

Rewrite System:

dec(enc(z_{1}, z_{2}^{+}), z_{2}^{−}) >_{r_{1}} z_{1}
head(cons(z_{1}, z_{2})) >_{r_{2}} z_{1}
tail(cons(z_{1}, z_{2})) >_{r_{3}} z_{2}

The part of E_{NS} concerning public key encryption has been explained earlier in the report. The function symbol cons(z_{1}, z_{2}) is the list constructor: it takes a head z_{1} and a tail z_{2} (which itself is a list) to obtain a new list. The function symbols head and tail are used to extract the head and tail from a list, respectively, as expressed in the rewrite rules r_{2} and r_{3}. Finally, the constant function symbol NIL represents the empty list.

For the present purpose we shall only be needing lists with two or three elements. Therefore we define the following notational short hands.

Definition 33. Pair construction, triple construction, and projection of first, second and third elements, are defined as follows:

[z_{1}, z_{2}] =^{Δ} cons(z_{1}, cons(z_{2}, NIL))
[z_{1}, z_{2}, z_{3}] =^{Δ} cons(z_{1}, [z_{2}, z_{3}])
fst(z) =^{Δ} head(z)
snd(z) =^{Δ} head(tail(z))
trd(z) =^{Δ} head(tail(tailz))

7.2.3 Process Identifiers and Public Keys

In the formal specification of the protocol in Applied π, principals are represented by processes. The informal protocol description requires that principals have identifiers which can be sent along in messages, e.g. in message 1 which includes the information that the message is from A to B. There is however no immediate way of identifying processes in Applied π (replication would pose problems for such identifiers). Instead we adopt the convention that principals are identified by their public keys.

As explained earlier we assume that public keys have been exchanged and are known to all principals prior to protocol execution. To model this assumption we simply include in the specification an active substitution with the public key for each principal. For instance there will be an active substitution {^{a^{+}}/_{z_{a}}} representing the public key for A. When other processes (e.g. B and potential intruders) refer to A’s public key, this reference must be through the variable z_{a} in the relevant active substitution because the seed a is private for principal A. If the public key were to be used directly to encrypt a term, the encrypted term could not be sent to A because scope extrusion would fail.

7.2.4 Agent Definitions and Choice

When specifying the protocol in Applied π it will be convenient to employ two notions which are not explicitly part of the calculus, namely agent definitions and nondeterministic choice. Agent definition are on the form

A_{1} =^{Δ} P_{1}

A_{2} =^{Δ} P_{2}

…

where P_{1} is the process we wish to identify with A_{1} etc. The agent identifiers may then occur in any process, the intuition being that the identifier A_{i} is replaced by its definition P_{i}, which may lead to recursion. Although agent identifiers are not explicitly part of the calculus, they can easily be encoded using the bang operator (!) [25, Section 3.4]. Hence we can safely use agent identifiers in the protocol specification.

Nondeterministic choice, +, can be used to write processes on the form P =^{Δ} \overline{a}⟨x⟩.P_{1} + \overline{a}⟨y⟩.P_{2}, the intuition being that P can choose nondeterministically to proceed as either \overline{a}⟨x⟩.P_{1} or \overline{a}⟨y⟩.P_{2}. Nondeterministic choice cannot generally be encoded in Applied π, but many special cases can [25, Section 3.2], including the output-guarded process P above. For instance, assuming that z ∉ fv(P_{1}, P_{2}), the process P above is observationally equivalent to the process

P′ =^{Δ} (νb)(\overline{b}⟨d⟩ | b(z).\overline{a}⟨x⟩.P_{1} | b(z).\overline{a}⟨y⟩.P_{2})

When specifying the protocol we shall use output-guarded nondeterministic choice, knowing that this can be encoded in the basic Applied π calculus.

7.2.5 The Specification

We are now ready to present the formal specification of the Needham-Schroeder Public Key Protocol in Applied π– the specification is given in Table 7.1.

The processes A and B represent the two main principals in the protocol. There is no explicit encoding of potential intruders since this aspect is implicit in processes being able to communicate with the environment. Note however the definition of process A: since A initiates the protocol, it must as a first step choose which principal to engage in a protocol run with. This initial choice is essential to include in the specification, since this is the choice leading to A contacting a potential intruder. We assume that A only has two friends which are identified by the public keys z_{b_{0}} and z_{b_{1}}. The first is intuitively the “correct” process B , identified by the public key variable z_{b_{0}}, while the second may be a hostile intruder and is identified by the public key variable z_{b_{1}}. Process A uses nondeterministic choice to decide which of these to initiate a protocol run with. The process T (i) generalises the first step of the protocol, where the argument i indicates which of A’s two friends should be contacted. The derivatives of A are indexed by the identifier (0 or 1) of the responder chosen in the first step.

The process P K consists of active substitutions representing the public key of A, the public key of the well-behaved process B, and the public key of a potential intruder. The process SP EC gathers the agents A and B in a coherent system together with P K, which reflects the assumption that public keys are known in advance. The secrecy of the key seeds a and b_{0} is modelled with name restriction to the relevant processes; so is the freshness of nonces n_{a} and n_{b_{0}}. Note that the intruders key seed n_{b_{1}} is not private.

Note how the processes A_{2}(i) and B_{3} use the conditional process construct to check if the expected nonce is received. If B_{3} receives the expected nonce, then the protocol run is successful and the process can continue its business in B_{5}. Before doing so, B_{4} announces the successful completion of the authentication by sending a “success message” on a distinguished channel s. The success action is necessary when describing the trace with a LA formula in the next section. The reason is that the test includes the private name n_{b_{0}} and, as we demonstrated

T (i) =^{Δ} \overline{c}⟨[z_{a}, z_{b_{i}}, enc([n_{a}, z_{a}], z_{b_{i}})]⟩
A =^{Δ} T (0).A_{1}(0) + T (1).A_{1}(1)
A_{1}(i) =^{Δ} c(y_{2}).A_{2}(i)
A_{2}(i) =^{Δ} if fst(dec(trd(y_{2}), a^{−})) =_{E} n_{a} then A_{3}(i) else F A
A_{3}(i) =^{Δ} \overline{c}⟨[z_{a}, z_{b_{i}}, enc(snd(dec(trd(y_{2}), a^{−})), z_{b_{i}})]⟩.A_{4}(i)
A_{4}(i) =^{Δ} …
B =^{Δ} c(y_{1}).B_{1}
B_{1} =^{Δ} \overline{c}⟨[z_{b_{0}}, fst(y_{1}), enc([fst(dec(trd(y_{1}), b_{0}^{−})), n_{b_{0}}], fst(y_{1}))]⟩.B_{2}
B_{2} =^{Δ} c(y_{3}).B_{3}
B_{3} =^{Δ} if dec(trd(y_{3}, b_{0}^{−})) =_{E} n_{b_{0}} then B_{4} else F B
B_{4} =^{Δ} \overline{s}⟨succ⟩.B_{5}
B_{5} =^{Δ} …
F A =^{Δ} …
F B =^{Δ} …
P K =^{Δ} {^{a^{+}}/_{z_{a}}} | {^{b^{0}^{+}}/_{z_{b_{0}}}} | {^{b^{1}^{+}}/_{z_{b_{1}}}}
SP EC =^{Δ} (νa, n_{a})A | (νb_{0}, n_{b_{0}})B | P K

Table 7.1: An Applied π specification of the Needham-Schroeder Public Key Protocol. The specification uses short hand notations for agent definitions and output-guarded choice which can be defined from the basic Applied π calculus. in Section 6.3, this kind of test cannot be made in the logic. Instead we ensure that the outcome of the test is readily observable by performing an output on channel s, and this output action can be captured in the logic.

The remainder of the specification should be fairly self explanatory. The processes A_{4}(i), B_{5}, F A and F B are left unspecified; the first two express the behaviour of the respective principals after a successful run of the authentication protocol (and may e.g. continue communication with a symmetric key generated from a nonce), and the last two processes specify the behaviour on unexpected input (which we will not concern ourselves with for the present purpose).

7.2.6 A Trace of The Attack

A formal derivation from the SP EC process, which demonstrates the attack on the protocol, is given in Table 7.2.

The active substitutions arising from the three process outputs have variables x_{1},x_{2} and x_{3}. For convenience we also represent the three environment inputs by active substitutions with variables y_{1},y_{2} and y_{3} which are under restriction. The labelled semantics prescribe that environment input is substituted directly into the process in question (since we are working with the early semantics). We then use the fact that A{^{M}/_{x}} ≡ (νx)({^{M}/_{x}} | A) to introduce a new active substitution with private variable.

7.3 Logical Properties

7.3.1 Capturing the Trace of the Attack

Here is a formula in the logic LA which expresses that a process can exhibit the trace shown in Table 7.2, and hence the formula is satisfied by the SP EC process:

A_{1} =^{Δ} ⟨νc̄⟩⟨c(y_{1})⟩⟨νc̄⟩⟨c(y_{2})⟩⟨νc̄⟩⟨c(y_{3})⟩⟨s̄⟩true

Note how we use the output action on the distinguished success channel to implicitly test if the input bound to y_{3} contains the expected nonce. The formula A_{1} is not in itself interesting though: we would also wish to express the security breach, i.e. that the nonce n_{b_{0}} is revealed to the environment by the end of the trace. This is where the underlying logic of frames becomes useful. The variable y_{3} is bound to the term [a^{+}, b_{0}^{+}, enc(n_{b_{0}}, b_{0}^{+})]. As a first attempt, one might assert that the encrypted nonce n_{b_{0}} contained in this message can be decrypted using environment knowledge:

A_{2} =^{Δ} ⟨νc̄⟩⟨c(y_{1})⟩⟨νc̄⟩⟨c(y_{2})⟩⟨νc̄⟩⟨c(y_{3})⟩⟨s̄⟩

∃x∃x′∃x′′(trd(y_{3}) > x ∧ dec(x, x′) > x′′)

Recall that existential quantification ranges over the synthesis of the frame in question, which intuitively corresponds to the environment knowledge. Note also

7.3. LOGICAL PROPERTIES

SP EC ≡(νa, n_{a})(\overline{c}⟨ξ_{1}⟩.A_{1}(1)) | (νb_{0}, n_{b_{0}})c(y_{1}).B_{1} | P K
≡⟶^{νx_{1}\overline{c}⟨x_{1}⟩}(νa, n_{a})(\{^{ξ_{1}}/_{x_{1}}\} | A_{1}(1)) | (νb_{0}, n_{b_{0}})c(y_{1}).B_{1} | P K
≡(νa, n_{a}, b_{0}, n_{b_{0}})({^{ξ_{1}}/_{x_{1}}} | A_{1}(1) | c(y_{1}).B_{1}) | P K
⟶^{c(y_{1})}≡(νa, n_{a}, b_{0}, n_{b_{0}}, y_{1})({^{ξ_{1}}/_{x_{1}}} | {^{ξ_{2}}/_{y_{1}}} | A_{1}(1) | B_{1}) | P K
=(νa, n_{a}, b_{0}, n_{b_{0}}, y_{1})(\{^{ξ_{1}}/_{x_{1}}\} | \{^{ξ_{2}}/_{y_{1}}\} | A_{1}(1) | \overline{c}⟨ξ_{3}⟩.B_{2}) | P K
≡⟶^{νx_{2}.\overline{c}⟨x_{2}⟩}(νa, n_{a}, b_{0}, n_{b_{0}}, y_{1}, y_{2})(\{^{ξ_{1}}/_{x_{1}}\} | \{^{ξ_{2}}/_{y_{1}}\} | \{^{ξ_{3}}/_{x_{2}}\} | A_{1}(1) | B_{2}) | P K
=(νa, n_{a}, b_{0}, n_{b_{0}}, y_{1}, y_{2})({^{ξ_{1}}/_{x_{1}}} | {^{ξ_{2}}/_{y_{1}}} | {^{ξ_{3}}/_{x_{2}}} | c(y_{2}).A_{2}(1) | B_{2}) | P K
⟶^{c(y_{2})}≡(νa, n_{a}, b_{0}, n_{b_{0}}, y_{1}, y_{2})({^{ξ_{1}}/_{x_{1}}} | {^{ξ_{2}}/_{y_{1}}} | {^{ξ_{3}}/_{x_{2}}} | {^{ξ_{4}}/_{y_{2}}}
| (if ξ_{5} =_{E} n_{a} then A_{3} else F A) | B_{2}) | P K
→(νa, n_{a}, b_{0}, n_{b_{0}}, y_{1}, y_{2})({^{ξ_{1}}/_{x_{1}}} | {^{ξ_{2}}/_{y_{1}}} | {^{ξ_{3}}/_{x_{2}}} | {^{ξ_{4}}/_{y_{2}}} | A_{3} | B_{2} | P K
=(νa, n_{a}, b_{0}, n_{b_{0}}, y_{1}, y_{2})(\{^{ξ_{1}}/_{x_{1}}\} | \{^{ξ_{2}}/_{y_{1}}\} | \{^{ξ_{3}}/_{x_{2}}\} | \{^{ξ_{4}}/_{y_{2}}\} | \overline{c}⟨ξ_{6}⟩.A_{4} | B_{2} | P K
≡⟶^{νx_{3}\overline{c}⟨x_{3}⟩}(νa, n_{a}, b_{0}, n_{b_{0}}, y_{1}, y_{2})(\{^{ξ_{1}}/_{x_{1}}\} | \{^{ξ_{2}}/_{y_{1}}\} | \{^{ξ_{3}}/_{x_{2}}\} | \{^{ξ_{4}}/_{y_{2}}\} | \{^{ξ_{6}}/_{x_{3}}\} | A_{4} | B_{2} | P K
=(νa, n_{a}, b_{0}, n_{b_{0}}, y_{1}, y_{2})({^{ξ_{1}}/_{x_{1}}} | {^{ξ_{2}}/_{y_{1}}} | {^{ξ_{3}}/_{x_{2}}} | {^{ξ_{4}}/_{y_{2}}} | {^{ξ_{6}}/_{x_{3}}} | A_{4} | c(y_{3}).B_{3} | P K
⟶^{c(y_{3})}≡(νa, n_{a}, b_{0}, n_{b_{0}}, y_{1}, y_{2}, y_{3})({^{ξ_{1}}/_{x_{1}}} | {^{ξ_{2}}/_{y_{1}}} | {^{ξ_{3}}/_{x_{2}}} | {^{ξ_{4}}/_{y_{2}}} | {^{ξ_{6}}/_{x_{3}}} | {^{ξ_{7}}/_{y_{3}}}
| A_{4} | if ξ_{8} =_{E} n_{b_{0}} then B_{4} else F B) | P K
→(νa, n_{a}, b_{0}, n_{b_{0}}, y_{1}, y_{2}, y_{3})({^{ξ_{1}}/_{x_{1}}} | {^{ξ_{2}}/_{y_{1}}} | {^{ξ_{3}}/_{x_{2}}} | {^{ξ_{4}}/_{y_{2}}} | {^{ξ_{6}}/_{x_{3}}} | {^{ξ_{7}}/_{y_{3}}}
| A_{4} | \overline{s}⟨succ⟩.B_{5}) | P K
≡⟶^{νx_{4}\overline{c}⟨x_{4}⟩}(νa, n_{a}, b_{0}, n_{b_{0}}, y_{1}, y_{2}, y_{3})(\{^{ξ_{1}}/_{x_{1}}\} | \{^{ξ_{2}}/_{y_{1}}\} | \{^{ξ_{3}}/_{x_{2}}\} | \{^{ξ_{4}}/_{y_{2}}\} | \{^{ξ_{6}}/_{x_{3}}\} | \{^{ξ_{7}}/_{y_{3}}\}
| {^{succ}/_{x_{4}}} | A_{4} | B_{5}) | P K

ξ_{1} = [z_{1}, z_{b_{1}}, enc([n_{a}, z_{a}], z_{b_{1}})]  [a^{+}, b_{1}^{+}, enc([n_{a}, a^{+}], b_{1}^{+})]
ξ_{2} = [z_{a}, z_{b_{0}}, enc([fst(dec(trd(x_{1}), b_{1}^{−})), z_{a}], z_{b_{1}})]  [a^{+}, b_{0}^{+}, enc([n_{a}, a^{+}], b_{0}^{+})]
ξ_{3} = [z_{b_{0}}, fst(y_{1}), enc([fst(dec(trd(y_{1}), b_{0}^{−})), n_{b_{0}}], fst(y_{1}))] [b_{0}^{+}, a^{+}, enc([n_{a}, n_{b_{0}}], a^{+})]
ξ_{4} = [z_{b_{1}}, z_{a}, trd(x_{2})]  [b_{1}^{+}, a^{+}, enc([n_{a}, n_{b_{0}}], a^{+})]
ξ_{5} = fst(dec(trd(y_{2}), a^{−}))  n_{a}
ξ_{6} = [z_{a}, z_{b_{1}}, enc(snd(dec(trd(y_{2}), a^{−})), z_{b_{1}})]  [a^{+}, b_{1}^{+}, enc(n_{b_{0}}, b_{1}^{+})]
ξ_{7} = [z_{a}, z_{b_{0}}, enc(dec(trd(x_{3}), b_{1}^{−}), z_{b_{0}})]  [a^{+}, b_{0}^{+}, enc(n_{b_{0}}, b_{0}^{+})]
ξ_{8} = dec(trd(y_{3}, b_{0}^{−}))  n_{b_{0}}

Table 7.2: A trace of the attack on the Needham-Schroeder Public Key Protocol. The trace is shown in the top part of the table and relies on auxiliary definitions of terms as given in the bottom part, which consists of two columns: the left column gives the actual terms, while the right column gives the corresponding normal forms of the terms after applying active substitutions. that we have to use an existentially quantified variable x′′ instead of directly using n_{b_{0}} because this is a private name. Does the process SP EC satisfy A_{2}? The answer is no, because b_{0}^{−} is not in the frame synthesis of the relevant derivative of SP EC. The reason is that the name b is private in process B and is not revealed to the environment at any point in the trace. This corresponds to the intuition of the attack: the nonce n_{b_{0}} is not obtained by decrypting the message embedded in y_{3}, but rather by using A as an oracle and tricking A into decrypting the message embedded in y_{3}.

Hence an alternative formulation is called for:

A_{3} =^{Δ} ⟨νc̄⟩⟨c(y_{1})⟩⟨νc̄⟩⟨c(y_{2})⟩⟨νc̄⟩⟨c(y_{3})⟩⟨s̄⟩∃x(trd(y_{3}) = enc(x, z_{b_{0}}))

This formula asserts that there is some synthesis term (x) which is syntactically equal to the term encrypted in y_{3}, namely n_{b_{0}}. The process SP EC does satisfy A_{3} because n_{b_{0}} is in the frame synthesis of the relevant derivative of SP EC. More precisely, the frame of the second last derivate of SP EC is given as follows:

φ = (νa, n_{a}, b_{0}, n_{b_{0}}, y_{1}, y_{2}, y_{3})({^{ξ_{1}}/_{x_{1}}} | {^{ξ_{2}}/_{y_{1}}} | {^{ξ_{3}}/_{x_{2}}} | {^{ξ_{4}}/_{y_{2}}} | {^{ξ_{6}}/_{x_{3}}} | {^{ξ_{7}}/_{y_{3}}})

The interesting term is ξ_{6} (bound to x_{3}) which, when the private active substitutions are applied, reduces to the triple [a^{+}, b_{1}^{+}, enc(n_{b_{0}}, b_{1}^{+})]. Since the name b_{1} is free in φ, the last term of this triple can be decrypted so we have that

ecores(x_{3}, φ) = {a^{+}, b_{1}^{+}, enc(n_{b_{0}}, b_{1}^{+}), n_{b_{0}}}

Since ecores(φ) ⊆ S(φ) we have that n_{b_{0}} ∈ S(φ), confirming the satisfaction

φ ⊨_{LF} ∃x(trd(y_{3}) = enc(x, z_{b_{0}}))

and hence SP EC ⊨ A_{3}.

Yet another approach would be employ the technique in the proof of Proposition 3 in [2], which states that the problem of deciding static equivalence reduces to deciding membership of the synthesis set in theories which include public-key axioms. The idea is to add an active substitution with a fresh private name encrypted under the public key generated from n_{b_{0}} to the SP EC process:

SP EC′ =^{Δ} SP EC | (νh){^{enc(h,n_{b_{0}}^{+})}/_{y}}

Then the nonce n_{b_{0}} can be deduced by the environment in the end of a successful protocol run exactly if SP EC′ satisfies the following formulae:

A_{4} =^{Δ} ⟨νc̄⟩⟨c(y_{1})⟩⟨νc̄⟩⟨c(y_{2})⟩⟨νc̄⟩⟨c(y_{3})⟩⟨\overline{s}⟨succ⟩⟩∃x∃x′(dec(y, x) > x′)

The formula A_{3} describes the desired assertion more directly than A_{4}, but A_{4} has the advantage of also working in a setting with symmetric key encryption. If the message containing the nonce n_{b_{0}} were encrypted with a symmetric key not known by the environment, the term containing the nonce n_{b_{0}} could not be reconstructed in the logic and hence syntactical equality could not be tested as in A_{3}.

7.3.2 General Safety Properties – Invariance

We have now demonstrated that the logic is sufficiently strong to capture the attack on the Needham-Schroeder Public Key Protocol. However the formulae A_{3} and A_{4} exhibited above were designed with the specific attack in mind. In a more general situation, when one is faced with a protocol specification to be verified, one would wish to express more general safety properties, e.g. that there is no possible trace leading to the disclosure of the nonce n_{b_{0}}.

More specifically, we would like to assert that whenever an (arbitrary) execution trace of the protocol leads to the input of y_{3} in B_{3} followed an output of the success message, the nonce embedded in the input cannot be deduced by the environment. This amounts to asserting that the following formula (which is just the last part of A_{3}) holds invariantly – i.e. in any possible derived state of SP EC:

A_{5} =^{Δ} ⟨c(y_{3})⟩⟨\overline{s}⟨succ⟩⟩¬∃x(trd(y_{3}) = enc(x, z_{b_{0}}))

If we assume that A_{4}(i), B_{5}, F A and F B are finite processes, in the sense that they do not afford infinite transition sequences, then the SP EC process is also finite. In this case invariance can be defined using only constructs from the basic logic LA. Let U be any finite set of names and variables. We then define invariance of A in k steps inductively as follows:

Inv_{U}^{0}(A) =^{Δ} A
Inv_{U}^{k+1}(A) =^{Δ} A ∧ [τ]Inv_{U}^{k}(A)∧
⋀_{u∈U}[ū]Inv_{U}^{k}(A) ∧ [νū]Inv_{U}^{k}(A) ∧ [u(x)]Inv_{U}^{k}(A)

Recall that the box modalities express necessity, so e.g. [τ]A expresses that no matter how an internal reduction is performed, the derived process must satisfy A. Hence the formula Inv^{k}(A) expresses that no matter how a process performs k consecutive actions, the resulting derived process must satisfy A.

Let U be the set of variables and names occurring in SP EC and let k_{max} be the upper bound on the length of possible transition sequences that SP EC can afford. We are now equipped to express a safety property which asserts that SP EC does not reveal the nonce n_{b_{0}} to the environment at any point in its execution:

A_{6} =^{Δ} Inv_{U}^{k_{max}}(A_{5})

Clearly SP EC ⊭ A_{6} as exemplified by the formula A_{3} given in the previous subsection, i.e. the safety property is not satisfied by our specification.

The definition of the invariance operator relies on processes with finite-length transition sequences (not to be mistaken for processes with finite states). However, systems with infinite behaviour arise in many settings where the above definition of invariance therefore would not suffice. A standard solution is to introduce process variables and recursion into the logic and thereby obtain a μcalculus [17]. This allows invariance to be defined as a maximal fixed point of an appropriate semantic function over a complete lattice [6, Section 5.2]. Tarski’s Fixed Point Theorem [6, Appendix A] gives us that a unique such fixed point exists if the function is monotonic, and in order to satisfy this one would have to omit negation from the logic. We leave further developments in this direction for future work.

7.4 Summary

This chapter has demonstrated how the logic for Applied π can be applied to express properties of security protocols. We have introduced the Needham-Schroeder Public Key Protocol and shown a well known “man in the middle” attack in which an intruder may learn a secret nonce. We have modelled the protocol in Applied π and shown a transition sequence leading to the attack. Finally we have discussed how the logic for Applied π may be used to express properties of the protocol, and presented formulae which capture the attack.

Conclusion

We have introduced Abadi and Fournet’s Applied π calculus and presented a logic for the calculus which characterises labelled bisimilarity and hence also observational equivalence. The motivation is similar to that of Applied π itself, namely generality: the logic can be adapted to a particular application simply by defining a suitable function signature and equational theory.

Since labelled bisimilarity contains a condition on static equivalence on frames, the first step towards a logic for Applied π is a logic for frames which characterises static equivalence. A logic for frames in turn relies on a definition of static equivalence which does not contain a universal quantification over arbitrary terms. The following section summarises the major contributions of this report, and the subsequent section gives pointers to future work.

8.1 Contributions

8.1.1 Strong Static Equivalence

CHAPTER 8. CONCLUSION

The first major contribution of this report is an strong version of static equivalence, ≈_{ss}, in which frames may be distinguished by testing on reduction of terms in addition to equality. We have argued that strong static equivalence is meaningful in applications. But strong static equivalence is particularly useful because a refined definition, ≈′_{ss}, can be given which does not depend on universal quantification over arbitrary terms. The refined definition is based on the notion of ecores (extended cores, which intuitively are the minimal relevant terms which can be deduced from a frame): corresponding terms in the two frames must be equal up to ecores, and any syntactic equalities and reductions on contexts over ecores which hold in one frame must also hold in the other. We then show that ≈_{ss} and ≈′_{ss} coincide in independent convergent subterm theories, which are the theories we have considered in this report. The refined definition is used as a basis for the logic of frames and to show that this logic characterises strong static equivalence. A further refinement, ≈′′_{ss}, which is also shown to be equivalent to ≈_{ss}, is given and used as a basis for characteristic formulae in the logic of frames. Finally we show that strong static equivalence coincides with the standard static equivalence in cases where frames do not contain inaccessible terms. This is for example satisfied by theories of symmetric key encryption and by theories of public key encryption if public keys are assumed to always be known.

8.1.2 A Logic for Frames

The second major contribution of this report is a first order logic for frames, LF, which characterises strong static equivalence and which is amenable to construction of characteristic formulae. LF includes the atomic propositions M_{1} =_{E} M_{2} (equality), M_{1} > M_{2} (reduction) and M_{1} = M_{2} (syntactic equality) which allow direct reasoning about the terms in a frame. Common to all three is that M_{1} and M_{2} may not contain private names of a frame in order for the frame to satisfy them. LF also contains first order quantification on the form ∃x(A) ranging over the synthesis of a frame (i.e. any terms which can be constructed from ecores), which allows indirect reasoning about the terms that can be deduced from a frame and greatly increases the expressiveness of the logic. This enables formulae which e.g. express that there exists a term y (known by the environment) such that x_{1} can be decrypted with y to obtain x_{2}

8.1.3 A Logic for Applied π

The third and final major contribution of this report is a modal logic for Applied π, LA, which characterises labelled bisimilarity on processes. LA is obtained by adding suitable Hennessy-Milner style modalities to LF. More specifically, we add the modalities ⟨τ⟩A_{1} (possibility of internal reduction), ⟨ā⟩A_{1} (possibility of some output on a), ⟨νā⟩A_{1} (possibility of bound output on a) and ⟨a(x)⟩A_{1} (possibility of input of some term bound to x on a). We have further demonstrated how a restricted version of match can be defined based on the underlying frame logic, and likewise how a matching input modality ⟨a(^{M}/_{x})⟩A_{1} (possibility of input of term M on a) can be defined from the standard input modality and match. The result is a logic which can reason both about the dynamic behaviour and static characteristics of processes, and which can be used to make assertions on the form process P can perform an input of an encrypted term M_{1} followed by some output, after which the decryption key for the term M_{1} is known by the environment Finally, we have demonstrated how LF can be applied to capture a well known attack on the Needham-Schroeder Public Key Protocol.

8.2 Future Work

Many interesting directions for future work still remain, and in this section we discuss a few of them.

8.2. FUTURE WORK

8.2.1 A Broader Class of Theories.

In this report we have focused on independent convergent subterm theories. We have argued that the assumption of independence (namely that destructor function symbols do not occur inside rewrite rules) is not very strong. However the assumption of subterm theories is rather strong, and convergent theories which are not subterm theories arise in many practical applications. For example, in [19] an analysis of security protocols based on weaknesses in block chaining modes is carried out. A block chaining mode such as ECB (Electronic Code Book) specifies how a clear text can be broken into a list of blocks which are encrypted separately. A decryption function symbol operating on lists could therefore be defined as follows (where the cons(·, ·) function symbol is the list constructor from the theory E_{NS} defined in Subsection 7.2.2):

dec(cons(enc(z_{1}, z_{2}), z_{3}), z_{2}) > cons(z_{1}, dec(z_{3}, z_{2}))

This is however not a subterm rule. Hence it would be interesting to extend the results in this report to convergent theories which are not necessarily subterm theories. We expect this to be fairly easy since we only use the assumption of subterm theories to argue that the reduct of a context over ecores is itself a context over ecores. However, a more careful definition of cores and ecores may be necessary.

8.2.2 Expressiveness

We have demonstrated how the logic LA can be used to reason about an authentication protocol. One of the key motivations for a logic for Applied π is generality, so one would hope that the logic captures other logics given a suitable equational theory. We have suggested that LA resembles the Spi logic in a theory of symmetric key encryption. There are also similarities to the BAN logic [11] which has been used to reason about authentication protocols. The BAN logic includes formulae such as ”P sees X”, which asserts that process P can see message X based on the messages it has received in its current state; this resembles existential quantification over synthesis terms in LA. Therefore, a general future direction could be to investigate the expressiveness of LA in relation to existing logics.

8.2.3 Algorithms and Complexity

Decidability of refined strong static equivalence and of satisfiability in the logics clearly rely on finding algorithms for computing the analysis, cores and ecores of a frame. Although we are fairly confident that such algorithms exist, we have not paid much attention to them in this report. Hence a possible future direction would be to devise and implement such algorithms. It would also be interesting to analyse the time complexity of deciding static equivalence in convergent subterm theories using our refined definitions of strong static equivalence. In particular it would be interesting to investigate if one could match or improve on the polynomial time bound given in [2].

8.2.4 Tool Support

Analysis of models in Applied π is supported by the tool ProVerif [8] by Bruno Blanchet. The motivation for introducing a logic for Applied π is to provide an alternative approach to specifying security properties about a model. Hence it would be of interest to extend ProVerif with support for our logic LA.

8.2.5 Recursion

In Chapter 7 we described how the logic LA can be used to specify properties about a security protocol. We also motivated the need for invariance formulae, which can be realised by introducing recursion and hence obtaining a μ-calculus. This extension has however been left for future work and, although standard, may involve making restrictions to the logic such as disallowing negation.

Bibliography

[1] Martín Abadi, Mathieu Baudet, and Bogdan Warinschi. Guessing attacks and the computational soundness of static equivalence. In FoSSaCS, volume 3921 of Lecture Notes in Computer Science, pages 398–412. Springer, 2006.

[2] Martín Abadi and Véronique Cortier. Deciding knowledge in security protocols under equational theories. In Proc. 31st Int. Coll. Automata, Languages, and Programming (ICALP’2004), volume 3142 of Lecture Notes in Computer Science, pages 46–58. Springer, 2004.

[3] Martín Abadi and Véronique Cortier. Deciding knowledge in security protocols under (many more) equational theories. In CSFW ’05: Proceedings of the 18th IEEE Computer Security Foundations Workshop (CSFW’05), pages 62–76, Washington, DC, USA, 2005. IEEE Computer Society.

[4] Martín Abadi and Cedric Fournet. Mobile values, new names, and secure communication. In POPL ’01: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 104– 115, New York, NY, USA, 2001. ACM Press.

[5] Martín Abadi and Andrew D. Gordon. A calculus for cryptographic protocols: The Spi calculus. In Fourth ACM Conference on Computer and Communications Security, pages 36–47. ACM Press, 1997.

[6] Luca Aceto, Anna Ingólfsdóttir, Kim G. Larsen, and Jiri Srba. Reactive Systems: Modelling, Specification and Verification. DRAFT. Unpublished, 2006.

[7] Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.

[8] Bruno Blanchet. An efficient cryptographic protocol verifier based on prolog rules. In CSFW ’01: Proceedings of the 14th IEEE Workshop on Computer Security Foundations, page 82. IEEE Computer Society, 2001.

[9] Michele Boreale, Rocco De Nicola, and Rosario Pugliese. Proof techniques for cryptographic processes. SIAM J. Comput., 31(3):947–986, 2001.

[10] Johannes Borgström. Static equivalence is harder than knowledge. To appear in Proceedings of EXPRESS 2005.

[11] Michael Burrows, Martín Abadi, and Roger Needham. A logic of authentication, from proceedings of the royal society, volume 426, number 1871, 1989. In William Stallings, Practical Cryptography for Data Internetworks, IEEE Computer Society Press, 1996. 1996.

[12] D. Dolev and A. Yao. On the security of public key protocols. IEEE Transactions on Information Theory, 29(2):198–208, 1983.

[13] Ulrik Frendrup, Hans Hüttel, and Jesper Nyholm Jensen. Modal logics for cryptographic processes. Electr. Notes Theor. Comput. Sci., 68(2), 2002.

[14] Ulrik Frendrup and Jesper Nyholm Jensen. Bisimilarity in the Spi-calculus. Master’s thesis, Aalborg University, Department of Computer Science, 2001.

[15] Matthew Hennessy and Robin Milner. Algebraic laws for nondeterminism and concurrency. J. ACM, 32(1):137–161, 1985.

[16] Tony Hoare and Robin Milner. Grand challenges for computing research. Comput. J., 48(1):49–52, 2005.

[17] Dexter Kozen. Results on the propositional mu-calculus. Theor. Comput. Sci., 27:333–354, 1983.

[18] Steve Kremer and Mark Ryan. Analysis of an electronic voting protocol in the Applied Pi calculus. In Shmuel Sagiv, editor, ESOP, volume 3444 of Lecture Notes in Computer Science, pages 186–200. Springer, 2005.

[19] Steve Kremer and Mark D. Ryan. Analysing the vulnerability of protocols to produce known-pair and chosen-text attacks. In Riccardo Focardi and Gianluigi Zavattaro, editors, Proceedings of the 2nd International Workshop on Security Issues in Coordination Models, Languages and Systems (SecCo’04), volume 128 of Electronic Notes in Theoretical Computer Science, pages 84–107. Elsevier Science Publishers, May 2005.

[20] Gavin Lowe. Breaking and fixing the Needham-Schroeder Public-Key Protocol using fdr. In TACAs ’96: Proceedings of the Second International Workshop on Tools and Algorithms for Construction and Analysis of Systems, pages 147–166, London, UK, 1996. Springer-Verlag.

[21] Robin Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer-Verlag, 1980.

[22] Robin Milner. Communicating and Mobile Systems – The Pi Calculus. Cambridge University Press, 1999.

[23] Robin Milner, Joachim Parrow, and David Walker. Modal logics for mobile processes. Theoretical Computer Science, 114(1):149–171, 1993.

[24] Roger M. Needham and Michael D. Schroeder. Using encryption for authentication in large networks of computers. Commun. ACM, 21(12):993–999, 1978.

[25] Joachim Parrow. Handbook of Process Algebra, chapter An introduction to the Pi-calculus. Elsevier, 2001.

[26] D. Sangiorgi and D. Walker. Some results on barbed equivalences in Picalculus. In Proc. CONCUR ’01, volume 2154, 2001.

[27] OpenSSL:  The  open  source  toolkit  for  SSL/TLS.

http://user.it.uu.se/ joachim/intro.ps.

Recent BRICS Report Series Publications

RS-06-19 Michael David Pedersen. Logics for The Applied π Calculus. December 2006. viii+111 pp.

RS-06-18 Ma�gorzata Biernacka and Olivier Danvy. A Syntactic Correspondence between Context-Sensitive Calculi and Abstract Machines. dec 2006. iii+39 pp. Extended version of an article to appear in TCS. Revised version of BRICS RS-05-22.

RS-06-17 Olivier Danvy and Kevin Millikin. A Rational Deconstruction of Landin’s J Operator. December 2006. ii+37 pp. Revised version of BRICS RS-06-4. A preliminary version appears in the proceedings of IFL 2005, LNCS 4015:55–73.

RS-06-16 Anders Møller. Static Analysis for Event-Based XML Processing. October 2006. 16 pp.

RS-06-15 Dariusz Biernacki, Olivier Danvy, and Kevin Millikin. A Dynamic Continuation-Passing Style for Dynamic Delimited Continuations. October 2006. ii+28 pp. Revised version of BRICS RS-05-16.

RS-06-14 Giorgio Delzanno, Javier Esparza, and Jiří Srba. Monotonic Set-Extended Prefix Rewriting and Verification of Recursive Ping-Pong Protocols. July 2006. 31 pp. To appear in ATVA ’06.

RS-06-13 Jiří Srba. Visibly Pushdown Automata: From Language Equivalence to Simulation and Bisimulation. July 2006. 21 pp. To appear in CSL ’06.

RS-06-12 Kristian Støvring. Higher-Order Beta Matching with Solutions in Long Beta-Eta Normal Form. June 2006. 13 pp. To appear in Nordic Journal of Computing, 2006.

RS-06-11 Kim G. Larsen, Ulrik Nyman, and Andrzej Wasowski. An Interface Theory for Input/Output Automata. June 2006. 40 pp. Appears in Misra, Nipkow and Sekerinski, editors, Formal Methods: 14th International Symposium, FM ’06 Proceedings, LNCS 4085, 2006, pages 82–97.

RS-06-10 Christian Kirkegaard and Anders Møller. Static Analysis for Java Servlets and JSP. June 2006. 23 pp. Full version of paper presented at SAS ’06.

RS-06-9 Claus Brabrand, Robert Giegerich, and Anders Møller. Analyzing Ambiguity of Context-Free Grammars. April 2006. 19 pp.