Most networking applications will be deployed in scenarios where several copies or sessions of the applications can run in parallel. Sometimes messages from one session may be used to launch an attack on another session running in parallel.
These attacks are known in the literature, e.g. [44], as parallel session attacks.
To illustrate the problem, assume that the scenario consists of a number of parallel sessions:
P1|. . .|Pp|. . .|Pq |. . .|Pk
Here eachPi represents a session where, for example, the two principalsA3 and B5are engaged in communication over the network.
Interference between sessions occur when something from one session, say Pp, interferes with something from another session, say Pq. This interference can take place directly because some part of session Pp communicates with some part of session Pq, or indirectly because an attacker redirects something from sessionPp to sessionPq.
Interference between sessions is not always a problem because the application may contain safeguards that filters out undesirable effects of session interference.
However,
aparallel session attackoccurs whenever interference between session causes a security property to be violated.
To figure out whether an arbitrary security property is violated as a result of interference between two sessions is, in general, a difficult problem cf. [60, 4, 62, 28]. However, if the nature of the security property is such that it directly mentions sessions then it need not be hard to track whether a parallel session attack occur. For example, in LySa sessions can be modelled such that an index, i, on a value denotes that the value comes from theith session. In this setup, an authentication property such as
[atcidest{c0i}]
explicitly states that the encryption point ci and the decryption point c0i are both expected to be within the same session,i. Violations of the above property that involves other session, i.e. crypto-points with other indices than i, will by definition be a parallel session attack.
The following sections will elaborate on this idea and discuss how parallel sessions can be modelled using the meta level of LySa in such a way that indices indicate, which session a process belongs to. Next, it is shown how the the analysis can be used to guarantee the absence of arbitrary parallel session attacks on the authentication property whenever session are modelled in this special way.
7.3.1 A Scenario for Parallel Sessions
To begin with, only a simple model of parallel sessions is discussed. More general scenarios will be considered in Section 7.3.3. The simple model assumes that a session of an application can be modelled by the meta level processM in such a way that the indexed parallel composition
|i∈S M
describes the scenario of parallel sessions. That is, M in itself describes one session but is parameterised by the indexi. The meta level process then describes a scenario of all the parallel sessions and these sessions are distinguished only by the indices i taken from the set S. To see this, assume that M V P and letS be some set{a1, . . . , p, . . . , q, . . . , ak}. The scenario of parallel sessions as described by|i∈S M then instantiates to
P[i7→a1]|. . .|P[i7→p]|. . .|P[i7→q]|. . . P[i7→ak]
as well as subprocesses with fewer parallel composites. In the following thejth process in this parallel composition will be referred to as sessionPj.
Next consider the authentication annotations of the processM. Whenever these annotations are of the form
[atcidest{c0i}] or [atc0iorig{ci}]
they specify an intra session property. That is, they require that destination and origin must be within the same session, which is represented by index i.
Now,
aparallel session attack occurs if an intra session property is violated by decryption of a value from another session.
For example, letPp be an arbitrary session containing an intra session property of the form [atcporig{c0p}]. If a valueVq, from some other sessionPq, is success-fully decrypted in atcp then the authentication property will be violated. This happens because crypto-points in the annotations ofVq cannot have the indexp since this index is only available inside session Pp. Note that this violation will by definition be a parallel session attack.
7.3.2 Analysing Parallel Sessions
The analysis can be used to guarantee the absence of violations of intra session properties between two arbitrary sessions Pp andPq described by a meta level process of the form |i∈S M. This is done simply by choosing the canonical assignment of indices for the indexing setS such thatbpc 6=bqc.
Corollary 7.8 states that the analysis reports a non-empty ψ for any seman-tic violation up to the assignment of canonical crypto-points. Recall that the assignment of canonical crypto-points respects the assignment of canonical in-dices. Because the analysis is performed with bpc 6= bqc, any violation of an intra session property due to decryption inPp of a value fromPq, or vice versa, is reported by the analysis. More precisely, when the analysis reports errors of the form
(bc0qc,bcpc)∈ψ or (bcpc,bc0qc)∈ψ
it signifies possible parallel session attacks occurring between sessions Pp and Pq. Conversely, if the authentication analysis holds with an empty ψ then it guarantees that there are no violations of intra session properties due to inter-ference between sessionPpandPq. That is, there are no parallel session attacks between these two session.
Thus, the analysis can be used to guarantee absence of parallel session attacks for two arbitrary, but fixed, parallel session Pp and Pq where p, q ∈ S of a scenario described by |i∈S M. In fact, it suffices to conduct the analysis only once on |i∈S M with bSc fixed such thatbpc 6=bqcto account for all parallel session attacks caused by violations of intra session properties in this scenario.
This follows from the fact that the analysis only distinguishes elements up to canonicity as discussed below.
Consider the scenario |i∈S M and let S ={a1, . . . , ai, . . . , p, . . . , aj, . . . , q, . . .}.
Then fix the canonical assignmentbScsuch thatbpc=pandbqc=q(and that
p6=q). It is now obvious that the analysis result found under this assignment of canonical indices will be identical to anyisomorphic assignment of canonical indices to the set S. For example, an isomorphic assignment that hasbaic=p and bajc = q for some i and j will give the exact same analysis result. This happens because the analysis only considers canonical values, which in particular is coined by Lemma 6.6, which concerns the assignment of canonical indices.
In summary, the analysis is capable guaranteeing the absence of parallel session attacks between two given sessions described by the scenario|i∈S M. Because the analysis gives the same result for any isomorphic assignments of canonical indices, this analysis result will guarantee the absence of arbitrary parallel session attacks between any two session instantiated overS.
Example 7.10Below is an encoding of the pure nonce handshake in a scenario where all principalsAi and Bi share the same keyK. The indexing parallel is used the describe parallel sessions where principalAimakes a nonce handshake with principalBi:
letX ⊆Nin(ν K)
|i∈X (ν ni)hAi, Bi, nii.(Bi, Ai; xi).decryptxi as{ni;}K[ataiorig{bi}]in 0
| (Ai, Bi;yi).hBi, Ai,{yi}K[atbidest{ai}]i.0
In this scenario the index i on names, variables, or crypto-points signifies that they belong to the ith session. TakingbNc={1,2} the implementation of the analysis finds that
ψ={(b1, a2),(b2, a1)}
Thus, the analysis reports possibleparallel session attacks because the differing indices in the pairs signify that something encrypted in sessionPp withbpc= 1 may wrongfully be decrypted in another sessionPq withbqc= 2 and vice versa.
To see that there really is a violation of the property one must find an execution that leads to the above violation of the authentication property. This can be attempted for any two session taking their indexes fromN. Below it is done for the two indices 1 and 2. Consider the following message exchange:
A1 A2 B2 Attacker
1.1 hA1, B1, n1i (;zA1, zB1, zn1).
2.1 hA2, B2, n2i (;zA2, zB2, zn2).
2.10 (A2, B2;y2) hzA2, zB2,zn1i.
2.2 hB2, A2,{y2}K[atb2dest{a2}]i (zB2, zA2;ze).
1.2 (B1, A1;x1) hzB1, zA1, zei.0
After the last message exchangex1 has become bound to the value ofzei.e. to {n1}K[atb2 dest{a2}]. The following successful decryption and pattern match can then take place
decrypt{n1}K[atb2dest{a2}]as{n1;}K[ata1orig{b1}]in 0→0
This decryption violates the authentication property and it represents a par-allel session attack because something encrypted at principal B2 is wrongfully decrypted at principalA1. With the assignment of canonical indices that takes b1c= 1 andb2c= 2 this accounts for the error (b2, a1) inψ. With the isomorphic assignment of canonical indicesb1c= 2 andb2c= 1 it furthermore accounts for
the error (b1, a2) inψ.
7.3.3 Generalising the Scenario
The above treatment only considers meta level processes where one indexed parallel is used to describe parallel sessions. The development can easily be extended to allow definitions of parallel sessions with multiple indexed parallel compositions.
In general, a session must be characterised by a number of indices, which are defined by indexing parallel compositions. An intra session property will be any authentication property that by the indices on crypto-points specifies that des-tination and origin must come from the same session. Whenever the analysis is carried out it is paramount that the canonical indexing set for each of these in-dices contains at least two distinct canonical elements. In that case, the analysis will be able to distinguish any two arbitrarily chosen parallel sessions.
Example 7.11Consider again the nonce handshake but this time in a scenario where each principal Ai may communicate with all principals Bj. This will be modelled using two nested indexed parallel compositions. A session is now characterised by being indexed with indexij:
letX ⊆Nin let Y ⊆Nin(ν K)
|i∈X|j∈Y (ν nij)hAi, Bj, niji.(Bj, Ai;xij).
decryptxij as{nij;}K[ataijorig{bij}]in 0
| |j∈Y |i∈X (Ai, Bj;yij).hBj, Ai,{yij}K[atbijdest{aij}]i.0
The authentication properties in the process above are intra session properties because indices ij are the same for the at part, and the orig and dest part, respectively. Notice that this model of the scenario is very similar to the one for the message passing nonce-handshake in Example 6.1.
TakingbNc={1,2}the analysis holds whenever
ψ⊇ {(b11, a21),(b11, a12),(b11, a22),(b12, a11),(b12, a21),(b12, a22), (b21, a11),(b21, a12),(b21, a22),(b22, a11),(b22, a21),(b22, a12)}
Because the indices in all the pairs of crypto-point are pairwise distinct these error messages represent possible parallel session attacks on sessions whereApis trying to communicate toBq. For example, takingbpc= 2 andbqc= 1 the first error, (b11, a21), represents interference in a session betweenAp andBq from a session betweenAq andBq.
The protocol can be modified such that each sessionij uses its own shared key Kij. For a version of the process that has been modified in this way, the analysis holds forψ=∅ and thereby it guarantees absence of parallel attacks.
In conclusion, the meta level analysis can be used to analyse parallel sessions and to guarantee the absence of parallel session attacks on the destination and origin authentication property. The approach is restricted to consider parallel sessions attacks in processes where sessions are modelled using the indexed par-allel construct. This style of modelling can, in the view of the author, be quite natural as illustrated, for example, in Section 7.5.