One of the most significant security risk is the one that comes when attacks is launched by insiders. These attacks are particularly hard to withstand because insiders are awarded certain credentials that may be used in an attack. In order to discuss insider attacks it is convenient to distinguish betweenlegitimate princi-pals that will not launch attacks andillegitimateprincipals that may do so. Any communication with an illegitimate principal may, of course, be compromised in an attack. The interesting point is therefore whether illegitimate principals can also compromise the security of communication between legitimate principals.
7.4.1 Legitimate Principals
As illustrated in many of the previous examples, principals can be modelled by using the indexed parallel composition. In the examples seen so far, these principals only behave as they are suppose to and thereby model legitimate principals. Furthermore, the restriction operator has been used to model that the credentials of these legitimate principals, such as keys and nonces, are initially protected from attackers.
Below is an example of how one of the most classical security protocols, namely Needham and Schroeder’s public key protocol [104], can be encoded in a scenario consisting of legitimate principals, only.
Example 7.12The encoding of Needham and Schroeder’s public key protocol below models a scenario where principalsAiinitiates a session with all principals Bj. For simplicity the protocol is given without the server that distributes public keys. Instead, all principals are initially assumed to know the public keysKA+i andKB+j of all the principals.
The first replicated process LySa encoding below models the role of the initiator Ai initiating a session with Bj while the second replicated process models Bj
responding to a session initiated byAi. Notice that the scope of the restriction
of the keys spans all the principals. Technically, this means that the public and private keys of all the principals might have been used anywhere within this scope. However, inspecting the process below it is clear that the keys are only used as intended. The restrictions, on the other hand, ensure to none of the keys are available outsiders. authentication for the final message of Needham-Schroeder public key protocol is ensured in a scenario consisting of legitimate principals, only.
7.4.2 Illegitimate Principals
Many of the applications that are used in modern distributed systems may, however, also be used by principals that are not necessarily trustworthy. For example, an application used within some company may need to deal out cre-dentials to the employees. However, in a large cooperation it is implausible that all employees are trusted will all of the companies secrets. Another example is applications used for secure communication on the internet. Just because cre-dentials need to be handed out to provide secure communication between two principals, it does not mean that every principal should have access to all the secure communication that takes place.
To account for these situations it will be necessary to consider a setup that also models illegitimate principals. That is, one must consider a setup such as
P |Pil
where P represents the legitimate principals andPil represents the illegitimate principals. All these principals may communicate with each other and share credentials. However, Pil may behave in all sorts of strange ways and try to launch attacks onP. Hence, the point of interest is to track what happens when P is under attack from anarbitrary processes,Pil, which acts as the illegitimate principals.
It has already been discussed how to analyse the behaviour of arbitrary processes.
This is done by introducing a hardest attacker,Phard, and perform the analysis ρ, κ|=P |Phard
The very same technique can be used when analysing setups that include illegiti-mate principals. Here, the analysis ofPhardwill correspond to the the behaviour of all arbitrary processesPil, which act as illegitimate principals.
In summary, to analyse a setup consisting of legitimate and illegitimate princi-pals, one only needs to supply the processP that models the legitimate princi-pals. It is, however, important to stress thatP must include any communication with the illegitimate principals. On the other hand, the illegitimate principals, Pil, will not need to be modelled explicitly because the analysis ofPhardaccounts for their behaviour.
To complete the model of the setup, one must ensure that the credentials ofPil, such as keys and certificates, are known to Phard. This can, for example, be done by lettingP send the credentials in clear on the network. Alternatively, the credentials can be put as free names inside P, because all free names are initially known byPhard.
The above discussion has taken place using the object level syntax and analy-sis of LySa. It can, however, readily be lifted to the meta level analyanaly-sis, the authentication analysis, etc.
Example 7.13Consider the scenario from Example 7.12. To model both legit-imate and illegitlegit-imate principals, the set of principalsAi andBi withi∈Zwill be partitioned into two sets. The legitimate principals will have an indexi∈Z+ while the illegitimate principals take their indexi∈Z−0.
The legitimate part of the system can then be modelled as the scenario be-low. It describes how the legitimate principals Ai and Bj with i, j ∈ Z+ can communicate withall other principals:
The last two lines in the scenario ensures that all the credentials of the illegiti-mate principals are known to the attacker. Note in particular that the private keysKA−i andKB−i withi∈Z−0 ofAi andBi, respectively, are given to the at-tacker. All these credentials enables the attacker to act as illegitimate principals that may attack the legitimate part of the protocol.
When the protocol is analysed in the above scenario with bZ−
0c = {0} and bZ+c={1} the analysis is no longer able to guarantee destination and origin
authentication. Instead, it reports
ψ={(a10, c•),(c•, b01),(c•, b11)}
as possible violation of the authentication property.
The model of illegitimate principals in Example 7.13 lets the attacker play the role of the illegitimate principals. Whenever a legitimate principal communi-cates with one of these illegitimate principals it will, therefore, be communicat-ing directly with the attacker. Recall that the attacker is annotated with the crypto-point c•. However, in Example 7.13 the messages sent to the illegiti-mate principals, i.e. to the attacker, have annotations with crypto-points of the form aij and bij. Consequently, the authentication property may be violated due to the fact that these annotations do not comply with the way illegitimate principals are modelled.
To rectify the situation, annotations in a principal that communicates with an illegitimate principal will have the crypto-point c• added to all annotations in messages meant for an illegitimate principal. These crypto-points are added systematically by ensuring that dest and orig annotations have c• added every time the meta level analysis unfolds an indexed parallel where the canonical index represents an illegitimate principal.
Example 7.14 (Continued from Example 7.13) The analysis from Exam-ple 7.13 has bZ−0c={0} as the canonical index for the illegitimate principals.
Whenc• is added to the annotations where the analysis uses the index 0, some of the violation in Example 7.13 disappear. However, the analysis is still not able to guarantee authentication because of the following possible violation of the authentication property:
ψ={(c•, b11)}
This violation does, in fact, correspond to the attack found by Lowe [85] where an illegitimate principal (at c•) can successfully spoof messages to a legitimate responder (atbijfori, j∈Z+), instead of the message that was suppose to come
from another legitimate principal.
Hereby, it has been illustrated that the analysis techniques suffice to deal with open systems that contains arbitrarily many illegitimate principals.