SPEC 0.2: A User Manual
Contents
1. where M and N are messages or an output pair written M N We write a bitrace by separating the i o pairs with a dot For example here s a bitrace a b x x enc z a enc a b Recall our convention that a and b are names whereas x is a variable rep resenting unknown values Implicitly the ordering of elements of the bitrace represents a timestamp of the message pairs In this case the pair of processes first output respectively a and b and then input an unspecified x before outputing respectively enc x a and enc x b The empty bitrace is denoted by A bitrace can be seen as a pair of symbolic traces where the input values can be left unspecified Bitraces are subject to certain well formedness criteria which can be found in Tiu09 The essence of those criteria is that the two symbolic traces that the bitrace represent are observationally indistinguishable from the view point of an intruder The technical definition of observationally indistinguishability of traces is a bit complicated but here is a simplified ac count When an intruder observes a symbolic trace what he is observing is not the identity of a particular message or messages but rather what sorts of operations one can do with them For example in a sequence of messages or a trace such as k enc m k m following bitrace notations we use dots to separate individual messages what the intruder observes is t2. nu k a lt enc a k gt This process generates a fresh key k and encrypts the name a with k and sends it off on channel a Having defined the two processes we can query SPEC to check whether they are equivalent SPEC bisim P Q Checking bisimilarity for nu ni n2 a lt enc ni n2 gt n1 aja lt ni gt 0 and nu ni a lt enc a ni gt 0 The two processes are bisimilar Size of bisimulation set 2 Use show_bisim to show the set Running time Os Note that the two processes are actually observationally equivalent because an attacker cannot distinguish the message output by P and that output by Q as the attacker does not have access to the key k which is freshly generated Moreover the guard m a in P makes sure that the output action a m can never be executed so it is essentially equivalent to 0 A yes or no answer may not be particularly convincing especially if the processes are large and complicated SPEC provides a facility to produce an evidence of the claimed equivalence in the form of a bisimulation To show such a proof use the following command SPEC show_bisim 1 Bitrace First process nu ni n2 a enc ni n2 5 n1 a a ni 0 Second process nu n1 a enc a n1 0 2 Bitrace enc ni n2 enc a n2 o First process ni a la lt ni gt 0 Second process 0 SPEC gt In this case it is particularly simple We ll see the meaning of the output in Sec
3. enc b ma P Q where x is a variable n and m are non constant names and b is a constant represents the set containing 20 x8 enc n8 m1 enc b m30 P0 Q0 where is an renaming substitution 5 3 Examples We show here a simple but interesting example to illustrate features of the bisimulation output The SPEC distribution contains a number of small and big examples in the directory examples Some of these examples encode a number of security protocols These examples may produce very large bisimulation sets in the order of hundreds to more than a thousand elements and may take quite a while to execute Example 1 Let P1 a x v k a enc z k v m a enc m enc a k m a Q1 a x v k a enc z k v m a enc m enc a k r a m a The process P1 inputs a term via channel a binds it to z and output an en crypted message enc r k It then generates a new channel m sends it off encrypted with the key enc a k Here the name a is a constant so it is known to the intruder The process then sends a message on the newly generated channel m Although the channel m is a secret generated by P1 and it is not explicitly extruded the intruder can still interact via m if it feeds the name a to Pl hence binds x to a As a result the symbolic output enc x k can be concretized to enc a k which can be used to decrypt enc m enc a k to obtain m The process Q1 is very similar except that i
4. zero D nabla x1 bisim cons out nm xi nm x1 nil nu x2N nu x3 outp ct x1 en x2 x3 zero nu x2 outp mm x1 en ct x1 x2 zero The bisimulation set consists of those entries marked with P Notice that the names in the entries of the table are V quantified This reflects the fact that the bisimulation set is closed under renaming 18 Note that in the SPEC interface one can also output the bisimulation set in the Bedwyr syntax using the command stsave bisim raw 7 Extensions to Bedwyr This section is intended only for readers familiar with the Bedwyr system Please refer to the Bedwyr website http slimmer gforge inria fr bedwyr for an introduction to the Bedwyr system The Bedwyr version used to implement SPEC is a modification of the official release of Bedwyr The reason for this modification is mainly because that the decision procedure for checking bitrace consistency needs to manipulate sub stitutions of the object level i e spi calculus variables explicitly and perform unification on them The implementation encodes object level variables and names as rigid terms in Bedwyr but dynamically convert these to logic vari ables and back in order to access the built in unification procedure of Bedwyr As a consequence some of the modifications to Bedwyr introduce non logical features that allow abstracting away logic variables The logical interpreta tions of these additional featu
5. call these names constants Hence the intruder also possesses the following capability e Constant testing the ability to recognise a constant In the user interface of SPEC any free names entered by the user are considered constants The purpose of introducing constants as public names is to reduce the size of bitraces when checking for equivalence as these constants need not be included in the bitraces A consistent bitrace is then a bitrace where all possible observations applying to its first projection are also valid observations on its second projection and vice versa This is related to the notion of static equivalence in the applied pi calculus AF01 where a bitrace can be seen as a pair of statically equivalent frames AF01 A bisimulation is a set of triples of the form h P Q where h is a con sistent bitrace and P and Q are processes satisfying some closure conditions see Tiu09 Two processes P and Q are observationally equivalent or more precisely bisimilar if we can exhibit a bisimulation set containing the triple P Q 5 Checking process equivalence and understand ing its outputs Let us start by defining a couple of simple processes SPEC P nu x y a lt enc x y gt a lt b gt SPEC Q nu x y a lt enc b y gt a lt b gt This defines two processes P and Q We can use the command show_defs to show the process definitions we entered so far SPEC gt show_defs P nu ni1
6. checking bisimilarity is located in the file src defs bisim def We first invoke Bedwyr and load this file 4 src bedwyr src defs bisim def Bedwyr 1 4 alpha2 revision 861 welcomes you This software is under GNU Public License Copyright C 2005 2012 Slimmer project For a little help type help The predicate for bisimulation checking is called bisim and it takes three ar guments the first one is for bitrace and the second and the third are processes we want to check equivalence for A bitrace is represented as a list of i o pairs in Bedwyr The type bt_pair denotes the set of i o pairs and it has the following constructors e in tm tm bt pair used to encode input pairs and e out tm tm bt pair used to encode output pairs Lists are encoded using the standard polymorphic constructors nil for the empty list and cons for constructing a new list given an element and another list What the SPEC interface does when checking bisimilarity is basically calling the bisim predicate with the empty list as the bitrace For example for checking bisimilarity of v m k a enc m k 0 and v K a enc a k 0 one would type the following query nabla aX bisim nil nu m nu kN outp ct a en m k zero nu kN outp ct a en ct a k zero Yes More y 17 The V quantifier provides a new name Here we assume that a is a constant Working directly in Bedwyr allows us to enter a more flexible quer
7. found X a More y y No more solutions abstract a 8 a a o Here a and 8 can be any types A query like abstract T Abs T abstracts the logic variables in T of type 8 and apply the constructor Abs to each abstraction and unify the result with T For example abstract pr X Y abs T Solution found X X Y Y T abs x1 abs x2 pr x1 x2 More y y No more solutions Note that because abstract can abstract any logic variables and because the underlying proof search engine of Bedwyr is untyped the abstraction produced by abstract may not always respect the type of the constructor abs For example consider the above example If pr is of type a gt 8 gt a for some distinct types o and f and abs is of type a a then the above query will still succeed despite the fact that abs is applied to terms of both types Hence type checking at the user level does not guarantee runtime type soundness well typed programs don t go wrong In the future we plan to integrate type checking directly into the Bedwyr engine so that it only abstracts variables of the correct types rigid a o This is a meta level assertion predicate The query Crigid X will throw an exception hence causes the prover to abort if X is not a ground term This predicate is mainly used as an assertion in SPEC prover to ensure that no logic variable leaks occur when converting an object variable to
8. n2 a lt enc n1 n2 gt a lt b gt 0 Q nu ni n2 a lt enc b n2 gt a lt b gt 0 SPEC gt Notice that SPEC automatically renames the bound variables x and y to its internally generated fresh names n1 and n2 in this case In general SPEC will prefix any bound names or names freshly generated with the letter n The engine also performs a conversion as neccessary to avoid name clashes As discussed in the previous section free names in a process entered by the user are automatically considered as constants by SPEC with the consequence that they are known publicly to the intruder 10 Recall from Section 2 that the command bisim allows use to check for bisim ilarity SPEC bisim P Q Checking bisimilarity for nu ni n2 a lt enc ni n2 gt a lt b gt 0 and nu ni n2 a lt enc b n2 gt a lt b gt 0 The two processes are bisimilar Size of bisimulation set 2 Use show_bisim to show the set Running time Os What the implementation of bisimulation in SPEC does is basically unfold the transitions of P and Q in locked steps and at each step the messages input output by the processes are added to the current bitrace initially it is the empty bitrace At each step SPEC also checks that the bitrace produced in that step is consistent The bisimulation set produced by SPEC can be displayed using show_bisim SPEC gt show_bisim 1 Bitrace First process nu n1 n2 a lt enc ni1 n2 gt a lt b gt 0 Second p
9. puter Security Foundations Symposium CSF 2010 pages 307 321 IEEE Computer Society 2010 Alwen Tiu A trace based bisimulation for the spi calculus An extended abstract In APLAS volume 4807 of Lecture Notes in Computer Science pages 367 382 Springer 2007 Alwen Tiu A trace based bisimulation for the spi calculus CoRR abs 0901 2166 2009 23
10. recursive definitions so in particular in the definition of a process identifer A the same identifier cannot occur in the body of the definition 3 1 Concrete syntax The concrete syntax accepted by the parser of SPEC is very similar to the abstract one described previously We follow the following conventions with respect to names and identifiers e Names and variables are represented by any alpha numeric strings that start with a lower case letter e g a b etc e Process identifiers are represented by any alpha numeric strings that start with a capital letter e g A B We also allow the underscore _ letter e g as in Agent A The concrete syntax for each construct follows closely the abstract syntax given previously except for the v operator which is represented by the keyword nu For example the following processes 0 A a b c a x r b c 0 A a b c a enc b k 0 v x y a x a y 0 v a a x 0 are respectively written in the concrete syntax as 0 Afa b c a x x lt b c gt 0 Afa b c a lt enc b k gt 0 nu x y a x aXy 0 nu x a lt x gt 0 3 2 Operator precedence associativity and simplication To ease writing down and reading processes we adopt the following conven tions e All the unary operators e g input output prefix the match operator the replication and the restriction operator have higher precedence than the parallel composition For example the expressio
11. the native code Ocaml compiler ocamlopt since it is much faster If for some reason this feature is not desired it can be disabled using configure disable native code 2 2 Running SPEC To run the SPEC user interface type src spec This will bring up the command line interface SPEC An equivalence checker for the spi calculus Version 0 2 This software is under GNU Public License Copyright c 2011 2013 Alwen Tiu SPEC gt At the command line interface we can define processes to be checked for equiva lence The precise syntax will be given in Section 3 Here is an example process just as an illustration SPEC P nu m k a lt enc m k gt n a a lt m gt Reading spi definition Here the symbol to the left of is a process identifier and the expression to the right is the process itself In this case P is a process that creates two fresh names m and k and output the encrypted message enc m k representing a message that is obtained by encrypting m with key k on channel a It then performs a useless check on whether m is equal to a which is always false because m needs to be a fresh name before outputting m on channel a Every definition or any other statement in the command prompt must ends with a semicolon By default SPEC treats free names in a process as public names i e they are known to the intruder In this case the only public name is a Let us define another process SPEC Q
12. SPEC 0 2 A User Manual Alwen Tiu Research School of Computer Science The Australian National University 1 Overview SPEC for Spi calculus Equivalence Checker is an equivalence checker for a ver sion of Abadi and Gordon s spi calculus AG99 The spi calculus is an extension of the z calculus MPW92 with operators encoding cryptographic primitives In this implementation we consider only a symmetric key encryption As shown in AG99 the spi calculus can be used to encode security protocols and via a notion of observational equivalence security properties such as secrecy and authentication can be expressed and proved Intuitively observational equivalence between two processes means that the observable actions of the processess cannot be distinguished in any execution environment which may be hostile e g if it represents an active attacker trying to compromise the protocol The formal definition of observational equivalence AG99 involves infinite quantification over all such execution environments and is therefore not an effective definition that can be implemented Several approx imations have been proposed AG98 BNP02 BBN04 BN05 Tiu07 Tiu09 the current implementation of SPEC is based on a notion of open bisimulation pro posed in Tiu07 Tiu09 In particular the decision procedure implemented here derives from TD10 It is important to note that the notion of observational equivalence as formalised in the spi calcu
13. a logic variable and vice versa 20 e trace o This nullary predicate returns the value of the trace flag set via the trace command see below It can be used by programs to toggle on off printing of traces or other debugging information e abort o This predicate aborts the proof search and returns to the toplevel query if in interactive mode Two new system level commands have been introduced e trace on off This system level command sets the trace flag Note the system only sets the flag to true false The use of this flag is up to the program Its value can be read off by a program via the predicate trace e itsave table predicate filename This will save the table for a predicate to a definition file A proved entry will become the argument of a predicate called proved Similarly an unproved entry will be the argument of an unproved predicate 7 1 Modifications to the tabling mechanism The tabling mechanism now allows for matching of table entries up to renaming of V variables As an example consider this very simple program inductive q X Y println Proved without using table and consider this query nabla x nabla y q x y Proved without using table Yes More y n Bedwyr executes the body of the definition clause for q which prints a message and stores the goal in the table Now the second time the query is repeated nabla x nabla y q x y Yes More y we s
14. cess 3 2 enc n1 n2 VIT a IHR mi 3 w I nc n3 enc a n2 M89 xw m x S Fo oR 4 Bi trace nl nY enc n1 n2 enc n1 n2 First process Second process v n3 enc n3 enc a n2 nl a ns la 0 14 5 Bi trace nl n1l enc n1 n2 enc n1 n2 enc n3 enc a n2 enc n3 enc a n2 First process n3 a 0 Second process nl al a cals w A few notes on the output produced by SPEC e Typesetting of names and variables Variables are typeset by prepending the variables with a question mark Bound names and non constant names are typeset using italised fonts while constants are un italicised e The original process pair is given in item 1 The unfolding sequence pro ceeds as follows 1 3 4 gt 5 gt 1 Notice that in moving from 5 to 1 the input pair disappears from the bitrace This is because the variable nl gets instantiated to a which is a constant hence public knowledge and it is removed by the simplification step of SPEC e Equivariance of bisimulation Notice that in proceeding from 5 to 1 there is an implicit renaming performed by SPEC Without renaming the bitrace in item 1 would have been the following enc a n2 enc a n2 enc n3 enc a n2 enc n3 enc a n2 6 Interacting at the Bedwyr level This section is intended only for readers familiar with t
15. d names Spi calculus names constants and variables are encoded using additonal unary operators applied to these unsorted names e tm the set of terms i e messages Constructors for terms are as follows ct name tm This is used ot encode constant var name tm This is used to encode variables nm name tm This is used to encode names other than constants pr tm tm tm This encodes pairing enc tm tm tm This encodes symmetric encryption e proc this is the type of processes Constructors for processes are as follows zero proc The 0 process par proc proc proc Parallel composition nu tm proc proc Restriction match tm tm proc proc Matching inp tm tm proc proc Input prefix outp tm tm proc proc Output prefix let tm tm tm proc proc Let operator case tm tm tm proc proc Case operator bang proc proc Replication 16 For example the process v y a z r y 0 a y 0 will be represented as the simply typed term assuming we have a term a of type name nu Ay par inp ct a Ax match x y zero outp ct a y zero Note that the nu operator binds only one name at a time so to encode multiple binders such as v x y x y 0 we iterate the nu operator twice i e nu Ax nu Ay match x y zero 6 2 Running the bisimulation checker To main procedure for
16. ee that the print statement is not executed because Bedwyr proves the query by a lookup in the table of previously proved queries and does not execute the body of the clause To see the effect of automatic renaming consider this query nabla x nabla y q y x Yes More y where the roles of x and y are exchanged This query is also executed successfully by a table lookup as the goal can be matched to the table entry by renaming y to x We see that adding vacuous V quantification does not affect this equivariant matching as in the following query 21 nabla x nabla yN nabla z q x Z Yes More y What the tabling lookup checks is that q has two distinct V variables as argu ments So the following query will not match the table as a consequence the message in the body of the clause will again be printed nabla x q X X Proved without using table Yes More y Acknowledgment This work is supported by the ARC Discovery grants DP0880549 and DP110103173 The author would like to thank David Baelde for many useful correspondences regarding the implementation of the Bedwyr system and Quentin Heath for many improvements to the Bedwyr proof engine used to implement SPEC References AF01 Mart n Abadi and C dric Fournet Mobile values new names and secure communication In POPL pages 104 115 2001 AG98 Mart n Abadi and Andrew D Gordon A bisimulation method for cryptographic protocols Nord J C
17. hat he can use the first message in the sequence to decrypt the second message and obtain a message that is identical to the third message in the sequence Here the particular names used in the message is unimportant as long as he could do those two operations of decryption and message comparison So from this perspective the intruder would consider the following sequence of messages observationally equivalent to the previous one l enc n 1 n despite the fact that we use different names However the intruder will be able to detect a difference with the following trace assuming m and n are distinct names l enc n 1 m as the intruder notices that the result of decrypting the second message with the first message as the key produces a different message than the third one More specifically the observational capabilities of an intruder as formalised in AG98 can be summarised as follows e Decryption the ability to decrypt an encrypted message given the right key e Projection the ability to extract components of a pair e Equality testing the ability to compare two messages for syntactic equal ity For the purpose of simplifying the implementation of SPEC we assume an additional capability we assume that the intruder has knowledge of a set of public names as in the notion of frames in Abadi and Gordon s frame bisim ulation AG98 That is we shall designate a certain set of names to be public names We shall simply
18. he Bedwyr system Please refer to the Bedwyr website http slimmer gforge inria fr bedwyr for an introduction to the Bedwyr system The SPEC proof engine is implemented on top of a modified version of Bed wyr The Bedwyr codes for SPEC are contained in the subdirectory src defs Here is a brief description of the important definition files in that directory l This automatic renaming is a built in feature of Bedwyr so it is not possible to alter it without modifiying the search engine of Bedwyr It is a by product of equivariance tabling implemented in Bedwyr See Section 7 15 e bisim def This is the main module that implements the bisimulation checking e bitrace def This module implements procedures related to bitraces in particular the decision procedure for checking bitrace consistency e intruder def This module implements a decision procedure for solving deducibility constraints under the Dolev Yao intruder model It is used in the decision procedure for bitrace consistency e spi def This module implements the operational semantics of the spi calculus 6 1 Intermediate syntax of processes The theoretical foundation of Bedwyr is based on a variant of Church s simple theory of types All expressions in Bedwyr are encoded as simply typed A terms For the implementation of SPEC we introduce among others the following types for the syntactic categories of terms and processes e name the set of unsorte
19. liar with the Bedwyr system and describe various extensions to the Bedwyr system that are implemented to support the proof engine of SPEC 2 A quick start 2 1 Downloading and compiling SPEC The latest version of SPEC can be downloaded from the project page http users cecs anu edu au tiu spec The SPEC distribution includes a modified version of the Bedwyr prover SPEC is implemented using the Ocaml language and has currently been tested only on the Linux operating system To compile SPEC download the SPEC package from the website given above and unpack it in a directory of your choice For the purpose of this tutorial we assume that the unpacked files are located in the spec directory inside the user s home directory The structure of the distribution consits of the following directories e src Contains the source codes for both the modified Bedwyr and SPEC related files The core engine of SPEC is located in the subdirectory src defs these are program files that will be run in the Bedwyr proof engine e doc Contains the manual of SPEC e examples Contains some examples of processess and protocols To compile the distribution run the following commands cd HOME spec configure make This will create two executables spec and bedwyr in the subdirectory src If you are not interested in tweaking the Bedwyr codes the program spec is all you need to be aware of Just as Bedwyr by default SPEC is built using
20. lus assumes a model of intruder known as the Dolev Yao model DY83 This means among others that we assume that the encryption function is perfect in the sense that an attacker is not able to decrypt an encrypted message unless he she knows the key The current version of SPEC is still at the alpha testing phase and al lows only modeling symmetric encryptions It is also not yet optimised for performance The tool can only reason about equivalence or more precisely bisimilarities of finite processes i e those without recursion It cannot yet be realistically used to decide equivalence of protocols with unbounded sessions this will require more sophisticated techniques In future releases it is hoped that more encryption operators will be supported and more functionalities will be added in particular facilities to do symbolic trace analyses correspondence assertions type checking and model checking The proof engine of SPEC is implemented in an improved version of the Bed wyr model checking system BGM 07 but the user interface is implemented directly in Ocaml utilising a library of functions available from Bedwyr The user however does not need to be aware of the underlying Bedwyr implemen tation and syntax in order to use the tool Readers who are interested only in using SPEC for checking process equiv alence should read Section 2 Section 3 Section 4 and Section 5 Section 6 and Section 7 are intended for readers fami
21. n v x a x a y x y 0 a y 0 represents the process v a z a y fe y 0 a y 0 e The paralel composition associates to the right Thus P Q R is the same as P Q R e We can omit the trailing 0 in input ouput prefixed processes For example we write a x a y instead of a x a y 0 3 3 Inputing process definitions As mentioned in Section 2 the definition of a process identifier can be entered at the SPEC command prompt by ending it with a semicolon SPEC checks whether all free names in the body of the definition are in the parameters of the definition If there is a name in the body which does not occur as a parameter SPEC gives a warning Process definitions can also be imported from a file To do so simply write down the definitions in a file with each definition ended with a semicolon To load the definition use load For example the following loads the file wideMouthedFrog spi in the examples subdirectory SPEC load examples wideMouthedFrog spi 8 process definition s read Use show_defs to show all definitions SPEC The definition of a particular process identifier can be queried using the com mand show_def followed by the identifier For example SPEC show_def P P nu ni n2 a lt enc n1 n2 gt ni a a lt n1 gt 0 SPEC gt The command show_defs will show all the definitions entered so far 4 Some theoretical backgrounds This section is intended to provide a ve
22. ollowing grammar M N a x M N enc M N where a denotes a name and x denotes a variable Names are considered to be constants i e they cannot be instantiated by other terms wherease variables can be instantiated The need for variables arises from the need to symbolically represent input values which can range over an infinite set of messages when unfolding the transitions of a process The message M N represents a pair of messages M and N and enc M N represents a message M encrypted with key N using a symmetric encryption function Note that the key here can itself be any term We assume a set of process identifiers ranged over by capital letters such as A B etc The purpose of a process identifier is to simplify the writing of a process by acting as a sort of macros for processes A process identifier may be assigned an arity representing the number of arguments it accepts The language of processes is given by the following grammar Pu A a a4 O0 a z P a M M 2 N P v a1 m P P P P let x y M in P case M of enc z N in P The intuitive meaning of each of the process construct except for process iden tifier which is explained later is as follow e 0 is a deadlocked process It cannot perform any action e a a P is an input prefixed process The variable x is a binder whose scope is P The process accepts a value on channel a binds it to the variable x and evolves in
23. omput 5 4 267 303 1998 AG99 Martin Abadi and Andrew D Gordon A calculus for crypto graphic protocols The spi calculus Information and Computation 148 1 1 70 1999 BBNO4 Johannes Borgstr m S bastien Briais and Uwe Nestmann Sym bolic bisimulation in the spi calculus In Philippa Gardner and Nobuko Yoshida editors CONCUR volume 3170 of Lecture Notes in Computer Science pages 161 176 Springer 2004 BGM 07 David Baelde Andrew Gacek Dale Miller Gopalan Nadathur and Alwen Tiu The Bedwyr system for model checking over syntactic expressions In Frank Pfenning editor 21th Conference on Auto mated Deduction number 4603 in LNAI pages 391 397 Springer 2007 BN05 Johannes Borgstr m and Uwe Nestmann On bisimulations for the spi calculus Mathematical Structures in Computer Science 15 3 487 552 2005 22 BNP02 DY83 MPW92 TD10 Tiu07 Tiu09 Michele Boreale Rocco De Nicola and Rosario Pugliese Proof techniques for cryptographic processes SIAM Journal of Comput ing 31 3 947 986 2002 D Dolev and A Yao On the security of public key protocols IEEE Transactions on Information Theory 2 29 1983 Robin Milner Joachim Parrow and David Walker A calculus of mobile processes Part II Information and Computation pages 41 77 1992 Alwen Tiu and Jeremy E Dawson Automating open bisimulation checking for the spi calculus In Proceedings of the 23rd IEEE Com
24. res are currently unclear so the implementation of SPEC in this modified Bedwyr does not inherit the meta logical properties of the logic underlying Bedwyr BGM 07 It is therefore more appropriate to view this modified Bedwyr as a programming framework rather than a proper logi cal framework like it was designed to be However as the bisimulation checker in SPEC can actually output a bisimulation set as a witness of observational equivalence unsoundness of Bedwyr is not a real concern as that witness can be checked for correctness independently of the Bedwyr engine The list of non logical predicates added to Bedwyr is given below All these are prefixed with an underscore _ e not o o This is the standard negation as failure as in prolog e if o o 0 o This is an if then else operator The query if P Q R is basically equivalent to P Q V not P Q The slight difference is that the second disjunct will not be tried if the query P succeeds e distinct o o Calling distinct P directs bedwyr to produce only distinct answer substitutions For example if a predicate p is defined as follows pa pa then querying p X in Bedwyr will answer with the same answer substitu tion twice p X 19 Solution found X a More y y Solution found X a More y y No more solutions If we apply the distinct operator only one answer substitution is given distinct p X Solution
25. rocess nu n1 n2 a lt enc b n2 gt a lt b gt 0 2 Bitrace enc ni n2 enc b n2 o First process a lt b gt 0 Second process a lt b gt 0 SPEC The original processes are listed in the first item which get unfolded into the second item In the second item we notice that the first process is actually equal to the second process SPEC recognises this automatically and stops the unfolding at this point as bisimilarity is reflexive The resulting bitrace at each step is also given As we said earlier input or output messages are appended to the current bitrace at each step 5 1 Separation of names in bisimulation An important thing to note in reading a bisimulation triple h P Q is that the names other than constants used in the first projection of the bitrace h and process P are unrelated to the names used in the second projection of h and Q This is because names represent entities that may be generated internally by the processes via scope extrusion and may be unknown to the intruder hence their identities are not something which is generally observable See AG98 for an explaination of this 11 5 2 Equivariance of bisimilarity Another important thing to keep in mind when reading the output bisimulation set produced by SPEC is that each triple in the set represents an equivalence class of triples modulo renaming of variables and names but excluding con stants Thus a triple such as x x enc n m4
26. ry brief account of the notion of bisim ulation used in SPEC in order to understand its output For a more detailed account the reader is refered to Tiu07 Tiu09 The procedure to prove observational equivalence implemented by SPEC is based on a notion strong open bisimulation for the spi calculus developed in Tiu07 Open bisimulation is sound with respect to observational equivalence in the sense that when two processes are open bisimilar they are also observa tionally equivalence However it is not complete as there are observationally equivalent processes that cannot be proved using open bisimulation This is not specific to our notion of bisimulation rather it is a feature of strong bisimulation which do not abstract away from internal unobservable transitions For exam ple the process v x x a x y a b and the process a b are observationally equivalent but are not strongly bisimilar A bisimulation is essentially a set that satisfies some closure conditions We shall not explain in details what those conditions are these can be found in Tiu09 TD10 Instead we shall only illustrate what the members of such a bisimulation look like Our notion of bisimulation is parametric on a structure which we call bitraces A bitrace represents a history of the input output actions of the pair of processes being checked for bisimilarity A bitrace is essentially a list of i o pairs An i o pair is either an input pair written M N
27. t puts a guard on the possibility of interacting on m by insisting that z a The above informal reasoning about the behavior of P1 shows that it should be observationally equivalent to Q1 Before we try proving the bisimilarity of P1 and Q81 first execute the fol lowing command SPEC gt reflexive off Reflexivity checking is disabled 12 This instructs SPEC to disable an optimisation i e the reflexivity checking Reflexivity checking allows SPEC to conclude immediately that identical pairs of processes are bisimilar Disabling this allows us to see a bit more clearly how the bitraces in the bisimulation set in the following example change from one entry to another After disabling reflexivity checking and running the command bisim P1 Q1 we get that the two processes are indeed bisimilar The bisimulation set pro duced can be displayed using the show_bisim command but here we shall try to output it in a LaTeX format 1 Bi trace First process S m N A enc nl n2 g v gl x aoa 3 w nc n3 enc a n2 a m o Second process a n1 n2 enc n1 n2 n3 1 oY od enc n3 enc a n2 3 A A NEA a es 2 Bi trace enc a n1 enc a n1 enc n2 enc a n1 enc n2 enc a n1 First process 0 Second process 0 13 3 Bi trace nl n1 First process v Vor aT oa 3 w Second pro
28. tion 5 There are also a couple of other forms of output as we ll see in Section 5 2 3 Available commands There are some meta commands available in SPEC which can be queried by using the help command The list of commands is as follows e help Display the help message e exit Exit the program e equivariant Turning the equivariant tabling on off See Section 7 1 By default equivariant is always set to on e reflexive Turning reflexivity checking on off e load file Load a process definition file e reset Clears the current session This removes all process definitions defined in the current session e show_bisim Displays the bisimulation set of the most recent bisimula tion query e save_bisim file Save the current bisimulation set to a file e save_bisim_latex file Save the current bisimulation set to a file in the LaTeX format e save_bisim_raw file Save the current bisimulation set in the inter nal Bedwyr syntax e itshow def name Show the definition for an agent e show_defs Show all the definitions e time on off Show hide the execution time of a query e trace on off Enable disable trace printing 3 Syntax of processes The spi calculus generalises the 7 calculus by allowing arbitrary terms to be output instead of just simple names To define the language of processes we first need to define the set of terms or messages The set of terms allowed is defined by the f
29. to P e a M P is an output prefixed process It outputs a term M on channel a and evolves into P e M N P is a process which behaves like P when M is syntactically equal to N but is otherwise a deadlocked process e v zi 24 P is a process that creates m new names and behaves like P The v operator also called the restriction operator binds the name Ds bal e P Q is a paralel composition of P and Q e P is a replicated process it represents an infinite paralel copies of P e let x y M in P The variables x and y are binders whose scope is P This process checks that M decomposes to a pair of messages and binds those messages to x and y respectively e case M of enc z N in P The variable x here is a binder whose scope is P This process checks that M is a message encrypted with key N decrypts the encrypted message and binds it to x A process definition is a statement of the form A z1 24 P where A is a process identifier of arity n and P is a process We call A z1 24 the head of the definition and P its body The variables z 2x4 are the pa rameters of the definition A process identifier that occurs in a process P must be applied to arguments which are names For example if A is defined as A x y 2 z y z 2 0 then it can be used in a process such as this a z a y a z A a y 2 This process is equivalent to where the definition of A is expanded SPEC does not allow
30. y such as attaching a non trivial bitrace to the bisimulation pair For this we shall utilise the predicate toplevel_bisim This predicate works as bisim except it also checks the bitrace for consistency whereas bisim does not check for consistency For example instead of assuming a as constant we could assume it is non constant name using the constructor nm We will need to add this name explicitly in the bitrace otherwise the bisimulation checker will reject it nabla aX toplevel bisim cons out nm a nm a nil nu m nu kN outp nm a en m k zero nu kN outp nm a en nm a k zero Yes More y 6 3 Bisimulation output in Bedwyr syntax The predicate bisim is declared as a coinductive predicate in bisim def This means that Bedwyr automatically saves successful or failed proof search asso ciated with the bisim predicate in a table The set of bisimulation associated with the current bisimulation query can be displayed using the amp show table command For example continuing the previous example one can display the entries of the table as follows dshow table bisim Table for bisim contains P Proved D Disproved P nabla x1 nabla x2 nabla x3 bisim cons out nm x3 nm x3 cons out en nm x2 nm x1 en nm x3 nm x2 nil zero zero P nabla x1 bisim cons out nm x1 nm x1 nil nu x2 nu x3 outp nm x1 en x2 x3 zero nu x2N outp nm x1 en nm x1 x2
Download Pdf Manuals
Related Search