The analysis is specified over an infinite set of values,V, that contain infinitely many terms built from encryption and blinding. However, as described above, we can encode the infinite sets of terms into tree grammars using a finite number of rules. To prepare the reader for this transformation, we will first present a short introduction to some theory of tree grammars and how this is specifically used in the analysis, before we present the finite analysis.
The following presentation of tree grammars is based on the introduction to the subject in [9] and [13].
6.3.1 Tree Grammars
A tree grammar Gis a finite structure (N,Σ, R, S), whereN is the set of non-terminals, Σ is called a signature, Ris a finite mapping of rules andS∈N is a start symbol.
The signature Σ is a finite set of function symbols each associated with a number, its arity; eg. the signature {fi, gj, . . . , hk} contains the function symbols f throughh, where f has arityi,g hasj, etc.
The terms are build by applying function symbols to other terms. Given a signature Σ and a set of terms X, we define the inductively smallest set of termsT(Σ, X) as
T(Σ, X) =X∪ {f(t1, . . . , tk)|fk∈Σ∧ ∧ki=1ti∈T(Σ, X)}
The function symbols with arity 0 are called constants, and iff is a constant the elementf() is often just written as f. A set of terms generated from an empty set of termsT(Σ,∅), that is a set generated only using constants, is called the set ofground terms. These sets can be regarded as a formal languages over terms, and as terms are often called trees, these languages are calledtree languages.
Generally the rule mapping R maps terms over non-terminals into terms over non-terminals. However, as we will only work with normalised regular tree grammars, we require thatRis a mapping from non-terminals into terms created by applying function symbols purely to non-terminals. This means that R has the functionality R:N→℘(B(Σ, N)) where the setB is as defined below.
B(Σ, X) ={f(A1, . . . , Ak)|fk ∈Σ∧ ∧ki=1Ai∈X}
Note that B(Σ, X) is a subset of T(Σ, X) and that the setX is not included in B(Σ, X). If an elementu is in R(A), the pair (A, u) is called a rule in the grammar, and we write that Ais thehead of the rule anduis thebody of the rule.
Given a (normalised regular) tree grammarG= (N,Σ, R, S) one can generate a set of ground terms starting from a non-terminalA for which there is a rule in the grammar (A, u). This set, denotedL(G, A), is defined as the smallest set satisfying
L(G, A) ={f(t1, . . . , tk)|f(A1, . . . , Ak)∈R(A)∧ ∧ki=1ti∈L(G, Ai)}
Note that alsoL(G, A) is a subset ofT(Σ,∅). Since the definition actually only needs the rule mappings, L(G, A) is sometimes just writtenL(R, A). The tree languages generated by the tree grammarG, is the set of ground terms generated by starting at the start symbol S, hence
L(G) =defL(G, S)
As a final note about tree grammars, one may recall from tree automata theory that languages generated by normalised regular tree grammars are equivalent to recognisable tree languages, which are closed under union, intersection and complementation [13].
6.3.2 Tree Grammars for the Analysis
In the analysis, the component ϑv : Lab →℘(V) uses canonical values bV alc;
ie. sets of ground terms over a signature of canonical names and encrypted and blinded values. Each of these sets constitute a tree language, and the idea is to get a finite representation of these sets by using tree grammars. This means that each setϑv(l) will be represented by a unique tree grammar (Nl,Σl, Rl, Sl), such thatϑv(l) =L((Nl,Σl, Rl, Sl), l). The components of this grammar are ex-plained below.
Non-terminals. A specific tree grammar is used to describe all possible values a specific termEl can evaluate to, and it is therefore natural to let the set of non-terminals be the set of labels;Lab.
Signature. Each term will be either a name, an encryption or a blinding.
Therefore we will regard names as constants and encryptions and blindings as k-ary function symbolssenc,aencandblirepresenting symmetric encryptions, asymmetric encryptions and blindings respectively. In order to make the signa-ture finite we will only use arities used in analysis of a processP. Hence for a
specific processP we have the signature
ΣLYSA def= {bnc0 |nis a name used inP} ∪
{senc`,Lk+1|kis the arity of a symmetric encryption annotated with`andL inP} ∪
{aenc`,Lk+1|kis the arity of a asymmetric encryption annotated with`andL inP} ∪
{bli`,Lk+1 |kis the arity of a blinding annotated with`andL inP}
Often the term bli`,Lk+1(A0, A1, . . . , Ak) will be written using the much more familiar [[A1, . . . , Ak]]`A
0[destL] and the same style of notation will be used for symmetric and asymmetric encryptions.
Rule mappings. We wantL((Lab,ΣLYSA, Rl, Sl), l) to represent the setϑv(l), therefore the rule mappings will overlap. So instead of storing the rule mappings of all labels in each grammar, we will use one common mapping component γ to store all label mappings.
Start symbol. As we wantL((Lab,ΣLYSA, Rl, Sl), l) to represent the setϑv(l) the start symbol will always bel.
All grammars will be on the form (Lab,ΣLYSA, Rl, l), which is often just referred to asRl as all other components can easily be derived from this rule mapping.
As all rule mappings are stored in one common componentγ, all grammars will often just be referred to asγ. With these changes the components of the finite analysis are as presented in Table6.5.
γ : Lab→B(ΣLYSA, Lab) Rules in the tree grammars ρf : bX c →℘(Lab) Variable environment
κf ∈ ℘(Lab∗) Network component
ψ ∈ ℘(C × C) Error component
u ∈ B(ΣLYSA, Lab) Bodies of tree grammar rules
` ∈ C Crypto-points
l ∈ Lab Labels on terms / non-terminals
Table 6.5: Components used in the finite analysis
6.3.3 The Finite Analysis
In the finite analysis we replace the evaluation of terms with the tree grammars in γ. This yields the following predicates ρf, γ |=f El and ρf, κf, ψ, γ |=f P. The finite analysis of blinding is presented in Table6.6and described in detail below.
(FBli) ρf, γ|=f [[El11,· · ·, Eklk]]`
E0l0[destL]l iff ∧ki=0ρf, γ|=f Eili∧[[l1,· · ·, lk]]`l
0[destL]∈γ(l)
(FUBli) ρf, κf, ψ, γ|=f unblindElas[[E1l1,· · ·, Ejlj;xlj+1j+1,· · ·, xlkk]]`
E0l0[origL]inP iff ρf, γ|=f El∧ ∧ji=0ρf, γ|=f Eili∧
(∀[[l10,· · ·, l0k]]`l00
0[destL0]∈γ(l) : (∧ji=0L(γ, l0i)∩EL(γ, li)6=∅)⇒
∧ki=j+1l0i∈ρf(bxic) ∧ρf, κf, ψ, γ|=f P∧ (` /∈ L0∨`0∈ L ⇒/ (`0, `)∈ψ))
∧
(∀{|lsig1 |}`sig
lsig0 [destLsig]∈γ(l) :∀[[l10,· · ·, l0k0]]`l00
0[destL0]∈γ(lsig1 ) : j= 0∧k= 1∧(L(γ, l00)∩EL(γ, l0)6=∅)⇒
{|l01,· · ·, lk00|}`lsigsig 0
[destLsig]∈γ(l1)∧ l1∈ρf(bx1c)∧ ρf, κf, ψ, γ|=f P∧
(` /∈ L0∨`0∈ L ⇒/ (`0, `)∈ψ))
Table 6.6: Step 2 - The finite analysis
The analysis of the blinding term is is rather straightforward, note however that the component ϑv is no longer part of the specification, but is implicitly represented byγ. In the analysis of unblinding the pattern matching is changed correspondingly. Two termsE1l1 and E2l2 may match if the intersection of the set of values they may evaluate to is non-empty; that isL(γ, l1)∩L(γ, l2)6=∅.
In the verbose analysis this matching is done using the membership operator
E which ignores annotations, hence we now introduce an intersection operator which ignores annotations as well. This operator is defined as follows1:
S1∩ES2={V ∈S1∪S2|V ES1∧V ES2}
In the second part of the analysis of unblinding, we need to divide the search for signed blinded LYSAterms up into two parts. First we must find all labels of
1This definition is a corrected version of the one presented in [9], where it was defined as S1∩ES2={V ∈S1∪S2|V ∈S1∧VES2}. Notice however, that the flawed version will not introduce any flaws to the analysis, as long as it is only used to check for non-emptiness.
LYSAterms which are signed, then we must find all blinded sequences (of any length) of labels for terms that belong to these labels. If the analysis finds any LYSA terms which satisfies the conditions, a new unblinded (but still signed) term is generated. This new term must be assigned to a fresh label, and the most natural choice for this label would be a label l1 for the variable x1. Therefore we extend the syntax of the unblinding process by adding labels to the variables being bound as well. This yields the following new syntax
P ::= . . . |unblindEl as[[E1l1,· · ·, Ejlj;xlj+1j+1,· · · , xlkk]]`El0 0
[origL]inP We also extend the analysis to ensure thatρf(bx1c) holds this label.