BRICS. Logics for The Applied π Calculus. BRICS RS M. D. Pedersen: Logics for The Applied π Calculus. Basic Research in Computer Science - PDF

Description
BRICS RS M. D. Pedersen: Logics for The Applied π Calculus BRICS Basic Research in Computer Science Logics for The Applied π Calculus Michael David Pedersen BRICS Report Series RS ISSN

Please download to get full document.

View again

of 30
All materials on our website are shared by users. If you have any questions about copyright issues, please report us to resolve them. We are always happy to assist you.
Information
Category:

Biography

Publish on:

Views: 27 | Pages: 30

Extension: PDF | Download: 0

Share
Transcript
BRICS RS M. D. Pedersen: Logics for The Applied π Calculus BRICS Basic Research in Computer Science Logics for The Applied π Calculus Michael David Pedersen BRICS Report Series RS ISSN December 2006 Copyright c 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: Telefax: Internet: BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs: 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, i 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 reduciii tion 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. Consequentlythe 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. iv 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 v 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. vi Contents 1 Introduction Brief History The Applied π Calculus Static Equivalence Process Logics Objectives and Contributions Outline of the Report Preliminaries Syntax of Applied π Semantics of Applied π Equivalences in Applied π Summary A Refined Definition of Strong Static Equivalence Previous Work Initial Definitions The Refined Definition Examples Summary Results On The Refined Definition ss implies ss ss implies ss Conditions under which s and ss Coincide Summary A Logic for Frames Motivation Syntax and Semantics Characterisation Characteristic Formulae Summary vii CONTENTS 6 A Logic for Applied π Syntax Semantics Match and Matching Input Modality Characterisation Summary An Application to the Needham-Schroeder Public Key Protocol The Needham-Schroeder Public Key Protocol The Specification Logical Properties Summary Conclusion Contributions Future Work viii 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 -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 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 1 CHAPTER 1. INTRODUCTION 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,isan 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 bwould 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)a enc(b, k + ).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+ )/ x1 } { k / x2 } P ) The sub-processes { enc(b,k+ )/ x1 } and { k / x2 } 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 2 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+ )/ x1, k / x2 } 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+ x1, k / x2, b / x3 } ϕ 2 =(νk,b){ enc(enc(b,b+ ),k + )/ x1, k / x2, )/ enc(b,b+ x3 } ϕ 3 =(νk,b){ enc(enc(b,k+ ),k + )/ x1, k / x2, b / x3 } 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 band dec(enc(enc(b, b + ),k + ),k )= E enc(b, b + ) andany 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 3 CHAPTER 1. INTRODUCTION 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 equivalen
Related Search
Similar documents
View more...
We Need Your Support
Thank you for visiting our website and your interest in our free products and services. We are nonprofit website to share and download documents. To the running of this website, we need your help to support us.

Thanks to everyone for your continued support.

No, Thanks