# Relationships between the Phase Retrieval Problem and Permutation Invariant
Embeddings

Radu Balan and Efstratos Tsoukanis
Department of Mathematics, University of Maryland, College Park, MD 20742
Emails<EMAIL_ADDRESS><EMAIL_ADDRESS>
(March 31, 2023)

###### Abstract

This paper discusses the connection between the phase retrieval problem and
permutation invariant embeddings. We show that the real phase retrieval
problem for $\displaystyle\mathbb{R}^{d}/O(1)$ is equivalent to Euclidean
embeddings of the quotient space $\displaystyle\mathbb{R}^{2\times d}/S_{2}$
performed by the sorting encoder introduced in an earlier work. In addition,
this relationship provides us with inversion algorithms of the orbits induced
by the group of permutation matrices.

##  I Introduction

The phase retrieval problem has a long and illustrious history involving
several Nobel prizes along the way. The issue of reconstruction from magnitude
of frame coefficients is related to a significant number of problems that
appear in separate areas of science and engineering. Here is an incomplete
list of some of these applications and reference papers: crystallography [1,
2, 3]; ptychography [4, 5]; source separation and inverse problems [6, 7];
optical data processing [8]; mutually unbiased bases [9, 10], quantum state
tomography [11, 12]; low-rank matrix completion problem [13, 14]; tensor
algebra and systems of multivariate polynomial equations [15, 16, 17]; signal
generating models [18, 19], bandlimited functions [20, 21], radar ambiguity
problem [22, 23], learning and scattering networks [24, 25, 26].

In [27], this problem was shown to be a special form of the following setup.
Let $\displaystyle H$ denote a real or complex vector space and let
$\displaystyle A=\\{a_{i}\\}_{i\in I}$ be a frame for $\displaystyle H$. The
phase retrieval problem asks whether the map $\displaystyle H\ni
x\mapsto\alpha_{A}(x)=\\{|{\operatorname{\langle}x,a_{i}\operatorname{\rangle}}|\\}_{i\ni
I}\in l^{2}(I)$ determines $\displaystyle x$ uniquely up to a unimodular
scalar.

In this paper we focus on the finite dimensional real case of this problem
(see also [28]), namely when $\displaystyle H=\mathbb{R}^{d}$. In this case, a
frame $\displaystyle\mathcal{A}=\\{a_{1},\ldots,a_{D}\\}\subset\mathbb{R}^{d}$
is simply a spanning set. The group $\displaystyle O(1)=\\{-1,+1\\}$ acts on
$\displaystyle H$ by scalar multiplication. Let $\displaystyle\hat{H}=H/O(1)$
denote the quotient space induced by this action, where the equivalence
classes (orbits) are

$\displaystyle[x]=\\{x,-x\\}~{}~{},~{}~{}{\text{for}}~{}x\neq
0~{}~{},~{}~{}[x]=\\{0\\}~{}~{},~{}~{}\text{for}~{}x=0.$

The analysis operator for this frame is

$T_{A}:H\rightarrow\mathbb{R}^{D}~{}~{},~{}~{}T_{A}(x)=({\operatorname{\langle}x,a_{k}\operatorname{\rangle}})_{k=1}^{D}.$
(1)

The relevant nonlinear map $\displaystyle\alpha_{A}$ is given by taking the
absolute value of entries of $\displaystyle T_{A}$:

$\alpha_{A}:H\rightarrow\mathbb{R}^{D}~{}~{},~{}~{}\alpha_{A}(x)=(|{\operatorname{\langle}x,a_{k}\operatorname{\rangle}}|)_{k=1}^{D}.$
(2)

Notice $\displaystyle\alpha_{A}$ produces a well-defined map on
$\displaystyle\hat{H}$, which, with a slight abuse, but for simplicity of
notation, will be denoted also by $\displaystyle\alpha_{A}$. Thus
$\displaystyle\alpha_{A}([x])=\alpha_{A}(x)$.

Another customary notation that is often employed: a frame is given either as
an indexed set of vectors,
$\displaystyle\mathcal{A}=\\{a_{1},\ldots,a_{D}\\}$, or through the columns of
a $\displaystyle d\times D$ matrix $\displaystyle A$. The matrix notation is
not canonical, but this is not an issue here. We always identify
$\displaystyle H=\mathbb{R}^{d}$ with its columns vector representation in its
canonical basis.

######  Definition 1.

We say that (the columns of a matrix) $\displaystyle A\in\mathbb{R}^{d\times
D}$ form/is a phase retrievable frame, if
$\displaystyle\alpha_{A}:\widehat{\mathbb{R}}^{d}\to\mathbb{R}^{D}$,
$\displaystyle\alpha_{A}(x)=(|{\operatorname{\langle}x,a_{k}\operatorname{\rangle}}|)_{k=1}^{D}$
is an injective map (on the quotient space).

In a different line of works [29, 30, 31, 32] it was recognized that the phase
retrieval problem is a special case of Euclidean representations of metric
spaces of orbits defined by certain unitary group actions on Hilbert spaces.
Specifically, the setup is as follows. Let $\displaystyle V$ denote a Hilbert
space, and let $\displaystyle G$ be a group acting unitarily on $\displaystyle
V$. Let $\displaystyle\hat{V}=V/G$ denote the metric space of orbits, where
the quotient space is induced by the equivalence relation $\displaystyle
x,y\in V$, $\displaystyle x\sim y$ iff $\displaystyle y=g.x$, for some
$\displaystyle g\in G$. Here $\displaystyle g.x$ represents the action of the
group element $\displaystyle g\in G$ on vector $\displaystyle x$. For the
purposes of this paper we specialize to the finite dimensional real case,
$\displaystyle V=\mathbb{R}^{n\times d}$ and $\displaystyle G=S_{n}$, is the
group of $\displaystyle n\times n$ permutation matrices acting on
$\displaystyle V$ by left multiplication. Other cases are discussed in
aforementioned papers. In particular, in [30] the authors have shown a deep
connection to graph deep learning problems. In [31], the authors linked this
framework to certain graph matching problems and more. The bi-Lipschitz
Euclidean embedding problem for the finite dimensional case is as follows.
Given $\displaystyle\hat{V}=V/G$, construct a map
$\displaystyle\beta:V\rightarrow\mathbb{R}^{m}$ so that, (i)
$\displaystyle\beta(g.x)=\beta(x)$ for all $\displaystyle g\in G$,
$\displaystyle x\in V$, and (ii) for some $\displaystyle 0<A\leq B<\infty$,
and for all $\displaystyle x,y\in V$,

$A\,\operatorname{{\mathbf{d}}}([x],[y])\leq{\|\beta(x)-\beta(y)\|}\leq
B\,\operatorname{{\mathbf{d}}}([x],[y])$ (3)

where $\displaystyle\operatorname{{\mathbf{d}}}([x],[y])=\inf_{g\in
G}{\|x-g.y\|}_{V}$ is the natural metric on the quotient space
$\displaystyle\hat{V}$.

In [30] the following embedding was introduced. Let $\displaystyle
A\in\mathbb{R}^{d\times D}$ be a fixed matrix (termed as key) whose columns
are denoted by $\displaystyle a_{1},\ldots,a_{D}$. The induced encoder
$\displaystyle\beta_{A}:V\rightarrow\mathbb{R}^{n\times D}$ is defined by

$\beta_{A}(X)=\downarrow(XA)=\left[\begin{array}[]{ccc}\Pi_{1}Xa_{1}&\cdots&\Pi_{D}Xa_{D}\end{array}\right]$
(4)

where $\displaystyle\Pi_{k}\in S_{n}$ is the permutation matrix that sorts in
decreasing order the vector $\displaystyle Xa_{k}$. It was shown in [30] that,
for $\displaystyle D$ large enough, $\displaystyle\beta_{A}$ provides a bi-
Lipschitz Euclidean embedding of $\displaystyle\hat{V}$. This motivates the
following definition.

######  Definition 2.

We say that $\displaystyle A\in\mathbb{R}^{d\times D}$ is a universal key for
$\displaystyle\mathbb{R}^{n\times d}$ if
$\displaystyle\beta_{A}:\widehat{\mathbb{R}^{n\times
d}}\rightarrow\mathbb{R}^{n\times D}$,
$\displaystyle\beta_{A}(X)\\!=\downarrow\\!(XA)$ is an injective map (on the
quotient space).

The purpose of this paper is to show the equivalence between the real phase
retrieval problem, specifically the embedding $\displaystyle\alpha_{A}$, and
the permutation invariant embedding $\displaystyle\beta_{A}$ defined above, in
the special case $\displaystyle n=2$.

##  II Main Results

Recall the Hilbert spaces $\displaystyle H=\mathbb{R}^{d}$ and $\displaystyle
V=\mathbb{R}^{2\times d}$. For $\displaystyle A\in\mathbb{R}^{d\times D}$
recall also the encoders
$\displaystyle\alpha_{A}:\hat{H}\rightarrow\mathbb{R}^{D}$ and
$\displaystyle\beta_{A}:\hat{V}\to\mathbb{R}^{2\times D}$ given respectively
by
$\displaystyle\alpha_{A}(x)=(|{\operatorname{\langle}x,a_{k}\operatorname{\rangle}}|)_{k\in[D]}$,
and $\displaystyle\beta_{A}(X)\\!=\downarrow\\!(XA)$. Our main result reads as
follows.

######  Theorem 3.

In the case $\displaystyle n=2$, the following are equivalent.

  1. 1.

$\displaystyle\alpha_{A}$ is injective, hence the columns of $\displaystyle A$
form a phase retrievable frame;

  2. 2.

$\displaystyle\beta_{A}$ is injective, hence $\displaystyle A$ is a universal
key.

######  Remark 4.

Perhaps it is not surprising that, if an equivalence between the phase
retrieval problem and permutation invariant representations is possible, then
this should occur for $\displaystyle n=2$. This statement is suggested by the
observation that $\displaystyle O(1)$ is isomorphic with $\displaystyle
S_{2}$, the group of the $\displaystyle 2\times 2$ permutation matrices. What
is surprising that, in fact, the two embeddings are intimately related, as the
proof and corollaries show.

###### Proof of Theorem 3.

Let $\displaystyle X\in V=\mathbb{R}^{2\times d}$. Denote by $\displaystyle
x_{1},x_{2}\in\mathbb{R}^{d}$ its two rows transposed, that is

$\displaystyle X=\left[\begin{array}[]{c}x_{1}^{T}\\\
x_{2}^{T}\end{array}\right].$

Notice that, for each $\displaystyle k\in[D]$, the $\displaystyle k^{th}$
column of $\displaystyle\beta_{A}(X)$ is given by

$\displaystyle\displaystyle\downarrow(Xa_{k})=\begin{bmatrix}max({\operatorname{\langle}x_{1},a_{k}\operatorname{\rangle}},{\operatorname{\langle}x_{2},a_{k}\operatorname{\rangle}})\\\
min({\operatorname{\langle}x_{1},a_{k}\operatorname{\rangle}},{\operatorname{\langle}x_{2},a_{k}\operatorname{\rangle}})\end{bmatrix}.$

The key observations are the following relationships between $\displaystyle
min$, $\displaystyle max$, and the absolute value $\displaystyle|\cdot|$:

$\displaystyle\displaystyle|u-v|$ $\displaystyle\displaystyle=$
$\displaystyle\displaystyle max(u,v)-min(u,v)$ $\displaystyle\displaystyle
u+v$ $\displaystyle\displaystyle=$ $\displaystyle\displaystyle
max(u,v)+min(u,v)$ $\displaystyle\displaystyle max(u,v)$
$\displaystyle\displaystyle=$
$\displaystyle\displaystyle\frac{1}{2}(u+v+|u-v|)$ $\displaystyle\displaystyle
min(u,v)$ $\displaystyle\displaystyle=$
$\displaystyle\displaystyle\frac{1}{2}(u+v-|u-v|)$
$\displaystyle\displaystyle|\,|u|-|v|\,|$ $\displaystyle\displaystyle=$
$\displaystyle\displaystyle min(|u-v|,|u+v|)$

In particular, these show that:

$\displaystyle\displaystyle\begin{bmatrix}1&-1\\\
1&1\end{bmatrix}\beta_{A}(X)=\begin{bmatrix}1&-1\\\
1&1\end{bmatrix}\cdot\downarrow(XA)=$
$\displaystyle\displaystyle=\begin{bmatrix}|{\operatorname{\langle}x_{1}-x_{2},a_{1}\operatorname{\rangle}}|,&\dots&,|{\operatorname{\langle}x_{1}-x2,a_{D}\operatorname{\rangle}}|\\\
{\operatorname{\langle}x_{1}+x_{2},a_{1}\operatorname{\rangle}},&\dots&,{\operatorname{\langle}x_{1}-x_{2},a_{D}\operatorname{\rangle}}\end{bmatrix}$
$\displaystyle\displaystyle=\begin{bmatrix}(\alpha_{A}(x_{1}-x_{2}))^{T}\\\
(T_{A}(x_{1}+x_{2}))^{T}\end{bmatrix}$

Where, $\displaystyle T_{A}$ was introduced in equation (1).

$\displaystyle(1)\to(2):$ Suppose that $\displaystyle\alpha_{A}$ is injective.
Let $\displaystyle X=\begin{bmatrix}x_{1}^{T}\\\ x_{2}^{T}\end{bmatrix}$ and
$\displaystyle Y=\begin{bmatrix}y_{1}^{T}\\\ y_{2}^{T}\end{bmatrix}$, such
that $\displaystyle\beta_{A}(X)=\beta_{A}(Y)$. Then

$\displaystyle\displaystyle\begin{bmatrix}1&-1\\\
1&1\end{bmatrix}\beta_{A}(X)=\begin{bmatrix}1&-1\\\
1&1\end{bmatrix}\beta_{A}(Y)$ $\displaystyle\displaystyle\implies$
$\displaystyle\displaystyle\begin{bmatrix}(\alpha_{A}(x_{1}-x_{2}))^{T}\\\
T_{A}(x_{1}+x_{2})^{T}\end{bmatrix}=\begin{bmatrix}(\alpha_{A}(y_{1}-y_{2}))^{T}\\\
T_{A}(y_{1}+y_{2})^{T}\end{bmatrix}.$

But now,
$\displaystyle\alpha_{A}(x_{1}-x_{2})=\alpha_{A}(y_{1}-y_{2}))\implies
x_{1}-x_{2}=y_{1}-y_{2}\text{ or }x_{1}-x_{2}=y_{2}-y_{1}$ and

$\displaystyle T_{A}(x_{1}+x_{2})=T_{A}(y_{1}+y_{2})^{T}\implies
x_{1}+x_{2}=y_{1}+y_{2}$

Thus we have that

$\displaystyle\left\\{\begin{array}[]{rcl}x_{1}&=&y_{1}\\\
x_{2}&=&y_{2}\end{array}\right\\}\text{ or
}\left\\{\begin{array}[]{rcl}x_{1}&=&y_{2}\\\
x_{2}&=&y_{1}\end{array}\right\\}$

Either case means

$\displaystyle\displaystyle\iff X=Y\text{ or }X=\begin{bmatrix}0&1\\\
1&0\end{bmatrix}Y$ $\displaystyle\displaystyle\iff[X]=[Y]$

So, $\displaystyle\beta_{A}$ is injective.

$\displaystyle(2)\to(1):$ Suppose that $\displaystyle\beta_{A}$ is injective.
Let $\displaystyle x,y\in\mathbb{R}^{d}$ such that
$\displaystyle\alpha_{A}(x)=\alpha_{A}(y)$, i.e.
$\displaystyle|{\operatorname{\langle}x,a_{k}\operatorname{\rangle}}|=|{\operatorname{\langle}y,a_{k}\operatorname{\rangle}}|$,
$\displaystyle\forall k\in[D]$. Let $\displaystyle X=\begin{bmatrix}x^{T}\\\
-x^{T}\end{bmatrix}$ and $\displaystyle Y=\begin{bmatrix}y^{T}\\\
-y^{T}\end{bmatrix}$. Then,

$\displaystyle\begin{bmatrix}1&-1\\\
1&1\end{bmatrix}\beta_{A}(X)=\begin{bmatrix}\alpha_{A}(2x)^{T}\\\
T_{A}(0)^{T}\end{bmatrix}=2\begin{bmatrix}\alpha_{A}(2x)^{T}\\\
0\end{bmatrix}$

and

$\displaystyle\begin{bmatrix}1&-1\\\
1&1\end{bmatrix}\beta_{A}(X)=\begin{bmatrix}\alpha_{A}(2y)^{T}\\\
T_{A}(0)^{T}\end{bmatrix}=2\begin{bmatrix}\alpha_{A}(2y)^{T}\\\
0\end{bmatrix}$

Thus $\displaystyle\beta_{A}(X)=\beta_{A}(Y)$. Since $\displaystyle\beta_{A}$
is assumed injective, it follows that $\displaystyle X=Y$ or $\displaystyle
X=\begin{bmatrix}0&1\\\ 1&0\end{bmatrix}Y$. So, $\displaystyle x=y$ or
$\displaystyle x=-y$. We conclude that $\displaystyle[x]=[y]$, so
$\displaystyle\alpha_{A}$ is injective.

∎

######  Corollary 5.

If $\displaystyle\beta_{A}$ is injective, then $\displaystyle D\geq 2d-1$.

######  Corollary 6.

If $\displaystyle D=2d-1$, then $\displaystyle\beta_{A}$ is injective if and
only if $\displaystyle A$ is a full spark frame.

Both results follow necessary and sufficient conditions established in, e.g.
[27]. Recall that a frame in $\displaystyle\mathbb{R}^{d}$ is said full spark
if any subset of $\displaystyle d$ vectors is linearly independent (hence
basis).

######  Remark 7.

Assume $\displaystyle D=2d-1$. Note the embedding dimension for
$\displaystyle\hat{V}=\widehat{\mathbb{R}^{2\times d}}$ is $\displaystyle
m=2(2d-1)=4d-2=2\,dim(V)-2$. In particular this shows the minimal dimension of
bi-Lipschitz Euclidean embeddings may be smaller than twice the intrinsic
dimension of the Hilbert space where the group acts on. Both papers [30] and
[31] present (bi)Lipschitz embeddings into
$\displaystyle\mathbb{R}^{2\,dim(V)}$.

######  Remark 8.

As was derived in the proof, $\displaystyle\alpha_{A}$,
$\displaystyle\beta_{A}$ and $\displaystyle T_{A}$ are intimately related:

$\beta_{A}\left(\left[\begin{array}[]{c}x_{1}^{T}\\\
x_{2}^{T}\end{array}\right]\right)=\frac{1}{2}\left[\begin{array}[]{cc}1&1\\\
-1&1\end{array}\right]~{}\left[\begin{array}[]{c}\alpha_{A}(x_{1}-x_{2})^{T}\\\
T_{A}(x_{1}+x_{2})^{T}\end{array}\right]$ (5)

In particular, any algorithm for solving the phase retrieval problem solves
also the inversion problem for $\displaystyle\beta_{A}$. Let
$\displaystyle\omega_{A}:\mathbb{R}^{D}\rightarrow\mathbb{R}^{d}$ denote a
left inverse of $\displaystyle\alpha_{A}$ on the metric space
$\displaystyle\widehat{\mathbb{R}^{d}}$. This means
$\displaystyle\omega_{A}(\alpha_{A}(x))\sim x$ in
$\displaystyle\mathbb{R}^{d}/O(1)$. Denote by $\displaystyle
T_{A}^{{\dagger}}$ a left inverse of the analysis operator (e.g., the
synthesis operator associated to the canonical dual frame). Thus
$\displaystyle T_{A}^{{\dagger}}T_{A}=I_{d}$. Then an inverse for
$\displaystyle\beta_{A}$ is:

$\beta_{A}^{-1}(Y)=\frac{1}{2}\left[\begin{array}[]{c}T_{A}^{\dagger}(y_{2})+\omega_{A}(y_{1})\\\
T_{A}^{\dagger}(y_{2})-\omega_{A}(y_{1})\end{array}\right]$ (6)

where $\displaystyle Y=\left[\begin{array}[]{c}y_{1}^{T}\\\
y_{2}^{T}\end{array}\right]$.

######  Remark 9.

Equations (6) suggest a lower dimensional embedding than
$\displaystyle\beta_{A}$. Specifically, first we compute the average
$\displaystyle y_{1}=\frac{1}{2}(x_{1}+x_{2})$ which is of size
$\displaystyle\mathbb{R}^{d}$, and then encode the difference $\displaystyle
x_{1}-x_{2}$ using $\displaystyle\alpha_{A}$, $\displaystyle
y_{2}=\alpha_{A}(x_{1}-x_{2})$. We obtain the following modified encoder,
$\displaystyle\tilde{\beta}_{A}:\mathbb{R}^{2\times
d}\rightarrow\mathbb{R}^{d+D}$:

$\tilde{\beta}_{A}(x)=\left[\begin{array}[]{cc}\frac{1}{2}(x_{1}+x_{2})^{T}&\alpha_{A}(x_{1}-x_{2})^{T}\end{array}\right].$
(7)

With the $\displaystyle\omega_{A}$ left inverse of $\displaystyle\alpha_{A}$,
the inverse of $\displaystyle\tilde{\beta}_{A}$ is given by:

$\tilde{\beta}_{A}^{-1}(Y)=\left[\begin{array}[]{c}y_{1}+\frac{1}{2}\omega_{A}(y_{2})\\\
y_{1}-\frac{1}{2}\omega_{A}(y_{2})\end{array}\right]$ (8)

where $\displaystyle y_{1}=Y(1:d)$ and $\displaystyle y_{2}=Y(d+1:d+D)$. In
the case when $\displaystyle D=D_{min}=2d-1$, the minimal embedding dimension
is $\displaystyle m=d+D=3d-1$ (instead of $\displaystyle 4d-2$ or
$\displaystyle 4d=2\,dim(V)$).

Reference [30] shows that an upper Lipschitz bound for embedding
$\displaystyle\beta_{A}$ is $\displaystyle\sigma_{1}(A)$, where
$\displaystyle\sigma_{1}(A)$ is the largest singular value of $\displaystyle
A$. Same reference shows that if $\displaystyle\beta_{A}$ is injective then
there is also a strictly positive lower Lipschitz bound without providing a
formula. Using Equation 5 we provide explicit estimates of these bounds.

######  Theorem 10.

Assume $\displaystyle A\in\mathbb{R}^{d\times D}$ is a universal key for
$\displaystyle\mathbb{R}^{2\times d}$ (i.e.,
$\displaystyle\beta_{A}:\widehat{\mathbb{R}^{2\times
d}}\rightarrow\mathbb{R}^{2\times D}$ is injective), or, equivalently
(according to Theorem 3), the columns of $\displaystyle A$ form a phase
retrievable frame in $\displaystyle\mathbb{R}^{d}$ (i.e.,
$\displaystyle\alpha_{A}:\widehat{\mathbb{R}^{d}}\to\mathbb{R}^{D}$ is
injective). Then both $\displaystyle\alpha_{A}$ and $\displaystyle\beta_{A}$
are bi-Lipschitz with same Lipschitz constants, where distances are given by
$\displaystyle\operatorname{{\mathbf{d}_{PR}}}([x],[y])=\min({\|x-y\|},{\|x+y\|})$
on $\displaystyle\hat{H}$, and
$\displaystyle\operatorname{{\mathbf{d}}}([X],[Y])=\min_{P\in
S_{2}}{\|X-PY\|}$ on $\displaystyle\hat{V}$, respectively. The optimal upper
and lower Lipschitz constants are given by:

$A_{0}=\min_{I\subset[D]}\sqrt{\sigma_{d}^{2}(A[I])+\sigma_{d}^{2}(A[I^{c}])}~{}~{},~{}~{}B_{0}=\sigma_{1}(A)$
(9)

where $\displaystyle\sigma_{1}(A)$ is the largest singular value of
$\displaystyle A$ (equals the square-root of upper frame bound) and
$\displaystyle\sigma_{d}(A[J])$ is the $\displaystyle d^{th}$ singular value
of submatrix of $\displaystyle A$ indexed by $\displaystyle J$. Furthermore,
these bounds are achieved by the following vectors. Let $\displaystyle I_{0}$
denote a optimal partition in (9) and let $\displaystyle u_{1}$,
$\displaystyle u_{2}$ denote the normalized left singular vectors of
$\displaystyle A[I_{0}]$ and $\displaystyle A[I_{0}^{c}]$, respectively, each
associated to the $\displaystyle d^{th}$ singular value. Let $\displaystyle u$
be the normalized principal left singular vector associated to $\displaystyle
A$ (i.e., associated to the largest singular value). Then:

  1. 1.

The upper Lipschitz constant $\displaystyle B_{0}$ is achieved as follows: (i)
for map $\displaystyle\alpha_{A}$ by vectors $\displaystyle x_{\max}=u$ and
$\displaystyle y_{\max}=0$; (ii) for map $\displaystyle\beta_{A}$ by vectors
$\displaystyle X_{\max}=\left[\begin{array}[]{c}u^{T}\\\ 0\end{array}\right]$
and $\displaystyle Y_{\max}=0$.

  2. 2.

The lower Lipschitz constant $\displaystyle A_{0}$ is achieved as follows: (i)
for map $\displaystyle\alpha_{A}$ by vectors $\displaystyle
x_{\min}=u_{1}+u_{2}$ and $\displaystyle y_{\min}=u_{1}-u_{2}$; (ii) for map
$\displaystyle\beta_{A}$ by vectors $\displaystyle
X_{\min}=\left[\begin{array}[]{c}(u_{1}+u_{2})^{T}\\\ 0\end{array}\right]$ and
$\displaystyle Y_{\min}=\left[\begin{array}[]{c}u_{1}^{T}\\\
u_{2}^{T}\end{array}\right]$.

######  Remark 11.

The optimal Lipschitz constants for the map $\displaystyle\alpha_{A}$ were
obtained in [33, 34], including the optimizers. However, for reader’s
convenience, we prefer to give direct proofs of these results.

###### Proof.

  1. 1.

Upper Lipschitz constants.

(i) Let $\displaystyle x,y\in\mathbb{R}^{d}$. Then

$\displaystyle\displaystyle\scriptstyle{\|\alpha_{A}(x)-\alpha_{A}(y)\|}^{2}=\sum_{i=1}^{D}||{\operatorname{\langle}a_{i},x\operatorname{\rangle}}|-|{\operatorname{\langle}a_{i},y\operatorname{\rangle}}||^{2}=$
$\displaystyle\displaystyle=\scriptstyle\sum_{i=1}^{D}\min\left(|{\operatorname{\langle}a_{i},x-y\operatorname{\rangle}}|^{2},|{\operatorname{\langle}a_{i},x+y\operatorname{\rangle}}|^{2}\right)\leq$
$\displaystyle\displaystyle\scriptstyle\leq\min\left(\sum_{i=1}^{D}|{\operatorname{\langle}a_{i},x-y\operatorname{\rangle}}|^{2},\sum_{i=1}^{D}|{\operatorname{\langle}a_{i},x+y\operatorname{\rangle}}|^{2}\right)$
$\displaystyle\displaystyle\scriptstyle\leq\sigma_{1}^{2}(A)\operatorname{{\mathbf{d}_{PR}}}([x],[y])^{2}.$

So $\displaystyle\sigma_{1}(A)$ is an upper Lipschitz bound for the map
$\displaystyle\alpha_{A}$. Now for $\displaystyle x_{\max}=u,y_{\max}=0$
notice that

$\displaystyle\displaystyle\scriptstyle{\|\alpha(x_{\max})-\alpha(y_{\max})\|}^{2}=\sum_{i=1}^{D}|{\operatorname{\langle}a_{i},u\operatorname{\rangle}}|^{2}=$
$\displaystyle\displaystyle\scriptstyle=\sigma_{1}^{2}(A){\|u\|}^{2}=\sigma_{1}^{2}(A)\operatorname{{\mathbf{d}_{PR}}}([x_{\max}],[y_{\max}])^{2}.$

Thus, the upper Lipschitz constant $\displaystyle\sigma_{1}(A)$ is in fact
optimal (tight).

(ii) Map $\displaystyle\beta_{A}$. Let $\displaystyle
X,Y\in\mathbb{R}^{2\times D}$ and $\displaystyle P_{0}\in S_{2}$ be a
permutation that achieves the distance between $\displaystyle X$ and
$\displaystyle Y$, i.e.
$\displaystyle{\|X-P_{0}Y\|}=\operatorname{{\mathbf{d}}}([X],[Y])$. Note that

$\displaystyle\displaystyle\scriptstyle{\|\beta_{A}(X)-\beta_{A}(Y)\|}^{2}=\sum_{k=1}^{D}{\|(\Pi_{k}X-\Xi_{k}Y)a_{k}\|}^{2}=$
$\displaystyle\displaystyle\scriptstyle=\sum_{k=1}^{D}{\|(\Xi_{k}^{T}\Pi_{k}X-Y)a_{k}\|}^{2}$

for some $\displaystyle\Pi_{k},\Xi_{k}\in S_{2}$ that align the vectors. From
rearrangement lemma we have that

$\displaystyle\scriptstyle{\|(\Pi_{k}X-\Xi_{k}Y)a_{k}\|}\leq{\|(X-P_{0}Y)a_{k}\|},~{}\forall
k\in[D]$

so,

$\displaystyle\displaystyle\scriptstyle\sum_{k=1}^{D}{\|(\Xi_{k}^{T}\Pi_{k}X-Y)a_{k}\|}^{2}\leq$
$\displaystyle\displaystyle{\|A\|}^{2}{\|{\|X-P_{0}Y\|}\|}^{2}$
$\displaystyle\displaystyle=$
$\displaystyle\displaystyle\scriptstyle\sigma_{1}^{2}(A)\operatorname{{\mathbf{d}}}([X],[Y])^{2}.$

Therefore, we conclude that $\displaystyle\sigma_{1}(A)$ is an upper Lipschitz
constant for map $\displaystyle\beta_{A}$. We still need to show that this
bound is achieved (i.e., it is optimal). For $\displaystyle X_{\max}$ and
$\displaystyle Y_{\max}$ defined in part 1) of 10,

$\displaystyle\displaystyle\scriptstyle{\|\beta_{A}(X_{\max})-\beta_{A}(Y_{\max})\|}^{2}={\|\beta_{A}(X_{\max})\|}^{2}=\sum_{k=1}^{D}{\operatorname{\langle}u,a_{k}\operatorname{\rangle}}^{2}=\sigma_{1}^{2}(A).$

and $\displaystyle\operatorname{{\mathbf{d}}}(X_{\max},Y_{\max})=1$. Thus
$\displaystyle B_{0}$ is the optimal Lipschitz constant both for
$\displaystyle\alpha_{A}$ and for $\displaystyle\beta_{A}$.

  2. 2.

Lower Lipschitz constants.

(i) Let $\displaystyle x,y\in\mathbb{R}^{d}$ and define the auxiliary set

$\displaystyle\scriptstyle
S=S(x,y):=\\{j\in[D]~{}:|~{}{\operatorname{\langle}x-y,a_{j}\operatorname{\rangle}}|\leq|{\operatorname{\langle}x+y,a_{j}\operatorname{\rangle}}|\\}$

Then

$\displaystyle\displaystyle\scriptstyle{\|\alpha(x)-\alpha(y)\|}^{2}=\sum_{i=1}^{D}\left||{\operatorname{\langle}a_{i},x\operatorname{\rangle}}|-|{\operatorname{\langle}a_{i},y\operatorname{\rangle}}|\right|^{2}=$
$\displaystyle\displaystyle=\scriptstyle\sum_{i\in
S}|{\operatorname{\langle}a_{i},x-y\operatorname{\rangle}}|^{2}+\sum_{i\in
S^{c}}|{\operatorname{\langle}a_{i},x+y\operatorname{\rangle}}|^{2}\geq$
$\displaystyle\displaystyle\scriptstyle\sigma_{d}^{2}(A[S])+\sigma_{d}^{2}(A[S^{c}])\operatorname{{\mathbf{d}_{PR}}}([x],[y])^{2}\geq
A_{0}^{2}\operatorname{{\mathbf{d}_{PR}}}([x],[y])^{2}.$

So $\displaystyle A_{0}$ is a lower Lipschitz bound for
$\displaystyle\alpha_{A}$, but we still need to show that it is optimal.

Let $\displaystyle I_{0}$ be the optimal partition, and let $\displaystyle
u_{1}$, $\displaystyle u_{2}$ be normalized left singular vectors as in the
statement of 10. Then:

$\displaystyle\displaystyle\scriptstyle{\|\alpha_{A}(u_{1}+u_{2})-\alpha_{A}(u_{1}-u_{2})\|}^{2}=$
$\displaystyle\displaystyle\scriptstyle=\sum_{i=1}^{D}||{\operatorname{\langle}a_{i},u_{1}+u_{2}\operatorname{\rangle}}|-|{\operatorname{\langle}a_{i},u_{1}-u_{2}\operatorname{\rangle}}||^{2}=$
$\displaystyle\displaystyle=\scriptstyle\sum_{i=1}^{D}\min\left(|{\operatorname{\langle}a_{i},2u_{2}\operatorname{\rangle}}|^{2},|{\operatorname{\langle}a_{i},2u_{1}\operatorname{\rangle}}|^{2}\right)\leq$
$\displaystyle\displaystyle\scriptstyle\leq 4\,\left(\sum_{i\in
I_{0}}|{\operatorname{\langle}a_{i},u_{1}\operatorname{\rangle}}|^{2}+\sum_{i\in
I_{0}^{c}}|{\operatorname{\langle}a_{i},u_{2}\operatorname{\rangle}}|^{2}\right)$
$\displaystyle\displaystyle\scriptstyle=4(\sigma_{d}^{2}(A[I_{0}])+\sigma_{d}^{2}(A[I_{0}^{c}]))=A_{0}^{2}\operatorname{{\mathbf{d}_{PR}}}([u_{1}+u_{2}],[u_{1}-u_{2}])^{2},$

where we used again that $\displaystyle|\,|a|-|b|\,|=min(|a-b|,|a+b|)$ for any
two real numbers $\displaystyle a,b\in\mathbb{R}$, and, for the inequality, at
every $\displaystyle i\in[D]$ we made a choice between the two terms. Since
the reverse inequality is also true, it follows that $\displaystyle
x_{\min}=u_{1}+u_{2}$ and $\displaystyle y_{\min}=u_{1}-u_{2}$ achieve the
lower bound $\displaystyle A_{0}$ for $\displaystyle\alpha_{A}$.

(ii) Consider now the map $\displaystyle\beta_{A}$. Let $\displaystyle
X,Y\in\mathbb{R}^{2\times d}$ and define the auxiliary set

$\displaystyle\displaystyle\scriptstyle S=S(X,Y):=\\{$
$\displaystyle\displaystyle\scriptstyle
j\in[D]~{}:|~{}{\operatorname{\langle}x_{1}-x_{2}-y_{1}+y_{2},a_{j}\operatorname{\rangle}}|\leq$
$\displaystyle\displaystyle\scriptstyle\leq|{\operatorname{\langle}x_{1}-x_{2}+y_{1}-y_{2},a_{j}\operatorname{\rangle}}|\\}$

Then, using Equation 5 we have that

$\displaystyle\scriptstyle{\|\beta_{A}(X)-\beta_{A}(Y)\|}^{2}=$
$\displaystyle\scriptstyle\frac{1}{2}\left({\|\alpha_{A}(x_{1}-x_{2})-\alpha_{A}(y_{1}-y_{2})\|}^{2}+{\|T_{A}(x_{1}+x_{2}-y_{1}-y_{2})\|}^{2}\right)=$
$\displaystyle\scriptstyle\frac{1}{2}\sum_{j\in
S}|{\operatorname{\langle}x_{1}-x_{2}-y_{1}+y_{2},a_{j}\operatorname{\rangle}}|^{2}+|{\operatorname{\langle}x_{1}+x_{2}-y_{1}-y_{2},a_{j}\operatorname{\rangle}}|^{2}+$
$\displaystyle\scriptstyle+\frac{1}{2}\sum_{j\in
S^{c}}|{\operatorname{\langle}x_{1}-x_{2}+y_{1}-y_{2},a_{j}\operatorname{\rangle}}|^{2}+|{\operatorname{\langle}x_{1}+x_{2}-y_{1}-y_{2},a_{j}\operatorname{\rangle}}|^{2}=$
$\displaystyle\scriptstyle=\sum_{j\in
S}|{\operatorname{\langle}x_{1}-y_{1},a_{j}\operatorname{\rangle}}|^{2}+|{\operatorname{\langle}x_{2}-y_{2},a_{j}\operatorname{\rangle}}|^{2}+$
$\displaystyle\scriptstyle+\sum_{j\in
S^{c}}|{\operatorname{\langle}x_{1}-y_{2},a_{j}\operatorname{\rangle}}|^{2}+|{\operatorname{\langle}x_{2}-y_{1},a_{j}\operatorname{\rangle}}|^{2}\geq$
$\displaystyle\scriptstyle\geq\sigma_{d}^{2}(A[S])\left({\|x_{1}-y_{1}\|}^{2}+{\|x_{2}-y_{2}\|}^{2}\right)+$
$\displaystyle\scriptstyle+\sigma_{d}^{2}(A[S^{c}])\left({\|x_{1}-y_{2}\|}^{2}+{\|x_{2}-y_{1}\|}^{2}\right)\geq$
$\displaystyle\scriptstyle\geq
A_{0}^{2}\operatorname{{\mathbf{d}}}([X],[Y])^{2}.$

Therefore $\displaystyle A_{0}$ is a lower Lipschitz constant for
$\displaystyle\beta_{A}$.

It remained to prove that this bound is tight, i.e., it is achieved. Let
$\displaystyle X_{\min}$ and $\displaystyle Y_{\min}$ be as in the statement
of 10. Then

$\displaystyle\scriptstyle{\|\beta_{A}(X_{\min})-\beta_{A}(Y_{\min})\|}^{2}=$
$\displaystyle\scriptstyle\frac{1}{2}\left({\|\alpha_{A}(u_{1}+u_{2})-\alpha_{A}(u_{1}-u_{2})\|}^{2}+{\|T_{A}(u_{1}+u_{2}-u_{1}-u_{2})\|}^{2}\right)=$
$\displaystyle\scriptstyle\frac{1}{2}\left({\|\alpha_{A}(u_{1}+u_{2})-\alpha_{A}(u_{1}-u_{2})\|}^{2}\right)=A_{0}^{2}\operatorname{{\mathbf{d}}}([X_{\min}],[Y_{\min}])^{2}$

where the last equality follows from the fact that the lower Lipschitz
constant of $\displaystyle\alpha_{A}$ is achieved by $\displaystyle
u_{1}+u_{2}$ and $\displaystyle u_{1}-u_{2}$, and the fact that
$\displaystyle\operatorname{{\mathbf{d}}}([X_{\min}],[Y_{\min}])^{2}=2$.

So $\displaystyle A_{0}$ is indeed the optimal lower Lipschitz constant for
$\displaystyle\beta_{A}$.

∎

##  III Conclusion

In this paper we analyzed two representation problems, one arising in the
phase retrieval problem and the other one in the context of permutation
invariant representations. We showed that the real phase retrieval problem in
a finite dimensional vector space $\displaystyle H$ is entirely equivalent to
the permutation invariant representations for the space $\displaystyle
V=\mathbb{R}^{2\times dim(H)}$. Our analysis proved that phase retrievability
is equivalent to the universal key property in the case of encoding
$\displaystyle{2\times d}$ matrices. This result is derived based on the
lattice space structure $\displaystyle(\mathbb{R},+,min,max)$. It is still an
open problem to understand the relationship between $\displaystyle\alpha_{A}$
and $\displaystyle\beta_{A}$ in the case $\displaystyle n>2$. A related
problem is the implementation of the sorting operator using a neural network
that has ReLU as activation function (or, even the absolute value
$\displaystyle|\cdot|$). Efficient implementations of such operator may yield
novel relationships between $\displaystyle\alpha_{A}$ and
$\displaystyle\beta_{A}$, in the case $\displaystyle n\geq 3$.

## Acknowledgment

The authors have been supported in part by a NSF award under grant DMS-2108900
and by the Simons Foundation.

## References

  * [1] N. Kasai, M. Kakudo, and Kasai-Kakudo…, _X-ray Diffraction by Macromolecules_. Springer, 2005, vol. 80.
  * [2] R. W. Gerchberg, “A practical algorithm for the determination of plane from image and diffraction pictures,” _Optik_ , vol. 35, no. 2, pp. 237–246, 1972\.
  * [3] J. R. Fienup, “Phase retrieval algorithms: a comparison,” _Applied optics_ , vol. 21, no. 15, pp. 2758–2769, 1982.
  * [4] G. Zheng, _Fourier ptychographic imaging: A MATLAB® tutorial_. Morgan & Claypool Publishers, 2016.
  * [5] N. Sissouno, F. Boßmann, F. Filbir, M. Iwen, M. Kahnt, R. Saab, C. Schroer, and W. zu Castell, “A direct solver for the phase retrieval problem in ptychographic imaging,” _Mathematics and Computers in Simulation_ , vol. 176, pp. 292–300, 2020.
  * [6] A. Oppenheim, J. Lim, G. Kopec, and S. Pohlig, “Phase in speech and pictures,” in _ICASSP’79. IEEE International Conference on Acoustics, Speech, and Signal Processing_ , vol. 4. IEEE, 1979, pp. 632–637.
  * [7] R. Balan, “On signal reconstruction from its spectrogram,” in _2010 44th Annual Conference on Information Sciences and Systems (CISS)_. IEEE, 2010, pp. 1–4.
  * [8] P. J. Winzer, “Modulation and multiplexing in optical communications,” in _Conference on Lasers and Electro-Optics_. Optica Publishing Group, 2009, p. CTuL3.
  * [9] P. Delsarte, J.-M. Goethals, and J. J. Seidel, “Spherical codes and designs,” in _Geometry and Combinatorics_. Elsevier, 1991, pp. 68–93.
  * [10] R. Balan, B. G. Bodmann, P. G. Casazza, and D. Edidin, “Painless reconstruction from magnitudes of frame coefficients,” _Journal of Fourier Analysis and Applications_ , vol. 15, no. 4, pp. 488–501, 2009.
  * [11] T. Heinosaari, L. Mazzarella, and M. M. Wolf, “Quantum tomography under prior information,” _Communications in Mathematical Physics_ , vol. 318, no. 2, pp. 355–374, 2013.
  * [12] M. Kech and M. M. Wolf, “Quantum tomography of semi-algebraic sets with constrained measurements. preprint,” _ArXiv_ , vol. 1507, 2015.
  * [13] E. J. Candes, T. Strohmer, and V. Voroninski, “Phaselift: Exact and stable signal recovery from magnitude measurements via convex programming,” _Communications on Pure and Applied Mathematics_ , vol. 66, no. 8, pp. 1241–1274, 2013.
  * [14] E. J. Candes, Y. C. Eldar, T. Strohmer, and V. Voroninski, “Phase retrieval via matrix completion,” _SIAM review_ , vol. 57, no. 2, pp. 225–251, 2015\.
  * [15] X. Li and V. Voroninski, “Sparse signal recovery from quadratic measurements via convex programming,” _SIAM Journal on Mathematical Analysis_ , vol. 45, no. 5, pp. 3019–3033, 2013.
  * [16] E. J. Candès and X. Li, “Solving quadratic equations via phaselift when there are about as many equations as unknowns,” _Foundations of Computational Mathematics_ , vol. 14, pp. 1017–1026, 2014.
  * [17] A. Conca, D. Edidin, M. Hering, and C. Vinzant, “An algebraic characterization of injectivity in phase retrieval,” _Applied and Computational Harmonic Analysis_ , vol. 38, no. 2, pp. 346–356, 2015.
  * [18] S. Shamma, “Analysis of speech dynamics in the auditory system,” _Dynamics of Speech Production and Perception: Life and Behavioural Sciences_ , pp. 335–342, 2006.
  * [19] J. Li, Y. Xie, P. Stoica, X. Zheng, and J. Ward, “Beampattern synthesis via a matrix approach for signal power estimation,” _IEEE Transactions on Signal Processing_ , vol. 55, no. 12, pp. 5643–5657, 2007.
  * [20] G. S. Thakur, “Reconstruction of bandlimited functions from unsigned samples,” _Journal of Fourier Analysis and Applications_ , vol. 17, pp. 720–732, 2010.
  * [21] Y. Chen, C. Cheng, Q. Sun, and H. Wang, “Phase retrieval of real-valued signals in a shift-invariant space,” _Applied and Computational Harmonic Analysis_ , vol. 49, no. 1, pp. 56–73, 2020.
  * [22] P. Jaming, “Phase retrieval techniques for radar ambiguity problems,” _Journal of Fourier Analysis and Applications_ , vol. 5, pp. 309–329, 1999\.
  * [23] ——, “Uniqueness results for the phase retrieval problem of fractional fourier transforms of variable order,” _arXiv preprint arXiv:1009.3418_ , 2010.
  * [24] S. Mallat, “Group invariant scattering,” _Communications on Pure and Applied Mathematics_ , vol. 65, no. 10, pp. 1331–1398, 2012.
  * [25] J. Bruna and S. Mallat, “Invariant scattering convolution networks,” _IEEE transactions on pattern analysis and machine intelligence_ , vol. 35, no. 8, pp. 1872–1886, 2013.
  * [26] S. Bahmani and J. Romberg, “Phase retrieval meets statistical learning theory: A flexible convex relaxation,” in _Artificial Intelligence and Statistics_. PMLR, 2017, pp. 252–260.
  * [27] R. Balan, P. Casazza, and D. Edidin, “On signal reconstruction without noisy phase,” _Appl.Comput.Harmon.Anal._ , vol. 20, pp. 345–356, 2006.
  * [28] A.S. Bandeira, J. Cahill, D. Mixon, A.A. Nelson, “Saving phase: Injectivity and stability for phase retrieval,” _Appl. Comp. Harm. Anal._ , vol. 37, no. 1, pp. 106–125, 2014.
  * [29] A. H. J. Cahill, A. Contreras, “Complete set of translation invariant measurements with lipschitz bounds,” _Appl. Comput. Harm. Anal._ , vol. 49, no. 2, pp. 521–539, 2020.
  * [30] R. Balan, N. Haghani, and M. Singh, “Permutation invariant representations with applications to graph deep learning,” 2022.
  * [31] J. Cahill, J. W. Iverson, D. G. Mixon, and D. Packer, “Group-invariant max filtering,” _arXiv:2205.14039 [cs.IT]_ , pp. 1–35, 2022.
  * [32] N. Dym and S. J. Gortler, “Low dimensional invariant embeddings for universal geometric learning,” _arXiv:2205.02956 [cs.LG]_ , pp. 1–23, 2022.
  * [33] R. Balan and Y. Wang, “Invertibility and robustness of phaseless reconstruction,” _Applied and Comput. Harmon. Analysis_ , vol. 38, no. 3, pp. 469–488, 2015.
  * [34] R. Balan and D. Zou, “On lipschitz analysis and lipschitz synthesis for the phase retrieval problem,” _Linear Algebra and Applications_ , vol. 496, pp. 152–181, 2016.


Security is a subject of increasing attention in our actual society in order to protect critical resources from information disclosure, theft or damage. The informal model of attack trees introduced by Schneier, and widespread in the industry, is advocated in the 2008 NATO report to govern the evaluation of the threat in risk analysis. Attack-defense trees have since been the subject of many theoretical works addressing different formal approaches.

In 2017, M. Audinot et al. introduced a path semantics over a transition system for attack trees. Inspired by the latter, we propose a two-player  interpretation of the attack-tree formalism. To do so, we replace transition systems by concurrent game arenas and our associated semantics consist of strategies. We then show that the emptiness problem, known to be -complete for the path semantics, is now -complete. Additionally, we show that the membership problem is -complete for our two-player interpretation while it collapses to in the path semantics.

§ INTRODUCTION

Security is a subject of increasing attention in our actual society in
order to protect critical resources from information disclosure, theft
or damage. The informal model of attack trees was first introduced by
Schneier [15] to schematically model possible
threats one could execute against an information system. Attack trees
have then been widespread in the industry and are advocated in the 2008
NATO report to govern the evaluation of the threat in risk
analysis. The attack tree model is also a subject of increasing attention in the
community of formal methods with a lot of different formal
approaches <cit.> (see the survey [16]).

The first formal model of attack trees introduced
in [15] aimed at describing a possible attack
over a system by refining the main attack goal into sub-goals using
either an operator $OR$ or an operator $AND$ to coordinate those
refinements. The analysis conducted over those trees is "static" in
the sense that the attacked system does not evolve during the
attack. As such, there is no concept of a goal happening before or
after another. In [6], the authors introduce a first
formal semantics that can be qualified as "dynamic" by allowing a new
operator, operator $SAND$ (for sequential $AND$), to specify that
sub-goals must be attained in a given order. Considering that the $SAND$
operator is now commonly accepted, the authors of [1] propose a
path semantics for attack trees over a transition system.

In this paper, our goal is to present a new semantics for attack trees
in order to be able to model more realistic scenarios: we want our
attacker to be able to adapt her actions according to the behavior of
the environment – typically, a defender who tries to protect the
system. This setting naturally yields a two-player semantics. Our
approach is inspired by [1] where we generalize the
path semantics to a game-theoretic framework, yielding a strategy
semantics for attack trees, without changing their syntax.

While the path semantics from [1] is compositional in
a natural way, it turns out that the strategy semantics does not have
such a nice property. Indeed, although composition of strategies is
possible (see for example [11]), there is no
immediate solution to compose two strategies in order to get a
strategy that achieves the disjunction of what the formers
achieve. This situation makes it difficult to design a compositional strategy semantics for attack trees. We therefore develop a non-trivial strategy semantics
that is not compositionally obtained per se, but that makes use of the
former compositional path semantics.

To our knowledge, our proposal is the first game-theoretic semantics
for attack trees, and should not be mixed-up with the multi-player
setting induced by the so-called classic model of attack-defense
trees in the literature (see [9]): attack-defense
trees are attack trees equipped with a new operator to express that
some defender could use a countermeasure to prevent attacker from
achieving her goal. Although well-understood in a "static" framework,
we are not aware of any formal semantics of attack-defense trees for
the “dynamic” one, over transition systems. This missing piece
of work makes it difficult to conduct a comparison with our
contribution, but, from the fact that the defender in our setting is fully
formalized, as an opponent in the game arena, while the defender in
attack-defense trees takes the form of an abstract entity, it seems that those two formalisms are not expressing the same kind of problems.

Our contribution in this paper is twofold.

We first develop a clean mathematical setting to obtain a formal
strategy semantics for attack trees. For pedagogical reasons, we
choose to consider a simplified version of the attack trees
of [1] where atomic goals (at the leaves of the
trees) are reachability goals with no preconditions. However, at
the price of tedious definitions, the strategy semantics we propose
can be adapted to atomic goals with preconditions. Regarding the
design of this semantics, we heavily rely on the older one
of [1] based on paths, and we justify our approach by
providing evidence that a compositional strategy semantics is

Second, we exploit the attack tree semantics to address and study the
complexity of two decision problems: the non-emptiness problem
and the membership problem. The former consists in determining
if the semantics of an input tree is non-empty, while the latter
consists in determining if an input element belongs to the semantics of
an input tree. Our results are summarized in <Ref>,
where we distinguish between the path semantics and the strategy

Complexity results

1c|     Paths semantics     Strategy semantics

Non-Emptiness Problem     -complete     -complete

Membership Problem         -complete

Importantly, both decision problems have a practical counterpart. The
non-emptiness of the path semantics of a tree reflects a situation
where there exists a favorable scenario for attacker to perform her
attack, while the non-emptiness of the strategy semantics reflects an
intrinsic vulnerability of an information system. Regarding the
membership problem for the path semantics, we are interested in
knowing whether a log file of some information system execution makes
evidence of an attack, while for the strategy semantics, we wonder if
an attack policy is successful.

The paper is organized as follows. We start in <Ref>
with an introductory example explaining informally the difference
between path semantics and strategy semantics. After some background work in <Ref>, we
introduce in <Ref> the formal model of attack trees
and define the path semantics inspired by [1] as well
as our new strategy semantics. We then study the complexity of the
Non-Emptiness and the Membership problems
in <Ref>.

§ INTRODUCTORY EXAMPLE

Consider a thief (the attacker) who wants to steal some document inside a safe of a building without being seen. The building is composed of two rooms. The first room has two entrance doors (called door 1 and door 2) from the street. There is a guard keeping the entrance doors, but he can only control the bypassing of one of the two entrance doors at a time. The first room has also another door that leads to the second room. This door is locked but the key to unlock it is in the first room.  There is also a camera in the first room monitoring the door to the second room. The second room contains a safe with the document that the thief wants to steal. Therefore, in order for the thief to attain his goal, he needs to enter the first room (by either door that is not currently controlled by the guard), then deactivate the camera and collect the key (in whichever order he wants) and finally unlock and go through the door leading to the second room. The thief can be seen by the guard if they appen to be in front of the same door or by the camera if activated when he is in front of the door to room 2. Figure <ref> gives a picture of the situation where the thief is still outside of the building and the guard controls the second door.

[Building plan]

[Graph representation of the possibles positions of the thief and the guard at the entrance of the building.]

[state] (q)   $(o,m)$;
[state] (q0)  [above=of q] $(o,d_1)$;
[state] (q1) [below=of q] $(o,d_2)$;
[state] (q2) [right=of q0] $(d_2,d_1)$;
[state] (q3) [right =of q1] $(d_2,d_2)$;
[state] (q4) [right=of q] $(d_2,m)$;
[state] (q2') [left=of q0] $(d_1,d_1)$;
[state] (q3') [left =of q1] $(d_1,d_2)$;
[state] (q4') [left=of q] $(d_1,m)$;
(blu) at (8,4.8) $\{\propdtwo\}$;
(blu) at (8,0) $\{\propdtwo\}$;
(blu) at (8.4,-4.8) $\{\propdtwo,$ $\}$;
(blu) at (-8.4,-4.8) $\{\propdone\}$;
(blu) at (-8.4,0) $\{\propdone\}$;
(blu) at (-8.4,4.8) $\{\propdone,$ $\}$;

(q) edge node  (q1)
edge node  (q0)
edge node  (q2)
edge node  (q3)
edge node  (q2')
edge node  (q3')
(q0) edge node  (q2)
edge node  (q4)
edge node  (q2')
edge node  (q4')
edge node  (q)
edge [loop above] node  ()
(q1) edge node  (q3)
edge node  (q4)
edge node  (q3')
edge node  (q4')
edge node  (q)
edge [loop below] node  ()

Introductory example building

In security, it is common to use an attack tree to model the goal of the attacker. An attack tree is a tree where each node describes a goal and the children of a node describe a refinement into sub-goals of the parent goal. To model those refinements, it is common to use three operators:

* $OR$ operator means that at least one sub-goal needs be achieved to have the goal accomplished,

* $SAND$ operator, read "sequential and", means that the sub-goals need be achieved in the left-to-right order to have the goal accomplished,

* $AND$ operator means that the sub-goals need be achieved (in whatever order) to have the goal accomplished.

In Figure <ref>, we describe the goal of the thief by means of an attack tree. To distinguish the different types of nodes, we draw a curved line below an $AND$ operator, a curved arrow below a $SAND$ operator and nothing below an $OR$ operator.

[scale=0.85,every text node part/.style=align=center, node distance=3cm]
[draw, ellipse] (p) at (0,0) ;
[draw, ellipse] (q) at (-3,-2) ;
[draw, ellipse, text width = 1.5cm] (r) at (3,-2) enter room 2;
[draw, ellipse] (truc) at (0,-2) ;
(q) – (p) – (r);
[->] (-1.2,-0.8) to[bend right] (1.2,-0.8);
[draw, ellipse, text width = 1.5cm] (s) at (-6,-4) cross first door unseen;
[draw, ellipse, text width = 1.5cm] (t) at (-3,-4) cross second door unseen;
[draw, ellipse, text width = 1.5cm] (u) at (0,-4) deactivate camera;
(s) – (q) – (t);
[-] (0, -2.8) to[bend right] (1.2,-2.8);
[draw, ellipse, text width = 1.5cm] (v) at (3,-4) find key;
(u)–(truc) – (v);

An attack tree to model the goal of our thief.

We focus our attention on the very first part of our problem, that is, the sub-goal of the thief to enter the building. We start by fixing a set of proposition $\Prop=\{\propdone, \propdtwo, $$\}$ where $\propdone$ holds when the thief is in front of the first door, $\propdtwo$ holds when the thief is in front of the second door and holds when the guard sees the thief because they meet in front of the same door. The goal "crossing the first door unseen" of the thief can be modelled by the formula $\propdone \land \lnot\propseen$ and the goal "crossing the second door unseen" is modelled by the formula $\propdtwo \land \lnot \propseen$. If we assume that the guard can switch door whenever he wants but leaves the two doors unguarded for a brief amount of time during his motion, we can model the situation using the graph of Figure <ref> where each state consists of a pair in the set $\{o, d_1, d_2\} \times \{m, d_1, d_2\}$. For a pair $(a,b)$, element $a$ determines the position of the thief ($o$ means that he is still outside the building, while $d_i$ indicates he is at door $i$) and element $b$ determines the position of the guard ($m$ means that he is currently in motion between the two doors, leaving them both unguarded). We write next to each state which propositions hold in it.

In a path semantics, a successful attack for goal $\propdone \land \lnot \propseen$ consists of a sequence of states (a word) such that the valuation of the last state of this sequence satisfies formula $\propdone \land \lnot \propseen$. In particular, the sequence $(o,m), (d_1,d_2)$ is a successful attack. Now, if we want to consider a successful attack for the attack tree consisting of the "OR" operator of objective $\propdone \land \lnot \propseen$ and $\propdtwo \land \lnot \propseen$, it is enough to consider the union of the set of all attacks for objective $\propdone \land \lnot \propseen$ with the set of all attacks for objective $\propdtwo \land \lnot \propseen$.

However, in the strategy semantics we introduce in this paper, we consider that an attack is successful if the attacker has a strategy that grants him to reach the states he needs to attain, independently of the environment. In our example, we can see that the thief has no strategy starting at position $(o,m)$ to achieve goal $\propdone \land \lnot \propseen$. Indeed, if the first move of the guard consists on going to door 1 and he then does not move any more, there is no way for the thief to cross the first door while unseen. Similarly, there is no strategy starting at position $(o,m)$ to achieve goal $\propdtwo \land \lnot \propseen$. However, if we consider the "OR" operator of the two goals $\propdone \land \lnot \propseen$ and $\propdtwo \land \lnot \propseen$, the strategy of the thief consisting in waiting for the guard to go to one of the two doors and then going to door 1 if the guard is at door 2 and vice versa is a successful strategy. Later, we will use similar a similar example to show that a compositional definition for a strategy semantics cannot be achieved.

§ PRELIMINARY NOTIONS

Formal languages
Given an alphabet (a finite set of symbols) $\alphabet$, notation $\alphabet^*$
represents the set of finite words (sequences of symbols) over
the alphabet $\alphabet$, with typical element $\word=\letter_1 \ldots \letter_n \in \alphabet^*$; the empty word is written $\eword$. On
the other hand, the set of infinite words is denoted by
$\alphabet^\omega$. A subset $L \subseteq \alphabet^*$ is a language.

Given a word $\word=\letter_1 \ldots \letter_n \in \alphabet^*$, its set of
prefixes is the language $\Prefixes(\word)=\{\letter_1 ... \letter_i
| i\leq n\} \cup \{\eword\}$, and we write
$\word' \prefix \word$ whenever $\word' \in \Prefixes(\word)$.

A language $\lang$ is prefix-closed if $\word \in \lang$ implies $\word'\in \lang$ for every $\word' \prefix \word$.

The concatenation of a word $\word=\letter_1 \ldots \letter_n$ with another word $\word'=\letter_1' \ldots \letter_m'$ is the word $\word\word'=\letter_1 \ldots \letter_n\letter_1' \ldots \letter_m'$. The concatenation of a word with a language is defined in the usual
way: for $\word \in \alphabet^*$ and $\lang \subseteq \alphabet^*$,
we let $\word\lang:=\{\word\word'| \word' \in \lang\}$.

Game theory and game arena
To formalize a strategy semantics for attack trees, we need standard two-player, zero-sum, perfect information games that we recall here.

A game arena is a finite graph on which two players play a game of unbounded duration. We choose to consider concurrent games, meaning that, at each round, each player makes an action. To define it properly, we consider two players called Player $1$ and Player $2$ and a finite set of propositions $\Prop$.

A two-player game arena is a tuple $\arenaa$ where:

* $\Pos=\{\pos, ...\}$ is a finite set of positions.

* $\Act=\Act_1 \times \Act_2$ is a finite set of actions, as a product of the sets of actions of each player.

* $\arenaf: \Pos  \times \Act \to \Pos$ is a transition function,

* $\arenav:\Pos \to \mathcal{P}(\Prop)$ is a valuation function.

In our introductory example of <Ref>, if we consider the set of actions for the thief: $\{$wait, go-to-Door-1, go-to-Door-2$\}$ and the following set of actions for the defender: $\{$stay-at-current-door, leave-current-door, go-to-Door-1, go-to-Door-2$\}$, then it is easy to see that the graph drawn in Figure <ref> forms a game arena.

For the rest of this paper, we fix a game arena $\arenaa$.

For a game position $\pos \in \Pos$, we define
$\nextpos{\pos}=\{\pos'\in \Pos| $ $\arenaf(\pos, \act)=\pos'$ for
some $\act \in \Act \}$ the set of all positions reachable from $\pos$
in one step. For convenience, we assume that each player $\player$ can play every action $\act$ in $\Act_\player$ at each position of the game arena, so that for each
position $\pos \in \Pos$, we have $\nextpos{\pos} \neq \emptyset$. A play $\play$ is an infinite sequence of positions of the form
$\pos_0 \pos_1 \pos_2 .... \in \Pos^\omega$ such that for each
$i \in \mathbb{N}$, there is $\act \in \Act$ such that
$ \arenaf(\pos_i,\act)= \pos_{i+1}$. For $i \in \mathbb{N}$, we let
$\play_i=\pos_i$ be the $i^{th}$ position of play $\play$. The set
of all plays is denoted by $\Plays(\arena)$. Each non-empty prefix
$\hist$ of a play is called a history and the set of all
histories is denoted by $\Hist(\arena)$. For a history
$\hist \in \Hist(\arena)$, we define $last(\hist)$ as the last
position of $\hist$. For $\pos \in \Pos$, we also use the notations
$\Plays(\arena, \pos)$ and $\Hist(\arena, \pos)$ to denote the set of
all plays starting from $\pos$ ($\play_0=\pos$) and the set of all histories starting
from $\pos$, respectively.

Winning plays for Player $1$ are obtained from a distinguished subset $\win_1 \subseteq \Plays(\arena)$. As we consider zero-sum games, all plays in $\win_1\backslash \Plays(\arena)$ are winning for Player $2$.

Classically, we introduce the notion of strategy, as a map prescribing how a player plays depending on the current history: a strategy $\strat^\player$ for the Player $\player$ is a map $\strat^\player:\Hist(\arena) \to \Act_i$. The set of all strategies for the Player $\player$ is denoted as $Strat^\player$.

A history $\hist=\pos_0\pos_1...\pos_m$ is consistent with a strategy $\strat^\player$ if for each $1 \leq i \leq m$, there exists $\act=(\act_1, \act_2) \in \Act$ such that we have $\arenaf(\pos_i,\act)=\pos_{i+1}$ and $\strat^\player(\pos_0\pos_1...\pos_i)=\act_\player$. We say that a play $\play$ is consistent with a strategy $\strat^\player$ if all prefixes of $\play$ are histories consistent with $\strat^\player$. The set of all plays consistent with $\strat^\player$ is denoted by $\out(\strat^\player)$. From a game position $\pos$ we say that a strategy is winning if all outcomes starting at $\pos$ are winning. In other words, for a strategy of say Player $1$, a strategy $\strat$ is winning if $\out(\strat) \cap \Plays(\arena, \pos) \subseteq \win_1$.

A classic kind of concurrent games are the reachability games. In such games, a player wants to reach some positions while the other player tries to prevent it from happening. These games are clearly zero-sum. More formally, we say that a game is a reachability game for Player $1$ if there exists $\reachwin \subseteq \Pos$ such that $\win_1=\{\play \in Plays(\arena)| \play_i \in \reachwin$ for some $i \in \mathbb{N}\}$.

In a game arena, we says that a position $\pos$ satisfies the formula $\formula$ if its valuation $\arenav(\pod)$ satisfies the formula in classic propositional logic, denoted by $\pos \models \formula$. Note that a Boolean formula $\formula$ over $\Prop$ describes the reachability game $(\arena, \reachwin)$ where $\reachwin=\{\pos \in \Pos|\pos \models \formula\}$.

§ ATTACK TREES AND THEIR SEMANTICS

In this section, we start with the formal definition of attack tree used in this paper. Then we develop two semantics for attack trees: the path semantics and the strategy semantics.

§.§ Syntax of attack trees

To formalize attack trees, we start by fixing a set of propositions $\Prop$.

An attack tree $\att$ over $\Prop$ is:

* either a leaf composed of a unique Boolean formula $\formula$ over $\Prop$,

* or an expression $OP(\att_1,...,\att_n)$ where $OP$ ranges over $OR$, $AND$ and $SAND$ and $\att_1, ...,\att_n$ are attack trees.

We define the size of an attack tree $\att$, noted $\sizeatt{\att}$, by the number of its nodes.

We will formalise the example introduced in Section <ref>. To represent the situation, we use the following set of propositions:  $\Prop=\{\propdone,\propdtwo, \propseen, \texttt{C},\texttt{K},\texttt{R2}\}$. We have that $\propdone$ holds when the thief has crossed the first door, $\propdtwo$ holds when the thief has crossed the second door, $\propseen$ holds when the guard sees the thief, $\texttt{C}$ holds when the camera is on, $\texttt{K}$ holds when the thief has the key and finally $\texttt{R2}$ holds when the thief is in the second room.

We can now  propose a formal definition for the attack tree in Figure <ref>: $\att= \break SAND(OR(\propdone \land \lnot \propseen, \propdtwo \land \lnot \propseen), AND(\texttt{C},\texttt{ K}), \texttt{R2})$ to model the objective of the attacker. The graph representation of $\att$ is given by Figure <ref>.

[scale=0.85,every text node part/.style=align=center]
[draw, ellipse] (p) at (0,0) ;
[draw, ellipse] (q) at (-3,-2) ;
[draw, ellipse, text width = 1.5cm] (r) at (3,-2)  $\texttt{R2}$;
[draw, ellipse] (truc) at (0,-2) ;
(q) – (p) – (r);
[->] (-1.2,-0.8) to[bend right] (1.2,-0.8);
[draw, ellipse, text width = 1.5cm] (s) at (-6,-4) $\propdone \land \lnot \propseen$;
[draw, ellipse, text width = 1.5cm] (t) at (-3,-4)  $\propdtwo \land \lnot \propseen$;
[draw, ellipse, text width = 1.5cm] (u) at (0,-4)  $\texttt{C}$;
(s) – (q) – (t);
[-] (0, -2.8) to[bend right] (1.2,-2.8);
[draw, ellipse, text width = 1.5cm] (v) at (3,-4)  $\texttt{K}$;
(u)–(truc) – (v);

Formal version of the attack tree in Figure <ref>.

Let us notice that the attack trees used in [1] are in fact slightly different: the leaves of the attack trees of that paper are of the form $<\formula_1, \formula_2>$ with $\formula_1$ and $\formula_2$ two Boolean formulas. Formula $\formula_1$ describes a precondition for the objective to begin with and formula $\formula_2$ describes the postcondition for the objective to be granted. However, in this paper, we never consider preconditions. So a leaf $\formula$ of our attack trees can be seen as a leaf $<true, \formula>$ of attack trees introduced in [1]. Although the semantics defined in this paper could also be defined for attack trees with preconditions, not considering them makes the setting more pedagogical.

The first semantics for attack trees we introduce is a path semantics inspired by [1]. Informally, in the path semantics, we consider all sequences of events that lead to a successful attack. The idea is to determine which scenarios are favourable for the attacker. One could also say that an attack can occur if the attacker is lucky.

The second semantics is our main contribution, and is named the strategy semantics for attack trees. In this approach, the attacker should not rely on an opportunity offered by the environment but should be able to find the right sequence of actions whatever the environment does. Otherwise said, an attack is not a favourable scenario anymore but a winning strategy for attacker in some two-player game arena.

§.§ Path semantics for attack trees

To give a path semantics over our trees, we first need to fix a transition system to model which actions/sequences of actions can be executed by the attacker in the system. A transition system is composed of a finite set of states together with a transition relation between pairs of states. We decided not to label every transition with an action as we only consider perfect information here. We also provide a valuation function to our transition system, informing which propositions of $\Prop$ holds in a state of the transition system.

A transition system over $\Prop$ is a triplet $\transall$ where:

* $\transS$ is a finite set of states,

* $\transf \subseteq \transS\times \transS$ is a relation of transitions,

* $\transv:S \to \mathcal{P}(\Prop)$ is a valuation function.

The size of $\trans$, noted $\sizetrans{\trans}$, is defined by its number of states.

We can see from  <Ref> that a transition system is a notion close to a game arena. Indeed, it is easy to associate a transition system with a game arena $\arenaa$, by merging the two players into a single one in the following way: $\trans_\arena =(\Pos, \{(\pos, \pos') \in \Pos \times \Pos |$ there exists $\act \in \Act$ such that $\arenaf(\pos, \act)=\pos'\},\arenav)$. Later, we denote $\trans_\arena$ by $\arena$ when it is clear from the context.

For the rest of this section, we fix a transition system $\transall$  over $\Prop$. A path in a transition system is a finite non-empty sequence of states $\path=\transs_0\transs_1...\transs_n$ such that, for each $0\leq i <n$,  $(\transs_i, \transs_{i+1}) \in \transf$. The size of a path is its number of states. We denote the set of all paths in $\trans$ by $\Path_\trans$.

In order to define the path semantics we need to introduce operators over paths.

Let $\path=\transs_0\transs_1...\transs_n$ and $\path'=\transs'_0\transs'_1...\transs'_m$ be two paths in $\trans$ with $n,m\geq 0$. The synchronised concatenation of $\path_1$ and $\path_2$ is defined only if $\transs_n=\transs'_0$ and is given by t $\path \concatsync \path'= \transs_0\transs_1...\transs_n\transs'_1...\transs'_m$.

We lift this operations to sets of paths the following way: if $\Path_1$ and $\Path_2$ are two sets of paths, then $\Path_1 \concatsync \Path_2=\{\path_1 \concatsync \path_2 | \path_1 \in \Path_1$ and $\path_2 \in \Path_2\}$.

The authors of  [1] introduce the operator of parallel composition of paths. However, our definition of attack trees grants us the possibility to use a simpler operator.

Let $\Path_1$, $\Path_2$ be two sets of paths of $\trans$. The merge of $\Path_1$ and $\Path_2$ is the set of paths $\Path_1 \andword \Path_2 =\{\path_1 \in \Path_1 |$ there exists $ \path_2 \in \Path_2 $ such that $\path_2\prefix \path_1\} \cup \{\path_2 \in \Path_2 |$ there exists $ \path_1 \in \Path_1 $ such that $\path_1\prefix \path_2\}$

Unlike the parallel composition of [1], thanks to the transitivity of the prefix relation, the merge operator is associative.

We can now define our path semantics.

Let $\att$ be a attack tree over $\Prop$. The path semantics of $\att$ over $\trans$ is the set of paths $\semword{\att}{\trans}$ inductively defined as follow:

* $\semword{\formula}{\trans} = \{\transs_0\transs_1...\transs_n \in \Path_\trans |  \transs_n \models \formula\}$

* $\semword{OR(\att_1, ..., \att_n)}{\trans}=\semword{\att_1}{\trans} \cup ... \cup \semword{\att_n}{\trans}$

* $\semword{SAND(\att_1, ..., \att_n)}{\trans}=\semword{\att_1}{\trans} \concatsync ... \concatsync \semword{\att_n}{\trans}$

* $\semword{AND(\att_1, ..., \att_n)}{\trans}=\semword{\att_1}{\trans} \andword ... \andword \semword{\att_n}{\trans}$

It is easy to verify that the semantics of Definition <ref> is equivalent to the one introduced in [1] if we restrict to the attack trees whose leaves are of the form $< true,\formula>$.

Remark that, in our framework, for $\formula_1$ and $\formula_2$ two formulas over $\Prop$, the interpretation of $SAND(\formula_1,\formula_2)$ is that $\formula_1$ must hold at some point and $\formula_2$ must hold at some point afterwards. This requirement does not prevent $\formula_2$ from holding before $\formula_1$.

We also want to point out that our semantics consider that the simultaneity of objectives is always successful: for $\formula_1$ and $\formula_2$ two formulas over $\Prop$, if $\formula_1$, $\formula_2 \in \transv(\transs)$, then $\transs \in \semword{SAND(\formula_1, \formula_2)}{\trans}$ and $\transs \in \semword{AND(\formula_1, \formula_2)}{\trans}$.

If we consider the game arena $\arena$ given in <Ref>, we have that $(d_1,d_2) \models \propdone \land \lnot \propseen$, thus the path $(o,m)(d_1,d_2) \in \semword{\propdone \land \lnot \propseen}{\arena}$. This gives us also $(o,m)(d_1,d_2) \in \semword{OR(\propdone \land \lnot \propseen, \propdtwo \land \lnot \propseen )}{\arena}$.

§.§ Strategy semantics for attack trees

We start this section by formally defining strategic trees as well as some handful operators over them. We use a definition of a tree really close to the one made from prefix-closed languages (for example in <cit.>) except that we fix a letter to represent the root.

A strategic tree (written s-tree for short) over an alphabet $\alphabet$ is a language $\stree$ of the form $\letter \lang$ with $\letter \in \Sigma$ and $\lang$ is a prefix-closed language over $\alphabet$.

For an s-tree $\stree=\letter\lang$, $\letter$ is called the root. For a word $\word \in \stree$, if there exists no $\word' \in \stree$ such that $\word\prefix\word'$ then we call $\word$ a leaf. The set of all leaves of $\stree$ is denoted by $\leaves(\stree)$. For two words $\word, \word' \in \stree$ such that $\word\prefix\word'$, if there exist no $\word'' \in \stree$ such that $\word\prefix\word''\prefix\word'$, then we says that $\word$ is the parent  of $\word'$ and $\word'$ is a child of $\word$. The set of all children of a word $\word$ in a s-tree $\stree$ is denoted by $\children_\stree(\word)$. The depth of an s-tree is the size of the longest word in it.

Figure <ref> shows an s-tree over the alphabet $\Pos$, the set of positions of the game arena of <Ref>.

As in <Ref>, for the particular case where alphabet $\alphabet$ is the set of positions on some game arena, we develop several notions on s-trees and show that strategies can be presented as s-trees.

For the rest of this section we fix a game arena $\arenaa$.

The next lemma asserts that all histories consistent with a strategy and starting from a given position form an s-tree.

Let $\strat$ be a strategy for some player and $\pos \in \Pos$ be a game position. The language $\stree^{\strat}_\pos=Prefixes(\out(\strat)) \cap \Hist(\arena, \pos)$ is an s-tree over alphabet $\Pos$, and is called the s-tree associated with $\strat$ from position $\pos$.

The proof is straightforward from the definition of $\stree^{\strat}_\pos$.

By <Ref>, each branch of $\stree^{\strat}_\pos$ is the succession of all prefixes (in terms of words) of a play consistent with $\strat$. Reciprocally, each play consistent with $\strat$ and starting from position $\pos$ is represented by a branch of $\stree^{\strat}_\pos$. Therefore $\stree^{\strat}_\pos$ fully describes the strategy $\strat$ starting from position $\pos$.

Consider the game arena $\arena$ given in Figure <ref> and the strategy $\strat$ for the thief consisting in waiting one unit of time, then, if the guard is at some door, going to the other door and if the guard is currently in motion, waiting another unit of time before going to the door where the guard will not be. If we call this strategy $\strat$, the strategic tree $\stree^\strat_{(o,d_1)}$ is given in Figure <ref>.

[$(o ; d_1)$[$(o;d_1)(o;m)$[$(o;d_1)(o;m)(o;d_1)$[$...(d_2;d_1)$][$...(d_2;m)$]][$(o;d_1)(o;m)(o;d_2)$[$...(d_1;d_2)$][$...(d_1;m)$]]][$(o;d_1)(o;d_1)$[$(o;d_1)(o;d_1)(d_2;d_1)$][$(o;d_1)(o;d_1)(d_2;m)$]]]

strategic tree $\stree^{\strat}_{(o,d_1)}$

As we put the focus on attack trees, we take the convention that, in the game arena, Player $1$ is called Attacker and Player $2$ is called Defender. In this setting, Attacker tries to achieve an attack that is described by some attack tree $\att$, while Defender tries to prevent it from happening. In other words, the winning plays for the Attacker are given as $\win_\attacker=\semword{\att}{\arena}$. Our strategy semantics consists of the set of  winning strategies for this game.

We start by motivating a construction only for a leaf attack tree. The strategy semantics for an attack tree $\phi$ is the set of all strategies that are winning for the reachability game defined by $\phi$.
Remark that for the case of reachability games, once a winning position is reached, the continuation of the play does not matter. Therefore, for reachability games, the s-tree corresponding to a winning strategy can be cut as a finite tree: this cut consists in removing all children of a node describing a history ending in a position where $\formula$ holds. This way of cutting motivates the definition of prefix of s-trees as follows:

Let $\stree$ be an s-tree over $\alphabet^*$. An s-tree $\stree'$ is a prefix of $\stree$ if $root(\stree')=root(\stree)$, and $\stree'\subseteq \stree$, and
for every $\word \in \stree'\setminus \leaves(\stree')$, we have $\children_{\stree'}(\word)=\children_{\stree}(\word)$.

For the s-tree $\stree^\strat_{(o,d_1)}$ of Figure <ref> and the two trees given in Figure $\ref{Fig:prefix}$, we have $\stree_a$ is a prefix of $\stree^\strat_{(o,d_1)}$, but $\stree_b$ is not because $\children_{\stree^\strat_{(o,d_1)}}(o,d_1)=\{(o,d_1)(o,m), (o,d_1)(o,d_1)\}\neq \children_{\stree_b}(o,d_1)\break =\{(o,d_1)(o,d_1)\}$.

[$(o ; d_1)$[$(o;d_1)(o;m)$][$(o;d_1)(o;d_1)$[$(o;d_1)(o;d_1)(d_2;d_1)$][$(o;d_1)(o;d_1)(d_2;m)$]]]

[$(o ; d_1)$[$(o;d_1)(o;d_1)$[$(o;d_1)(o;d_1)(d_2;d_1)$][$(o;d_1)(o;d_1)(d_2;m)$]]]

two s-trees: $\stree_a$ (left) and $\stree_b$ (right)

With this notion of prefix, it is immediate to characterise attack trees that witness a strategy.

Consider a leaf attack tree $\formula$, and write $\formula \subseteq Pos$ for the set of positions where $\formula$ holds. Consider $\strat$ a strategy for Attacker in the reachability game $(\arena, \phi)$ and $\stree^{\strat}_\pos$ the associated s-tree  from position $\pos$. A finite s-tree $\cst$ is a witness of $\strat$ from position $\pos$ if $\cst$ is a finite prefix of $\stree^{\strat}_\pos$, and $\leaves(\stree) \subseteq \Pos^*\formula$.

<Ref> can be generalised to an arbitrary reachability condition $\reachwin \subseteq \Pos$ as follows: $\stree$ is a witness of $\strat$ from position $\pos$ if $\cst$ is a finite prefix of $\stree^{\strat}_\pos$ and $\hist \in \leaves(\stree)$ implies $last(h)\in \reachwin$.

In the game arena of <Ref>, if we consider the reachability condition $\reachwin=\{(o,m),\break (d_2,m), (d_2,d_1)\}$, then the attack tree $\stree_a$ of <Ref> is a witness for the s-tree $\stree^\strat_{(o,d_1)}$ drawn in <Ref>.

<Ref> leads us to the following intuitive lemma.

Let $\strat$ be a strategy for Attacker and $\reachwin$ be a winning condition. Then $\strat$ is a winning strategy for $(\arena, \reachwin)$ from position $\pos \in \Pos$ if, and only if, there exists a witness $\cst$ of $\strat$ from $\pos$.

The proof relies on the König's Lemma.

Thus, for a leaf $\formula$, the strategy semantics is all witnesses that can be constructed from a winning strategy over the reachability game defined by $\formula$. Moreover, an s-tree is in the semantics of a leaf attack tree if it is a prefix of some strategy and if all its leaves are in the path semantics of the attack tree. The former condition guarantees that our s-tree has the shape of a strategy, while the latter guarantees that the strategy is winning. As we will see below, those are the two conditions we use to define the strategy semantics of arbitrary attack trees.

For the first condition, we say that an s-tree $\stree$ is well-formed if there exists a strategy $\strat$ and a position $\pos$ such that $\stree$ is a prefix of $\stree^\strat_\pos$. For the second condition, we use the following definition:

Let $\att$ be an attack tree. A $\att$-s-tree is a finite s-tree $\stree$ over $\Pos$ such that $\leaves(\stree)\subseteq \semword{\att}{\arena}$.

Since for a leaf attack tree $\formula$, we have $\semword{\formula}{\arena}=\Pos^*\formula $, a witness $\stree$ (<Ref>) is a $\formula$-s-tree.
We now have all the material to define the strategy semantics of an attack tree.

Let $\att$ be an attack tree. The strategy semantics associated with $\att$, written $\sem{\att}{\arena}$ is the set of all well-formed $\att$-s-trees.

In particular, $\sem{\formula}{\arena}$ is the set of all witnesses in the reachability game $(\arena,\formula)$.

We can see that the idea is far from the one of attack-defence trees in [8]. In attack-defence trees, the countermeasure is a structure similar to an attack tree whose semantics describes paths that prevent an attack from succeeding, and by no means a strategy of the attacker's opponent in the arena.

Now that we defined our semantics, we might want to know if it can be obtained in a compositional manner
? Namely, if the semantics of a compound tree can be defined in terms of the semantics of its subtrees: More formally.. can we define $\sem{OP(\att_1, ..., \att_n)}{\arena}$ on the basis of $\sem{\att_1}{\arena}, ...,\break \sem{\att_n}{\arena}$? Sadly, the answer is no:

Consider the game arena defined in Figure <ref>. Obviously, our attacker here will be the thief while the guard will do the defender role. We also consider a new proposition: $Start$ which only holds at position $\{o,m\}$. We have that the semantics of $SAND(start, \propdone\land \lnot \propseen)$ is empty. Indeed, the guard can choose to only keep door $1$ and thus, the thief will not be able to attain $\propdone$ while remaining unseen. Similarly, $\sem{SAND(start, \propdtwo\land \lnot \propseen)}{\arena}$ is empty. However, the strategy consisting on waiting one unit of time then going through the door not controlled by the guard is a winning strategy, it is easy to construct a witness for that strategy that attains the objective of $OR(SAND(start, \propdone\land \lnot \propseen),SAND(start,\propdtwo\land \lnot \propseen))$ and thus is in its strategy semantics.

The previous example showcases an empty semantics for $\att_1$ and $\att_2$ but a non-empty one for $OR(\break \att_1, \att_2)$. This is because, for $\formula_1$ and $\formula_2$ two propositional formulas over $\Prop$, there are more strategies to achieve $\formula_1\lor\formula_2$ than strategies only achieving $\formula_1$ or only achieving $\formula_2$. We can for example consider a strategy that, depending on the move of the opponent, chooses whether it prefers to attain $\formula_1$ or to attain $\formula_2$.

Remark that, using the "merge" operator of [11] provides us a compositional semantics for attack trees with $SAND$-only operators. However, we have already argues that the $OR$ operator have some problems just as the $AND$ operator for more elaborate examples. Still, it is possible to tune the semantics so that it becomes compositional for the AND operator, at the price of loosing clarity, but more regrettably without solving the hopeless case of the OR operator.

§ DECISION PROBLEMS OVER ATTACK TREES

In this section, we discuss two common decision problems over semantics of attack trees and determine their complexities with respect to the path semantics and the strategy semantics. The first problem we consider is the Non-Emptiness problem. This problem consists of, given an attack tree and a game arena, deciding whether its semantics is not empty:

The Non-Emptiness problem is the following decision problem for a fixed semantics $\semgeneral{\cdot}{\arena}$ of attack trees:
Input: $\arena$, a game arena, $\att$, an attack tree.
Output: $Yes$ if $\semgeneral{\att}{\arena}\neq \emptyset$, $No$ otherwise.

The Non-Emptiness problem for the path semantics is denoted
by PNE while the Non-Emptiness problem for the strategy semantics
is denoted SNE. A positive instance of PNE tells us that Attacker has a
favourable scenario to attack. A positive instance of SNE tells us that Attacker has a strategy (it
is possible for him to attack successfully the system independently of
the defender/environment comportment).

We now turn to the Membership problem.

The Membership problem is the following decision problem for a fixed attack tree semantics $\semgeneral{\cdot}{\arena}$ of  of type $X$:
Input: $\arena$, a game arena, $\att$, an attack tree and $x \in X$.
Output: Yes if $x \in \semgeneral{\att}{\arena}$, No otherwise.

The Membership problem for the path semantics is denoted by PM while the Membership problem for the strategy semantics is denoted SM. PM consists of determining whether a path is an attack or not. It can be really useful if we have an attack tree describing an attack goal over an information system and a log file of that system. Determining if the system has been attacked is equivalent to determining whether the path described by the log file is in the path semantics of the attack tree or not. The idea behind SM is different: it is useful to determine whether a strategy is winning or not for a given attack objective. We start to analyse the complexity of PM and take advantage of it for the proofs of the other results. We then consider SNE. After that, PNE is easily determined as a particular case of SNE and we finish by SM whose proof uses similar and simpler constructions than the one for SNE.

If we use attack trees with preconditions, the problem PM is -hard; this comes from the fact that the packed interval covering problem, which can be easily captured by the parallel composition (see [13]), is -complete (see [14]). However, PM becomes simpler if we discard preconditions:

PM is in .

For a polynomial algorithm, we use the fact that a word is in
the semantics of an attack tree, then adding an arbitrary prefix to it
keeps it in the semantics. As a consequence, we do not need to recompute
which sub-goals of the attack tree are satisfied whenever we add a position in front of a path. Thus, the shape of the problem is well-suited for a backward
induction over the input path. Moreover, determining if a given input
path satisfies an attack tree knowing whether it satisfies the sub-trees can be done in linear time over the size of the
attack tree.

We now turn to the complexity of SNE.

SNE is -complete.

For the membership, we construct an alternating algorithm (see [2])
solving the problem that can be executed in polynomial time. This
algorithm consists of synthesizing a history over the game arena and
then verifying that this history is an attack (by <Ref>, this verification is doable in polynomial time). To construct this history, we finitely iterate first to make a non-deterministic existential guess for
the action of Attacker and then a non-deterministic universal
guess for the action of Defender. We then
show that the resulting history is in the path semantics of the input attack tree $\att$  if,
and only if, the strategy semantics of $\att$ is not empty. We guarantee a polynomial time execution, namely that the resulting
history need not be too long with the following lemma.

Let $\arenaa$ be a game arena and $\att$ be an attack tree with $n$ leaves. If $\sem{\att}{\arena} \neq \emptyset$, then there exists $\stree \in \sem{\att}{\arena}$ of depth $d \leq |\Pos| \times n$.

The basic idea behind to prove <Ref> is that, memoryless strategies suffice in reachability games (see [4]).

We design Algorithm <ref> to solve SNE whose idea is explained above and show that it belongs to .

$SNE(\arena, \att$)

Input: $\arena$ a game arena and $\att$ an attack tree with $n$ leaves Output: $True$ if $\sem{\att}{\arena}\neq \emptyset$, $False$ otherwise.

[1]

$\hist \leftarrow$ empty list
$\pos \leftarrow$ [$\exists$]guess position in $\Pos$
$size(\hist)< |Pos| \times n$
[$\exists$]guess break or not
$\act_1 \leftarrow$ [$\exists$]guess action in $\Act_\attacker$
$\act_2 \leftarrow$ [$\forall$]guess action in $\Act_\defender$
$\hist.append(\arenaf(last(\hist),(\act_1, \act_2)))$
$\hist \in \semword{\att}{\arena}$

Algorithm <ref> is an alternating polynomial-time algorithm and solves SNE.

We start by showing the complexity of the algorithm, then we show its correctness.

From the loop at Line 4, it is executed polynomially many times in the size of the input attack tree and of the game arena. We also know (<Ref>) that the condition $\hist \in \semword{\att}{\arena}$ at Line 10 can be evaluated in polynomial, therefore, Algorithm <ref> is polynomial-time alternating.

Assume Algorithm <ref> returns $True$, then, for each choice made by universal guess, there exists a choice made by existential guess guaranteeing that the obtained history is in $\semword{\att}{\arena}$. As a consequence, the choices made by the existential guesses reflect a strategy in the game arena that satisfies $\att$ so, $\sem{\att}{\arena}\neq \emptyset$. Conversely, if $\sem{\att}{\arena}\neq \emptyset$, then there exists (by Lemma <ref>) an s-tree $\stree$ of depth $\leq |Pos| \times n$. Thus the existential guesses can simply follow the strategy given by $\stree$ and then choose to go out from the main loop by the "break" command at Line 5 of Algorithm <ref> whenever the sequence of choices (existential and universal) in the execution is reflected by a full branch of the s-tree $\stree$.

For the -hardness of SNE, our construction is inspired by the one in [1]: the authors reduce (in polynomial time) the SAT problem to the PNE problem with attack trees (using preconditions). In fact, even if in that paper, authors use attack trees with preconditions, we can adapt it without preconditions. We can even cast the approach to QBF that we first recall:

The quantified Boolean formula (QBF) is the following decision problem:
Input: a formula of the form $Q_1 x_1, ..., Q_n x_n \psi(x_1, ..., x_n)$ with $Q_i \in \{\exists, \forall\}$ and $\psi$ a Boolean formula in conjunctive normal form over propositions $x_1, ..., x_n$.
Output: $Yes$ if the input formula is true, $No$ otherwise.

The QBF problem can be reduced to SNE in polynomial time.

It is easy to understand the reduction principle on an example.

Consider the formula $\psi=\exists x_1 \forall x_2 \exists x_3, x_1 \land
(x_2 \lor x_3) \land (\lnot x_2 \lor x_3)$. Let $C_1=x_1$, $C_2=(x_2 \lor x_3)$ and $C_3=(\lnot x_2 \lor x_3)$ be the three clauses in $\psi$. The game arena $\arena$
associated with this formula is drawn in Figure <ref>: for each position $v_i$ (resp. $\lnot v_i$), the proposition $p_i$ holds if $v_i \in C_i$ (resp. $\lnot v_i \in C_i$). Remark that this game arena is a special case of game arena called turn-based game arena: only one player makes an action in each position, we say that a position belongs to the player who can play on it. We decide classically which position belongs to each player based on quantifiers of $\psi$ (see the proof of <Ref> for further explanations). We represent Attacker positions with a circle and Defender positions with a square (position $\pos_3$ and position $\lnot pos_3$ have only one successor position, therefore, it does not matter which player makes the move; by convention, we say they belong to the attacker). Then, $\psi$ holds if, and only if, $\sem{SAND(start, AND(p_1,p_2,p_3))}{\arena}\neq \emptyset$.

[scale=0.6,node distance = 0.1cm and 0.5cm]

[state] (q0)   $Start$;
[draw, regular polygon, regular polygon sides=4, minimum size=1.6cm] (a) [above right=of q0] $\pos_1$;
[draw, regular polygon, regular polygon sides=4, minimum size=1.5cm] (la) [below right=of q0] $\lnot \pos_1$;
[state] (b) [ right=of a] $\pos_2$;
[state] (lb) [ right=of la] $\lnot \pos_2$;
[state] (c) [ right=of b] $\pos_3$;
[state] (lc) [ right=of lb] $\lnot \pos_3$;

(bu) at (-2,0) $\{start\}$;
(blu) at (2.5,3.2) $\{p_1\}$;
(blu') at (2.5,-3.2) $\emptyset$;
(r) at (5,3.2) $\{p_2\}$;
(s) at (5,-3.2) $\{p_3\}$;
(t) at (7.5, 3.2) $\{p_2,p_3\} $;
(u) at (7.5, -3.2) $ \emptyset$;

(q0) edge node  (a)
edge node  (la)
(a) edge node  (b)
edge node  (lb)
(la) edge node  (b)
edge node  (lb)
(b) edge node  (c)
edge node  (lc)
(lb) edge node  (c)
edge node  (lc)
(c) edge [loop right] node  ()
(lc) edge [loop right] node  ()

[draw, ellipse] (p) at (0,0) ;
[draw, ellipse] (q) at (-1,-1.2) $start$;
[draw, ellipse] (r) at (1,-1.2) ;
[draw, ellipse] (s) at (0,-2.4) $p_1$;
[draw, ellipse] (t) at (1,-2.4) $p_2$;
[draw, ellipse] (u) at (2,-2.4) $p_3$;

[->] (-0.5,-0.6) to[bend right] (0.5,-0.6);
[-] (0.5,-1.8) to[bend right] (1.5,-1.8);
(q) – (p) – (r) – (s);

Game arena and attack tree associated to the formula given in Example <ref>

We now start the proof of <ref>:

Let $Q_1 x_1, ..., Q_n x_n \psi(x_1, ..., x_n)$ with $Q_i \in \{\exists, \forall\}$ and with $\psi$ a Boolean formula over variables $x_1, ..., x_n$ be an instance of the QBF problem. Since $\psi$ is in conjunctive normal form, we can write it as $\psi=\psi_1 \land ... \land \psi_k$ with $\psi_i$ denoting disjunctive clauses containing literals of the form $x_j$ or $\lnot x_j$ with $x_i \in \{x_1, ..., x_n\}$.

We consider the set of propositions $\Prop=\{Start, p_1, ..., p_k\}$
with the following game arena:$\arenaa$, where $\Pos=\{Start\} \cup
\{\pos_i | 1 \leq i \leq n\} \cup \{\lnot \pos_i | 1 \leq i \leq
n\}$, $\Act_\attacker = \Act_\defender = \{True,\break False\}$. If $Q_0=\exists$, then position $Start$ is an Attacker position, otherwise, it's a defender position. Moreover, playing action $True$ at position $start$ leads to position $\pos_1$ while playing $False$ leads to position $\lnot pos_1$. Similarly, for each $2 \leq i \leq n$, if $Q_i= \exists$ then $\pos_{i-1}$ and $\lnot\pos_{i-1}$ are Attacker positions, otherwise, they are Defender positions. Furthermore, playing $True$ at position $\pos_{i-1}$ or $\lnot\pos_{i-1}$ leads to position $\pos_i$ while playing $False$ leads to $\lnot\pos_{i}$. Positions $\pos_n$ and $\lnot \pos_n$ are Attacker positions, moreover, the transitions over those two positions are self loops.

We define $\arenav(Start)=\{Start\}$ and for each $i \leq i \leq n$,
$\arenav(\pos_i)=\{p_j | x_i \in \psi_j\}$ and $\arenav(\lnot
\pos_i)=\{p_j | \lnot x_i \in \psi_j\}$. From this definition, if we
consider that the attacker tries to satisfy the input QBF formula
and the defender tries to prevent it, we have a classic game. We then
only need to show that the objective of the attacker can be well
described using an attack tree, which is the case by considering
$\att=SAND(Start, AND(p_1, ..., p_n))$. Indeed, if there exists a
strategy to satisfy the input QBF formula, then this strategy
satisfies $\psi_1, ..., \psi_k$ and thus, can be executed in the
constructed game arena to achieve $AND(p_1, ..., p_n)$ while starting
at position $Start$, therefore, that strategy is in
$\att$. Conversely, if $\sem{\att}{\arena}\neq\emptyset$, then one of such strategies assures that we satisfy the
input QBF instance.

By <Ref> , SNE is -hard, which achieves the proof of <Ref>.

We now turn to PNE.

PNE is -complete.

For the -membership, since our problem is a particular case of the problem discussed in [1], it is at least as easy. For the -hardness we reduce SAT: if we apply the same construction as in the proof of Lemma <ref>, since we cannot leave any choice for the defender in a transition system and the path semantics is defined over a transition system and not a game arena, we can reduce formulas of QBF only using $\exists$ operators. In other words, we can reduce SAT. In fact, by doing so, we are doing the exact construction of the proof in [1]. Moreover the attack tree with preconditions $AND(<start, \formula_1>, ..., <start, \formula_n>)$ used in that paper is completely equivalent to $SAND(start, AND(\formula_1, ..., \formula_n))$ in our formalism. Thus the proof in [1] can be well adapted for our problem.

Lastly, we study SM.

SM is -complete.

For the membership, we can use the same idea as for the membership of the SNE except that, now, we already know the strategy of the attacker, we thus do not need to use any existential guess for the action of Attacker. In other words, it is equivalent to simply considering Defender choosing a branch of the attack tree and  then verifying if it forms an attack or not. Therefore, we use a variant of Algorithm <ref> without existential choices, this gives us a algorithm.

For the hardness, we still use the idea of the construction behind the SNE, but now, we consider that only the actions of Defender matter in the progress of the game arena. This way, we can reduce the UNSAT problem, known to be -complete, to SM. The UNSAT problem is nothing less than the sub-problem  of the QBF problem where an instance of the problem only uses "$\forall$" quantifiers.

This concludes the discussion over decision problems; our results are summarised in <Ref>.

§ FUTURE WORK

In this paper, we proposed a strategy semantics for attack trees, useful to tackle some practical questions (SNE and SM) not expressible with standard semantics provided by the literature. The price to pay is to renounce a compositional semantics of attack trees. One way to regain it might be to consider a strategy semantics based on a tree automata: we associate with each attack tree a tree automaton recognising its strategy semantics. This is currently work. Moreover, being able to consider automata recognising the strategy semantics allows us to model attack scenarios with constraints, for example, considering that the attacker cannot perform a given action more than a certain amount of time.

Moreover, we are currently exploring the possibility to expand the path and the strategy semantics to attack-defense trees. The main idea is to consider a counter operator in attack trees. This generalisation could lead to a better understanding of the differences between the strategy semantics and the attack-defence tree formalism.

[1]
authorMaxime Audinot,
authorSophie Pinchinat &
authorBarbara Kordy
(year2017): titleIs my attack tree correct?
In: booktitleEuropean Symposium on Research in
Computer Security, organizationSpringer, pp.
pages83–102, 10.1007/978-3-319-66402-6_7.

[2]
authorAshok K Chandra &
authorLarry J Stockmeyer
(year1976): titleAlternation.
In: booktitle17th Annual Symposium on
Foundations of Computer Science (sfcs 1976), organizationIEEE,
pp. pages98–108, 10.1109/SFCS.1976.4.

[3]
authorHubert Comon, authorMax
Dauchet, authorRémi Gilleron, authorFlorent Jacquemard, authorDenis Lugiez, authorChristof Löding, authorSophie Tison & authorMarc Tommasi
(year2008): titleTree automata techniques and

[4]
authorLuca De Alfaro,
authorThomas A Henzinger &
authorOrna Kupferman
(year2007): titleConcurrent reachability
journalTheoretical computer science
volume386(number3), pp. pages188–217,

[5]
authorRoss Horne, authorSjouke
Mauw & authorAlwen Tiu (year2017): titleSemantics for
specialising attack trees based on linear logic.
journalFundamenta Informaticae
volume153(number1-2), pp. pages57–86,

[6]
authorRavi Jhawar,
authorBarbara Kordy,
authorSjouke Mauw,
authorSaša Radomirović &
authorRolando Trujillo-Rasua
(year2015): titleAttack trees with sequential
In: booktitleIFIP International Information
Security and Privacy Conference, organizationSpringer, pp.
pages339–353, 10.1007/978-3-319-18467-8_23.

[7]
authorAivo Jürgenson &
authorJan Willemson
(year2008): titleComputing exact outcomes of
multi-parameter attack trees.
In: booktitleOTM Confederated International
Conferences" On the Move to Meaningful Internet Systems",
organizationSpringer, pp. pages1036–1051,

[8]
authorBarbara Kordy,
authorSjouke Mauw,
authorSaša Radomirović &
authorPatrick Schweitzer
(year2010): titleFoundations of attack–defense
In: booktitleInternational Workshop on Formal
Aspects in Security and Trust, organizationSpringer, pp.
pages80–95, 10.1007/978-3-642-19751-2_6.

[9]
authorBarbara Kordy,
authorSjouke Mauw,
authorSaša Radomirović &
authorPatrick Schweitzer
(year2014): titleAttack–defense trees.
journalJournal of Logic and Computation
volume24(number1), pp. pages55–87,

[10]
authorSjouke Mauw &
authorMartijn Oostdijk
(year2005): titleFoundations of attack trees.
In: booktitleInternational Conference on
Information Security and Cryptology, organizationSpringer, pp.
pages186–198, 10.1007/11734727_17.

[11]
authorSoumya Paul,
authorRamaswamy Ramanujam &
authorSunil Simon
(year2015): titleAutomata and compositional
strategies in extensive form games.
In: booktitleModels of Strategic Reasoning,
publisherSpringer, pp. pages174–201,

[12]
authorSophie Pinchinat,
authorBarbara Fila,
authorFlorence Wacheux &
authorYann Thierry-Mieg
(year2019): titleAttack trees: a notion of
missing attacks.
In: booktitleInternational Workshop on Graphical
Models for Security, organizationSpringer, pp.
pages23–49, 10.1007/978-3-030-36537-0_3.

[13]
authorSophie Pinchinat,
authorFrançois Schwarzentruber &
authorSébastien Lê Cong
(year2020): titleLibrary-Based Attack Tree
In: booktitleInternational Workshop on Graphical
Models for Security, organizationSpringer, pp.
pages24–44, 10.1007/978-3-030-62230-5_2.

[14]
authorAbdallah Saffidine,
authorSébastien Lê Cong,
authorSophie Pinchinat &
authorFrançois Schwarzentruber
(year2019): titleThe Packed Interval Covering
Problem is NP-complete.
journalarXiv preprint arXiv:1906.03676.

[15]
authorBruce Schneier
(year1999): titleAttack trees.
journalDr. Dobb’s journal
volume24(number12), pp. pages21–29,

[16]
authorWojciech Wideł,
authorMaxime Audinot,
authorBarbara Fila &
authorSophie Pinchinat
(year2019): titleBeyond 2014: Formal Methods for
Attack Tree–based Security Modeling.
journalACM Computing Surveys (CSUR)
volume52(number4), pp. pages1–36,