Contents
1. though the situation will improve as value passing is introduced Techniques such as Skolemisation deducing results concerning all messages from veri fications on place holders might also be appropriate here In any case some simplifications will have to be made perhaps concerning the maximum number of encryptions in order to regain finitude of the message space and some additional justification of these assumptions will then be required to derive general correctness This should not present any problems since the protocols themselves will only perform encryptions to a certain level generally no more than two and so any interference involving deeper levels will be detected in any case But nevertheless it will be necessary to prove that the imposition of a bound does not rule out any attacks on a protocol in order to have confidence in the results of the analysis Additional modelling issues The modelling of the enemy as a separate process allows for the possibility of introducing tactics in the state space exploration when model checking for ex ample by restricting the number of messages that the enemy will place on the medium By accompanying enemy interference with the performance of events we may introduce tactics by introducing further con straints in parallel refining the system This may prove useful when attempting to detect flaws since a flaw in a refinement will be a flaw in the original system but correctness of2. 7 cannot obtain messages that were intended for some other user For analysis purposes we will consider the system from the God s eye view the only user which might obtain messages intended for some other user will be user 0 Hence confidentiality will be captured as a spec ification requiring that any message output to user 0 must have actually been sent to user 0 We restrict at tention to the message set M as being those messages which are intended to remain confidential We also as sume they cannot be generated by user 0 which would be true for example for signed messages though this is a simplifying assumption that is not justified in all circumstances This assumption is implicit in the def inition since otherwise 0 could simply guess any con fidential message Other messages such as encrypted messages or control messages will in general be avail able to eavesdroppers but confidentiality is not con cerned with protecting these These considerations may be captured as a trace specification Definition 3 1 NET provides confidentiality for the set of messages M if and only if NET sat Vm M etr out 0 USER m F tr in USER 0 m F This definition states that any message m which is out put to user 0 i e evidenced by a message out 0 i m in the trace tr must have initially been sent to user 0 i e there must be some j for which in j 0 m appears in the trace This may also be expressed within t
3. and source from the body of the message Again there are other possibilities for example if the message is to be broadcast to all users then no explicit destination field is required INPUT B 0 trans i j 2 MEDIUM B U i j Here the channel trans is of type USER USER MESSAGE A message trans i j m should be thought of as node i sending an input j m to the medium indicating the wish that message m be delivered to node j Thus is the source j the destination and m the message We have abstracted away refusals in the sense that input can never be refused which amounts to making the assumption that nothing can be deduced from how or when the messages are accepted This is a reason able assumption since there are protocols currently in use to perform tasks such as masking network traffic Hence at this level of abstraction we can assume that messages are always accepted by the network If this is later felt to be unrealistic the definition of INPUT can be altered accordingly so that messages may not be input after the number of messages in the network reaches some capacity threshold The process OUTPUT allows output from the medium OUTPUT B ea rec jlitag gt MEDIUM B i j 2 Here the channel rec is of type USER USER MESSAGE A message rec j i m corresponds to the receipt of a message m by node j which is labelled as coming from source node 7 Note that an empty external choice is simply equiv alent to
4. arises from the fact that the users of this ser vice such as people and applications programs do not have control over the medium and so it is possible for malicious agents to intercept or interfere with network traffic The need for confidentiality in the face of an insecure medium creates the need for some form of en cryption and the need for authenticity when message forgery is possible also raises the need for some form of security mechanism A common approach to modelling this situation is to consider a set of nodes as connected to the medium which is modelled as a single process Although the medium will in general consist of a network of pro cesses this network may be considered at a higher level of abstraction as a single process The only interactions the nodes may have with other nodes must be through this medium As discussed earlier we will find it con venient to model malicious interference by means of a separate enemy process node 0 which manipulates the essentially passive medium Thus the service provided to the users is modelled as The nodes are unable to interact directly so their op eration is entirely interleaved They all communicate with the medium by means of channels trans and rec used by the nodes to transmit and receive messages respectively Quite often the distinction between a user and the node by which the user communicates with the net work is blurred when addressing security properties A
5. equivalent to the assertion NET sat tr out 0 USER M It is straightforward using the process algebra to show that if a system provides confidentiality for two sets M1 and M2 separately then it provides confiden tiality for both sets simultaneously if NET out 0 USER M1 STOP NET and NET out 0 USER M2 STOP NET then NET out 0 USER M1U M2 STOP NET out 0 USER M1 STOP out 0 USER M2 STOP NET out 0 USER M2 STOP NET Message Authentication This property requires that messages can be guar anteed to be authentic in the sense that a particu lar message purporting to have come from a particular source really did come from that source Authentica tion requires that messages cannot be forged In abstract terms event 6 authenticates event a if the observation of b is possible only if a occurred previously the observation of 6 provides evidence of a s previous occurrence Definition 3 3 Event b authenticates event a in pro cess P if and only if P sat AUTH tr where AUTH tr trb O gt trla 0 Observe that this specification does not restrict the number of occurrences of event b to each occurrence of event a The expression of this property in terms of a sat specification demonstrates that it is preserved by re finement This specification can also be captured as a process algebraic equation P a b STOP P a STOP And since it is
6. intersects with that of a NODE sat kernel TRANS tr N kernel a Of course more complex specifications might be more appropriate for example that the messages added to the network by the nodes do not intersect with a though those that were passed to the node may be passed back NODE sat kernel TRANS tr N kernel a kernel REC tr This latter specification is in fact met by NODE 5 Discussion Model checking This paper has been concerned with the expression of particular security properties and protocols within the framework of CSP in order to provide a founda tion for analysis and verification This approach is mo tivated in part by the availability of model checking tools such as FDR 1 and the work has always pro ceeded with an eye on applicability of these tools How ever it is inevitable that there will be some practical difficulties and it may be necessary to adapt some of the properties When this becomes necessary we will have to establish that the properties we are checking do indeed correspond to the properties presented in this paper or at least that results obtained by application of the tools allow us make the inferences we require For example the sets PLAINTEXT and MESSAGES will generally be infinite even when the base sets are very small This makes them unsuit able for direct analysis by means of model checking using current February 1996 state of the art technol ogy
7. on out 0 only those messages it deduces have been gen erated by the legitimate users in particular ignoring those messages in M that it puts onto the medium and then reads back via leak We will not pursue this fur ther in this paper but will observe that it is a situation to bear in mind Nodes We must consider the nodes which are the link between the user and the medium to be under the control of the user It is the nodes that will provide the security facilities required by the users such as en crypting and deciphering messages The finite set of all nodes will be labelled using the set USER 0 1 n The nodes provide the means by which users send messages over the network A user communicating with the network is in fact communicating with the corresponding node Nodes interact with users by inputting plaintext messages with intended destina tions and outputting such messages together with their source The process NODE thus communi cates with its user via channels in i and out i of type USER PLAINTEXT An input in i j7 m to node NODE is interpreted as a request from user 7 to send message m to user j Similarly an output communi cation out i j m is interpreted as delivery to user i of message m purporting to come from j Nodes with the exception of node 0 interact with the medium by transmitting possibly enciphered messages together with other control messages in tended recipients and any other mess
8. 94 2 J W Gray and J McLean Using temporal logic to specify and verify cryptographic protocols progress re port In Proceedings of the eighth IEEE Computer Se curity Foundations Workshop 1995 3 C A R Hoare Communicating Sequential Processes Prentice Hall 1985 4 C Meadows Applying formal methods to the analysis of a key management protocol Journal of Computer Security 1 1 1992 5 A W Roscoe Lecture notes on domain theory 1986 Oxford University 6 A W Roscoe Prospects for describing specifying and verifying key exchange protocols in CSP and FDR 1994 Formal Systems Europe Ltd 7 S A Schneider Modelling security properties with csp 1996 Royal Holloway Technical Report CSD TR 96 04
9. S sat E1g tr ENEMY S sat E2s tr MEDIUM B sat M1g tr MEDIUM B sat M2s tr NODE sat N1g tr where Elg tr kernel ADD tr C kernel S U kernel INIT U kernel LEAK tr E2s tr kernel OUTo tr C kernel S U kernel INIT U kernel LEAK tr M1g tr kernel LEAK tr C kernel B U kernel TRANS tr U kernel ADD tr M2s tr kernel REC tr C kernel B U kernel TRANS tr U kernel ADD tr Ni1g tr kernel TRANS tr C kernel REC tr Proof This is a standard mutual recursion proof in CSP The full proof has been omitted for reasons of space Some further process algebra manipulation details in the full paper finally yields the required result Theorem 4 3 The network is secure NODE trans 1 rec 1 MEDIUM leak add kill ENEMY sat tr out 0 0 4 Proof The strategy of the proof is as follows we will use the properties established in Lemma 4 2 to prove that the kernels of all messages passed around the sys tem must be contained in the kernel of INIT Since it is given that a kernel INIT it follows that a can never be passed along channel out 0 The proof could easily be adapted to take other nodes into account In fact descriptions of the other nodes are not even necessary all that is required of them is that they meet some particular specification for example that they do not transmit any messages whose kernel
10. STOP so when the set B is empty i e the medium contains no messages there is no possibility of output Finally the process A B describes the possible in teractions with the medium due to Intruder Actions A perfectly secure medium would treat this part of the process description as STOP In cases we are consider ing we model the ways in which the medium is suscep tible to interference Here the medium is vulnerable to having messages removed added or leaked IA B kill O _ MEDIUM B b if B42 MEDIUM if B 2 a dd i j gt MEDIUM B U i j 2 p leak i j e gt MEDIUM B ij E Enemy action In modelling the enemy we are concerned with mes sages that the enemy is able to generate These may be used to disrupt a protocol or may correspond to information about what the enemy has discovered con cerning supposedly confidential messages Certain assumptions may be made concerning the enemy depending on the property that is under analy sis When checking confidentiality it is often assumed that the enemy is unable to generate those messages M which can be generated by the users that should be kept confidential On the other hand when checking authentication it should be assumed that the enemy as well as the honest users is capable of generating those messages whose authenticity is ensured by the protocol since if the enemy is unable to generate them then there is no need for an
11. Security properties and CSP Steve Schneider Royal Holloway University of London Egham Surrey TW20 0EX Abstract Security properties such as confidentiality and au thenticity may be considered in terms of the flow of messages within a network To the extent that this characterisation is justified the use of a process algebra such as Communicating Sequential Processes CSP seems appropriate to describe and analyse them This paper explores ways in which security properties may be described as CSP specifications how security mech anisms may be captured and how particular protocols designed to provide these properties may be analysed within the CSP framework The paper is concerned with the theoretical basis for such analysis A sketch verification of a simple example is carried out as an illustration 1 Introduction Security protocols are designed to provide proper ties such as authentication key exchanges key distri bution non repudiation proof of origin integrity con fidentiality and anonymity for users who wish to ex change messages over a medium over which they have little control These properties are often difficult to characterise formally or even informally The proto cols themselves often contain a great deal of combinato rial complexity making their verification extremely dif ficult and prone to error This paper promotes the view that process algebra can provide a single framework both for modelling pr
12. ages employed by the protocol being used The channels used are trans i for transmission and rec i for receipt of mes sages These channels are of type USER MESSAGE where the set MESSAGE contains both plain and en crypted messages as discussed later A communica tion trans i j m corresponds to NODE placing mes sage m with destination j onto the medium A com munication rec i j m corresponds to NODE receiving message m from the medium with source purporting to be j The description of a NODE process will depend on the security property we are aiming to verify of the network For confidentiality authenticity anonymity and integrity its description will consist of a CSP im plementation of the particular protocol under analysis For example an extremely simple protocol to provide confidentiality of messages sent from user 1 to user 2 will be implemented using NODE s public key pe and secret key s as follows NODE in 1 2 a2 gt trans 1 2 po a gt NODE NODE rec 2 7 y gt STOP if so y PLAINTEXT out 2 j sa y NODE otherwise where s9 po z z for any message z Observe that this protocol does not ensure authenticity The situation is different in the case of non repudiation judge s viewpoint and the judge does not have con trol over the nodes used in a non repudiation protocol In fact from the judge s viewpoint the parties could each be dishonest Indeed it is this possibility that generates
13. aim to be live some thing good should occur in that they will be designed to achieve goals such as delivery of messages But there is a distinction to be drawn between the security re quirements implemented by such a protocol and its liveness requirements which are important for commu nication but which are generally independent of secu rity It is possible that there are some security proper ties which can be expressed only as liveness properties these are outside the scope of this paper Hence the traces model for CSP will be adequate for our present needs to analyse properties of the form something bad should not happen it is sufficient to focus on what systems may do rather than what they must do All equivalences and refinements expressed in this paper are therefore grounded in the traces model This paper is structured as follows The relevant CSP notation is introduced in Section 2 Section 3 con tains a discussion of how the properties of confidential ity and authentication may be captured within CSP independently of security protocols Section 4 discusses the modelling of security protocols and of the networks on which they are implemented and contains an exam ple verification of of a toy confidentiality property to illustrate the material finally Section 5 discusses the approach and its potential 2 CSP notation CSP is an abstract language designed specifically for the description of communication patterns o
14. always the case that P a STOPE P a b STOP the condition is equivalent to P a b STOP EP a STOP For example the process P a gt b STOP b gt c gt STOP has c authenticating b a gt STOP P b STOP P b c STOP but it does not have b authenticating a P a b STOP STOP b gt c STOP P a STOP In other words a b event can occur even if a did not occur previously In the context of sending and receiving messages we would require a received message out j i m to authen ticate a sent message in i j m In other words receipt of the message i m m from i by node j is possible only if that message was sent by node i Thus on a sys tem NET consisting of the medium enemy and nodes the property to check would be out j i m NET in i j m STOP STOP For example a buffer process COPY in z gt out z gt COPY has out z authenticating in z for any z no message can be output unless it has previously been input This characterisation of authentication can be pro moted to sets of events The set B authenticates the set A in P if any message in B authenticates any of the messages in A In other words if any of the mes sages in B is seen then one of the messages in A must previously have occurred This is captured as follows Definition 3 4 B authenticates A in P if and only if P AUB STOP P A STOP This form mi
15. any messages that can be generated from its initial set INIT together with the messages S that have since come into its possession ADD S O add i j e ENEMY S INITUSta Observe that this description incorporates the ability of the enemy to manipulate message address fields thus giving the impression that a message comes from a source other than the genuine source If the enemy is considered to be simply an eaves dropper with no power to add messages to the medium then the ADD component would simply be modelled as STOP or omitted entirely The third option allows it to observe any message currently on the medium LEAK S leak i j gt ENEMY S U a The final option is included to model the enemy s knowledge of particular messages This is accomplished by allowing the enemy to output any message that can in fact be generated KNOWS S out 0 0 2 gt ENEMY S INITUSFa The channel out 0 is used to indicate those messages that the enemy can deduce from what has already been seen together with what was known initially The argument S represents the set of messages that the enemy has already seen Normally this will be the empty set at the beginning of a protocol run but it is possible to model the effect that possession of a partic ular key might have on the vulnerability of a protocol by including such a key or some other message in the set S Observe that we have allowed the insertion of any message in
16. authentication protocol For integrity it is assumed that the enemy is capable of generating messages from M These assumptions may be incorporated into the de scription of the enemy which may then be parame terised by a set of messages S that it has seen and a set of messages NIT that it is initially able to gener ate The assumptions can be expressed as conditions on INIT and on the set of messages M which the par ticular security property is concerned with The question also arises as to whether it is suffi cient to model enemy actions using a single ENEMY process In principle it is possible that a number of malicious agents acting together might effect an at tack where a single agent would be unable to do so Whether or not this is possible in the model being de veloped here depends on the actual description of the process ENEMY In fact the description to be pre sented enjoys the property that ENEMY ENEMY ENEMY Hence for all analysis done at the level of traces we see that any number of enemies acting together are encapsulated within the description of a single enemy In addition to the messages that can be generated from those messages already seen the enemy is able to generate particular plaintext messages Furthermore the enemy should be considered to be in possession of all of the nodes public keys and all of the users names We therefore use a set INIT to model all of the infor mation initially in th
17. components of systems They are the entities that are described using CSP and they are de scribed in terms of the possible events that they may engage in The process STOP is the process that can engage in no events at all it is equivalent to deadlock If P is a process then the process a P is only able to initially perform a following which it will behave in the way described by P The process P O Q pro nounced P choice Q can behave either as P or as Q its possible communications are those of P and those of Q An indexed form of choice O Pi is able to behave as any of its arguments P Processes may also be composed in parallel If A is a set of events then the process P A Q behaves as P and Q acting concurrently with the requirement that they have to synchronise on any event in the syn chronisation set A events not in A may be performed by either process independently of the other A special form of parallel operator in which the two components do not interact on any events is P Q which is equiv alent to P Q Processes may be recursively defined by means of equational definitions Process names must appear on the left hand side of such definitions and CSP expres sions which may include those names appear on the right hand side For example the definition LIGHT on gt off LIGHT defines a process LIGHT whose only possible e haviour is to perform on and off alternately T
18. e possession of the enemy Thus we have PUBLIC C INIT and USER C INIT The relation F gives the capability of the enemy to generate messages from messages already in its possession The CSP description of the enemy will use this relation The set S records those messages that have been read from the medium This is initialised to so ENEMY is defined to be ENEMY where ENEMY S KILIS ADD S LEAK S KNOWS S The first option allows the enemy to kill a message to remove it from the medium It is described simply as KILL S kill ENEMY S In fact when dealing with trace properties of commu nication protocols the ability of the enemy to kill mes sages is entirely irrelevant Although the possible re moval of messages from the medium can interfere with liveness properties of communications protocols it can not compromise properties expressed only in terms of traces This is because the medium allows the reorder ing of messages so any particular message could al ways be ignored and remain in the medium without being killed Any protocol that guarantees a security property if the enemy is unable to kill messages will therefore guarantee it in any case An equally useful definition of KILL S would be STOP which would be equivalent to omitting this option entirely The second course of action available to the enemy is to insert any message that it can generate onto the medium These are
19. e that best illustrates the bene fits of the process algebra approach since process alge bra would be of more use in exploring subtle patterns of interactions between different parties here the in teractions are fairly simple However it illustrates the approach Although the proof of such an obvious prop erty seems unduly long it is also lengthier than might be expected in 4 and 2 This is because a significant amount of formalisation needs to be done before the proof can actually proceed The example consists of a legitimate user who en crypts received messages with a particular key and re turns them to the medium This could be described as a legitimate node number 1 for definiteness which receives messages on rec 1 encrypts them and returns them on trans 1 The process algebra is as follows NODE rec 1 j x gt trans 1 j k lt NODE where k is a key possessed by NODE The aim is to establish that the enemy cannot obtain a particular message a that it does not already possess This is expressed as confidentiality with respect to a NET NET out 0 0 a STOP or alternatively as NET sat tr out 0 0 a We make the standard assumption for confidentiality that the enemy is not in possession of any messages containing a KERNEL a kernel INIT We may take the description of NET to consist of the node NODE the initially empty medium MEDIUM and the enemy who has initially learned not
20. es to other parties and receiving messages from other parties We will assume a universal set MESSAGE of all messages that might be sent by any party and we will consider the users to be numbered up to n USER 0 1 n The channel employed by user 7 to input messages to the network will be the input channel in i of type USER MESSAGE An input of the form in i j m is considered an instruction from user 7 to transmit mes sage m to user j on in 0 Figure 1 High level view of the network The channel employed by user 7 to receive messages output from the network will be the output channel out i of type USER MESSAGE An output of the form out i j m is considered to be receipt by user i of message m sent by user j Users requirements on the network are expressed in terms of the behaviour of the network as a whole and CSP has been used successfully for some years in the description and analysis of communications proto cols Common safety and liveness properties are read ily expressed in terms of the possible behaviour of the network with respect to the users For example the property that no spurious messages are generated is captured as a safety property that requires any output message to have previously been input if out i j m appears in a trace then in j 2 m must have already occurred The liveness requirement that no message is lost can be formalised as follows for any input mes sage in i j7 m the corresponding
21. f concur rent system components that interact through message passing It is underpinned by a theory which supports analysis of systems described in CSP It is therefore well suited to the description and analysis of network protocols protocols can be described within CSP as can the relevant aspects of the network Their interac tions can be investigated and certain aspects of their behaviour can be verified through use of the theory This section introduces the notation and ideas used in this paper In particular only the traces model for CSP is used here For a fuller introduction to the language the reader is referred to 3 Events Systems are modelled in terms of the events that they can perform The set of all possible events fixed at the beginning of the analysis is denoted Events may be atomic in structure or may consist of a number of distinct components For example an event put 5 consists of two parts a channel name put and a data value 5 An example of events used in this paper are those of the form c i j m consisting of a channel c a source 7 a destination 7 and a message m If M and N are sets of messages then M N will be the set of messages m n m EM AneN If misa single message then we elide the set brackets and define m N to be m N Thus for example the set of events i N m i n m n N A channel c is said to be of type M if any message c m X has that m M Processes Processes are the
22. for PLAINTEXT In the case we have given above these functions will be defined as follows kernel p kernelo p kernel k 4k kernel k m kernel m kernel m U kernel me u t kernelg pi U kernelg p2 kernelo u kernelo t kernelo pi pe kernel m m2 This definition contains a clause for each clause of MESSAGE reflecting the data structure in a natural way The function kernel lifts to sets in the obvious way Message properties An intruder is able to manipulate the medium in particular ways The approach taken here of using events to signal particular modes of interference in preference to having them occur nondeterministically was originally taken in 6 The advantage of this ap proach is that it allows greater control over the level and type of interference that may occur However the enemy is not capable of producing all messages for example it cannot generate a message encrypted with a key it does not have though of course it could reproduce such a message if it had previously received it In fact the messages the intruder is able to generate will depend on the messages it has already seen pass as network traffic the messages it is already able to generate and the keys it has seen or which it owns We will use an information system 5 to define which messages can be generated by the enemy It will have a trivial consistency relation any set of messages is co
23. ght be useful when we wish to check that a message is genuine even when its origina tor is unknown This could be captured as the set out 7 USER m authenticating the set in USER j m The authenticating message indicates that some honest node generated the original message The buffer process COPY has the weaker property of out M authenticating in M no output can occur before input This property is strictly weaker than the previous property in which every output authenticates a corresponding input For example a random bit gen erator which allows any bit to be output following any input bit RAND in z gt out 0 gt RAND out RAND also has out 0 1 authenticating in 0 1 no bit can be output if there wasn t previously an input but does not have out z authenticating in z for any particular z The definition provides a straightforward proof of transitivity of authentication if C authenticates B and B authenticates A then C authenticates A P AU C STOP P A STOP C STOP AU B STOP C STOP AUBUC STOP BUC STOP A STOP B A A STOP A STOP U B STOP STOP YYYY 4 The network Architecture A common architecture for which security protocols are designed consists of a network of nodes typically workstations which are able to communicate asyn chronously by sending messages to each other over a medium which acts as a postal service The need for security
24. he CSP process algebra Theorem 3 2 A process NET provides confidential ity in the sense of Definition 3 1 if and only if Vm M NET in USER 0 m STOP NET out 0 USER m STOP in USER 0 m This states that if input of message m from any user to user 0 is blocked then so is output of message m to user 0 Observe that this is not equivalent to NET in USER 0 M STOP NET out 0 USER M STOP in USER 0 M For example NET in 1 0 m1 out 0 l m1 gt in 1 2 m2 out 0 l m2 STOP meets the latter equivalence but not the former a message m2 from user 1 to user 2 has been output by user 0 and this breaches confidentiality assuming m1 m2 M This property may also be captured in the traces model as the property CONF CONF tr messages tr out 0 USER M C messages tr in USER 0 M This states that the messages from message set M output from user 0 must be a subset of those that were sent to it In other words user 0 cannot obtain any messages from M that are not sent to it The fact that this property is a sat specification means that it is preserved by refinement A simplification Observe that if no messages are ever sent to 0 perhaps if users are communicating with users they know and trust to be honest then the characterisation of con fidentiality may be simplified since no messages will ever be sent to user 0 The definition simplifies to NET sat Vm M e tr o
25. hing ENEMY It will prove useful to extract certain sets of mes sages from traces of the system LEAK tr m di je tr leak i j m O ADD tr m di je tr add i jj mF O TRANS tr m 3j etr trans k j m O REC tr m j etr rec k j m O OUTo tr m tr out 0 0 m O MESS tr LEAK tr U ADD tr U TRANS tr U REC tr U OUTo tr Lemma 4 1 The kernel function is closed under the generates relation i e B F m kernel m C kernel B Proof By considering all of the clauses that define the relation F Al A2 A3 M1 M2 K1 K2 K3 and K4 The result follows for each clause so it is true for the relation In order to prove confidentiality of NET with re spect to a we will use certain properties of its compo nents The required properties are described in the following lemma They combine information about the state of the components as maintained in and B and events that have occurred extracted from the trace A combination of information from both these sources is often required in establishing this kind of re sult State based approaches commonly include a his tory variable as a component of the state in order to record trace information The approach taken here is closer to event based approaches which provide some way of extracting the state of the system from its trace Lemma 4 2 The component processes meet the fol lowing specifications ENEMY
26. ield will be required as part of the message as well as the mes sage itself and possibly an encryption It is not clear at this stage how best to handle encrypted messages in order to maintain the possibility that the number of encryption levels may be arbitrarily large a recursive data structure will be required perhaps along the lines of MESSAGE PLAINTEXT KEY KEY MESSAGE MESSAGE MESSAGE and even plaintext messages might have some non trivial structure PLAINTEXT USER TEXT PLAINTEXT PLAINTEXT This is not the only structure appropriate for mes sages For example in a key exchange protocol keys themselves take on a dual role being used to en crypt messages but also comprising the messages to be encrypted Thus for key exchange mechanisms the set KEY should also be included as possible PLAINTEXT Other cryptographic mechanisms such as hash functions may be included as possible mes sages in which case the definition of MESSAGE might be extended with two extra lines HASH and HASH MESSAGE For the purposes of this paper we will use the definition of MESSAGE as given above while remembering that this can be varied according to modelling needs It will also prove useful when considering what an enemy may deduce about messages it has received to be able to extract the information in messages An extraction function kernel may be defined by struc tural induction on MESSAGE and kernelg defined
27. mation is not accidentally used in the protocol description the responses of a node should not be dependent on information which is available only at the high level view In some circumstances a node may not have knowledge concerning its com munication partner in other cases a protocol may be invoked only when communicating with partic ular known and trusted users how this knowledge and trust is obtained is outside the scope of this report In this report we will follow the high level view This means we can postulate the existence of an enemy whose identity is known and can be used in the for mulation of security properties We will use 0 USER as the name of this enemy process Later we will jus tify the decision to use only a single enemy by arguing that further enemies do not increase the vulnerability of protocols the single enemy in a sense encapsulates the behaviour of all enemies Confidentiality Confidentiality for a particular set of messages M is achieved when users may communicate any mes sage drawn from the set M without the possibility of any user other than the intended recipient receiving it In other words if an input in i j m occurs then any subsequent output out h l m must be for user j ie h j Thus given user j and message m if an output out j i m occurs for some 7 then some user not necessarily 1 must have sent that message to j there must be some previous input of the form in l j m Thus
28. mple as Meadows still requires a lengthy proof However part of the point of doing such a proof is to explore the relationship between the language theoretic ideas underpinning it and the invariant of the CSP recursive description It seems likely that this relationship will be similar in many proof of this type and we would hope to obtain theorems which allow results concern ing the language of messages that can be generated to be translated immediately to the CSP setting with out the need for a laborious manual translation A close relationship between CSP protocol descriptions and rules for generating messages would allow more natural proofs Once this is achieved we would expect the result that a particular set of rules cannot gener ate any message containing a to translate immediately into the result that the corresponding CSP description has the required confidentiality property Acknowledgements Thanks are due to Peter Ryan Richard Moore Irfan Zakiuddin Paul Gardiner Bill Roscoe Gavin Lowe Michael Goldsmith and Abraham Sidiropoulos for much lively discussion and perceptive comments on earlier versions of this work Thanks also to the anony mous referees for their careful reviewing of the paper and for their useful and constructive suggestions Thanks also to DRA Malvern for providing funding for this research References 1 Formal Systems Europe Ltd Failures divergences re finement user manual and tutorial 19
29. n authentication check that a particular server re mains up requires a response directly from that server rather than from the network operator responsible for it Hence in some cases it is appropriate to think of the user and the node as being the same entity However for the purposes of this paper we find it convenient to treat them as distinct All forms of interference will be modelled by an in truder process ENEMY NODE that is able to alter the condition of the medium via certain channels not available to the nodes The entire system will be de ic USER O NODE trans rec MEDIUM scribed by NET ic USER O NODE trans rec MEDIUM leak kill add ENEMY The process NET will always refer to this configura tion though it will generally be parameterised by par ticular descriptions of the node processes NODE and of the processes MEDIUM and ENEMY J t NETWORK Figure 2 Architecture of the network Messages The kind of messages that are transmitted and re ceived will depend upon the particular protocol being modelled so it is probably best at least initially to defer definition of the type of these channels until we come to model a protocol We can note that each node NODE will use channels trans i and rec i to interact with the medium so trans and rec may be thought of as denoting families of channels rather than single channels It is also likely that a destination f
30. nsistent The definition of the relation F of the in formation system will be dependent on and should en capsulate the encryption mechanism An information system defines a relation between finite sets of to kens and single tokens indicating when the token can be generated from the set In this case we will use the relationship to indicate when the enemy or indeed any other agent can generate a particular message given the messages it has already seen Consider an example in which messages may be en crypted by means of either secret keys or public keys There will be the set PUBLIC of all the nodes pub lic keys for simplicity we assume one for each node PUBLIC p i USER C KEY There will also be the set S of all the nodes secret keys one for each node SECRET s i USER C KEY This set is distinct from the set of public keys SECRET N PUBLIC Finally there will be a set of shared keys SHARED distinct both from public and secret keys SECRET N SHARED PUBLIC N SHARED The entailment relation F Pan MESSAGE x MESSAGE will be a relation between a finite set of messages that we think of as the enemy having seen and messages that the enemy can generate The re lation is closed under the axioms for an information system Al IfmeBthen BE m A2 If BE mand BC B then B Fm A3 If B F m for each m B and B F m then BFm We will abuse notation and allow the relation bet
31. otocols and for capturing secu rity properties facilitating verification and debugging It is a discussion paper proposing possible approaches rather than providing definitive answers It considers only confidentiality and authenticity here other prop erties have been considered in 7 It has been argued that security properties should be considered as properties concerning the flow of mes sages within a network To the extent that this char acterisation is justified the use of a process algebra such as CSP 3 seems appropriate to describe and anal yse them This paper considers ways in which security properties may be described using the notation of CSP how security mechanisms may be captured and how particular protocols designed to provide these proper ties may be analysed within the CSP framework The approach presented is rather general and it is clear that the modelling of particular properties and analysis of particular protocols will require tailoring of the model presented here But this paper aims at exploring a general approach rather than trying to con struct a universal model suitable for handling all pos sible security issues which is probably an unrealistic goal Security properties are generally properties requir ing that something bad should not occur though they are not exclusively of this form these tend to be con sidered as safety properties Of course particular com munication protocols will also
32. output out 7 1 m must eventually become available Generally these proper ties are expressed precisely and formally in terms of the semantic models of CSP Although it is necessary to know the internal struc ture of the network in order to demonstrate that it provides particular services the services or properties themselves should be expressible simply in terms of the interactions the network offers its users This is the case for common communications protocols and in this paper we take the view that security properties can be captured in the same way We therefore examine and offer definitions of these properties before considering the network at any finer level of detail There are two views from which security properties can be considered e from the viewpoint of the users of the network who do not know which other parties are to be trusted Properties expressed from this viewpoint will generally include assumptions implicitly or explicitly that a user s communication partner will not act contrary to the aims of the protocol For example that any shared secrets should not be disclosed to third parties e from a high level God s eye view which identi fies those nodes which follow their protocols faith fully and also identifies those which are engaging in more general activity perhaps in attempting to find a flaw in a protocol If this view is taken then care should be taken to ensure that this privileged infor
33. races The semantics of a process P is defined to be the set of sequences of events traces P that it may pos sibly perform Examples of traces include the empty trace which is possible for any process and on off on which is a possible trace of LIGHT A useful operator on traces is projection If A is a set of events then the trace tr A is defined to be the maximal subsequence of tr all of whose events are drawn from A If A is a singleton set a then we overload notation and write tr a for tr a Analysing processes Specifications are given as predicates on traces and a process P satisfies a specification S if all of its traces satisfy S P sat S amp Vtr traces P S A process P is refined by a process Q written P C Q if traces Q C traces P This means that if P meets a specification then Q will also meet it Model checking techniques allow the refinement rela tion P CE Q to be checked mechanically for finite state processes using the tool FDR 1 Since two pro cesses are equal if each refines the other this means that equality of processes can also be checked using FDR 3 Security properties A network provides a means for users such as people or applications programs to communicate by sending and receiving messages This situation may be mod elled at a high level of abstraction in CSP as a process NET which provides to each user two ways of inter acting with it sending messag
34. refined protocols does not imply that the original one is correct unless it can be demonstrated that the introduction of the tactic does not rule out any possible attacks Non repudiation seems to be a completely different kind of property Each party in a non repudiating ex change of messages is concerned that the other might not be honest Furthermore it is not enough for each party to be satisfied that the other party received the required messages each party aims to obtain evidence sufficient to convince an outside party that the ex change took place Directions Meadows example appears to be particularly straightforward which is what makes it a good ex ample for comparing different approaches because the proof rests on the fact that at no stage is the infor mation required to generate the message a ever intro duced into the system the invariant for the system is therefore fairly simple and does not rely particularly on encryption and decryption properties but simply on the property that no generation of messages by the F relation can introduce new information It will be harder to find suitable invariants for scenarios where information is present in encrypted form such as com munication between two users via a shared key where it will be necessary to prove that at no stage could it ever be decrypted More subtle properties of encryp tion and decryption will be required It seems disappointing that such a simple exa
35. sed to encapsulate properties of encryption For example if encryption were com mutative then we could include the rule K5 ki k a m H k k m Medium The description of MEDIUM involves a number of decisions about the best way to model the network medium We must allow the possibility of an intruder who is able to manipulate the medium in particular ways This could be done by building the intruder into the medium so the medium itself has the capability of in terfering with message traffic in particular ways but we prefer to follow Roscoe s approach 6 of including a separate model of the intruder This second ap proach gives greater separation between the medium itself which would then be considered as essentially a passive service provided to the various nodes and a ma licious agent who has particular capabilities to manip ulate the medium in particular ways The capabilities of this agent will be made more explicit and manipu lation of the medium will be associated with particular events which will make attacks on protocols easier to follow and understand The medium containing the set of messages B may be described initially as MEDIUM where MEDIUM B INPUT B OUTPUT B IA B The process INPUT B permits input to the medium We must decide on the type of messages that the medium will accept and offer For the purposes of this paper we will separate out the destination
36. the need for a non repudiation protocol in the first place The judge has to allow for the possibility that each node has the capabilities of node 0 Thus non repudiation has to be established in the context of nodes which can kill add and leak messages as well as interact with the medium in the usual ways The nodes for which non repudiation should be established In this case verification is from the are therefore NODE M in i j 2 gt NODE M U 2 out ilj e gt NODE M INITUMF a sean os trans i j e gt NODE M rec i j7 az gt NODE M U zx kill NODE M O wrur addliljle NODE M leak 1 j 2 gt NODE M U zx From a modelling point of view the interfaces of these processes with the network must be expanded to in clude the channels add leak and kill Since the node is able to generate its own plaintext messages the in i channel is perhaps redundant but is retained as a source of messages so that particular non repudiation protocols will refine this node The set of messages M corresponding to the initial state of the node will contain all of the keys which the node may use to encrypt and decrypt messages Meadows example In order to illustrate the above material we will present a simple example used in 4 and 2 It is not even a protocol but is instead a simple example designed purely for illustrative purposes In fact it is not the kind of exampl
37. to the medium so in particular false sources can be attached to messages Rerouting of a message can also be modelled by having the enemy read it via leak kill it this is cleaner though not essential as al ready discussed and then add the same message with a different destination field back to the medium Now the assumption that is made in the case of con fidentiality can be formalised We are assuming that none of the messages that we wish to keep confiden tial are in fact in the kernel of the messages that can initially be generated by the enemy M N kernel INIT On the other hand for integrity and authenticity we are implicitly assuming that MAINIT in the sense that protocols designed to provide these services are intended to deal with messages that can be generated by an enemy When checking a confidentiality protocol strong use is made of this assumption since if the enemy can out put a message that is supposed to be confidential then the protocol is considered to be insecure However there are situations such as key exchange where a pro tocol is designed to provide both confidentiality and authenticity in which case it is reasonable to begin analysis with M N INIT In such situations the above modelling of what the enemy knows is not ade quate and it would be necessary to construct a more sophisticated complex model of the enemy which keeps track of incoming and outgoing messages and outputs
38. ut 0 USER m which is equivalent to the simpler form NET sat tr out 0 USER M This property may be expressed entirely within the process algebra in a number of different ways The first way captures the idea that if attention is focussed en tirely upon events from out 0 USER M then nothing should be observed NET out 0 USER M STOP The process STOP is a refinement of NET x out 0 USER M since in the traces model STOP is a refinement of every process so achieving equality is equivalent to obtaining refinement in the other direc tion STOP C NET out 0 USER M An alternative characterisation is obtained by consider ing the effects of preventing NET from performing any events in out 0 USER M A system providing confi dentiality should not be affected by this restriction NET NET out 0 USER M STOP Since restricting the behaviour of NET can only reduce its behaviours it follows automatically that the restric tion is a refinement of NET Hence the processes are equivalent precisely when there is a refinement in the other direction NET out 0 USER M STOP C NET A final characterisation regards the system as accept able if every event it can perform is in the set X out 0 USER M In other words everything it can per form is also possible for a process which can always perform any of those events RUNS out 0 usER M NET All of these characterisations are provably
39. ween possibly infinite sets and messages StmesjaTcseTim We encapsulate the way in which messages can be generated by considering the possible structures for a message M1 BEmABE k gt BEk m M2 BEmABEm BE m m where m m and m are messages and k is a key Certain properties of particular encoding mecha nisms may also be captured by providing additional inference rules For example the relationship between secret and public keys may be captured by the follow ing pair of rules K1 pi si m F m K2 s pi m F m where p P and 5 E S For example these rules allow us to deduce the obvi ous result that possession of a message encrypted with a secret key s m say together with possession of the public key allows the original message to be re trieved 1 m F si m Al 2 pi si m F pi Al 3 m F pi si m MI 1 2 4 pi si m F m 3 K1 A3 The appropriate rule for shared keys is that possession of a shared key together with a message encrypted with that key allows generation of the original message K3 k k m m if k SHARED It is also possible to encode various other deductions we might wish to include in the capability of the enemy for example deducing a key from observing both an encoded message and that message in plaintext K4 m k m F k The rules that we give model different encryption and decryption capabilities of the enemy The rules can also be u
Download Pdf Manuals
Related Search
PDF pdf pdf editor pdffiller pdf to word pdf to jpg pdf merger pdf combiner pdf converter pdf editor free pdf reader pdfescape pdf to excel pdf24 pdf compressor pdf to png pdf to word converter pdf viewer pdf24 creator pdf-xchange editor pdf to jpeg pdf files pdf to excel converter pdf converter free pdf history pdf24 tools