C'est précisément ce résultat qui permet de supposer à tout moment des hypothèses sur les variables présentes dans une clause. Ainsi, la plupart du temps, ce renommage est fait implicitement et afin d'alléger les théorèmes et leurs preuves, on passe sous silence cette partie du calcul : on parle de variables “fraîches” et les théorèmes sont énoncés “à un renommage près”. Toutefois, pour pouvoir supposer telle ou telle hypothèse, il est nécessaire d'appliquer ce lemme en instanciant les ensembles de variables mis en jeu. L'adaptation de ce lemme d'indépendance dans le Calcul des Constructions a donc conduit à expliciter comment, à partir d'une requête R admettant une dérivation $d_1$ et d'un ensemble fini de variables Z, on peut construire une dérivation $d_2$, à partir de la même requête, n'utilisant pour renommer les clauses que des variables appartenant à un ensemble Y tel que Z et Y soient disjoints. Cette construction passe bien sûr par l'explicitation des substitutions de renommage et des unificateurs utilisés et peut être vue comme une opération de renommage portant sur une dérivation.

<figure><img src="image_12.png" /></figure>

Ce résultat est absolument indispensable si l'on veut pouvoir formaliser la preuve du théorème de complétude.

**Combiner des dérivations** En effet, la preuve du théorème de complétude s'obtient par induction sur la longueur de la requête initiale et une étape de cette preuve consiste à affirmer que si chaque atome d'un ensemble d'atomes ne contenant pas de variables admet une réfutation, alors en combinant ces réfutations, on peut obtenir une réfutation à partir de la requête constituée de tous les atomes présents dans cet ensemble :

[84] (...) *by induction hypothesis, P ∪ {θBᵢ} has a refutation for i = 1, ..., k.*
Because each θBᵢ is ground, these refutations can be combined into a refutation
of P ∪ {θB₁, ..., θBₖ} (...)

Cependant combiner des dérivations est une opération délicate, puisque, afin que la dérivation à construire satisfasse à chaque étape les hypothèses de séparation des variables, il est nécessaire de pouvoir renommer chacune des réfutations initiales. Ici encore, il s'agit d'expliciter dans Coq comment on peut construire la dérivation finale en exhibant les substitutions de renommage et les unificateurs qui vont permettre d'obtenir une telle dérivation.

<figure><img src="image_13.png" /></figure>
Ce résultat s'obtient par induction sur le nombre de réfutations initiales et sa preuve utilise constamment le lemme de "renommage" des dériva\c{c}ions présenté dans le paragraphe précédent.

Aussi, si la formalisation effectuée ne conduit à aucun résultat nouveau, elle permet toutefois d'éclairer toute une partie du calcul effectué par un programme logique : le renommage des variables. La formalisation de ce processus dans le Calcul des Constructions permet de garantir la validité des résultats prouvés, en rendant explicites toutes les étapes de renommage à faire dans les preuves et dans les implantations.

B.2.2 Plongement superficiel : Formaliser pour mieux comprendre

Motivations

Les résultats classiques de la programmation logique formalisés dans le système Coq qui viennent d’être présentés concernent les calculs finis (i.e., définissent une sémantique pour les SLD-réfutations). En effet, il existe une tradition en informatique qui veut que tout “bon” programme soit un programme dont l’exécution termine. La programmation logique n’échappe pas à cette tradition et les propriétés de terminaison des programmes logiques ont fait l’objet de nombreux travaux. Toutefois, certains programmes ont “naturellement” vocation à donner lieu à une exécution infinie et l’étude de la sémantique des “calculs” infinis est désormais envisagée dans divers paradigmes (λ-calcul, systèmes de réécriture, programmation logique, programmation concurrente par contraintes, ...) et permet d’abor- der des notions comme la concurrence, la réactivité ou encore la programmation synchrone. En effet, certains objets sont, par nature, infinis et les programmes qui permettent de les construire, même s’ils ne terminent pas, effectuent bien un calcul “utile en un certain sens”. Par exemple, dans le domaine de la programmation logique, le programme permettant de construire la liste (infinie) des entiers naturels consécutifs à partir d’un certain rang s’écrit :

$$
P = \{\mathbf{LN}(x, [x|l]) \leftarrow \mathbf{LN}(S(x), l)\} \quad (B.2)
$$

puisque pour tout $k \in \mathbb{N}$, une dérivation infinie à partir de la requête $\mathbf{LN}(k, l)$ fournit à chaque étape $i$ une approximation $[k, S(k), \dots, S^{i-1}(k)|l_i]$ de la liste des entiers naturels consécutifs à partir de $k$ :

$$
\begin{equation}
\begin{aligned}
& \mathbf{LN}(k, l) \\
& \quad \downarrow \\
& \mathbf{LN}(S(k), l_1) \\
& \quad \downarrow \\
& \mathbf{LN}(S^2(k), l_2) \\
& \quad \downarrow \\
& \quad \vdots \\
& \mathbf{LN}(S^{i-1}(k), l_{i-1}) \\
& \quad \downarrow \\
& \mathbf{LN}(S^i(k), l_i) \\
& \quad \downarrow \\
& \quad \vdots
\end{aligned}
\tag{B.3}
\end{equation}
\[
\begin{aligned}
& \theta_1 = \{x_1/k, l/[k|l_1]\} \\
& \theta_2 = \{x_2/S(k), l_1/[S(k)|l_2]\} \\
& \theta_i = \{x_i/S^{i-1}(k), l_{i-1}/[S^{i-1}(k)|l_i]\}
\end{aligned}
\]
$$
La limite de la suite correspondant aux approximations successives calculées à chaque étape de cette dérivation est la liste infinie des entiers consécutifs à partir de $k$. Cependant, toutes les dérivations infinies ne correspondent pas nécessairement à la construction d'un objet infini : certaines dérivations, appelées ici *dérivations infinies sur le domaine des termes finis*, sont infinies et ne "calculent à la limite" que des termes finis. De telles dérivations ne sont pas pour autant dénuées d'une sémantique et ne méritent pas, comme c'est l'usage, d'être reléguées dans une classe de dérivations qui seraient engendrées à partir de "mauvais programmes" : par exemple, il est possible d'écrire un programme logique donnant lieu à des dérivations infinies qui décrivent des séquences infinies d'"états" qui modélisent certains processus (par exemple, le célèbre problème du dîner des philosophes, ou plus généralement certains problèmes dont le graphe d'états est soit infini soit cyclique).

En programmation logique, il est courant de comprendre les dérivations comme des "preuves qui calculent" et c'est bien sûr l'aspect calculatoire de telles preuves qui permet l'utilisation de programmes logiques dans la résolution de problèmes. C'est aussi cet aspect calculatoire qui est considéré dans la littérature consacrée aux dérivations infinies [2, 3, 45, 52, 58, 84] : une dérivation infinie est alors vue comme un processus de calcul à l'infini d'un objet infini. En effet, les sémantiques proposées, qui reposent, pour la plupart, sur la notion de plus grand point fixe, cherchent toutes à capturer la notion d' "atome (infini) calculable à l'infini". Dans les deux principales approches existantes, l'univers du discours est complété de manière à disposer de termes infinis : dans [2, 3, 58, 84], une notion de distance entre termes permet de définir une complétion métrique de l'univers de Herbrand – dans [45], c'est une complétion par idéaux qui est envisagée. Hélas, ces approches sont toutes incomplètes (i.e., il existe des atomes infinis dans la dénotation de certains programmes qui ne sont pas "calculables à l'infini") : la complétude de l'approche métrique ne s'obtient qu'en rendant possible la présence de termes infinis dans les requêtes<fnref n="2" /> puisqu'elle est alors exprimée par<fnref n="3" /> :

$$ 
\begin{array}{l}
A \text{ (atome éventuellement infini)} \in \mathbf{gfp}(T_P) \\
\Leftrightarrow \text{il existe une dérivation équitable à partir de } A
\end{array}
$$

tandis que l'approche par idéaux, outre le fait qu'elle restreint la classe des programmes envisagés, donne seulement une sémantique pour une classe de dérivations infinies caractérisée en termes d'objets minimaux. Il semble qu'un des obstacles à la complétude de ces approches provienne de la difficulté à prendre en compte les dérivations infinies sur le domaine des termes finis : la construction d'un plus grand point fixe ne reflète pas la manière avec laquelle les termes infinis sont construits lors d'une dérivation infinie. Par exemple, si l'on considère l'approche métrique, la dénotation du programme $P = \{p(x) \leftarrow p(x)\}$ contient $p(f^\omega)$ même si le terme $f^\omega$ ne peut être construit dans une dérivation infinie (d'où la nécessité d'autoriser la présence de termes infinis dans les requêtes pour obtenir la complétude).

<footnote n="2">²Cette condition, explicitement mentionnée dans [104], ne correspond pas à la sémantique opérationnelle "standard". D'autre part, la présence de termes infinis dans les requêtes nécessite d'utiliser une version modifiée de l'algorithme d'unification. Enfin, le problème de la représentation des termes infinis dans le langage (fini) des requêtes se pose, même s'il peut dans certains cas être résolu en adoptant une représentation implicite (par exemple avec des contraintes) des termes infinis.</footnote>

<footnote n="3">³$T_P$ est l'opérateur de conséquence immédiate associé au programme $P$ et $gfp(T_P)$ dénote le plus grand point fixe de cet opérateur.</footnote>
La définition d'une sémantique par plus grand point fixe revient à identifier programmes logiques et définitions co-inductives et, puisque les dérivations sont avant tout des preuves, il semble pertinent d'envisager cette correspondance plus en profondeur en identifiant les dérivations (finies et infinies) et les termes du Calcul des Constructions (de type inductif et co-inductif) : il s'agit là d'un plongement superficiel des dérivations de la programmation logique dans le Calcul des Constructions. Pour ce faire, les clauses vont être considérées comme des signatures fonctionnelles de constructeurs de preuves. Cette comparaison permet de mettre en évidence les phénomènes d'incomplétude observés dans les approches existantes et montre que pour la classe des dérivations infinies sur le domaine des termes finis, il existe une correspondance directe entre dérivations (SLD) et preuves (par co-induction). Dans cette section, nous nous intéressons donc à la cohérence interne entre deux théories (programmation logique et définitions co-inductives).

## SLD-résolution et (Co-)induction

Rappelons qu'un ensemble peut être défini (co-)inductivement à l'aide d'un ensemble $\Phi$ de constructeurs de la forme $e \leftarrow E$ où $e$ est l'élément construit à partir d'un ensemble d'objets $E$. Dans le cas d'une définition inductive, l'ensemble ainsi défini, noté $\text{Ind}(\Phi)$, correspond à l'intersection de tous les ensembles $\Phi$-clos (i.e., les ensembles $A$ vérifiant pour chaque constructeur $e \leftarrow E$ de $\Phi$, $E \subseteq A \Rightarrow e \in A$) et contient tous les éléments obtenus en appliquant un nombre fini de fois les constructeurs. Dans le cas d'une définition co-inductive, l'ensemble défini, noté $\text{Colnd}(\Phi)$, correspond à l'union de tous les ensembles $\Phi$-denses (i.e., les ensembles $A$ tels que pour tout $a \in A$ il existe un ensemble $E \subseteq A$ tel que $a \leftarrow E$ est un constructeur de $\Phi$) et contient tous les éléments obtenus en appliquant un nombre de fois éventuellement infini les constructeurs. De manière équivalente, ces ensembles peuvent être définis à partir d'un opérateur monotone $T_{\Phi}$ défini à partir de $\Phi$ par :

$$ \mathcal{B} = \bigcup_{e \leftarrow E \in \Phi} \{\{e\} \cup E\} \qquad T_{\Phi}(A) = \{e \in \mathcal{B} \mid \exists e \leftarrow E \in \Phi \ E \subseteq A\} \quad (B.4) $$

On a alors $\text{Ind}(\Phi) = \cap_{T_{\Phi}(A) \subseteq A} A$ et $\text{Colnd}(\Phi) = \cup_{A \subseteq T_{\Phi}(A)} A$. Ces deux ensembles correspondent respectivement au plus petit point fixe ($\text{lfp}(T_{\Phi})$) et au plus grand point fixe ($\text{gfp}(T_{\Phi})$) de $T_{\Phi}$.

Définitions inductives et programmes logiques présentent de nombreuses similitudes. Un programme défini $P$ peut être vu comme un ensemble de constructeurs $[P]$ correspondant aux instances fermées (i.e., sans variables) des clauses de $P$. L'opérateur $T_{[P]}$ associé à cet ensemble de constructeurs, comme indiqué en (B.4), correspond exactement à l'opérateur de "conséquence immédiate" (traditionnellement noté $T_P$). D'autre part, une interprétation de Herbrand $I$ est un modèle de $P$ ssi $T_P(I) \subseteq I$, ou en d'autres termes, ssi $I$ est $T_{[P]}$-clos. Enfin, le plus petit modèle de Herbrand $M_P$ est défini comme l'intersection de tous les modèles de Herbrand ce qui, en termes de définitions inductives, revient à définir la dénotation de $P$ par l'ensemble $\text{Ind}([P]) = \text{lfp}(T_{[P]})^4$. Aussi, plutôt qu'un simple outil technique, les définitions inductives constituent une alternative naturelle au paradigme "logic programs as first-order theories". C'est cette idée qui est défendue par G.Huet [57] et L.C.Paulson et

<footnote n="4">⁴De plus, on a $\text{lfp}(T_{[P]}) = T_{[P]}^{\uparrow\omega}$ car le corps de chaque clause est fini, et donc, en termes de définitions inductives, $[P]$ est finitaire.</footnote>
<figure><img src="image_14.png" /><figcaption>FIG. B.1 – Chemin entre deux sommets d’un graphe orienté</figcaption></figure>

A.W.Smith [103, 57] et utilisée avec profit par P.Deransart et J.Maluszynski [35]. Cette lecture sémantique de la programmation logique permet de considérer un programme défini, non plus comme une théorie du premier ordre, mais comme la définition d'une "nouvelle logique". En adoptant ce point de vue, la dénotation d'un programme correspond à l'ensemble des théorèmes qu'il est possible de dériver à partir de cette logique. Cette approche conduit donc à identifier un programme à une définition inductive ou co-inductive, selon que l'on considère ou non les dérivations infinies. Malheureusement, cette identification n'est plus aussi fructueuse lors de la définition d'une sémantique pour les dérivations infinies. En effet, envisageons à présent plus en profondeur le paradigme "logic programs as co-inductive definitions". Pour cela, considérons les clauses C de la forme $A \leftarrow A_1, \dots, A_n$, en suivant l'isomorphisme de Curry-Howard, comme des signatures fonctionnelles de constructeurs de preuve (qui associent à partir des preuves $\pi_{A_i}$ des $A_i$ une preuve $\pi_A$ de A, A correspond alors au type du $\lambda$-terme $\pi_A$) et comparons les preuves représentées par les dérivations SLD avec celles représentées par des $\lambda$-termes. Avant de mener cette comparaison, rappelons qu'un $\lambda$-terme de preuve établissant une proposition $\phi$ peut être défini de manière récursive, et donc utiliser récursivement la preuve de $\phi$, sous certaines conditions. Il s'agit de la notion de "preuve gardée" introduite par T. Coquand dans le contexte de la théorie des types :

[26] In order to establish that a proposition $\phi$ follows from other propositions $\phi_1, \dots, \phi_q$, it is enough to build a proof term $e$ for it, using not only natural deduction, case analysis, and already proven lemmas, but also using the proposition we want to prove recursively, provided such a recursive call is guarded by introduction rules.

Cette condition syntaxique garantit le caractère "productif" d'une classe de $\lambda$-termes. Puisqu'à chaque transition d'une dérivation, une clause (i.e., un constructeur) est appliquée, les dérivations peuvent être vues comme des preuves "gardées". Voyons cela sur l'exemple typique du programme de la figure B.1 permettant de caractériser les chemins d'un graphe orienté. L'existence d'un cycle dans ce graphe rend possible la construction d'une dérivation infinie à partir de la requête $path(s_1, s_2)$ où $s_1$ est un sommet apparaissant sur un cycle et $s_2$ est un sommet quelconque. Par exemple, on a :

$$ 
\begin{array}{l@{\quad}c@{\quad}c@{\quad}c@{\quad}c@{\quad}c@{\quad}c}
\mathbf{path}(a, x) & \xrightarrow{c2} & \mathbf{edge}(a, y_1), \mathbf{path}(y_1, x) & \xrightarrow{a1} & \mathbf{path}(b, x) & & \\
& \xrightarrow{c2} & \mathbf{edge}(b, y_2), \mathbf{path}(y_2, x) & \xrightarrow{a2} & \mathbf{path}(c, x) & \quad (B.5) & \\
& \xrightarrow{c2} & \mathbf{edge}(c, y_3), \mathbf{path}(y_3, x) & \xrightarrow{a3} & \mathbf{path}(a, x) & \rightarrow \dots &
\end{array}
$$
Il est possible de construire le $\lambda$-terme $\pi_{ax}$ de type $\forall x \mathbf{path}(a, x)$ (qui vérifie bien la condition de garde puisque l'appel récursif à $\pi_{ax}$ est bien "gardé" par c2) correspondant à la dérivation (B.5) :

$$ \pi_{ax} := \lambda x. c2(a, b, x, a1, c2(b, c, x, a2, c2(c, a, x, a3, \pi_{ax}(x)))) $$

Les six premières transitions de la dérivation correspondent aux six applications des constructeurs, tandis que l'appel récursif correspond à la suite de la dérivation<fnref n="5" />. Un tel $\lambda$-terme peut être vu comme la définition récursive de la suite des clauses appliquées dans la dérivation et vice versa (néanmoins, il existe des dérivations infinies pour lesquelles cette suite de clauses n'est pas toujours calculable). Il existe donc bien une correspondance directe entre dérivations et $\lambda$-termes lorqu'aucun terme infini apparaît : les dérivations infinies qui ne construisent aucun terme infini correspondent à des preuves par co-induction. En présence de termes infinis, cette correspondance n'est plus immédiate : reprenons l'exemple du programme (B.2), vu comme une définition co-inductive. Il est alors possible de prouver, par co-induction, que la liste, notée from(k), des entiers consécutifs à partir de k vérifie bien LN(k, from(k)). Or, pour construire le $\lambda$-terme correspondant, il est nécessaire de disposer de cette liste définie<fnref n="6" /> par :

$$ \mathit{from} := \lambda n. \mathit{cons}(n, \mathit{from}(S(n))) $$

Le $\lambda$-terme s'écrit alors :

$$ \begin{align*} \pi_{LN} &:= \lambda n. \mathit{eq\_ind}(\begin{array}{@{}l@{}} \mathit{cons}(n, \mathit{from}(S(n))), \\ \qquad \lambda u. \mathit{LN}(n, u), \\ \qquad C(n, \mathit{from}(S(n)), \pi_{LN}(S(n))), \\ \qquad \mathit{from}(n), \\ \qquad \mathit{from\_unfold}(n) \end{array}) \end{align*} $$

où from\_unfold est la preuve de la proposition :

$$ \forall n \mathit{from}(n) = \mathit{cons}(n, \mathit{from}(S(n))) $$

et où eq\_ind correspond au schéma d'élimination de l'égalité (i.e., égalité à la Leibnitz) et associe une preuve de $P(y)$ à partir d'un élément $x$, d'un prédicat $P$, d'une preuve de $P(x)$, d'un élément $y$ et d'une preuve de $x = y$. La définition de ce terme est bien gardée puisque l'appel récursif à $\pi_{LN}$ est protégé par le constructeur $C$. On voit donc bien sur cet exemple que le $\lambda$-terme ne reflète pas le processus de construction de la liste infinie (dérivation (B.3)) : prouver par co-induction LN(k, from(k)) revient à appliquer une infinité de fois le constructeur de preuve $C$ en utilisant à chaque appel récursif la propriété from\_unfold.

<footnote n="5">⁵Un phénomène "rassurant" peut cependant être observé si l'on rajoute un argument au prédicat path correspondant à la longueur du chemin qui sépare les deux sommets considérés : dans ce cas, la longueur du chemin séparant le sommet $a$ du sommet $d$ est $S^\omega$ (la longueur du chemin considéré correspond à la longueur de la preuve de l'existence d'un chemin).</footnote>

<footnote n="6">⁶La définition de from est gardée puisque from est protégé par le constructeur cons. L'utilisation de termes infinis dans l'univers du discours revient à considérer une définition co-inductive pour les termes (les symboles de fonction sont les constructeurs).</footnote>
## Sémantique complète pour les dérivations infinies sur un domaine de termes finis

La lecture sémantique de la programmation logique présentée ci-dessus et dans [62, 64, 63, 65] m'a permis de définir une sémantique valide et complète pour les dérivations infinies qui ne construisent pas de termes infinis. Plus formellement, ces dérivations sont définies comme suit.

**Définition B.1** Une SLD-preuve sur le domaine des termes finis est soit une réfutation, soit une dérivation infinie équitable<fnref n="7" /> : $R_0 \xrightarrow{C_1,\theta_1} R_1 \to \dots \to R_{i-1} \xrightarrow{C_i,\theta_i} R_i \to \dots$ telle que $\forall k \ge 0 \ \exists p > k \ \forall q \ge p \ \theta_q \dots \theta_p \dots \theta_{k+1} R_k \approx \theta_p \dots \theta_{k+1} R_k$.

où $\approx$ dénote la relation d'équivalence au renommage près des variables. L'information calculée par ces dérivations doit donc l'être en un nombre fini d'étapes (i.e., pour chaque requête $R$ apparaissant dans la dérivation, il existe un certain rang à partir duquel la suite des instanciations de $R$ par les unificateurs est stationnaire).

Les propriétés de cette classe de dérivations s'établissent en identifiant un programme $P$ par l'ensemble de constructeurs défini par :

$$[P] = \{ \theta C \mid C \in P, \theta : X \to T_{\Sigma}[X] \}$$

qui correspondent aux instances (pouvant contenir des variables) des clauses du programme. Les résultats de validité et de complétude prouvés s'énoncent alors comme suit.

### Proposition B.1

- (Validité). Si il existe une SLD-preuve sur le domaine des termes finis :

$$A_1, \dots, A_n \xrightarrow{C_1, \theta_1} R_1 \to \dots \to R_{i-1} \xrightarrow{C_i, \theta_i} R_i \to \dots$$

à partir du programme $P$, alors il existe $k \ge 0$ tel que pour tout $i$ ($1 \le i \le n$) $\theta_k \dots \theta_1 A_i \in \text{Colnd}(\lceil P \rceil)$.

- (Complétude). Etant donné un programme $P$, si $A \in \text{Colnd}(\lceil P \rceil)$, alors il existe une SLD-preuve sur le domaine des termes finis à partir de $A$ avec le programme $P$ :

$$A \xrightarrow{C_1, \sigma_1} R'_1 \to \dots \to R'_{i-1} \xrightarrow{C_i, \sigma_i} R'_i \to \dots$$

telle que pour tout $i \ge 1$, $\sigma_i A = A$.

La propriété de complétude fournit ici une contre-partie opérationnelle du plus grand point fixe de $T_{\lceil P \rceil}$.

Les approches existantes dans la définition d'une sémantique pour les programmes logiques qui ne terminent pas sont exclusivement dédiées à la caractérisation d'objets infinis et aboutissent à une sémantique valide mais non complète. L'approche que j'ai suivie prend le parti opposé puisqu'elle ne s'applique qu'aux dérivations ne construisant aucun terme infini. Il s'agit là d'une restriction sur les dérivations qui a permis d'établir une sémantique valide et complète. Quoi qu'il en soit, la définition d'une sémantique pour

<footnote n="7">⁷Rappelons qu'une dérivation est équitable si elle échoue ou si pour tout atome $A$ y apparaissant, $A$ ou l'un de ses résidus est sélectionné en un nombre fini d'étapes.</footnote>
(toutes) les dériva\c{c}ions infinies ne connait pas encore de solution générale. Néanmoins,
les dériva\c{c}ions infinies sur le domaine des termes finis semblaient constituer un obstacle
à la complétude des approches existantes et les résultats présentés ici contribuent à une
meilleure compréhension du problème.
# Annexe C

## Pratique des méthodes formelles

### C.1 Changement de représentation

#### C.1.1 Réutilisation de preuves : définition d'isomorphismes au sein du langage de spécification

Dans la section B.1, nous avons présenté une formalisation de l'unification de termes du premier ordre. Toutefois, plutôt que de construire cette preuve formelle en suivant une approche classique (basée sur l'algorithme d'unification) et puisqu'une preuve formelle similaire avait été construite par J. Rouyer [115] pour un ensemble plus général, l'ensemble des quasi-termes, nous avons transposé la propriété d'unification, déjà établie, de l'ensemble des quasi-termes vers l'ensemble des termes. Il s'agissait donc de mettre en relation l'ensemble sur lequel porte la preuve cherchée avec le sous-ensemble correspondant de l'ensemble des quasi-termes, et de prouver la conservation du résultat. La principale difficulté provient de l'utilisation de fonctions partielles dans le formalisme du système Coq dans lequel seules les fonctions totales sont représentables.

#### Unification de quasi-termes

Afin d'illustrer leur technique de synthèse de programmes [88], Z. Manna et R.J. Waldinger ont dérivé l'algorithme d'unification à partir de la preuve de la “satisfaisabilité” des spécifications du problème de l'unification [87]. Cette preuve avait été formalisée par L.C. Paulson [102] dans le système LCF [46] mais porte sur un sur-ensemble de l'ensemble des termes. Un développement similaire a été effectué par J. Rouyer [115], avec la version 5.8 du système Coq. Cette version ne permettant pas les définitions d'ensembles mutuellement inductifs, la transcription de la définition exacte des termes, dans le calcul des constructions inductives, par la définition d'un type inductif de type ensemble (Set), ne fut pas possible. En effet, un terme de la forme $f(t_1, \dots, t_n)$ est construit à partir d'un symbole de fonction $f$ d'arité $n$ et d'une liste de termes $\ell$ de longueur $n$. Cependant, en utilisant la définition polymorphe des listes, la position du type TERM dans la définition d'un constructeur de type $\Sigma \to \text{list}(\text{TERM}) \to \text{TERM}$ correspond à une occurrence non positive de TERM [101]. Or, il n'est pas permis pour un objet $A$ d'être défini inductivement à l'aide d'un constructeur dans lequel $A$ n'apparaît pas positivement. De plus, le contrôle de l'arité des symboles fonctionnels ne peut se faire sans utiliser un type dépendant, ce
qui ne permettait pas l'extraction de programmes. Une structure de données intermédiaire plus générale regroupant termes et listes de termes en un seul type, correspondant à l'ensemble $Q_Σ[X]$ des quasi-termes, avait alors été définie par J.Rouyer en supprimant de la définition des termes tout ce qui est "contrôle" pour ne conserver que les notions "construktives". L'ensemble $Q_Σ[X]$ est donc défini inductivement à l'aide des quatre constructeurs suivants :

$$ V: X \to Q_Σ[X] \quad \text{Root: } Σ \to Q_Σ[X] \to Q_Σ[X] $$

$$ C: Σ \to Q_Σ[X] \quad \text{ConsArg: } Q_Σ[X] \to Q_Σ[X] \to Q_Σ[X] $$

V et C sont utilisés pour les variables et les constantes, Root permet d'obtenir des quasi-termes fonctionnels et ConsArg est utilisé pour construire des listes (non vides) de quasi-termes, correspondant aux arguments des symboles de fonction apparaissant dans les quasi-termes fonctionnels. Cependant, certains quasi-termes ne correspondent pas à des termes : c'est le cas des quasi-termes de la forme $\text{ConsArg}(q_1, q_2)$ et des quasi-termes pour lesquels le nombre des arguments associés à un symbole de fonction $f$ est différent de l'arité de $f$. De manière similaire, certains quasi-termes ne correspondent pas à des listes de termes, comme par exemple le quasi-terme $\text{ConsArg}(\text{ConsArg}(x, x), x)$.

## Définition de fonctions partielles

Dans les deux développements de L.C. Paulson et J. Rouyer, la propriété d'unification n'est pas obtenue directement sur l'ensemble des termes mais sur des structures de données plus générales. Toutefois, il existe une bijection entre un sous-ensemble de $Q_Σ[X]$ et l'ensemble des termes et il est possible de définir un prédicat caractérisant les quasi-termes "compatibles" avec la notion de termes. Afin de transposer la propriété d'unification vers l'ensemble des termes, il est nécessaire de définir une fonction ayant pour domaine un sous-ensemble de $Q_Σ[X]$ caractérisé par ce prédicat. Une telle restriction, sur le domaine d'une fonction, n'est pas permise dans le Calcul des Constructions. Les problèmes liés à la définition de telles fonctions dans des systèmes comme Coq, qui n'incorporent pas la notion de partialité, sont discutés par C. Dubois et V. Viguié Donzeau-Gouge dans [36].

Nous esquissons ici les deux techniques que nous avons utilisées pour représenter une fonction partielle permettant d'obtenir un terme à partir de certains quasi-termes dans le système Coq. A partir de deux ensembles, $E_1$ (quasi-termes) et $E_2$ (termes), définis inductivement, et d'un prédicat $P$ sur $E_1$, tel qu'il existe une bijection entre le sous-ensemble $E_1^P = \{e \in E_1 | P(e)\}$ de $E_1$ et $E_2$, on souhaite construire deux fonctions reliant $E_1^P$ et $E_2$. Les deux caractéristiques de ce problème sont :

- Le sous-ensemble $E_1^P$ est caractérisé par un prédicat, ce qui empêche toute définition "directe" de fonction ou de prédicat sur $E_1^P$ (ainsi, les formules $\forall e_1 \in E_1^P \varphi$ devront se lire $\forall e_1 \in E_1(P(e_1) \Rightarrow \varphi)$).

- On ne dispose pas de la bijection, mais seulement de la preuve de son existence, cette bijection est caractérisée via une relation $\equiv$ définie sur $E_1 \times E_2$ et vérifiant :

$$ \forall e_1 \in E_1^P (\exists e_2 \in E_2 (e_1 \equiv e_2 \wedge (\forall e'_2 \in E_2 (e_1 \equiv e'_2 \Rightarrow e'_2 = e_2)))) $$

$$ \forall e_2 \in E_2 (\exists e_1 \in E_1 (e_1 \equiv e_2 \wedge (\forall e'_1 \in E_1 (e'_1 \equiv e_2 \Rightarrow e'_1 = e_1)))) $$

On cherche à construire les deux fonctions $f_{12}$ et $f_{21}$ telles que :

$$ f_{12}: E_1^P \to E_2 \quad \forall e_1 \in E_1^P \quad e_1 \equiv f_{12}(e_1) $$

$$ f_{21}: E_2 \to E_1 \quad \forall e_2 \in E_2 \quad f_{21}(e_2) \equiv e_2 $$
La fonction $f_{21}$ se construit directement, puisqu'elle peut s'appliquer à l'ensemble $E_2$ tout entier, et vérifie $\forall e_2 \in E_2 P(f_{21}(e_2))$. La définition de $f_{12}$ est plus délicate, puisqu'elle est définie sur un ensemble caractérisé par un prédicat. Les deux solutions considérées pour la définition de $f_{12}$ consistent à considérer simultanément un élément de $E_1$ et la preuve qu'il satisfait bien le prédicat<fnref n="1" /> $P$.

La première solution repose sur l'utilisation de la règle d'élimination de la proposition False :

$$ \text{forall } P : \text{Set, False} \rightarrow P $$

qui permet d'envisager la définition de la fonction cherchée comme l'écriture d'un programme qui prend un argument $e_1$ satisfaisant une pré-condition $P$ et qui peut donc produire un résultat quelconque si son argument ne satisfait pas $P$ puisqu'un tel cas n'est pas possible (on dispose d'une preuve de $P(e_1)$) : en adoptant cette approche "langage de programmation", le résultat est construit à partir de son argument $e_1$ sachant qu'il vérifie forcément le prédicat $P$.

La deuxième solution consiste à exploiter non plus l'élément $e_1$, mais la preuve qu'il satisfait bien le prédicat $P$. Toutefois, puisque $P$ est un prédicat sur $E_1$ ($P: E_1 \rightarrow \text{Prop}$) et puisque $E_2$ est de type Set, il n'est pas possible de définir une fonction $f_{12}$ en considérant la structure de $P(e_1)$ : cela reviendrait utiliser un objet non informatif (i.e. sans contenu calculatoire) pour construire un objet informatif. Cette approche "langage de preuves" consiste donc à construire inductivement, pour tout élément $e_1$ de $E_1^P$, l'ensemble $P[e_1]$ des preuves de $P(e_1)$ ($P: E_1 \rightarrow \text{Set}$). Même si $P[e_1]$ et $P(e_1)$ semblent équivalents d'un point de vue logique, ils ne sont pas équivalents d'un point de vue "calculatoire". Une fois cet ensemble construit, l'utilisation de types dépendants permet de définir la fonction :

$$ f_{12} : \prod_{e_1 \in E_1} (P[e_1] \rightarrow E_2) $$

Cette fonction est définie récursivement sur la structure d'une preuve et permet de prendre en compte le contenu algorithmique d'une telle preuve. La fonction ainsi construite doit vérifier :

$$ \forall e_1 \in E_1 \quad \forall p \in P[e_1] \quad e_1 \equiv f_{12}(e_1, p) $$

Pour simplifier, on notera $p[e]$ la preuve de $P(e)$ et on écrira simplement $f_{12}(p[e_1])$ pour $f_{12}(e_1, p)$. Ces définitions permettent de considérer des preuves comme des objets d'une collection mathématique et donc de mener des raisonnements par induction sur ces preuves ou bien de construire des fonctions récursives sur ces preuves.

## Transposition de propriétés

Afin d'établir la propriété d'unification sur l'ensemble des termes à partir de la preuve de cette propriété sur l'ensemble des quasi-termes, il suffit maintenant de montrer que les

<footnote n="1">¹Afin de considérer l'ensemble $E_1$ tout entier (plutôt que $E_1^P$) comme domaine de la fonction $f_{12}$, nous pouvons ajouter à $E_2$ un élément "artificiel" et définir $E_2' = E_2 \cup \{\text{meaningless}\}$. La fonction $f_{12}$ vérifierait alors $f_{12}(e_1) = \text{meaningless}$ pour tous les éléments $e_1$ de $E_1$ ne satisfaisant pas le prédicat $P$. Mais cette solution ne fait que déplacer le problème.</footnote>
<figure><img src="image_15.png" /><figcaption>FIG. C.1 – Transposition de propriétés formelles</figcaption></figure>

fonctions entre termes et quasi-termes préservent la propriété d'unification. Replaçons nous dans le cadre plus général du paragraphe précédent. Puisque $E_2$ et un sous-ensemble de $E_1$ sont isomorphes, nous souhaitons transposer une propriété exprimée sur $E_1$ vers $E_2$. Considérons deux propriétés formelles $U_1$ (quasi-unification) et $U_2$ (unification), respectivement sur $E_1$ et $E_2$, telles que :

$$ \forall o_1, \dots, o_n \in E_1^P \quad U_1(o_1, \dots, o_n) \Rightarrow U_2(f_{12}(p[o_1]), \dots, f_{12}(p[o_n])) $$

Supposons que $E_1$ vérifie $U_1$ et montrons la propriété $U_2$ sur $E_2$. La preuve est obtenue en conduisant le raisonnement suivant (figure C.1). Soit $e_1, \dots, e_n$ des éléments de $E_2$, par hypothèse, on a $U_1(f_{21}(e_1), \dots, f_{12}(e_n))$ et puisque chaque $f_{21}(e_i)$ admet une preuve $p[e_i]$ de $P(f_{21}(e_i))$ dans $\mathcal{P}[f_{21}(e_i)]$, on a alors $U_2(f_{12}(f_{21}(p[e_1]), \dots, f_{12}(f_{21}(p[e_n]))). Or $f_{12}(f_{21}(p[e_i])) = e_i$ ce qui prouve la propriété $U_2$ pour les éléments de $E_2$.

### C.1.2 Réutilisation de preuves : Outil externe de transformation de preuves

L'atelier Focal a été utilisé pour construire une large bibliothèque de calcul formel [112]. L'intérêt principal du calcul formel par rapport aux méthodes numériques est de donner des résultats exacts, sans erreur d'arrondi. Mais le calcul formel perd beaucoup de son intérêt si ces résultats ne sont pas fiables. En effet, comme tous les programmes, les programmes de calcul formel sont sujets à des erreurs d'implantation qui peuvent provenir soit d'une
incorrection mathématique, soit d'une mauvaise interprétation de la sémantique. Dans le domaine du calcul formel, les spécifications mathématiques sont issues de l'algèbre classique et les propriétés sont souvent des théorèmes bien connus. Certains d'entre eux ont déjà été formalisés dans un autre cadre, soit dans Coq, soit dans un autre système comme Mizar, PVS, Theorema, etc. Il est évidemment intéressant de comprendre comment réutiliser toutes ces preuves dans le cadre de Focal. Il s'agit donc de faire "communiquer" deux assistants à la preuve dans le but de faire bénéficier l'un des preuves implantées par l'autre. Pour cela, il nous faut tout d'abord mieux cerner ce que peut signifier le mot réutilisation. Une preuve s'appuie sur un énoncé, effectué dans un cadre logique précis, mais également sur certains choix de présentation des données. Par exemple, alors que les structures mathématiques implantées dans la bibliothèque de calcul formel de Focal sont paramétrées par une relation d'équivalence, la majorité des développements existants en Coq utilisent l'égalité syntaxique, qui est une forme plus contrainte d'égalité, sans toutefois utiliser dans les preuves les propriétés plus fortes que cette relation vérifie. S'agit-il alors de réutiliser uniquement la preuve d'une propriété sur une structure particulière ou bien peut-on envisager de généraliser une preuve afin qu'elle corresponde à la preuve cherchée ? Nous présentons ici, au travers d'un exemple sur les groupes, le développement d'un outil permettant d'une part de généraliser une preuve en la paramétrant par une relation d'équivalence et un ensemble de propriétés que doit vérifier cette relation (il s'agit essentiellement de propriétés de congruence) et d'autre part de réutiliser cette preuve dans l'environnement Focal.

## Implantation des groupes dans les systèmes Coq et Focal

La notion de groupe est implantée dans les systèmes Coq et Focal. Toutefois, ces deux développements utilisent une représentation différente de l'égalité.

L'implantation avec Coq, obtenue par P. Castéran [21], repose sur l'égalité de Leibniz, implantée au coeur du système Coq. L'égalité de Leibniz, aussi appelée égalité propositionnelle, est caractérisée par les deux axiomes suivants où $=A$ dénote l'égalité propositionnelle sur le type $A$ :

$$ \forall A : \mathbf{Set} \quad \forall x : A \quad x =_A x \\ \forall A : \mathbf{Set} \quad \forall P : (A \to \mathbf{Prop}) \quad \forall x, y : A \quad x =_A y \Rightarrow (P x) \Rightarrow (P y) $$

En Coq, l'égalité est définie de manière inductive comme la plus petite relation binaire réflexive :

$$ \text{Inductive eq [A/Set;x:A]: A -> Prop := refl_equal : (eq A x x).} $$

et le schéma d'élimination (spécialisé au cas des prédicats non dépendants) associé à cette définition correspond au deuxième axiome cité ci-dessus. On établit aisément que la relation ainsi définie est symétrique et transitive. Une des principales propriétés de cette égalité est que toute fonction $f$ de $A$ dans $B$ préserve eq :

$$ f_{\text{equal}} : \forall A, B : \mathbf{Set} \quad \forall f : A \to B \quad \forall x, y : A \quad x =_A y \Rightarrow (f x) =_B (f y) $$

P. Castéran [21] fournit deux représentations différentes de la notion de groupe dans le système Coq :

- Un groupe additif est défini comme un ensemble non vide muni d'une loi de composition interne $\oplus$ associative, admettant un élément neutre 0, telle que chaque élément admette un opposé pour $\oplus$.
- Un groupe additif est défini comme un ensemble $E$ non vide muni d'une loi de composition interne $\oplus$ telle que pour tout $x$ dans $E$, les deux fonctions $f_x = (\lambda y : E. x \oplus y)$ et $g_x = (\lambda y : E. y \oplus x)$ soient surjectives.

P. Castéran montre alors l'équivalence de ces deux représentations.

L'implantation des groupes avec Focal repose exclusivement sur l'égalité des setoïdes. Un setoïde est défini comme un ensemble non vide muni d'une relation d'équivalence $\doteq$. Si $St_A$ (resp. $St_B$) est un setoïde construit sur le type $A$ (resp. $B$) et la relation d'équivalence $\doteq_A$ (resp. $\doteq_B$), un morphisme de setoïdes de $St_A$ dans $St_B$ est une fonction $f$ de $A$ dans $B$ qui préserve l'égalité, c'est-à-dire qui vérifie la propriété de compatibilité :

$$f_{\text{comp}} : \forall x, y : A \quad x \doteq_A y \Rightarrow (f x) \doteq_B (f y)$$

Tandis qu'avec l'égalité de Leibniz, toute fonction $f : A \to B$, définissable dans le système Coq, préserve l'égalité à travers la propriété $f_{\text{equal}}$, un terme $f$ de type $A \to B$ est un morphisme de setoïdes si et seulement si il est accompagné d'une preuve de compatibilité $f_{\text{comp}}$. Dans le système Focal, un groupe additif est défini comme un ensemble non vide muni d'une relation d'équivalence $\doteq$ et d'une loi de composition interne $\oplus$ associative, admettant un élément neutre 0, telle que $\doteq$ soit une congruence pour $\oplus$ et telle que chaque élément admette un opposé pour $\oplus$.

## Schéma de réutilisation

Afin de faire bénéficier le développement Focal des résultats prouvés dans le système Coq, nous avons développé un schéma de réutilisation composé de deux parties distinctes (voir figure C.1.2).

La première partie a pour but de transformer une preuve utilisant l'égalité de Leibniz en une preuve utilisant une égalité de setoïde. Passer de l'égalité de Leibniz à celle des setoïdes revient à généraliser l'égalité de Leibniz en une relation d'équivalence particulière qui satisfait la propriété de compatibilité de toutes les opérations sur son domaine. De nombreuses propriétés de compatibilité alors engendrées ne sont pas utilisées dans les preuves à réutiliser et l'étape de généralisation portera uniquement sur les propriétés $I_1, \dots, I_n$ dont on a réellement besoin. Alors que ces propriétés correspondent à des instances de la propriété de Leibniz dans le développement initial, elles devront être prouvées lors de la généralisation.

La transformation de la preuve que nous avons effectuée lors de cette étape repose sur les tactiques de "réécriture" associées aux relations d'égalité considérées. Deux tactiques du système Coq sont directement concernées par l'égalité. La tactique Rewrite du système Coq permet de mettre en œuvre la propriété de Leibniz eq_ind. Etant donné un but courant à prouver dans un contexte dans lequel figure en hypothèse le terme $h : (y = x)$, l'application de la tactique Rewrite $h$ permet de remplacer $y$ par $x$ dans le but courant. La tactique Replace $t_1$ with $t_2$ permet de remplacer les occurrences d'un terme $t_1$ par un terme $t_2$ dans un but et engendre un but supplémentaire qui consiste à prouver l'égalité $t_1 = t_2$. Lorsque la preuve en cours de construction met en jeu des setoïdes et des morphismes de setoïdes, il n'est plus possible d'utiliser ces tactiques : seules les propriétés de réflexivité, symétrie et transitivité qui définissent les relations d'équivalence ainsi que les propriétés de compatibilité des morphismes ($f_{\text{comp}}$) peuvent être appliquées. Afin de pouvoir réutiliser
<figure><img src="image_16.png" /><figcaption>FIG. C.2 – Schéma de réutilisation</figcaption></figure>

des preuves en Coq reposant sur l'égalité de Leibniz, dans le contexte des preuves en Focal reposant sur la notion de setoïde, il est nécessaire de disposer de tactiques sur les setoïdes similaires aux tactiques Rewrite et Replace. Dans [111], C. Renard propose un module d'extension Coq, qui permet de manipuler les égalités des setoïdes avec de nouveaux outils qui se comportent de façon analogue aux outils de l'égalité du système Coq. A l'aide de ce développement, il devient possible de déclarer un setoïde en fournissant le terme A de type Set ou Type correspondant au type des éléments du setoïde, la relation eqA de type A $\rightarrow$ A $\rightarrow$ Prop correspondant à la relation d'égalité considérée et le terme StA de type setoïde contenant une preuve que la relation eqA est bien une relation d'équivalence. Il devient également possible de définir un morphisme f en fournissant la preuve de la propriété de compatibilité de f. L'algorithme qui engendre l'obligation de preuve relative à la propriété de compatibilité est décrit dans [111]. La seule contrainte imposée au terme f est de ne pas contenir de produit dépendant. L'extension proposée par C.Renard fournit alors deux tactiques de réécriture sur les setoïdes Setoid_rewrite et Setoid_replace : si eq est une égalité de setoïde, la tactique Setoid_rewrite appliquée à un terme de la forme (eq t₁ t₂) remplace toute occurrence du terme t₁ par le terme t₂ à condition que dans le but courant toutes les opérations "traversées" soient des morphismes. Munis de ces nouvelles tactiques, nous pouvons alors définir un mécanisme de généralisation de preuves. Ce mécanisme procède comme suit :

1. La définition d'une relation d'équivalence sur l'ensemble E considéré est introduite.

2. Chaque occurrence de l'égalité (de Leibniz) = dans le développement Coq est remplacée par une occurrence de l'égalité de setoïde =S.

3. Les propriétés de congruence sont introduites pour les opérations que l'on souhaite
considérer comme des morphismes de setoïde.

4. Les trois tactiques Reflexivity, Symmetry et Transitivity H sont remplacées, dans les scripts de preuve, par les applications des propriétés de réflexivité, de symétrie et de transitivité établies pour la relation =S. De même, les occurrences (Rewrite H) et (Replace m with n) sont remplacées par les tactiques équivalentes (Setoid_rewrite H) et (Setoid_replace m with n).

Ainsi, le prototype réalisé automatise la généralisation de l'égalité de Leibniz au sein d'un développement Coq.

La seconde partie du schéma de réutilisation a pour but d' "encapsuler" un terme de preuve Coq de manière à l'utiliser comme preuve dans le système Focal. Ceci se traduit par la définition d'une tactique de preuve Focal qui se fonde sur la compilation en Coq d'une spécification Focal. Syntaxiquement, la tactique de réutilisation prend la forme :

{* Reuse (theoreme\_Coq instances). *}

et se place à l'endroit où la preuve est attendue. Le terme *theoreme\_Coq* est le théorème Coq à réutiliser. Les termes $t_1, ..., t_n$ désignés par *instances* correspondent à des termes Coq. Ce morceau de code Focal est compilé en un lemme Coq : le script généré com-mence par procéder à l'introduction des dépendances de déclarations et des paramètres puis applique la tactique *Exact* (*theoreme\_Coq* $t_1 t_2 ... t_n$). Les termes $t_1 t_2 ... t_n$ men-tionnés font référence directement aux objets manipulés par la spécification Coq obtenue par compilation. Pour utiliser cette tactique il faut donc connaître assez précisément cette traduction ou du moins quelques correspondances simples à établir et quasi-syntaxiques. Une des perspectives de ce travail est de proposer une syntaxe qui permettrait de relier les paramètres du théorème Coq à instancier avec les objets de la spécification Focal.

Le schéma de réutilisation proposé ici a été utilisé pour prouver dans l'atelier Focal quatre des résultats prouvés sur les groupes par P. Castéran dans le système Coq. Nous avons ainsi obtenu une spécification des groupes dans le système Focal mettant en jeu les deux propriétés de surjectivité présentées plus haut. La principale difficulté de ce travail provient du fait que la preuve à réutiliser est exprimée à l'aide d'un langage de tactiques.

La réutilisation de développements formels pose des problèmes difficiles – tant du point de vue théorique que du point de vue technique – et les perspectives de ce travail sont nom-breuses. Concernant l’outil présenté dans cette section, et au delà de l’aspect réutilisation, un tel outil devrait également permettre d’apporter une information sur la preuve réutili-sée, en fournissant les hypothèses sur la relation d’égalité qui sont réellement utilisées. À plus long terme, il serait intéressant d’étudier la réutilisation de manière plus approfondie. Plusieurs directions sont possibles :

- Plusieurs représentations équivalentes d'un même objet peuvent coexister et les pro-blèmes de changement de représentation méritent d'être étudiés plus en profondeur, tant d'un point de vue pratique, comme dans [86], que d'un point de vue théorique, comme dans [11].

- Abstraire un concept dans une preuve pour l'instancier de manière différente – comme nous l'avons fait pour la notion d'égalité – nécessite une étude plus poussée et une comparaison avec d'autres travaux comme par exemple le développement présenté dans [77].
- Un piste plus ambitieuse concerne la "communication" entre divers outils de développements formels. Ici encore, des problèmes théoriques se posent (il s'agit de faire "coïncider les logiques mises en jeu") [56, 95] et la mise en pratique pose également des problèmes "techniques" [27, 96, 41, 31].

### C.1.3 Preuves dans un architecture hiérarchique

Dans cette section, nous présentons une étude sur la réutilisation de preuves formelles dans le cadre de l'environnement Focal. Focal fournit un langage fonctionnel muni de traits objets avec lequel on peut écrire des spécifications, des programmes et des preuves. Les preuves portent sur des objets susceptibles d'être redéfinis lors de l'héritage. La possibilité de redéfinir une fonction pose cependant un problème puisque les preuves qui garantissent que la fonction redéfinie est conforme à sa spécification sont alors invalidées. Dans ce contexte, la question de la place des preuves dans la hiérarchie du graphe d'héritage se pose alors : faut-il prouver les spécifications au niveau le plus abstrait (au risque de devoir refaire les preuves en cas de redéfinition), ou bien faut-il prouver les spécifications au niveau le plus bas (au risque de devoir dupliquer les preuves) ? Cette question n'admet pas de réponse générale. Nous tentons ici de donner des critères sur la structure du code considéré pour répondre à cette question et nous esquissons une méthodologie de développement permettant de limiter l'impact des redéfinitions sur les preuves. Ce travail est détaillé dans [109].

#### Preuves invalidées par le mécanisme de redéfinition

Une preuve en Focal est soit un script Coq interprété dans le contexte de l'espèce où la propriété est prouvée, soit une preuve, contenant plus ou moins de détails, écrite en Cutter, le langage déclaratif sur lequel est basé le démonstrateur automatique Zenon. Il existe deux moyens d'introduire une preuve en Focal : soit en définissant un théorème, soit en démontrant une propriété déjà déclarée. L'une des formes syntaxiques possibles est la suivante :

```text
theorem T : theoreme
proof : [def : def Dep1 ... def Depn] ;
        [decl : decl Dep1 ... decl Depn] ;
        preuve ;
```

Les termes $def\_dep_k$ désignent les noms des méthodes définies (directement dans l'espèce ou par héritage) et les termes $decl\_dep_k$ désignent les méthodes déclarées. Le mot-clé `decl` indique que la preuve du théorème T dépend uniquement des types des méthodes `decl\_dep1`, ..., `decl\_depn`. En revanche, elle dépend également de la définition des méthodes `def\_dep1`, ..., `def\_depn`. Ces indications de dépendances explicitent donc de manière claire le contexte de la preuve<fnref n="2" />.

Lorsqu'une redéfinition de fonction invalide les preuves qui dépendent de cette définition, le compilateur demande à l'utilisateur de les refaire. Le choix de la place des preuves

<footnote n="2">²Dans Focal, certaines caractéristiques de la programmation orientée-objet ont été limitées afin d'éviter des constructions non correctes, par exemple la récursion ouverte qui peut mener à des incohérences lorsqu'elle est mal utilisée.</footnote>
dans la hiérarchie et la méthodologie de développement sont donc importants afin de limiter le nombre de preuves invalidées. Nous essayons ici d'éclairer ces choix et de les illustrer au travers d'un exemple. Considérons l'espèce Setoid contenant les méthodes suivantes :

<table><caption>ESPÈCE Setoid</caption><thead><tr><td>méthode</td><td>nom</td><td>type</td><td>définition</td></tr></thead><tbody><tr><td>déclarée</td><td>=</td><td>self → self → bool</td><td></td></tr><tr><td>déclarée</td><td>eq_refl</td><td>∀x ∈ self x = x</td><td></td></tr><tr><td>déclarée</td><td>eq_sym</td><td>∀x, y ∈ self x = y ⇒ y = x</td><td></td></tr><tr><td>déclarée</td><td>eq_trans</td><td>∀x, y, z ∈ self x = y ⇒ y = z ⇒ x = z</td><td></td></tr></tbody></table>

ainsi que les deux espèces définies dans la table C.1. Dans cette présentation des espèces, self désigne le type d'un élément de l'espèce, et and et not sont les opérateurs classiques sur les booléens. L'espèce Setoid représente la notion de setoïde, elle ne contient que des

<table><caption>ESPÈCE PartialOrder (hérite de l'espèce Setoid)</caption><thead><tr><td>méthode</td><td>nom</td><td>type</td><td>définition</td></tr></thead><tbody><tr><td>déclarée</td><td>≤</td><td>self → self → bool</td><td></td></tr><tr><td>déclarée</td><td>le_refl</td><td>∀x ∈ self x ≤ x</td><td></td></tr><tr><td>déclarée</td><td>le_asym</td><td>∀x, y ∈ self<br>x ≤ y ⇒ y ≤ x ⇒ x = y</td><td></td></tr><tr><td>déclarée</td><td>le_trans</td><td>∀x, y, z ∈ self<br>x ≤ y ⇒ y ≤ z ⇒ x ≤ z</td><td></td></tr><tr><td>définie</td><td>&lt;</td><td>self → self → bool</td><td>x &lt; y := x ≤ y and x ≠ y</td></tr><tr><td>définie</td><td>T</td><td>∀x, y ∈ self<br>x ≤ y ⇒ (x &lt; y ∨ x = y)</td><td>def : &lt;, decl : ≤<br>...preuve...</td></tr></tbody></table>

<table><caption>ESPÈCE OrderedSet (hérite de l'espèce PartialOrder)</caption><thead><tr><td>méthode</td><td>nom</td><td>type</td><td>définition</td></tr></thead><tbody><tr><td>déclarée</td><td>P</td><td>∀x, y ∈ self x ≤ y ∨ y ≤ x</td><td></td></tr><tr><td>définie</td><td>=</td><td>hérite de Setoid</td><td>x = y := x ≤ y and y ≤ x</td></tr><tr><td>définie</td><td>eq_refl<br>eq_sym<br>eq_trans</td><td>hérite de Setoid</td><td>def : =, decl : ...<br>...preuve...</td></tr><tr><td>redéfinie</td><td>&lt;</td><td>hérite de PartialOrder</td><td>x &lt; y := not y ≤ x</td></tr><tr><td>redéfinie</td><td>T</td><td>hérite de PartialOrder</td><td>def : &lt;, decl : ≤<br>...preuve...</td></tr></tbody></table>

<caption>TAB. C.1 – Définition des espèces PartialOrder et OrderedSet</caption>

méthodes déclarées. L'espèce PartialOrder hérite de l'espèce Setoid et correspond à la notion d'ordre partiel. Elle déclare une méthode $≤$ ainsi que les propriétés qui établissent que cette méthode correspond à un ordre partiel. Elle définit de plus une méthode $<$ correspondant à l'ordre strict associé à $≤$ et définit également une méthode T correspondant à une preuve d'une propriété reliant $≤$ et $<$. L'espèce OrderedSet hérite de l'espèce PartialOrder et correspond à la notion d'ordre total. Elle déclare la propriété P qui établit que $≤$ est une relation d'ordre totale et s'appuie sur cette propriété pour redéfinir la méthode $<$
afin d'en donner une implantation plus efficace. La preuve définissant la méthode T dans l'espèce *PartialOrder* est donc invalidée puisqu'elle dépend de la définition de <. Elle est donc redéfinie. D'autre part, l'espèce *OrderedSet* définit les méthodes =, eq_refl, eq_sym et eq_trans, seulement déclarées jusqu'alors. Cet exemple illustre une situation où une preuve est invalidée suite à la redéfinition d'une méthode. Si l'on considère uniquement la hiérarchie contenant ces trois espèces, il est clair que la preuve du théorème T développée dans l'espèce *PartialOrder* est inutile puisqu'aucune autre espèce hérite de *PartialOrder*. Une première indication pour déterminer la place d'une preuve au sein de la hiérarchie est donc donnée par la réponse à la question “existe-t-il des espèces qui héritent de la méthode dans laquelle figure la preuve et qui ne redéfinissent pas l'objet sur lequel porte la preuve ?”. Evidemment, dans le cas d'une réponse négative, cette preuve est inutile et il peut être intéressant de la différer. Toutefois, ce seul critère n'est pas satisfaisant puisqu'il préjuge des développements futurs basés sur la hiérarchie considérée.

Si le problème du choix de la place d'une preuve au sein d'une hiérarchie n'admet pas de
solution générale, il est en revanche possible d'adopter une méthodologie de développement
permettant de minimiser le nombre de preuves invalidées. Cette méthodologie procède en
trois temps. Elle consiste à déclarer, puis spécifier et enfin implanter chaque méthode intro-
duite<fnref n="3" />. Si l'on considère l'exemple précédent, la méthode < est seulement implantée (elle
n'est pas spécifiée) et n'a donc pas été introduite en respectant cette méthodologie. Les
définitions des espèces PartialOrder et OrderedSet obtenues en adoptant la méthodologie
proposée sont données dans la table C.2. La méthode < est seulement déclarée et spécifiée
par la méthode spec dans l'espèce PartialOrder. La méthode T ne dépend donc plus de la
définition de < mais seulement du type de la méthode spec. La définition de < est alors
introduite dans l'espèce OrderedSet et permet de définir la méthode spec. Cette preuve
dépend bien sûr de la définition de <. Toutefois, comme on le voit sur cet exemple, la mé-
thode T est insensible aux éventuelles redéfinitions de < qui n'invalideront que la méthode
spec. En suivant cette approche, les preuves de résultats “généraux” ne dépendent donc
que des spécifications des fonctions de base et ne sont pas invalidées lors de la redéfinition
de ces fonctions.

La méthodologie de développement suggérée ici peut être adaptée lorsque le développe-
ment à réutiliser n'a pas été obtenu en respectant les étapes successives de déclaration, de
spécification et d'implantation. En effet, dans ce cas, pour chaque preuve invalidée par le
mécanisme de redéfinition, il suffit d'ajouter une spécification pour chaque méthode définie
dont la preuve invalidée dépend. Il faut d'autre part modifier les indications de dépendances
de cette preuve en remplaçant les dépendances aux méthodes définies par des dépendances
aux spécifications de ces méthodes. La démarche est donc similaire à celle de la méthodo-
logie proposée : il s'agit de minimiser le nombre de dépendances aux définitions et pour
cela de trouver un ensemble de spécifications “minimales” pour chaque méthode définie de
manière à ce que les redéfinitions invalident les preuves les plus “simples” possibles.

<footnote n="3">³On peut noter que l'on retrouve dans ce schéma "nommer, spécifier, implanter" la démarche habituellement préconisée dans le développement logiciel sous la dénomination de "cycle en V". Cette méthode est d'ailleurs prescrite dans certaines normes comme la norme CEI61508.</footnote>
<table><caption>ESPÈCE PartialOrder (hérite de l'espèce Setoid)</caption><thead><tr><th>méthode</th><th>nom</th><th>type</th><th>définition</th></tr></thead><tbody><tr><td>déclarée</td><td>≤</td><td>self → self → bool</td><td></td></tr><tr><td>déclarée</td><td>le_refl</td><td>∀x ∈ self x ≤ x</td><td></td></tr><tr><td>déclarée</td><td>le_asym</td><td>∀x, y ∈ self<br>x ≤ y ⇒ y ≤ x ⇒ x = y</td><td></td></tr><tr><td>déclarée</td><td>le_trans</td><td>∀x, y, z ∈ self<br>x ≤ y ⇒ y ≤ z ⇒ x ≤ z</td><td></td></tr><tr><td>déclarée</td><td>&lt;</td><td>self → self → bool</td><td></td></tr><tr><td>déclarée</td><td>spec</td><td>∀x, y ∈ self x &lt; y ⇔ (x ≤ y ∧ ¬(x = y))</td><td></td></tr><tr><td>définie</td><td>T</td><td>∀x, y ∈ self<br>x ≤ y ⇒ (x &lt; y ∨ x = y)</td><td>decl :≤, spec<br>...preuve...</td></tr></tbody></table>

<table><caption>ESPÈCE OrderedSet (hérite de l'espèce PartialOrder)</caption><thead><tr><th>méthode</th><th>nom</th><th>type</th><th>définition</th></tr></thead><tbody><tr><td>déclarée</td><td>P</td><td>∀x, y ∈ self x ≤ y ∨ y ≤ x</td><td></td></tr><tr><td>définie</td><td>=</td><td>hérite de Setoid</td><td>x = y := x ≤ y and y ≤ x</td></tr><tr><td>définie</td><td>eq_refl<br>eq_sym<br>eq_trans</td><td>hérite de Setoid</td><td>def : =, decl : ...<br>...preuve...</td></tr><tr><td>définie</td><td>&lt;</td><td>hérite de PartialOrder</td><td>x &lt; y := not y ≤ x</td></tr><tr><td>définie</td><td>spec</td><td>hérite de PartialOrder</td><td>def : &lt;, decl :≤<br>...preuve...</td></tr></tbody></table>

<caption>TAB. C.2 – Déclarer, Spécifier, puis Implanter</caption>

## C.2 Un cadre générique pour la spécification de formalismes logiques

Afin de faciliter la spécification formelle, il est souhaitable, lorsque c'est possible, de développer ces spécifications au sein d'un cadre générique. Lorsque ce cadre existe déjà, il permet d'assister la spécification en rendant possible cette spécification par assemblage de "briques formelles" convenablement instanciées.

Dans cette section, nous présentons une implantation dans le système Coq d'un cadre formel destiné à assister la spécification et l'implémentation de "logiques". Nous considérons l'implantation dans le système Coq d'une variante de la notion de logiques générales introduite par J. Meseguer [91, 44]. Le développement obtenu a été utilisé pour implanter la logique des propositions et la logique équationnelle. Ce travail est décrit en détail dans [66].

### C.2.1 Spécification d'un cadre générique

La notion de logique générale permet d'abstraire les notions de syntaxe, de sémantique et de preuve d'une logique particulière :

- Syntaxiquement, une logique introduit un langage, défini par une collection {$S_i$} de
signatures (les symboles), une collection {$\sigma$} de morphismes entre certaines signatures, une collection {$\mathcal{F}_i$} de formules construites sur {$S_i$} et une collection {$\bar{\sigma}$} de morphismes étendant {$\sigma$} aux ensembles de formules.

- Les aspects sémantiques, capturés par la notion d'institution introduite par J.A.Goguen et R.M. Burstall [44], sont définis par une collection {$\mathcal{M}_i$} de modèles de {$S_i$}, d'une collection d'applications {$U_\sigma$} qui, pour chaque morphisme $\sigma: S_i \to S_j$, permet de transformer chaque modèle de $S_j$ en un modèle de $S_i$, et d'une collection {$\models_i$} de relations de satisfaction entre modèles et formules sur une signature.

- Les aspects "preuves" sont définis par une collection {$\vdash_i$} de relations de déduction permettant de caractériser les formules qu'il est possible de déduire à partir d'ensembles de formules.

A ces définitions s'ajoute un ensemble de propriétés qui pourront être réutilisées lors de la spécification d'une logique particulière. Tout d'abord, au niveau sémantique, la notion d'institution est accompagnée de la définition de la "condition de satisfaction" qui stipule que la notion de vérité induite par la relation de satisfaction est préservée par les changements de notations représentés par les morphismes. Plus formellement, cette propriété s'écrit :

$$ \forall \sigma: S_i \to S_j \quad \forall \varphi: \mathcal{F}_i \quad \forall M: \mathcal{M}_j \quad (U_\sigma(M) \models_i \varphi \Leftrightarrow M \models_j \bar{\sigma}(\{\varphi\})) $$

Une propriété similaire, appelée propriété de translation, est également introduite pour la relation de déduction : s'il existe un morphisme $\sigma: S_i \to S_j$, alors, pour tout ensemble $\Gamma$ de formules construites sur $S_i$ et pour toute formule $\varphi$ aussi construite sur $S_i$, si $\Gamma \vdash_i \varphi$ alors $\bar{\sigma}(\Gamma) \vdash_j \bar{\sigma}(\{\varphi\})$. A ce niveau, les propriétés de réflexivité, de transitivité et de monotonie de la relation $\vdash_i$ sont aussi formellement spécifiées. Jusqu'à présent les notions d'institutions et de systèmes de déduction, même si elles partagent une partie "syntaxe" commune, sont indépendantes. Les propriétés de validité et de complétude garantissent la cohérence entre ces deux volets d'une logique.

$$ \text{Validité} \quad \forall n: \mathbb{N} \quad \forall \varphi: \mathcal{F}_n \quad \forall \Gamma \quad \Gamma \vdash_n \varphi \Rightarrow (\forall M: \mathcal{M}_n M \models_n \Gamma \Rightarrow M \models_n \varphi) $$

$$ \text{Compléture} \quad \forall n: \mathbb{N} \quad \forall \varphi: \mathcal{F}_n \quad \forall \Gamma \quad (\forall M: \mathcal{M}_n M \models_n \Gamma \Rightarrow M \models_n \varphi) \Rightarrow \Gamma \vdash_n \varphi $$

Toutes ces définitions permettent de spécifier ce qu'est une logique générale : c'est la donnée d'une syntaxe, d'une institution et d'un système de déduction correct relativement à l'institution. On obtient ainsi une "brique formelle" paramétrée qui, une fois instanciée, permet la définition d'une logique particulière (figure C.3). Les définitions formelles que nous avons implantées dans le système Coq diffèrent un peu de celles que l'on peut trouver dans la littérature sur les logiques générales [91, 44]. En effet, notre objectif est de fournir un cadre le plus souple possible pour la spécification formelle de logiques pour l'informationique – en vue, par exemple, de la conception d'un langage de spécifications dédié à un domaine particulier. Par exemple, afin d'alléger notre formalisation, nous ne nous sommes pas placés dans le cadre de la théorie des catégories pour formaliser les notions de signatures et de morphismes entre signatures et par conséquent nous n'imposons ni l'existence d'un morphisme identité sur chaque signature, ni la propriété de composition des morphismes. D'autre part, les institutions qui pourront être définies dans notre cadre ne doivent pas nécessairement satisfaire la condition de satisfaction. En effet, on veut que certaines logiques qui ne satisfont pas cette condition – comme certaines logiques observables/raffinement – puissent être obtenues dans notre cadre. Par contre, nous imposons
<figure><img src="image_17.png" /><figcaption>FIG. C.3 – Logiques générales</figcaption></figure>

la propriété de correction pour une logique, qui n’est pas nécessairement requise dans les définitions originales.

### C.2.2 Instanciations

S'il est très général, le cadre défini ci-dessus n'est pas toujours facilement utilisable directement et il convient parfois de définir de nouvelles "briques formelles" intermédiaires entre le cadre et l'objet à formaliser. Ces nouvelles "briques formelles", également réutilisables, permettent d'automatiser certains aspects de la spécification. Par exemple, en pratique, les relations de déduction sont généralement définies à partir de systèmes formels constitués de règles de déduction. Aussi, nous avons défini une "brique formelle" réutilisable pour spécifier un système formel quelconque. Les paramètres de cette brique sont un alphabet $A$, un ensemble de formules $\mathbb{F}$ et un prédicat $\mathbb{R}$ caractérisant les instances des règles du système. Deux prédicats sont alors définis : le premier, noté $\mathcal{T}_{\mathbb{SF}}$, correspond à la notion de formules théorèmes qu'il est possible de dériver $via$ une preuve arborescente à partir d'un ensemble de formules, le second, noté $\vdash$, correspond à la notion de déduction qui caractérise les formules qu'il est possible de dériver $via$ une preuve "linéaire" (représentée par liste de formules) à partir d'un ensemble de formules. Ces deux prédicats sont prouvés équivalents ($\varphi \in \mathcal{T}_{\mathbb{SF}}[\Gamma] \Leftrightarrow \Gamma \vdash \varphi$) ce qui permet à l'utilisateur de choisir la forme de ses dérivaitions tout en pouvant passer d'une forme à l'autre. D'autre part, les propriétés de réflexivité, de transitivité et de monotonie de $\vdash$ sont prouvées. Enfin les spécifications formelles des propriétés de cohérence, de décidabilité, de saturation et d'indépendance des axiomes ainsi que les propriétés de validité et de complétude relativement à un ensemble de formules donné sont spécifiées. A partir de la "brique formelle" ainsi obtenue, nous avons défini un "pont formel" (figure C.4) qui permet de définir la partie "preuve" d'une logique générale à partir d'un système formel. La relation $\vdash$ correspond alors à la relation de déduction $\vdash$ du système formel. L'utilisation de ce "pont formel" permet de transposer automatiquement les propriétés de réflexivité, de transitivité et de monotonie sans avoir à les reprouver.
<figure><img src="image_18.png" /><figcaption>FIG. C.4 – Relations de déductions définies à partir de systèmes formels</figcaption></figure>

L'utilisation des deux briques formelles présentées a permis de définir complètement deux instances de logique générale : la logique des propositions et la logique équationnelle. Chacun de ces deux développements a été obtenu en suivant le même schéma d'assemblage de "briques formelles" illustré par la figure C.5. Toutefois, ce schéma d'assemblage ne présume en rien du style à adopter pour instancier sa propre logique : l'utilisateur peut développer sa propre logique avec le style qui lui convient, il suffit ensuite qu'il enrobe ses définitions. C'est par exemple ce qui a été fait lors de la définition des systèmes formels. Une des perspectives de ce travail consiste à définir une collection d'enrobages génériques.
<figure><img src="image_19.png" /><figcaption>FIG. C.5 – Définition d'une logique par assemblage</figcaption></figure>
# Annexe D

## Contrôle d'accès

Nous détaillons ici les résultats décrits dans le chapitre 2, et illustrons les concepts introduits à l'aide de modèles classiques de contrôle d'accès.

### D.1 Modèles de contrôle d'accès

#### D.1.1 Exemples de Politiques de contrôle d'accès

Dans le chapitre 2, nous avons défini une politique de contrôle d'accès $\mathbb{P}[\rho]$, basée sur un paramètre de sécurité $\rho$, par un quintuplet $\mathbb{P}[\rho] = (S, O, A, \Sigma, \Omega)$ où $S$ est un ensemble non vide de sujets, $O$ est un ensemble d'objets, $A$ est un ensemble de modes d'accès, $\Sigma$ est l'ensemble des états du système sur lequel la politique est mise en œuvre et $\Omega$ est le prédicat de sécurité définissant les états sûrs. Nous présentons ici la formalisation de quatre politiques classiques de contrôle d'accès qui nous serviront d'exemples par la suite.

##### Politique HRU

La politique HRU [51] est simplement spécifiée par un ensemble $m_D$ d'accès autorisés. Selon que l'on autorise ou non cet ensemble à évoluer durant la vie du système, cet ensemble peut être vu comme un paramètre de sécurité ou comme une fonction de sécurité. Evidemment, il peut être souhaitable de permettre la modification de cet ensemble par certains utilisateurs (et dans certaines conditions). La formalisation de la politique HRU que nous donnons ici considère donc $m_D$ comme une fonction de sécurité et ne spécifie aucun paramètre de sécurité. Un état peut donc être représenté par une paire $(m, m_D)$ où $m$ désigne l'ensemble des accès courants. On note $\Sigma_{HRU}$ l'ensemble des états. Le prédicat de sécurité $\Omega_{HRU}$ définit un état sûr comme un état pour lequel chaque accès courant est autorisé :

$$ \forall \sigma = (m, m_D) \in \Sigma_{HRU} \quad \Omega_{HRU}(\sigma) \Leftrightarrow m \subseteq m_D $$

On note $\mathbb{P}_{HRU}[\cdot] = (S, O, A, \Sigma_{HRU}, \Omega_{HRU})$ la politique ainsi définie.

##### Politique RBAC

La politique à base de rôles que nous formalisons ici correspond à la version RBAC96 [117]. Chaque utilisateur du système est associé à un ensemble de rôles qu'il peut endosser, et
chaque rôle est associé à un ensemble de permissions. Cette politique est paramétrée par un triplet $\rho_{RBAC} = (U, R, \leq_R)$ où $U$ est un ensemble d'utilisateurs (ici la notion de sujets est distincte de celle d'utilisateurs), et $R$ est un ensemble de rôles muni d'un ordre partiel $\leq_R$. Les fonctions de sécurité sont user, UA, PA et roles, où user : $S \to U$ permet de connaître l'utilisateur associé à un sujet, UA $\subseteq U \times R$ est une relation permettant de spécifier les rôles autorisés des utilisateurs, PA $\subseteq (O \times A) \times R$ est une relation permettant d'associer des permissions (c'est-à-dire des paires $(o, a) \in O \times A$) aux rôles et roles : $S \to \wp(R)$ spécifie l'ensemble des rôles activés par un sujet. Un état est donc représenté par un quintuplet $(m, user, UA, PA, roles)$ où $m$ désigne l'ensemble des accès courants. On note $\Sigma_{RBAC}$ l'ensemble des états. Un état $\sigma = (m, user, UA, PA, roles)$ vérifie le prédicat $\Omega_{RBAC}$ ssi les deux conditions suivantes sont satisfaites :

$$ \forall s \in S \quad \text{roles}(s) \subseteq \text{ER}(s, UA) $$

$$ \forall s \in S \quad \forall o \in O \quad \forall a \in A \quad (s, o, a) \in m \Rightarrow (o, a) \in \text{EP}(s, PA, \text{roles}) $$

où, étant donné un sujet $s \in S$, $\text{ER}(s, UA)$ définit l'ensemble des rôles que $s$ peut activer en respectant UA et $\leq_R$, et $\text{EP}(s, PA, roles)$ désigne l'ensemble des permissions associées au rôles activés par $s$ et à leurs sous-rôles :

$$ \text{ER}(s, UA) = \{r \in R \mid \exists r' \in R \ r \leq_R r' \wedge (\text{user}(s), r') \in UA\} $$

$$ \text{EP}(s, PA, roles) = \bigcup_{r \in \text{roles}(s)} \left\{ (o, a) \in (O \times A) \mid \begin{array}{l} \exists r'' \in R \ r'' \leq_R r \\ \wedge ((o, a), r'') \in \text{PA} \end{array} \right\} $$

On note $\mathbb{P}_{RBAC}[\rho_{RBAC}] = (S, O, A, \Sigma_{RBAC}, \Omega_{RBAC})$ la politique ainsi définie.

## Politique de Bell et LaPadula

La politique de Bell et LaPadula [12] repose sur une notion de niveaux de sécurité. Elle est donc paramétrée par un treillis $\rho_{BLP} = (\mathcal{L}, \leq, \Upsilon, \lambda)$. Chaque sujet et chaque objet est associé à un niveau de sécurité au moyen des fonctions de sécurité $f_s : S \to \mathcal{L}$ et $f_o : O \to \mathcal{L}$. Un état est donc représenté par un triplet $(m, f_s, f_o)$ où $m$ désigne l'ensemble des accès courants. On note $\Sigma_{BLP}$ l'ensemble des états. Le prédicat de sécurité $\Omega_{BLP}$ est défini par les deux propriétés spécifiées en (1.1) et (1.2). On note $\mathbb{P}_{BLP}[\rho_{BLP}] = (S, O, A, \Sigma_{BLP}, \Omega_{BLP})$ la politique ainsi définie.

## Politique de la Muraille de Chine

Dans le contexte de la politique de la Muraille de Chine [19], chaque objet du système appartient à une compagnie, et chaque compagnie appartient à une classe de conflit d'intérêt. Il existe en outre une classe spéciale de conflit d'intérêt, avec seulement une compagnie, contenant les informations "sanitisées" (c'est-à-dire publiques). Ces informations peuvent être lues par n'importe quel sujet, quels que soient les autres accès effectués par ce dernier. L'idée intuitive de cette politique est que les sujets peuvent accéder à de l'information tant que cette dernière n'est pas en conflit avec de l'information qu'ils possèdent déjà. Cette politique est paramétrée par un quintuplet $\rho_{CW} = (\mathbb{C}, \mathbb{E}, f_{\mathbb{C}}, c_0, d_0)$ où $\mathbb{C} = \{c_1, c_2, \dots, c_n\}$ est un ensemble de classes de conflit d'intérêt et $\mathbb{E}$ est un ensemble de compagnies. Chaque compagnie $d$ est associée à une classe de conflit d'intérêt $c_i = f_{\mathbb{C}}(d)$. Notons qu'à partir
d'une telle fonction $f_{\mathbb{C}} : \mathbb{E} \to \mathbb{C}$, il est possible de construire une fonction $f_{\mathbb{E}} : \mathbb{C} \to \wp(\mathbb{E})$ telle que $f_{\mathbb{E}}(c) = \{d \mid f_{\mathbb{C}}(c) = d\}$. Cette fonction associe à chaque classe de conflit un ensemble de compagnies. Les informations "sanitisées" peuvent être considérées comme apportant à la compagnie $d_0$, de la classe de conflit particulière $c_0$. Un état est représenté par une paire $(m, f_o)$ où $m$ désigne l'ensemble des accès courants et $f_o : \mathcal{O} \to \mathbb{E}$ est une fonction de sécurité associant à chaque objet une compagnie. On note $\Sigma_{CW}$ l'ensemble des états. Un état $\sigma = (m, f_o)$ vérifie le prédicat de sécurité $\Omega_{CW}$ ssi les deux conditions suivantes sont vérifiées :

$$ 
\begin{array}{l}
\forall s \in \mathcal{S} \ \forall o_1, o_2 \in \mathcal{O} \ \forall a_1, a_2 \in \mathcal{A} \\
\quad (s, o_1, a_1) \in m \wedge (s, o_2, a_2) \in m \Rightarrow f_o(o_1) = f_o(o_2) \vee f_{\mathbb{C}}(f_o(o_1)) \neq f_{\mathbb{C}}(f_o(o_2)) \\
\\
\forall s \in \mathcal{S} \ \forall o_1, o_2 \in \mathcal{O} \\
\quad (s, o_1, \mathsf{write}) \in m \wedge (s, o_2, \mathsf{read}) \in m \Rightarrow f_o(o_2) = d_0 \vee f_o(o_1) = f_o(o_2)
\end{array}
$$

La première propriété exprime que si un sujet accède à deux objets, alors soit ces objets appartiennent à la même compagnie, soit ces objets appartiennent à des objets associés à des classes de conflit différentes. La deuxième propriété exprime que dès que l'on accède en écriture à un objet, les seuls accès en lecture qui sont permis sont ceux qui portent sur des objets "sanitisés" ou appartenant à la compagnie de l'objet sur lequel un accès en écriture est effectué. Cette propriété exprime également que lorsque plusieurs objets associés à des classes de conflit différentes sont accédés en écriture, les seuls objets accessibles en lecture sont alors les objets de la compagnie $d_0$. On note $\mathbb{P}_{CW}[\rho_{CW}] = (\mathcal{S}, \mathcal{O}, \mathcal{A}, \Sigma_{CW}, \Omega_{CW})$ la politique ainsi définie.

A partir de ces définitions on montre le lemme suivant.

### Lemme D.1

1. $\mathbb{P}_{HRU}[]$, $\mathbb{P}_{RBAC}[\rho_{RBAC}]$, $\mathbb{P}_{BLP}[\rho_{BLP}]$ et $\mathbb{P}_{CW}[\rho_{CW}]$ sont des politiques compactes.

2. $\mathbb{P}_{HRU}[]$ et $\mathbb{P}_{RBAC}[\rho_{RBAC}]$ sont des politiques libres.

3. $\mathbb{P}_{BLP}[\rho_{BLP}]$ et $\mathbb{P}_{CW}[\rho_{CW}]$ ne sont pas des politiques libres.

## D.1.2 Modèles et implantations

### Définitions et propriétés

Dans le chapitre 2, un modèle a été défini comme la donnée d'une paire $M[\rho] = (\mathbb{P}[\rho], \mathcal{R})$ et d'une sémantique pour l'ensemble $\mathcal{R}$ de requêtes. Une implantation de $M[\rho] = (\mathbb{P}[\rho], \mathcal{R})$ est une paire $(\tau, \Sigma_I)$ où $\Sigma_I$ est un ensemble d'états initiaux, où $\tau : \mathcal{R} \times \Sigma \to \mathcal{D} \times \Sigma$ est une fonction de transition, et où $\mathcal{D} = \{\text{yes}, \text{no}\}$ est un ensemble de réponses.

On note $\Gamma_{\tau}(E)$ l'ensemble des états du système atteignables à partir d'un état appartenant à l'ensemble E en appliquant un nombre fini de fois la fonction $\tau$. De plus, on associe à toute implantation un ensemble de séquences d'états correspondant aux traces des exécutions qu'elle engendre :

$$ \mathrm{Exec}(\tau, \Sigma_I) = \bigcup_{n \in \mathbb{N}} \left\{ (\sigma_1, \dots, \sigma_n) \mid \begin{array}{l} \sigma_1 \in \Sigma_I \\ \wedge \quad \forall i (1 \le i \le n-1) \exists R \in \mathcal{R} \exists d \in \mathcal{D} \\ \quad \tau(R, \sigma_i) = (d, \sigma_{i+1}) \end{array} \right\} $$
Les propriétés de correction d'une implantation concernent essentiellement les propriétés de sécurité induites par le prédicat Ω et les propriétés relatives à la sémantique du langage de requêtes :

- $(\tau, \Sigma_I)$ est dite $\mathbb{P}[\rho]$-correcte (resp. $\mathbb{P}[\rho]$-complète) ssi tout état atteignable est sûr (resp. ssi tout état sûr est atteignable) :

$$ \Gamma_{\tau}(\Sigma_I) \subseteq \Sigma|_{\Omega} \quad (\text{resp. } \Sigma|_{\Omega} \subseteq \Gamma_{\tau}(\Sigma_I)) $$

- $\tau$ est dite $\mathbb{R}^+\text{-correcte}$ (resp. $\mathbb{R}^+\text{-correcte}$) ssi :

$$ \begin{array}{l} \forall \sigma_1, \sigma_2 \in \Sigma \ \forall R \in \mathcal{R} \ \tau(R, \sigma_1) = (\text{yes}, \sigma_2) \Rightarrow (R, \sigma_2) \in \mathbb{R}^+\text{-correcte} \\ (\text{resp. } \forall \sigma_1, \sigma_2 \in \Sigma \ R \in \mathcal{R} \ \tau(R, \sigma_1) = (\text{yes}, \sigma_2) \Rightarrow (\sigma_1, R, \sigma_2) \in \mathbb{R}^+\text{-correcte}) \end{array} $$

- $\tau$ est dite $\mathcal{W}$-conforme ssi :

$$ \begin{array}{l} \forall \sigma_1, \sigma_2 \in \Sigma \ \forall d \in \mathcal{D} \ \forall R \in \mathcal{R} \\ \tau(R, \sigma_1) = (d, \sigma_2) \Rightarrow \\ \quad \left( \begin{array}{l} d = \text{yes} \Rightarrow \left( \begin{array}{l} R \in \mathcal{R}^{\ominus} \Rightarrow \mathcal{W}(\sigma_1) \subseteq \mathcal{W}(\sigma_2) \\ \wedge R \in \mathcal{R}^{\ominus} \Rightarrow \mathcal{W}(\sigma_2) \subseteq \mathcal{W}(\sigma_1) \end{array} \right) \\ \wedge d = \text{no} \Rightarrow \mathcal{W}(\sigma_2) \subseteq \mathcal{W}(\sigma_1) \end{array} \right) \end{array} $$

On écrira $\mathbb{M}[\rho] \vdash (\tau, \Sigma_I)$ lorsque l'implantation $(\tau, \Sigma_I)$ du modèle $\mathbb{M}[\rho]$ est à la fois $\mathbb{P}[\rho]$-correcte et $\mathbb{R}^+\text{-correcte}$ (resp. et $\mathbb{R}\text{-correcte}$ et $\mathcal{W}$-conforme).

Nous introduisons également les deux propriétés supplémentaires suivantes :

- Etant donnée une relation d'équivalence $\equiv$ sur les états, $\tau$ est dite $\equiv$-préservante, ce que l'on note $\equiv \vdash \tau$, ssi :

$$ \begin{array}{l} \forall \sigma_1, \sigma_2, \sigma'_1, \sigma'_2 \in \Sigma \ \forall R \in \mathcal{R} \ \forall d \in \mathcal{D} \\ \left( \begin{array}{l} \sigma_1 \equiv \sigma_2 \\ \wedge \ \tau(R, \sigma_1) = (d_1, \sigma'_1) \wedge \tau(R, \sigma_2) = (d_2, \sigma'_2) \end{array} \right) \Rightarrow \left( \begin{array}{l} \sigma'_1 \equiv \sigma'_2 \\ \wedge \ d_1 = d_2 \end{array} \right) \end{array} $$

- $(\tau, \Sigma_I)$ est dite $\Gamma$-complète ssi :

$$ \forall \sigma_1, \sigma_2 \in \Gamma_{\tau}(\Sigma_I) \quad \Gamma_{\tau}(\sigma_1) = \Gamma_{\tau}(\sigma_2) $$

## Exemples

Nous reprenons ici les politiques introduites dans la section D.1.1 et notons :

$$ \begin{array}{ll} \mathbb{M}_{HRU}^{acc}[\quad] = (\mathbb{P}_{HRU}[\quad], \mathcal{R}^{acc}) & \mathbb{M}_{RBAC}^{acc}[\rho_{RBAC}] = (\mathbb{P}_{RBAC}[\rho_{RBAC}], \mathcal{R}^{acc}) \\ \mathbb{M}_{BLP}^{acc}[\rho_{BLP}] = (\mathbb{P}_{BLP}[\rho_{BLP}], \mathcal{R}^{acc}) & \mathbb{M}_{CW}^{acc}[\rho_{CW}] = (\mathbb{P}_{CW}[\rho_{CW}], \mathcal{R}^{acc}) \end{array} $$

les modèles qui leur sont associés en considérant l'ensemble des requêtes $\mathcal{R}^{acc}$ défini en (2.1) dont la sémantique est présentée dans le chapitre 2. Les fonctions de transition permettant d'implanter ces modèles sont données dans les tables D.1, D.2, D.3 et D.4. On montre que ces fonctions de transition permettent d'obtenir des implantations correctes.

## Lemme D.2

$$ \begin{align*} \Sigma_{HRU}^{I} &\subseteq \Sigma|_{\Omega_{HRU}} &\Rightarrow \mathbb{M}_{HRU}^{acc}[\quad] \vdash (\tau_{HRU}, \Sigma_{HRU}^{I}) \\ \Sigma_{RBAC}^{I} &\subseteq \Sigma|_{\Omega_{RBAC}} &\Rightarrow \mathbb{M}_{RBAC}^{acc}[\rho_{RBAC}] \vdash (\tau_{RBAC}, \Sigma_{RBAC}^{I}) \\ \Sigma_{BLP}^{I} &\subseteq \Sigma|_{\Omega_{BLP}} &\Rightarrow \mathbb{M}_{BLP}^{acc}[\rho_{BLP}] \vdash (\tau_{BLP}, \Sigma_{BLP}^{I}) \\ \Sigma_{CW}^{I} &\subseteq \Sigma|_{\Omega_{CW}} &\Rightarrow \mathbb{M}_{CW}^{acc}[\rho_{CW}] \vdash (\tau_{CW}, \Sigma_{CW}^{I}) \end{align*} $$
<table><caption>TAB. D.1 – Implantation du modèle $M_{HRU}^{acc}$ [ ]</caption><tr><td>τ<sub>HRU</sub>(R, σ) =</td><td><div style="text-align: center;"><span style="display: inline-block; border: 1px solid black; padding: 0 2px;">(yes, σ ⊕ (s, o, a))</span><span style="display: inline-block; border: 1px solid black; padding: 0 2px;">(yes, σ ⊖ (s, o, a))</span><span style="display: inline-block; border: 1px solid black; padding: 0 2px;">(no, σ)</span></div> if R = ⟨+, s, o, a⟩ ∧ (s, o, a) ∈ m<sub>D</sub><br>if R = ⟨−, s, o, a⟩<br>otherwise</td></tr></table>

<table><caption>TAB. D.2 – Implantation du modèle $M_{RBAC}^{acc}$ [ρ<sub>RBAC</sub> ]</caption><tr><td>τ<sub>RBAC</sub>(R, (m, user, UA, PA, roles))</td></tr><tr><td>= <div style="text-align: center;"><span style="display: inline-block; border: 1px solid black; padding: 0 2px;">(yes, (m ∪ {(s, o, a)}, user, UA, PA, roles))</span><span style="display: inline-block; border: 1px solid black; padding: 0 2px;">if R = ⟨+, s, o, a⟩ ∧ (o, a) ∈ EP(s, PA, roles)</span><span style="display: inline-block; border: 1px solid black; padding: 0 2px;">(yes, (m \ {(s, o, a)}, user, UA, PA, roles))</span><span style="display: inline-block; border: 1px solid black; padding: 0 2px;">if R = ⟨−, s, o, a⟩</span><span style="display: inline-block; border: 1px solid black; padding: 0 2px;">(no, (m, user, UA, PA, roles))</span><span style="display: inline-block; border: 1px solid black; padding: 0 2px;">otherwise</span></div></td></tr></table>

<table><caption>TAB. D.3 – Implantation du modèle $M_{BLP}^{acc}$ [ρ<sub>BLP</sub> ]</caption><tr><td>τ<sub>BLP</sub>(R, σ)</td><td>σ = (m, f<sub>s</sub>, f<sub>o</sub>)</td></tr><tr><td>= <div style="text-align: center;"><span style="display: inline-block; border: 1px solid black; padding: 0 2px;">(yes, σ ⊕ (s, o, read))</span><span style="display: inline-block; border: 1px solid black; padding: 0 2px;">if R = ⟨+, s, o, read⟩</span><span style="display: inline-block; border: 1px solid black; padding: 0 2px;">∧ f<sub>o</sub>(o) ≤ f<sub>s</sub>(s) ∧ {o' ∈ O | (s, o', write) ∈ Λ(σ) ∧ ¬(f<sub>o</sub>(o) ≤ f<sub>o</sub>(o'))} = ∅</span><span style="display: inline-block; border: 1px solid black; padding: 0 2px;">(yes, σ ⊕ (s, o, write))</span><span style="display: inline-block; border: 1px solid black; padding: 0 2px;">if R = ⟨+, s, o, write⟩</span><span style="display: inline-block; border: 1px solid black; padding: 0 2px;">∧ {o' ∈ O | (s, o', read) ∈ Λ(σ) ∧ ¬(f<sub>o</sub>(o') ≤ f<sub>o</sub>(o))} = ∅</span><span style="display: inline-block; border: 1px solid black; padding: 0 2px;">(yes, σ ⊖ (s, o, x))</span><span style="display: inline-block; border: 1px solid black; padding: 0 2px;">if R = ⟨−, s, o, x⟩</span><span style="display: inline-block; border: 1px solid black; padding: 0 2px;">(no, σ)</span><span style="display: inline-block; border: 1px solid black; padding: 0 2px;">otherwise</span></div></td></tr></table>

<table><caption>TAB. D.4 – Implantation du modèle $M_{CW}^{acc}$ [ρ<sub>CW</sub> ]</caption><tr><td>τ<sub>CW</sub>(R, (m, f<sub>o</sub>))</td></tr><tr><td>= <div style="text-align: center;"><span style="display: inline-block; border: 1px solid black; padding: 0 2px;">(yes, (m, f<sub>o</sub>))</span><span style="display: inline-block; border: 1px solid black; padding: 0 2px;">if R = ⟨+, s, o, x⟩ ∧ (s, o, x) ∈ m</span><span style="display: inline-block; border: 1px solid black; padding: 0 2px;">(yes, (m ∪ {(s, o, read)}, f<sub>o</sub>))</span><span style="display: inline-block; border: 1px solid black; padding: 0 2px;">if R = ⟨+, s, o, read⟩ ∧ f<sub>o</sub>(o) = d<sub>0</sub></span><span style="display: inline-block; border: 1px solid black; padding: 0 2px;">(yes, (m ∪ {(s, o, read)}, f<sub>o</sub>)</span><span style="display: inline-block; border: 1px solid black; padding: 0 2px;">if R = ⟨+, s, o, read⟩ ∧ f<sub>o</sub>(o) ≠ d<sub>0</sub></span><span style="display: inline-block; border: 1px solid black; padding: 0 2px;">∧ {o' ∈ O | (s, o', write) ∈ m ∧ f<sub>o</sub>(o) ≠ f<sub>o</sub>(o')} = ∅</span><span style="display: inline-block; border: 1px solid black; padding: 0 2px;">∧ {o' ∈ O | (s, o', read) ∈ m ∧ f<sub>o</sub>(o') ≠ f<sub>o</sub>(o)} = ∅</span><span style="display: inline-block; border: 1px solid black; padding: 0 2px;">(yes, (m ∪ {(s, o, write)}, f<sub>o</sub>)</span><span style="display: inline-block; border: 1px solid black; padding: 0 2px;">if R = ⟨+, s, o, write⟩</span><span style="display: inline-block; border: 1px solid black; padding: 0 2px;">∧ {o' ∈ O | (s, o', write) ∈ m ∧ f<sub>o</sub>(o') ≠ f<sub>o</sub>(o)} = ∅</span><span style="display: inline-block; border: 1px solid black; padding: 0 2px;">∧ {o' ∈ O | (s, o', read) ∈ m ∧ f<sub>o</sub>(o) ≠ f<sub>o</sub>(o') ∧ f<sub>o</sub>(o') ≠ d<sub>0</sub>} = ∅</span><span style="display: inline-block; border: 1px solid black; padding: 0 2px;">(yes, (m \ {(s, o, x)}, f<sub>o</sub>)</span><span style="display: inline-block; border: 1px solid black; padding: 0 2px;">if R = ⟨−, s, o, x⟩</span><span style="display: inline-block; border: 1px solid black; padding: 0 2px;">(no, (m, f<sub>o</sub>)</span><span style="display: inline-block; border: 1px solid black; padding: 0 2px;">otherwise</span></div></td></tr></table>
## Préordre sur les implantations

Nous introduisons ici un préordre sur les implantations d'un même modèle lorsque ce modèle repose sur une sémantique faible de l'ensemble des requêtes. Ce préordre nous permettra de comparer deux modèles en limitant le nombre d'implantations à considérer. Nous définissons tout d'abord le préordre $\sqsubseteq_\Gamma$ exprimant qu'une implantation $(\tau_1, \Sigma_I^1)$ est plus restrictive en termes d'états atteignables qu'une implantation $(\tau_2, \Sigma_I^2)$ ssi tout état atteignable par $(\tau_1, \Sigma_I^1)$ l'est également par $(\tau_2, \Sigma_I^2)$. Nous introduisons ensuite le préordre $\sqsubseteq_W$ sur les fonctions de transitions.

$$ \neg (\tau_1, \Sigma_I^1) \sqsubseteq_\Gamma (\tau_2, \Sigma_I^2) \Leftrightarrow \Gamma_{\tau_1}(\Sigma_I^1) \subseteq \Gamma_{\tau_2}(\Sigma_I^2) $$

- Etant données deux fonctions de transition $\tau_1$ et $\tau_2$ de $\mathcal{R} \times \Sigma$ vers $\mathcal{D} \times \Sigma$, $\tau_1 \sqsubseteq_W \tau_2$ ssi :

$$ \begin{array}{l} \forall \sigma, \sigma_1 \in \Sigma \quad \forall R \in \mathcal{R} \\ \tau_1(R, \sigma) = (\text{yes}, \sigma_1) \\ \Rightarrow \left( \begin{array}{ll} \exists \sigma_2 \in \Sigma & \tau_2(R, \sigma_2) = (\text{yes}, \sigma_1) \\ & \wedge R \in \mathcal{R}^{\mathcal{R}} \Rightarrow W(\sigma_2) \subseteq W(\sigma) \\ & \wedge R \in \mathcal{R}^{\mathcal{R}} \Rightarrow W(\sigma) \subseteq W(\sigma_2) \end{array} \right) \\ \wedge \tau_1(R, \sigma) = (\text{no}, \sigma_1) \Rightarrow W(\sigma_1) \subseteq W(\sigma) \end{array} $$

- La relation de préordre sur les implantations d'un modèle est définie par :

$$ (\tau_1, \Sigma_I^1) \sqsubseteq (\tau_2, \Sigma_I^2) \Leftrightarrow ((\tau_1, \Sigma_I^1) \sqsubseteq_\Gamma (\tau_2, \Sigma_I^2) \wedge \tau_1 \sqsubseteq_W \tau_2) $$

On peut alors prouver que toute implantation inférieure (selon $\sqsubseteq$) à une implantation correcte est elle-même correcte. Ce résultat sera utile lorsque nous envisagerons la comparaison de modèles de contrôle d'accès.

**Proposition D.1** *Soit $M[\rho]$ un modèle de contrôle d'accès et $(\tau_1, \Sigma_I^1)$ et $(\tau_2, \Sigma_I^2)$ deux implantations de $M[\rho]$. Si $(\tau_1, \Sigma_I^1) \sqsubseteq (\tau_2, \Sigma_I^2)$ et $M[\rho] \vdash (\tau_2, \Sigma_I^2)$ alors $M[\rho] \vdash (\tau_1, \Sigma_I^1)$.*

# D.2 Comparaison de modèles de contrôle d'accès

## D.2.1 Simulation d'implantations

### Préordre sur les modèles

Nous détaillons ici le mécanisme de comparaison introduit dans la section 2.2.1. Rappeons que ce mécanisme est utilisable pour comparer deux modèles partageant le même ensemble de requêtes muni d'une sémantique faible. La relation de préordre partiel $\leq$ introduite dans la définition 2.3 fait intervenir d'une part une relation d'équivalence $\equiv_t$ sur les états, et d'autre part une relation de simulation.

La relation d'équivalence $\equiv_t$ est définie comme l'intersection $\equiv_W \cap \equiv_{W_0} \cap \equiv_R$ où :

$$ \begin{align*} \sigma_1 \equiv_W \sigma_2 &\Leftrightarrow W(\sigma_1) = W(\sigma_2) \\ \sigma_1 \equiv_{W_0} \sigma_2 &\Leftrightarrow W_0(\sigma_1) = W_0(\sigma_2) \\ \sigma_1 \equiv_R \sigma_2 &\Leftrightarrow (\forall R \in \mathcal{R} (\sigma_1, R) \in \mathcal{R} \mid \Sigma \Leftrightarrow (\sigma_2, R) \in \mathcal{R} \mid \Sigma) \end{align*} $$

Intuitivement, deux états sont équivalents par $\equiv_t$ ssi ils ont le même passé (ils auraient pu être construits à partir des mêmes requêtes et leurs fonctions de sécurité permettent les mêmes ensembles d'accès) et le même futur (ils autorisent les mêmes ensembles d'accès).
Dans la définition 2.3, nous avons imposé que la relation de simulation $\kappa_\Sigma$ utilisée vérifie certaines propriétés (ce que nous avons noté $P_s(\kappa_\Sigma)$). Ces propriétés sont les suivantes :

- $\kappa_\Sigma$ est totale à gauche<fnref n="1" /> : intuitivement, $M_1[\rho_1]$ est plus restrictif que $M_2[\rho_2]$ ssi tout ce qui peut être fait avec $M_1[\rho_1]$ peut également l'être avec $M_2[\rho_2]$, il faut donc que tous les états de $\Sigma_1$ soient en relation avec des états de $\Sigma_2$.

- une autre contrainte consiste à imposer que deux états de $\Sigma_1$ équivalents selon $\equiv_{\iota_1}$ soient en relation avec des états de $\Sigma_2$ équivalents selon $\equiv_{\iota_2}$ et vice-versa. Intuitive-ment, deux états sont reliés s'il est possible de "faire les mêmes choses" à partir de ces deux états. Nous introduisons donc les deux propriétés suivantes requises pour $\kappa_\Sigma$ :

- $\kappa_\Sigma \subseteq \Sigma_1 \times \Sigma_2$ est dite $\iota$-fonctionnelle ssi :

$$ \forall \sigma_1, \sigma'_1 \in \Sigma_1 \forall \sigma_2, \sigma'_2 \in \Sigma_2 \\ \sigma_1 \equiv_{\iota_1} \sigma'_1 \wedge (\sigma_1, \sigma_2) \in \kappa_\Sigma \wedge (\sigma'_1, \sigma'_2) \in \kappa_\Sigma \Rightarrow \sigma_2 \equiv_{\iota_2} \sigma'_2 $$

- $\kappa_\Sigma \subseteq \Sigma_1 \times \Sigma_2$ est dite $\iota$-injective ssi :

$$ \forall \sigma_1, \sigma'_1 \in \Sigma_1 \forall \sigma_2, \sigma'_2 \in \Sigma_2 \\ \sigma_2 \equiv_{\iota_2} \sigma'_2 \wedge (\sigma_1, \sigma_2) \in \kappa_\Sigma \wedge (\sigma'_1, \sigma'_2) \in \kappa_\Sigma \Rightarrow \sigma_1 \equiv_{\iota_1} \sigma'_1 $$

Notons que si, pour les deux modèles, la relation $\equiv_\iota$ est l'égalite, alors la $\iota$-fonctionnalité correspond intuitivement à la notion de fonctionnalité<fnref n="2" />, et la $\iota$-injectivité à la notion d'injectivité<fnref n="3" />.

## Modèles réduits

La relation d'équivalence $\equiv_\iota$ permet de "réduire" un modèle afin de considérer les classes d'équivalence d'états plutôt que les états. Il s'agit ici de simplifier les raisonnements et d'identifier les informations pertinentes au regard de la politique de contrôle d'accès.

Etant donné un modèle $M[\rho]$ et le modèle réduit associé $M^\sharp[\rho]$, les implantations du premier peuvent être reliées aux implantations du deuxième, et inversement. En effet, pour toute implantation de $M[\rho]$, il est possible de construire une implantation de $M^\sharp[\rho]$ à l'aide de l'opérateur :

$$ \sharp : (\mathcal{R} \times \Sigma \to \mathcal{D} \times \Sigma) \to (\mathcal{R} \times \hat{e}(\Sigma) \to \mathcal{D} \times \hat{e}(\Sigma)) \\ \forall \sigma \in \hat{e}(\Sigma) \quad \forall R \in \mathcal{R} \quad \sharp(\tau)(R, \sigma) = (d, e(\sigma')) \quad \text{avec} \quad \tau(R, \sigma) = (d, \sigma') $$

Réciproquement, pour toute implantation de $M^\sharp[\rho]$, il est possible de construire une implantation de $M[\rho]$ à l'aide de l'opérateur :

$$ \flat : (\mathcal{R} \times \hat{e}(\Sigma) \to \mathcal{D} \times \hat{e}(\Sigma)) \to (\mathcal{R} \times \Sigma \to \mathcal{D} \times \Sigma) \\ \forall \sigma \in \Sigma \quad \forall R \in \mathcal{R} \quad \flat(\tau)(R, \sigma) = \tau(R, e(\sigma)) $$

On montre que les opérateurs $\sharp$ et $\flat$, lorsqu'ils sont appliqués à des implantations correctes, permettent d'obtenir des implantations correctes.

<footnote n="1">¹Une relation $R \subseteq X \times Y$ est dite totale à gauche ssi pour tout $x$ dans $X$ il existe un $y$ dans $Y$ tel que $(x, y) \in R$.</footnote>

<footnote n="2">²Une relation $R \subseteq X \times Y$ est dite fonctionnelle ssi pour tout $x$ dans $X$ et pour tout $y$ et $z$ dans $Y$ si $(x, y) \in R$ et $(x, z) \in R$ alors $y = z$.</footnote>

<footnote n="3">³Une relation $R \subseteq X \times Y$ est injective ssi pour tout $x$ et $z$ dans $X$ et $y$ dans $Y$, si $(x, y) \in R$ et $(z, y) \in R$ alors $x = z$.</footnote>
**Proposition D.2** Soient $M[\rho]$ un modèle et $M^{\sharp}[\rho]$ la réduction de ce modèle.

$$1. \quad M^{\sharp}[\rho] \vdash (\tau, \Sigma_I) \Rightarrow (M[\rho] \vdash (\flat(\tau), \Sigma_I) \wedge \equiv_{\iota} \flat(\tau))$$

$$2. \quad (M[\rho] \vdash (\tau, \Sigma_I) \wedge \equiv_{\iota} \tau) \Rightarrow M^{\sharp}[\rho] \vdash (\sharp(\tau), \hat{e}(\Sigma_I))$$

On montre d'autre part que l'opérateur $\sharp$ est monotone pour le préordre $\sqsubseteq$ sur les implantations.

Prouver qu'un modèle est plus restrictif qu'un autre nécessite de prendre en compte les propriétés relatives à la relation $\equiv_{\iota}$ ce qui peut compliquer considérablement la preuve. Cette difficulté disparaît dans le cas où cette relation correspond à l'égalité, c'est-à-dire lorsque les modèles considérés sont des modèles réduits. En effet, pour les modèles réduits, nous pouvons introduire un préordre $\leq_{\sharp}$ défini comme suit : $M_1^{\sharp}[\rho_1] \leq_{\sharp} M_2^{\sharp}[\rho_2]$, ssi il existe une relation $\kappa_{\Sigma}$ totale à gauche, injective et fonctionnelle telle que :

$$\begin{align*}
\forall \tau_1 : \mathcal{R} \times \Sigma_1 &\to \mathcal{D} \times \Sigma_1 \quad \forall \Sigma_I^1 \subseteq \Sigma_I \\
M_1^{\sharp}[\rho_1] &\vdash (\tau_1, \Sigma_I^1) \\
\Rightarrow \exists \tau_2 : \mathcal{R} \times \Sigma_2 &\to \mathcal{D} \times \Sigma_2 \quad \exists \Sigma_I^2 \subseteq \Sigma_I \\
M_2^{\sharp}[\rho_2] &\vdash (\tau_2, \Sigma_I^2) \wedge (\tau_1, \Sigma_I^1) \stackrel{\kappa_{\Sigma}}{\rightleftharpoons} (\tau_2, \Sigma_I^2)
\end{align*}$$

Il est alors possible de montrer qu'un modèle est plus restrictif qu'un autre (selon la définition 2.3) ssi le modèle réduit du premier est plus restrictif que le modèle réduit du deuxième (selon $\leq_{\sharp}$). Pour cela, on montre tout d'abord que si une implantation $I_1$ est simulée par une implantation $I_2$, alors l'implantation "réduite" de $I_1$ est simulée par l'implantation "réduite" de $I_2$ :

$$(\tau_1, \Sigma_I^1) \stackrel{\kappa_{\Sigma}}{\rightleftharpoons} (\tau_2, \Sigma_I^2)) \Rightarrow (\sharp(\tau_1), \hat{e}_1(\Sigma_I^1)) \stackrel{\kappa_{\Sigma}^{\uparrow}}{\rightleftharpoons} (\sharp(\tau_2), \hat{e}_2(\Sigma_I^2))$$

$$\text{où } \kappa_{\Sigma}^{\uparrow} = \{(e_1(\sigma_1), e_2(\sigma_2)) \mid (\sigma_1, \sigma_2) \in \kappa_{\Sigma}\}.$$

Ce résultat nous permet d'établir que deux modèles sont ordonnés par $\leq$ ssi leurs modèles réduits respectifs le sont par $\leq_{\sharp}$.

**Proposition D.3** $M_1[\rho_1] \leq M_2[\rho_2] \Leftrightarrow M_1^{\sharp}[\rho_1] \leq_{\sharp} M_2^{\sharp}[\rho_2]$

## Propriétés sur les relations de simulation

En fonction des propriétés vérifiées par la relation de simulation $\kappa_{\Sigma} \subseteq \Sigma_1 \times \Sigma_2$, la proposition D.4, que nous présentons ici, permet de comparer deux modèles $M_1[\rho_1]$ et $M_2[\rho_2]$ sans avoir à considérer toutes les implantations de $M_1[\rho_1]$. Les "bonnes propriétés" que la relation $\kappa_{\Sigma}$ doit vérifier sont définies comme suit :

- $\kappa_{\Sigma}$ est $\mathcal{W}$-monotone ssi :

$$\begin{gather*}
\forall \sigma_1, \sigma'_1 \in \Sigma_1 \quad \forall \sigma_2, \sigma'_2 \in \Sigma_2 \\
(\mathcal{W}(\sigma_1) \subseteq \mathcal{W}(\sigma'_1) \wedge (\sigma_1, \sigma_2) \in \kappa_{\Sigma} \wedge (\sigma'_1, \sigma'_2) \in \kappa_{\Sigma}) \Rightarrow \mathcal{W}(\sigma_2) \subseteq \mathcal{W}(\sigma'_2)
\end{gather*}$$

- $\kappa_{\Sigma}$ est $\Omega$-préservante ssi :

$$\forall \sigma_1 \in \Sigma_1 \quad \forall \sigma_2 \in \Sigma_2 \quad ((\sigma_1, \sigma_2) \in \kappa_{\Sigma} \wedge \Omega_1(\sigma_1)) \Rightarrow \Omega_2(\sigma_2)$$
- $\kappa_{\Sigma}$ est $\|\mathcal{R}\|_{\Sigma}$-préservante ssi :

$$ \forall \sigma_1 \in \Sigma_1 \forall \sigma_2 \in \Sigma_2 \forall R \in \mathcal{R} \\ ((\sigma_1, \sigma_2) \in \kappa_{\Sigma} \wedge (R, \sigma_1) \in \|\mathcal{R}\|_{\Sigma_1}) \Rightarrow (R, \sigma_2) \in \|\mathcal{R}\|_{\Sigma_2} $$

La proposition suivante montre que si une relation de simulation $\kappa_{\Sigma}$ entre deux modèles $M_1[\rho_1]$ et $M_2[\rho_2]$ est $\mathcal{W}$-monotone, il est possible de prouver que toute implantation correcte de $M_1[\rho_1]$ inférieure selon $\sqsubseteq$ à une implantation simulable par une implantation correcte de $M_2[\rho_2]$ est également simulable. Si la relation $\kappa_{\Sigma}$ est $\Omega$-préservante et $\|\mathcal{R}\|_{\Sigma}$-préservante, alors on peut montrer directement que toute implantation correcte de $M_1[\rho_1]$ est simulable par une implantation correcte de $M_2[\rho_2]$.

**Proposition D.4** Soient $M_1[\rho_1]$ et $M_2[\rho_2]$ deux modèles de contrôle d'accès et $\kappa_{\Sigma} \subseteq \Sigma_1 \times \Sigma_2$ une relation totale à gauche, injective, fonctionnelle et $\mathcal{W}$-monotone.

$$ \begin{array}{l} \forall (\tau_1, \Sigma_I^1), (\tau'_1, \Sigma_I'^1), (\tau'_2, \Sigma_I'^2) \\ \left( \begin{array}{l} M_1[\rho_1] \vdash (\tau_1, \Sigma_I^1) \wedge M_1[\rho_1] \vdash (\tau'_1, \Sigma_I'^1) \wedge M_2[\rho_2] \vdash (\tau'_2, \Sigma_I'^2) \\ \wedge (\tau_1, \Sigma_I^1) \sqsubseteq (\tau'_1, \Sigma_I'^1) \wedge (\tau'_1, \Sigma_I'^1) \stackrel{\kappa_{\Sigma}}{\rightleftharpoons} (\tau'_2, \Sigma_I'^2) \end{array} \right) \\ \Rightarrow \exists (\tau_2, \Sigma_I^2) \quad M_2[\rho_2] \vdash (\tau_2, \Sigma_I^2) \wedge (\tau_1, \Sigma_I^1) \stackrel{\kappa_{\Sigma}}{\rightleftharpoons} (\tau_2, \Sigma_I^2) \end{array} $$

$$ \text{2. Si } \kappa_{\Sigma} \text{ est } \Omega\text{-préservante et } \|\mathcal{R}\|_{\Sigma}\text{-préservante, alors pour toute implantation correcte } (\tau_1, \Sigma_I^1), \text{ il existe une implantation correcte } (\tau_2, \Sigma_I^2) \text{ telle que } (\tau_1, \Sigma_I^1) \stackrel{\kappa_{\Sigma}}{\rightleftharpoons} (\tau_2, \Sigma_I^2). $$

Ce résultat permet de montrer que si une implantation correcte d'un modèle est simulable, alors toute implantation qui lui est inférieure est aussi simulable. Il permet également de montrer que si la relation de simulation respecte des "bonnes propriétés", alors toute implantation du modèle est simulable. Nous pouvons à présent montrer que si pour toute implantation d'un modèle $M_1[\rho_1]$, il existe une implantation qui lui est supérieure par $\sqsubseteq$ et qui est simulable par une implantation de $M_2[\rho_2]$, alors $M_1[\rho_1] \leq M_2[\rho_2]$. Nous montrons également que si la relation de simulation vérifie de "bonnes propriétés", on obtient directement $M_1[\rho_1] \leq M_2[\rho_2]$.

**Proposition D.5** Soient $M_1[\rho_1]$ et $M_2[\rho_2]$ deux modèles de contrôle d'accès et $\kappa_{\Sigma} \subseteq \Sigma_1 \times \Sigma_2$ une relation totale à gauche, $\mathcal{W}$-monotone, $\iota$-fonctionnelle et $\iota$-injective.

$$ \begin{array}{l} \text{1. Si pour toute implantation } (\tau_1, \Sigma_I^1) \equiv_{\iota_1} \textit{-préservante telle que } M_1[\rho_1] \vdash (\tau_1, \Sigma_I^1), \\ \quad - \textit{il existe une implantation } (\tau'_1, \Sigma_I'^1) \equiv_{\iota_1} \textit{-préservante telle que } M_1[\rho_1] \vdash (\tau'_1, \Sigma_I'^1) \text{ et} \\ \quad (\tau_1, \Sigma_I^1) \sqsubseteq (\tau'_1, \Sigma_I'^1) \\ \quad - \textit{et s'il existe une implantation } (\tau'_2, \Sigma_I'^2) \equiv_{\iota_2} \textit{-préservante telle que } M_2[\rho_2] \vdash (\tau'_2, \Sigma_I'^2) \\ \quad \textit{vérifiant } (\tau'_1, \Sigma_I'^1) \stackrel{\kappa_{\Sigma}}{\rightleftharpoons} (\tau'_2, \Sigma_I'^2), \\ \quad \text{alors } M_1[\rho_1] \leq M_2[\rho_2]. \end{array} $$

$$ \text{2. Si } \kappa_{\Sigma} \text{ est } \Omega\text{-préservante et } \|\mathcal{R}\|_{\Sigma}\text{-préservante, alors } M_1[\rho_1] \leq M_2[\rho_2]. $$

Ainsi, avec la proposition D.5, pour montrer qu'un modèle est plus restrictif qu'un autre, il suffit de montrer que toutes les implantations $\sqsubseteq$-maximales<fnref n="4" /> sont simulables. De plus, si la relation de simulation préserve la politique de sécurité ainsi que la sémantique des requêtes, alors il est possible de montrer directement, sans considérer les implantations, qu'un modèle est plus restrictif qu'un autre.

<footnote n="4">⁴Une implantation $(\tau, \Sigma_I)$ d'un modèle $M[\rho]$ est $\sqsubseteq$-maximale ssi il n'existe pas une autre implantation $(\tau', \Sigma_I')$ de $M[\rho]$ telle que $(\tau, \Sigma_I) \sqsubseteq (\tau', \Sigma_I')$.</footnote>
## Application : Méthodologie et exemples

La démarche que nous avons adoptée pour établir qu’un modèle $M_1[\rho_1]$ est plus restrictif qu’un modèle $M_2[\rho_2]$ se décompose en deux étapes principales. Dans un premier temps, on construit un modèle intermédiaire $M_{12}[\rho_2]$ correspondant au modèle $M_1[\rho_1]$ exprimé dans le formalisme de $M_2[\rho_2]$. Pour ce faire, il faut bien sûr commencer par interpréter le paramètre de sécurité $\rho_1$ par un paramètre de sécurité $\rho_2 = \kappa_\rho(\rho_1)$, puis considérer les états. Cette interprétation permet de définir un prédicat de sécurité $\Omega_{12}$ sur $\Sigma_2$ à partir duquel le modèle $M_{12}[\kappa_\rho(\rho_1)]$ est défini. Ce mécanisme de traduction permet de définir une relation de simulation à partir de laquelle on établit $M_1[\rho_1] \le M_{12}[\kappa_\rho(\rho_1)]$. Il faut ensuite montrer que la politique définie par le prédicat $\Omega_{12}$ est plus restrictive que celle définie par $\Omega_2$, c’est-à-dire :

$$ \forall \sigma \in \Sigma_2 \quad \Omega_{12}(\sigma) \Rightarrow \Omega_2(\sigma) $$

Dans ce cas, on montre facilement que $M_{12}[\kappa_\rho(\rho_1)] \le M_2[\kappa_\rho(\rho_1)]$, ce qui nous permet d’établir :

$$ \forall \rho_1 \exists \rho_2 \quad M_1[\rho_1] \le M_2[\rho_2] $$

La méthodologie esquissée ci-dessus a été utilisée avec succès pour comparer entre eux les modèles de la Muraille de Chine, de Bell et LaPadula et RBAC. Nous présentons ici les grandes lignes du raisonnement permettant de montrer que le modèle $M_{CW}^{acc}[\rho_{CW}]$ de la Muraille de Chine est strictement plus restrictif que le modèle $M_{BLP}^{acc}[\rho_{BLP}]$ de Bell et LaPadula.

**Traduction : construction d'un modèle intermédiaire.** Pour montrer que le modèle de la Muraille de Chine est plus restrictif que le modèle de Bell et LaPadula, il faut tout d'abord donner une interprétation des concepts de $M_{CW}^{acc}[\rho_{CW}]$ par des concepts de $M_{BLP}^{acc}[\rho_{BLP}]$. Il s'agit d'exprimer à l'aide d'un treillis de niveaux de sécurité $\rho_{LCW}$ les notions de compagnies et de classes de conflits présentes dans le paramètre $\rho_{CW}$ de la Muraille de Chine. Ce treillis a bien sûr une forme particulière puisqu'il est issu d'une fonction de traduction $\kappa_\rho$ qui permet d'obtenir un treillis $\kappa_\rho(\rho_{CW}) = \rho_{LCW}$ à partir du paramètre $\rho_{CW}$. On cherche donc à montrer que $M_{CW}^{acc}[\rho_{CW}] \le M_{BLP}^{acc}[\rho_{LCW}]$. Il s'agit alors de spécifier comment présenter un état du système décrit dans le formalisme de la Muraille de Chine par un état “équivalent” décrit dans le formalisme de Bell et LaPadula. Concrètement, on définit donc une relation $\kappa_\Sigma \subseteq \Sigma_{CW} \times \Sigma_{BLP}$ qui permet de relier les états des deux formalismes et qui sera utilisée comme relation de simulation par la suite. Il reste alors à reformuler le prédicat $\Omega_{CW}$ qui spécifie la politique de la Muraille de Chine par un prédicat $\Omega_{LCW}$ exprimé dans le formalisme de Bell et LaPadula. On obtient finalement un nouveau modèle $M_{LCW}^{acc}[\rho_{LCW}]$. C'est à partir de ce modèle intermédiaire que nous allons pouvoir montrer que $M_{CW}^{acc}[\rho_{CW}] \le M_{BLP}^{acc}[\rho_{LCW}]$. Nous procédons en deux étapes : nous montrons tout d'abord $M_{CW}^{acc}[\rho_{CW}] \le M_{LCW}^{acc}[\rho_{LCW}]$ puis nous montrons $M_{LCW}^{acc}[\rho_{LCW}] \le M_{BLP}^{acc}[\rho_{LCW}]$.

**Comparaison du modèle original avec le modèle intermédiaire.** Nous avons montré que $M_{CW}^{acc}[\rho_{CW}] \le M_{LCW}^{acc}[\rho_{LCW}]$ en utilisant la proposition D.5. Nous avons donc tout d'abord montré que la relation $\kappa_\Sigma$ définie à l'étape précédente était totale à gauche, W-monotone, $\iota$-fonctionnelle et $\iota$-injective. Nous avons ensuite prouvé le résultat de deux manières différentes.
1. Nous avons prouvé que toute implantation correcte de la Muraille de Chine est inférieure (selon $\sqsubseteq$) à l'implantation classique $(\tau_{CW}, \Sigma_{CW}^I)$ de ce modèle (i.e. $(\tau_{CW}, \Sigma_{CW}^I)$ est la seule implantation maximale de la Muraille de Chine), et qu'il existe une implantation $(\tau_{LCW}, \Sigma_{LCW}^I)$ correcte du modèle de de Bell et LaPadula qui simule $(\tau_{CW}, \Sigma_{CW}^I)$. Le point 1) de la proposition D.5 nous permet alors de conclure que $M_{CW}^{acc}[\rho_{CW}] \le M_{LCW}^{acc}[\rho_{LCW}]$.

2. Nous avons prouvé que la relation $\kappa_{\Sigma}$ est $\Omega$-préservante et $\|\mathcal{R}\|_{\Sigma}$-préservante. Le point 2) de la proposition D.5 nous permet alors de conclure que $M_{CW}^{acc}[\rho_{CW}] \le M_{LCW}^{acc}[\rho_{LCW}]$.

Comparaison du modèle intermédiaire avec le modèle “cible”. Une fois la politique de la Muraille de Chine exprimée par le prédicat $\Omega_{LCW}$ dans le formalisme du modèle de Bell et LaPadula, il est facile de montrer que tout état vérifiant le prédicat $\Omega_{LCW}$ vérifie aussi le prédicat définissant la politique de Bell et LaPadula et on montre alors facilement que $M_{LCW}^{acc}[\rho_{LCW}] \le M_{BLP}^{acc}[\rho_{LCW}]$ ce qui, par transitivité, nous permet finalement d'établir que $M_{CW}^{acc}[\rho_{CW}] \le M_{BLP}^{acc}[\rho_{LCW}]$.

Cette méthodologie repose sur l'idée de séparer de manière claire les étapes de traduction et de comparaison. En revanche, pour montrer qu'un modèle $M_1[\rho_1]$ n'est pas plus restrictif qu'un modèle $M_2[\rho_2]$, on procède de manière différente. En effet, pour ce faire, on montre que :

$$ \exists \rho_1 \forall \rho_2 \quad M_1[\rho_1] \le M_2[\rho_2] $$

Il suffit donc de concevoir une valeur pour $\rho_1$ qui ne puisse pas être associée à un parramètre $\rho_2$ tel que $M_1[\rho_1] \le M_2[\rho_2]$. On montre en fait par un argument de cardinalité sur les ensembles d'états qu'il n'existe pas de relation de simulation permettant d'établir $M_1[\rho_1] \le M_2[\rho_2]$. Cette étape est grandement facilitée si l'on considère les modèles réduits (la proposition D.3 garantit la validité de ce procédé). Ainsi, pour montrer que $M_{BLP}^{acc}[\rho_{BLP}] \le M_{CW}^{acc}[\rho_{CW}]$, nous nous sommes appuyés sur le fait que dans le modèle de la Muraille Chine, il n'était pas possible d'interdire un accès en lecture si aucun autre accès n'est présent, contrairement au modèle de Bell et La Padula. Ainsi, pour la Muraille de Chine, le cardinal de l'ensemble des classes d'équivalence selon $\equiv_W$ est inférieur au cardinal de l'ensemble des classes d'équivalence selon $\equiv_W$ pour le modèle de Bell et LaPadula, ce qui permet de montrer facilement qu'il n'existe pas de relation de simulation $\iota$-injective.

En suivant cette méthodologie, nous avons également montré que :

$$ M_{BLP}^{acc}[\rho_{BLP}] \le M_{RBLP}^{acc}[\rho_{RBLP}] \le M_{RBAC}^{acc}[\rho_{RBLP}] $$

$$ M_{RBAC}^{acc}[\rho_{RBAC}] \le M_{BLP}^{acc}[\rho_{BLP}] $$

où $M_{RBLP}^{acc}[\rho_{RBLP}]$ représente l'interprétation à base de rôles du modèle de Bell et LaPadula. Il est alors possible de déduire que $M_{CW}^{acc}[\rho_{CW}] \le M_{RBAC}^{acc}[\rho_{RBAC}]$.

Ainsi, ces comparaisons nous permettent d'établir formellement qu'un système régi par le modèle de la Muraille de Chine peut être obtenu à partir d'un système régi par le modèle de Bell & LaPadula qui peut lui même être obtenu à partir d'un système régi par un modèle à base de rôle. De plus, nous avons également montré qu'il n'était pas possible d'implanter un système à base de rôles dans le formalisme de Bell & LaPadula et qu'il n'était pas
non plus possible d'implanter un système régi par le modèle de Bell & LaPadula dans le formalisme de la Muraille de Chine. Ces résultats fournissent des critères de choix entre ces trois modèles en indiquant ce qu'il est possible de faire avec. Il reste alors au concepteur d'un système à choisir le formalisme le mieux adapté à ses besoins en tenant compte de ces résultats.

## D.2.2 Simulation faible d'implantations

Nous détaillons à présent le mécanisme de comparaison introduit dans la section 2.2.2 et illustrons son utilisation pour la comparaison des modèles HRU, de Bell & LaPadula et à base de rôles.

### Propriétés sur les relations de simulation

La relation de préordre $\leq$ introduite dans la section 2.2.2 repose sur deux relations : la première, notée $\kappa_\Sigma$, permet de relier les états des deux modèles à comparer, la deuxième, notée $\kappa_R$, permet d'établir une correspondance "sémantique" entre les langages de requêtes des deux modèles à comparer. Nous introduisons ici les propriétés que doivent vérifier ces relations pour permettre la comparaison de deux modèles sans avoir à considérer toutes les implantations. D'une part, la relation $\kappa_\Sigma$ doit être $\Omega$-préservante et $W$-préservante, et d'autre part la relation $\kappa_R$ doit satisfaire les deux propriétés suivantes.

- La sémantique des requêtes, qui sont en relation par $\kappa_R$, doit préserver le prédicat de sécurité lorsque ces requêtes sont appliquées sur des états en relation par $\kappa_\Sigma$. Dans ce cas, on dit que $\kappa_R$ est $\Omega$-préservante :

$$ 
\begin{gather*}
\forall R_1 \in \mathcal{R}_1 \quad \forall (R_2^1, \dots, R_2^n) \in \mathcal{R}_2^* \quad \forall \sigma_1, \sigma_1' \in \Sigma_1 \\
((\sigma_1, R_1, (R_2^1, \dots, R_2^n))) \in \kappa_R \wedge \Omega_1(\sigma_1) \wedge (\sigma_1, R_1, \sigma_1') \in [\mathcal{R}_1]_{\Sigma_1} \wedge \Omega_1(\sigma_1') \\
\Rightarrow \left( \begin{array}{@{}l@{}}
\forall \sigma_2^0, \sigma_2^1, \dots, \sigma_2^n \in \Sigma_2 \\
\quad \Omega_2(\sigma_2^0) \wedge (\sigma_1, \sigma_2^0) \in \kappa_\Sigma \\
\quad \wedge (\sigma_2^0, R_2^1, \sigma_2^1) \in [\mathcal{R}_2]_{\Sigma_2} \\
\quad \wedge \dots \wedge (\sigma_2^{n-1}, R_2^n, \sigma_2^n) \in [\mathcal{R}_2]_{\Sigma_2}
\end{array} \right) \Rightarrow \left( \begin{array}{@{}l@{}}
\Omega_2(\sigma_2^1) \wedge \dots \wedge \Omega_2(\sigma_2^n)
\end{array} \right)
\end{gather*}
$$

- La sémantique des requêtes, qui sont en relation par $\kappa_R$, doit préserver la relation $\kappa_\Sigma$. Dans ce cas, on dit que $\kappa_R$ est $\kappa_\Sigma$-préservante :

$$ 
\begin{gather*}
\forall R_1 \in \mathcal{R}_1 \quad \forall (R_2^1, \dots, R_2^n) \in \mathcal{R}_2^* \quad \forall \sigma_1, \sigma_1' \in \Sigma_1 \quad \forall \sigma_2^0, \sigma_2^1, \dots, \sigma_2^{n-1}, \sigma_2^n \in \Sigma_2 \\
\left( \begin{array}{@{}l@{}}
\quad (\sigma_1, R_1, \sigma_1') \in [\mathcal{R}_1]_{\Sigma_1} \wedge (\sigma_2^0, R_2^1, \sigma_2^1) \in [\mathcal{R}_2]_{\Sigma_2} \wedge \dots \\
\quad \wedge (\sigma_2^{n-1}, R_2^n, \sigma_2^n) \in [\mathcal{R}_2]_{\Sigma_2} \wedge (\sigma_1, R_1, (R_2^1, \dots, R_2^n)) \in \kappa_R \wedge (\sigma_1, \sigma_2^0) \in \kappa_\Sigma
\end{array} \right) \\
\Rightarrow (\sigma_1', \sigma_2^n) \in \kappa_\Sigma
\end{gather*}
$$

On montre alors la proposition suivante.

**Proposition D.6** Soit deux modèles $M_1[\rho_1] = (\mathbb{P}_1[\rho_1], \mathcal{R}_1)$ et $M_2[\rho_2] = (\mathbb{P}_2[\rho_2], \mathcal{R}_2)$ tels que $[\mathcal{R}_1]_{\Sigma_1}$ et $[\mathcal{R}_2]_{\Sigma_2}$ soient fonctionnelles et totales à gauche$^5$. Si il existe deux relations totales à gauche $\kappa_\Sigma \subseteq \Sigma_1 \times \Sigma_2$ et $\kappa_R \subseteq \Sigma_1 \times \mathcal{R}_1 \times \mathcal{R}_2^*$ telles que $\kappa_\Sigma$ est $\Omega$-préservante et $W$-préservante et $\kappa_R$ est $\Omega$-préservante et $\kappa_\Sigma$-préservante, alors $M_1[\rho_1] \trianglelefteq M_2[\rho_2]$.

<footnote>$^5$Une relation ternaire $R \subseteq A \times B \times C$ est dite totale à gauche ssi pour tout $a \in A$ et $b \in B$, il existe $c \in C$ tel que $(a, b, c) \in R$.</footnote>
La preuve s'obtient en montrant que chaque implantation $(\tau_1, \Sigma_1^I)$ du modèle $\mathbb{M}_1[\rho_1]$ peut être simulée à partir de $\kappa_\Sigma$ et de la relation $\kappa'_R$ définie à partir de $\kappa_R$ et de $\tau_1$ comme suit :

$$ \begin{array}{l} \forall \sigma_1 \in \Sigma_1 \quad \forall R_1 \in \mathcal{R}_1 \quad \forall (R_2^1, \dots, R_2^n) \in \mathcal{R}_2^* \\ \phantom{\forall \sigma_1 \in \Sigma_1 \quad \forall R_1 \in \mathcal{R}_1 \quad \forall (R_2^1, \dots, R_2^n) \in \mathcal{R}_2^*} (\sigma_1, R_1, (R_2^1, \dots, R_2^n)) \in \kappa'_R \iff \left( \begin{array}{c} \begin{array}{l} \tau_1(R_1, \sigma_1) = (\text{yes}, \_ \\ \wedge (\sigma_1, R_1, (R_2^1, \dots, R_2^n)) \in \kappa_R \end{array} \\ \begin{array}{l} \tau_1(R_1, \sigma_1) = (\text{no}, \sigma_1) \\ \wedge (R_2^1, \dots, R_2^n) = (\text{Fail}) \end{array} \end{array} \right) \end{array} $$

En pratique, il n'est donc pas nécessaire de définir une relation $\kappa'_R$ pour chaque implantation à simuler, cette relation s'obtient directement à partir de l'implantation à simuler et de la relation $\kappa_R$ définie indépendamment des implantations.

## Applications

Nous illustrons ici l'utilisation de la proposition D.6 pour comparer les modèles HRU, de Bell & LaPadula et RBAC.

*Langages de requêtes administratives.* Les requêtes appartenant à l'ensemble $\mathcal{R}^{acc}$, défini en (2.1), permettant à un sujet de demander un accès ou le relâchement d'un accès, sont généralement accompagnées par un ensemble de requêtes, appelées requêtes administratives, permettant la modification des fonctions de sécurité. Bien sûr, l'application de ces requêtes doit être régie par une politique administrative. Nous donnons ici trois langages de requêtes administratives $\mathcal{R}_{HRU}^{adm}$, $\mathcal{R}_{BLP}^{adm}$ et $\mathcal{R}_{RBAC}^{adm}$ pour les politiques HRU, RBAC et de Bell et LaPadula ainsi que la définition d'une sémantique pour ces requêtes. La syntaxe (accompagnée d'une sémantique informelle) des requêtes considérées pour chacune de ces politiques est introduite dans la table D.5 tandis que la sémantique formelle de ces requêtes est définie dans la table D.6. Les modèles de contrôle d'accès que nous considérons ici sont obtenus à partir des ensembles de requêtes suivantes

$$ \begin{align*} \mathcal{R}_{HRU} &= \mathcal{R}^{acc} \cup \mathcal{R}_{HRU}^{adm} \cup \{\text{Success, Fail}\} \\ \mathcal{R}_{RBAC} &= \mathcal{R}^{acc} \cup \mathcal{R}_{RBAC}^{adm} \cup \{\text{Success, Fail}\} \\ \mathcal{R}_{BLP} &= \mathcal{R}^{acc} \cup \mathcal{R}_{BLP}^{adm} \cup \{\text{Success, Fail}\} \end{align*} $$

où Success et Fail sont les requêtes présentées page 30.

*Paramètres de sécurité.* Prouver qu'un modèle $\mathbb{M}_1[\rho_1]$ est plus restrictif qu'un autre modèle consiste tout d'abord à interpréter le paramètre de sécurité $\rho_1$ par un paramètre de sécurité $\rho_2 = \kappa_\rho(\rho_1)$ exprimé dans le formalisme du deuxième modèle. Il s'agit alors de montrer que $\mathbb{M}_1[\rho_1] \subseteq \mathbb{M}_2[\kappa_\rho(\rho_1)]$.

Lors de la comparaison des modèles HRU et RBAC, il suffit de montrer comment obtenir un paramètre de sécurité pour RBAC : les utilisateurs sont les sujets, chaque sujet est associé à un rôle (les rôles sont donc identifiés aux sujets) et la relation d'ordre sur les rôles est vide. Plus formellement, nous considérons le paramètre $\rho_1 = (S, S, \emptyset)$, et nous montrerons que :

$$ \begin{align*} \mathbb{M}_{HRU}[\cdot] &= (\mathbb{P}_{HRU}[\cdot], \mathcal{R}_{HRU}) \quad \subseteq \quad \mathbb{M}_{RBAC}[\rho_1] = (\mathbb{P}_{RBAC}[\rho_1], \mathcal{R}_{RBAC}) \\ \mathbb{M}_{RBAC}[\rho_{RBAC}] &= (\mathbb{P}_{RBAC}[\rho_{RBAC}], \mathcal{R}_{RBAC}) \quad \subseteq \quad \mathbb{M}_{HRU}[\cdot] = (\mathbb{P}_{HRU}[\cdot], \mathcal{R}_{HRU}) \end{align*} $$
<table><caption>TAB. D.5 – Requêtes administratives</caption><tbody><tr><td>R<sup>adm</sup><sub>HRU</sub></td><td></td></tr><tr><td>⟨+<sub>m<sub>D</sub></sub>, s, s', o, a⟩</td><td>s demande l'ajout de (s', o, a) dans m<sub>D</sub></td></tr><tr><td>⟨-<sub>m<sub>D</sub></sub>, s, s', o, a⟩</td><td>s demande le retrait de (s', o, a) de m<sub>D</sub></td></tr><tr><td>R<sup>adm</sup><sub>BLP</sub></td><td></td></tr><tr><td>⟨+<sub>f<sub>s</sub></sub>, s, s', l⟩</td><td>s demande à affecter à f<sub>s</sub>(s') la valeur l</td></tr><tr><td>⟨+<sub>f<sub>o</sub></sub>, s, o, l⟩</td><td>s demande à affecter à f<sub>o</sub>(o) la valeur l</td></tr><tr><td>R<sup>adm</sup><sub>RBACB</sub></td><td></td></tr><tr><td>⟨+<sub>UA</sub>, s, u, r⟩</td><td>s demande l'ajout de (u, r) dans UA</td></tr><tr><td>⟨-<sub>UA</sub>, s, u, r⟩</td><td>s demande le retrait de (u, r) de UA</td></tr><tr><td>⟨+<sub>PA</sub>, s, o, a, r⟩</td><td>s demande l'ajout de ((o, a), r) dans PA</td></tr><tr><td>⟨-<sub>PA</sub>, s, o, a, r⟩</td><td>s demande le retrait de ((o, a), r) de PA</td></tr><tr><td>⟨+<sub>roles</sub>, s, s', r⟩</td><td>s demande l'ajout de r dans roles(s')</td></tr><tr><td>⟨-<sub>roles</sub>, s, s', r⟩</td><td>s demande le retrait de r de roles(s')</td></tr></tbody></table>

ce qui permet d'établir que les modèles HRU et RBAC ont le même pouvoir d'expression. Ainsi, le choix d'un de ces deux modèles n'a pas d'incidence sur ce qu'il sera possible de spécifier avec, la seule différence réside dans le formalisme fourni par ces modèles.

Nous montrerons également que le modèle de Bell et LaPadula est strictement plus restrictif que le modèle RBAC. Aussi, étant donné le paramètre de sécurité $\rho_{BLP} = (\mathcal{L}, \leq, \gamma, \lambda)$, nous définissons le paramètre $\rho_3 = (S, \mathcal{L}, \leq)$ utile pour définir un modèle à base de rôles : les utilisateurs sont les sujets, chaque rôle correspond à un niveau de sécurité et la hiérarchie des rôles coïncide avec l'ordre $\leq$ sur les niveaux de sécurité. Nous montrerons donc que :

$$M_{BLP}[\rho_{BLP}] = (\mathbb{P}_{BLP}[\rho_{BLP}], \mathcal{R}_{BLP}) \triangleleft M_{RBAC}[\rho_3] = (\mathbb{P}_{RBAC}[\rho_3], \mathcal{R}_{RBAC})$$

*Relation de simulation entre états.* Les relations $\kappa_{\Sigma}^1 \subseteq \Sigma_{HRU} \times \Sigma_{RBAC}$, $\kappa_{\Sigma}^2 \subseteq \Sigma_{RBAC} \times \Sigma_{HRU}$ et $\kappa_{\Sigma}^3 \subseteq \Sigma_{BLP} \times \Sigma_{RBAC}$, permettant de relier les états “sémantiquement” équivalents, sont définies dans la table D.7. Nous montrons que ces relations satisfont les propriétés requises pour l'application de la proposition D.6.

**Lemme D.3** $\kappa_{\Sigma}^1, \kappa_{\Sigma}^2$ et $\kappa_{\Sigma}^3$ sont $\Omega$-préservantes et $\mathcal{W}$-préservantes.

A partir de la définition de la relation $\kappa_{\Sigma} \subseteq \Sigma_1 \times \Sigma_2$, il est possible d'exprimer le prédicat de sécurité $\Omega_1$ sur $\Sigma_1$ par un prédicat $\Omega_{12}$ sur $\Sigma_2$. Le prédicat $\Omega_{12}$ doit vérifier les deux propriétés suivantes :

$$ \begin{array}{l} \forall \sigma_1 \in \Sigma_1 \quad \forall \sigma_2 \in \Sigma_2 \quad ((\sigma_1, \sigma_2) \in \kappa_{\Sigma} \wedge \Omega_1(\sigma_1)) \Rightarrow \Omega_{12}(\sigma_2) \\ \forall \sigma_2 \in \Sigma_2 \quad \Omega_{12}(\sigma_2) \Rightarrow \Omega_2(\sigma_2) \end{array} \qquad (D.1) $$

La table D.8 contient les définitions des prédicats $\Omega^1$ exprimant la politique HRU dans le formalisme de la politique RBAC paramétrée par $\rho_1 = (S, S, \emptyset)$, $\Omega^2$ exprimant la politique RBAC dans le formalisme de la politique HRU, et $\Omega^3$ exprimant la politique de Bell et LaPadula dans le formalisme de la politique RBAC paramétrée par $\rho_3 = (S, \mathcal{L}, \leq)$. On montre que ces trois prédicats satisfont les propriétés (D.1).
$$ \|\mathcal{R}_{HRU}^{adm}\|_{\Sigma_{HRU}}^{+} $$

$$ ((m_1, m_D^1), \langle +_{m_D}, s, s', o, a \rangle, (m_2, m_D^2)) \in \|\mathcal{R}_{HRU}^{adm}\|_{\Sigma_{HRU}}^{+} \\ \Leftrightarrow (m_1 = m_2 \wedge m_D^2 = m_D^1 \cup \{(s', o, a)\}) $$

$$ ((m_1, m_D^1), \langle -_{m_D}, s, s', o, a \rangle, (m_2, m_D^2)) \in \|\mathcal{R}_{HRU}^{adm}\|_{\Sigma_{HRU}}^{+} \\ \Leftrightarrow (m_1 = m_2 \wedge m_D^2 = m_D^1 \setminus \{(s', o, a)\}) $$

$$ \|\mathcal{R}_{BLP}^{adm}\|_{\Sigma_{BLP}}^{+} $$

$$ ((m_1, f_s^1, f_o^1), \langle +_{f_s}, s, s', l \rangle, (m_2, f_s^2, f_o^2)) \in \|\mathcal{R}_{BLP}^{adm}\|_{\Sigma_{BLP}}^{+} \\ \Leftrightarrow (m_1 = m_2 \wedge f_s^2 = f_s^1[s' \leftarrow l]) $$

$$ ((m_1, f_s^1, f_o^1), \langle +_{f_o}, s, o, l \rangle, (m_2, f_s^2, f_o^2)) \in \|\mathcal{R}_{BLP}^{adm}\|_{\Sigma_{BLP}}^{+} \\ \Leftrightarrow (m_1 = m_2 \wedge f_o^2 = f_o^1[o \leftarrow l]) $$

$$ \|\mathcal{R}_{RBAC}^{adm}\|_{\Sigma_{RBAC}}^{+} $$

$$ ((m_1, \text{user}^1, \text{UA}^1, \text{PA}^1, \text{roles}^1), \langle +_{\text{UA}}, s, u, r \rangle, (m_2, \text{user}^2, \text{UA}^2, \text{PA}^2, \text{roles}^2)) \in \|\mathcal{R}_{\text{RBAC}}^{\text{adm}}\|_{\Sigma_{\text{RBAC}}}^{+} \\ \Leftrightarrow (m_1 = m_2 \wedge \text{user}^1 = \text{user}^2 \wedge \text{PA}^1 = \text{PA}^2 \wedge \text{roles}^1 = \text{roles}^2 \wedge \text{UA}^2 = \text{UA}^1 \cup \{(o, r)\}) $$

$$ ((m_1, \text{user}^1, \text{UA}^1, \text{PA}^1, \text{roles}^1), \langle -_{\text{UA}}, s, u, r \rangle, (m_2, \text{user}^2, \text{UA}^2, \text{PA}^2, \text{roles}^2)) \in \|\mathcal{R}_{\text{RBAC}}^{\text{adm}}\|_{\Sigma_{\text{RBAC}}}^{+} \\ \Leftrightarrow (m_1 = m_2 \wedge \text{user}^1 = \text{user}^2 \wedge \text{PA}^1 = \text{PA}^2 \wedge \text{roles}^1 = \text{roles}^2 \wedge \text{UA}^2 = \text{UA}^1 \setminus \{(o, r)\}) $$

$$ ((m_1, \text{user}^1, \text{UA}^1, \text{PA}^1, \text{roles}^1), \langle +_{\text{PA}}, s, o, a, r \rangle, (m_2, \text{user}^2, \text{UA}^2, \text{PA}^2, \text{roles}^2)) \in \|\mathcal{R}_{\text{RBAC}}^{\text{adm}}\|_{\Sigma_{\text{RBAC}}}^{+} \\ \Leftrightarrow (m_1 = m_2 \wedge \text{user}^1 = \text{user}^2 \wedge \text{UA}^1 = \text{UA}^2 \wedge \text{roles}^1 = \text{roles}^2 \wedge \text{PA}^2 = \text{PA}^1 \cup \{(o, a), r\}) $$

$$ ((m_1, \text{user}^1, \text{UA}^1, \text{PA}^1, \text{roles}^1), \langle -_{\text{PA}}, s, o, a, r \rangle, (m_2, \text{user}^2, \text{UA}^2, \text{PA}^2, \text{roles}^2)) \in \|\mathcal{R}_{\text{RBAC}}^{\text{adm}}\|_{\Sigma_{\text{RBAC}}}^{+} \\ \Leftrightarrow (m_1 = m_2 \wedge \text{user}^1 = \text{user}^2 \wedge \text{UA}^1 = \text{UA}^2 \wedge \text{roles}^1 = \text{roles}^2 \wedge \text{PA}^2 = \text{PA}^1 \setminus \{(o, a), r\}) $$

$$ ((m_1, \text{user}^1, \text{UA}^1, \text{PA}^1, \text{roles}^1), \langle +_{\text{roles}}, s, s', r \rangle, (m_2, \text{user}^2, \text{UA}^2, \text{PA}^2, \text{roles}^2)) \in \|\mathcal{R}_{\text{RBAC}}^{\text{adm}}\|_{\Sigma_{\text{RBAC}}}^{+} \\ \Leftrightarrow (m_1 = m_2 \wedge \text{user}^1 = \text{user}^2 \wedge \text{UA}^1 = \text{UA}^2 \wedge \text{PA}^1 = \text{PA}^2 \wedge \text{roles}^2 = \text{roles}^1[s' \leftarrow \text{roles}^1(s') \cup \{r\}]) $$

$$ ((m_1, \text{user}^1, \text{UA}^1, \text{PA}^1, \text{roles}^1), \langle -_{\text{roles}}, s, s', r \rangle, (m_2, \text{user}^2, \text{UA}^2, \text{PA}^2, \text{roles}^2)) \in \|\mathcal{R}_{\text{RBAC}}^{\text{adm}}\|_{\Sigma_{\text{RBAC}}}^{+} \\ \Leftrightarrow (m_1 = m_2 \wedge \text{user}^1 = \text{user}^2 \wedge \text{UA}^1 = \text{UA}^2 \wedge \text{PA}^1 = \text{PA}^2 \wedge \text{roles}^2 = \text{roles}^1[s' \leftarrow \text{roles}^1(s') \setminus \{r\}]) $$

TAB. D.6 – Sémantique des requêtes administratives
$$ \kappa_R^1 \subseteq \Sigma_{HRU} \times \mathcal{R}_{HRU} \times \mathcal{R}_{RBAC}^* $$

$$ \kappa_R^1 = \left\{ \begin{array}{l} ((m, m_D), \langle+, s, o, a\rangle, (\langle+, s, o, a\rangle)), \\ ((m, m_D), \langle-, s, o, a\rangle, (\langle-, s, o, a\rangle)), \\ ((m, m_D), \langle+_{m_D}, s, s', o, a\rangle, (\langle+_{PA}, s, o, a, s'\rangle)), \\ ((m, m_D), \langle-_{m_D}, s, s', o, a\rangle, (\langle-_{PA}, s, o, a, s'\rangle)) \end{array} \right\} $$

$$ \kappa_R^2 \subseteq \Sigma_{RBAC} \times \mathcal{R}_{RBAC} \times \mathcal{R}_{HRU}^* $$

$$ \kappa_R^2 = \left\{ \begin{array}{l} ((m, \text{user}, \text{UA}, \text{PA}, \text{roles}), \langle+, s, o, a\rangle, (\langle+, s, o, a\rangle)), \\ ((m, \text{user}, \text{UA}, \text{PA}, \text{roles}), \langle-, s, o, a\rangle, (\langle-, s, o, a\rangle)), \\ ((m, \text{user}, \text{UA}, \text{PA}, \text{roles}), \langle+_{\text{UA}}, s, u, r\rangle, (\text{Success})), \\ ((m, \text{user}, \text{UA}, \text{PA}, \text{roles}), \langle-_{\text{UA}}, s, u, r\rangle, (\text{Success})), \\ \left( (m, \text{user}, \text{UA}, \text{PA}, \text{roles}), \langle+_{\text{PA}}, s, o, a, r\rangle, \left( \text{List} \left( \bigcup_{s' \in S} \left\{ \begin{array}{l} \langle+_{m_D}, s, s', o, a\rangle \mid \exists r' \in R \\ r \le R \quad r' \wedge r' \in \text{roles}(s') \end{array} \right\} \right) \right) \right)), \\ \left( (m, \text{user}, \text{UA}, \text{PA}, \text{roles}), \langle-_{\text{PA}}, s, o, a, r\rangle, \left( \text{List} \left( \bigcup_{s' \in S} \left\{ \begin{array}{l} \langle-_{m_D}, s, s', o, a\rangle \mid \exists r' \in R \\ r \le R \quad r' \wedge r' \in \text{roles}(s') \end{array} \right\} \right) \right) \right)), \\ \left( (m, \text{user}, \text{UA}, \text{PA}, \text{roles}), \langle+_{\text{roles}}, s, s', r\rangle, \left( \text{List} \left( \bigcup_{s' \in S} \left\{ \begin{array}{l} \langle+_{m_D}, s, s', o, a\rangle \mid \exists r' \in R \\ r' \le R \quad r \wedge ((o, a), r') \in \text{PA} \end{array} \right\} \right) \right)), \\ \left( (m, \text{user}, \text{UA}, \text{PA}, \text{roles}), \langle-_{\text{roles}}, s, s', r\rangle, \left( \text{List} \left( \bigcup_{s' \in S} \left\{ \begin{array}{l} \langle-_{m_D}, s, s', o, a\rangle \mid \exists r' \in R \\ r' \le R \quad r \wedge ((o, a), r') \in \text{PA} \end{array} \right\} \right) \right) \right) \end{array} \right\} $$

$$ \kappa_R^3 \subseteq \Sigma_{BLP} \times \mathcal{R}_{BLP} \times \mathcal{R}_{RBAC}^* $$

$$ \kappa_R^2 = \left\{ \begin{array}{l} ((m, f_s, f_o), \langle+, s, o, a\rangle, (\langle+, s, o, a\rangle)), \\ ((m, f_s, f_o), \langle-, s, o, a\rangle, (\langle-, s, o, a\rangle)), \\ \left( (m, f_s, f_o), \langle+_{f_s}, s, s', l\rangle, \left( \begin{array}{l} \langle+_{\text{UA}}, s, s', l\rangle, \langle+_{\text{roles}}, s, s', l\rangle, \\ \langle-_{\text{roles}}, s, s', f_s(s')\rangle, \langle-_{\text{UA}}, s, s', f_s(s')\rangle \end{array} \right) \right)), \\ \left( (m, f_s, f_o), \langle+_{f_o}, s, s', l\rangle, \left( \begin{array}{l} \langle+_{\text{PA}}, s, o, \text{read}, l\rangle, \langle+_{\text{PA}}, s, o, \text{write}, l\rangle, \\ \langle-_{\text{PA}}, s, o, \text{read}, f_o(o)\rangle, \langle-_{\text{UA}}, s, o, \text{write}, f_o(o)\rangle \end{array} \right) \right) \end{array} \right\} $$

TAB. D.9 – Relations entre requêtes

*Comparaison des modèles.* Les lemmes D.3 et D.4, nous permettent d’utiliser la proposition D.6, pour établir formellement le lemme suivant.

**Lemme D.5**

$$ \begin{align*} \mathbb{M}_{HRU}[] &\subseteq \mathbb{M}_{RBAC}[(S, S, \emptyset)] \\ \mathbb{M}_{RBAC}[\rho_{RBAC}] &\subseteq \mathbb{M}_{HRU}[] \\ \mathbb{M}_{BLP}[\rho_{BLP}] &\subseteq \mathbb{M}_{RBAC}[(S, \mathcal{L}, \preceq)] \end{align*} $$

Nous montrons par ailleurs que le modèle RBAC n’est pas plus restrictif que le modèle de Bell et LaPadula.

**Lemme D.6** $\mathbb{M}_{RBAC}[\rho_{RBAC}] \not\subseteq \mathbb{M}_{BLP}[\rho_{BLP}]$

Il existe donc des situations pour lesquelles il n’est pas possible de simuler un système à base de rôles par un système mettant en œuvre la politique de Bell et LaPadula. Considérons par exemple un système pour lequel $S = \{s\}$ et $O = \{o\}$. Nous pouvons construire un état du système à base de rôles où $s$ n’a aucun droit sur $o$, alors que le système reposant sur la politique de Bell et LaPadula autorisera toujours l’accès en écriture de $s$ à $o$. Il n’existe donc pas de relation $\kappa_{\Sigma} \subseteq \Sigma_{RBAC} \times \Sigma_{BLP}$ qui soit $\mathcal{W}$-préservante.
## D.3 Analyse de flots

Nous complétons ici la présentation de l'analyse des flots d'information des modèles de contrôle d'accès faite dans la section 2.3 du chapitre 2. Nous illustrons également cette analyse en considérant les modèles HRU et de Bell et LaPadula.

### D.3.1 Flots engendrés par les exécutions d'un moniteur de référence

Dans la section 2.3.1, nous avons introduit des relations permettant de caractériser les flots d'information qui ont lieu lors d'une séquence d'états. La proposition suivante permet d'exprimer des propriétés de composition de ces relations lorsque les séquences d'états sont issues des exécutions d'une implantation d'un modèle de contrôle d'accès.

**Proposition D.7** *Soit $\mathbb{P}[\rho] = (\Sigma, \Omega)$ une politique de contrôle d'accès, $M[\rho] = (\mathbb{P}[\rho], \mathcal{R})$ un modèle de contrôle d'accès, $I = (\tau, \Sigma^I)$ une implantation de $M[\rho]$ et $F = \text{Exec}(\tau, \Sigma^I)$.*

1. Si $I$ est $\mathbb{P}[\rho]$-complète, alors $\hookrightarrow_{\Sigma|\Omega}^{OO} \hookrightarrow_F^{OO}$, $\hookrightarrow_{\Sigma|\Omega}^{OS} \hookrightarrow_F^{OS}$ et $\hookrightarrow_{\Sigma|\Omega}^{SO} \hookrightarrow_F^{SO}$.

2. Si $I$ est $\mathbb{P}[\rho]$-correcte, alors $\hookrightarrow_F^{OS} \subseteq \rightsquigarrow_{\mathbb{P}[\rho]}^{OS} \circ \hookrightarrow_F^{OO}$ et $\hookrightarrow_F^{SO} \subseteq \hookrightarrow_F^{OO} \circ \rightsquigarrow_{\mathbb{P}[\rho]}^{SO}$.

3. Si $I$ est $\mathbb{P}[\rho]$-correcte et $\hookrightarrow_{\Sigma|\Omega}^{OO}$ est transitive, alors $\hookrightarrow_F^{OO} \subseteq \hookrightarrow_{\Sigma|\Omega}^{OO}$, $\hookrightarrow_F^{OS} \subseteq \rightsquigarrow_{\mathbb{P}[\rho]}^{OS} \circ \hookrightarrow_{\Sigma|\Omega}^{OO}$ et $\hookrightarrow_F^{SO} \subseteq \hookrightarrow_{\Sigma|\Omega}^{OO} \circ \rightsquigarrow_{\mathbb{P}[\rho]}^{SO}$.

4. Si $I$ est $\mathbb{P}[\rho]$-complète est $\mathbb{P}[\rho]$ est libre, alors $\rightsquigarrow_{\mathbb{P}[\rho]}^{OS} \circ \hookrightarrow_{\Sigma|\Omega}^{OO} \hookrightarrow_F^{OS}$ et $\hookrightarrow_{\Sigma|\Omega}^{OO} \circ \rightsquigarrow_{\mathbb{P}[\rho]}^{SO} \subseteq \hookrightarrow_F^{SO}$.

5. Si $I$ est $\mathbb{P}[\rho]$-complète et $\Gamma$-complète, alors $\rightsquigarrow_{\mathbb{P}[\rho]}^{OS} \circ \hookrightarrow_F^{OO} \subseteq \hookrightarrow_F^{OS}$, et $\hookrightarrow_F^{OO} \circ \rightsquigarrow_{\mathbb{P}[\rho]}^{SO} \subseteq \hookrightarrow_F^{SO}$.

6. Si $\mathbb{P}[\rho]$ est libre et $I$ est $\mathbb{P}[\rho]$-correcte, alors $\hookrightarrow_F^{OS} \subseteq \hookrightarrow_{\Sigma|\Omega}^{OS}$ et $\hookrightarrow_F^{SO} \subseteq \hookrightarrow_{\Sigma|\Omega}^{SO}$.

### D.3.2 Mécanisme de détection de flots

Dans la section 2.3.2, nous avons introduit un formalisme permettant de spécifier un mécanisme de détection de flots. Nous définissons ici un tel mécanisme dans ce formalisme. Il s'agit de la formalisation d'un système de détection d'intrusion présenté dans [55, 54].

Le mécanisme de détection de flots que nous introduisons ici permet de détecter les flots engendrés par des séquences d'états produisant des flots ne respectant pas une certaine politique de flots $\rightsquigarrow^{OO}$ entre objets. Ce mécanisme peut être aussi utilisé pour des politiques de flots entre sujets et objets. Il suffit pour cela d'associer à chaque sujet $s$ un objet $o_s$. Dans ce cas, les objets du système sont les objets de l'ensemble $\mathcal{O}$ et les objets d'un ensemble $\mathcal{O}_S$ contenant les objets associés aux sujets. Bien sûr, les objets considérés par le prédicat de sécurité sont les objets de $\mathcal{O}$ et pour tout état $\sigma$, nous supposons :

$$ \{(s, o_s, \text{read}), (s, o_s, \text{write})\} \subseteq \Lambda(\sigma) \\ \text{et } ((s, o, a) \in \Lambda(\sigma) \wedge o \in \mathcal{O}_S) \Rightarrow o = o_s $$

Dans ce cadre, on montre facilement que :

$$ \hookrightarrow_{(\sigma_1, \dots, \sigma_n)}^{OS} = \{o_1 \hookrightarrow_{(\sigma_1, \dots, \sigma_n)}^{OO} o_2 \mid o_1 \in \mathcal{O} \wedge o_2 \in \mathcal{O}_S\} $$

$$ \hookrightarrow_{(\sigma_1, \dots, \sigma_n)}^{SO} = \{o_1 \hookrightarrow_{(\sigma_1, \dots, \sigma_n)}^{OO} o_2 \mid o_1 \in \mathcal{O}_S \wedge o_2 \in \mathcal{O}\} $$
**Proposition D.9** $\forall (\sigma_1, \sigma_2, \dots, \sigma_n) \in F \ \forall o \in \mathcal{O} \ T_{\sigma_n}^R(o) = \bigcap_{\{o_j | o_j \to^{\mathcal{O}} (\sigma_1, \dots, \sigma_n)} o} T_{\sigma_1}^R(o_j)$

Le système de “tags” permet de définir le prédicat $\mathcal{U}$ caractérisant les états d’alerte comme suit :

$$ \mathcal{U}(\sigma) \Leftrightarrow \exists o \in \mathcal{O} \ T_{\sigma}^{R}(o) \cap T_{\sigma}^{W}(o) = \emptyset $$

Nous montrons alors que le mécanisme de détection de flots ainsi obtenu est correct et complet.

**Proposition D.10** $\mathbb{F}[\rho, E, F, \rightsquigarrow_{\mathbb{F}}] = (\Sigma, \mathcal{U})$ est correct et complet.

### D.3.3 Application

Dans cette section, nous illustrons l’analyse des flots d’information d’un modèle de contrôle d’accès en considérant des variantes du modèle HRU et du modèle de Bell et LaPadula présentés précédemment. Ces variantes sont obtenues en imposant que toutes les informations de sécurité soient statiques durant la vie du système. Un état consiste donc juste en la description des accès courants effectués dans le système. On note ainsi $\Sigma^{acc} = \wp(\mathcal{A})$ l’ensemble des états de ces deux modèles (la définition des prédicats de sécurité $\Omega_{HRU}$ et $\Omega_{BLP}$ est inchangée). Il s’agit donc d’analyser les flots d’information pour les modèles définis comme suit :

$$ \begin{array}{ll} \rho'_{HRU} = m_D & \rho'_{BLP} = (\mathcal{L}, \leq, \gamma, \lambda, f_s, f_o) \\ \mathbb{P}'[\rho'_{HRU}] = (S, \mathcal{O}, \mathcal{A}, \Sigma^{acc}, \Omega_{HRU}) & \mathbb{P}'[\rho'_{BLP}] = (S, \mathcal{O}, \mathcal{A}, \Sigma^{acc}, \Omega_{BLP}) \\ \mathbb{M}'[\rho'_{HRU}] = (\mathbb{P}'[\rho'_{HRU}], \mathcal{R}^{acc}) & \mathbb{M}'[\rho'_{BLP}] = (\mathbb{P}'[\rho'_{BLP}], \mathcal{R}^{acc}) \end{array} $$

Les instances de ces modèles que nous utiliserons dans les exemples sont définies comme suit. Pour HRU, l’ensemble des accès autorisés peut être représenté par une matrice de droits d’accès et l’ensemble $m_D$ que nous considérons est spécifié par la matrice suivante :

<table><thead><tr><th></th><th>o<sub>1</sub></th><th>o<sub>2</sub></th><th>o<sub>3</sub></th><th>o<sub>4</sub></th></tr></thead><tbody><tr><th>Alice</th><td>read, write</td><td></td><td>read</td><td></td></tr><tr><th>Bob</th><td>read</td><td>read, write</td><td></td><td></td></tr><tr><th>Charlie</th><td></td><td>read, write</td><td></td><td>write</td></tr></tbody></table>

Pour le modèle de Bell et LaPadula, nous considerons le paramètre $\rho'_{BLP}$ représenté sur la figure D.1.

#### Analyse de flots

*Politiques de confidentialité et d’intégrité.* Les politiques de confidentialité et d’intégrité, exprimées en termes de flots d’information, induites pas les politiques de contrôle d’accès
<figure><img src="image_20.png" /><figcaption>FIG. D.1 – $\rho'_{BLP}$</figcaption></figure>

sont définies comme suit :

$$ \sim_{\mathbb{P}'_{HRU}[m_D]}^{OS} = \left\{ \begin{array}{ll} o_1 \to^{OS} \text{Alice,} & o_3 \to^{OS} \text{Alice,} \\ o_2 \to^{OS} \text{Bob,} & o_2 \to^{OS} \text{Charlie} \end{array} \right\} \quad o_1 \to^{OS} \text{Bob,} $$

$$ \sim_{\mathbb{P}'_{BLP}[\rho'_{BLP}]}^{OS} = \left\{ \begin{array}{ll} o_1 \to^{OS} \text{Alice,} & o_2 \to^{OS} \text{Alice,} \\ o_3 \to^{OS} \text{Bob,} & o_4 \to^{OS} \text{Bob,} \end{array} \right\} \quad o_3 \to^{OS} \text{Alice,} \quad o_4 \to^{OS} \text{Alice,} $$

$$ \sim_{\mathbb{P}'_{HRU}[m_D]}^{SO} = \{ \text{Alice} \hookrightarrow^{SO} o_1, \text{Bob} \hookrightarrow^{SO} o_2, \text{Charlie} \hookrightarrow^{SO} o_2, \text{Charlie} \hookrightarrow^{SO} o_4 \} $$

$$ \sim_{\mathbb{P}'_{BLP}[\rho'_{BLP}]}^{SO} = \left\{ \begin{array}{ll} \text{Alice} \hookrightarrow^{SO} o_1, & \text{Alice} \hookrightarrow^{SO} o_2, \\ \text{Charlie} \hookrightarrow^{SO} o_1, & \text{Charlie} \hookrightarrow^{SO} o_2, \\ \text{Bob} \hookrightarrow^{SO} o_1, & \text{Bob} \hookrightarrow^{SO} o_2, \end{array} \right\} \quad \begin{array}{ll} \text{Alice} \hookrightarrow^{SO} o_3, & \text{Alice} \hookrightarrow^{SO} o_4, \\ \text{Charlie} \hookrightarrow^{SO} o_3, & \text{Charlie} \hookrightarrow^{SO} o_4, \\ \text{Bob} \hookrightarrow^{SO} o_3, & \text{Bob} \hookrightarrow^{SO} o_4 \end{array} $$

Pour la politique de Bell et LaPadula, nous pouvons montrer que les relations $\sim_{\mathbb{P}'_{BLP}[\rho'_{BLP}]}^{OS}$ et $\hookrightarrow^{OO}_{Exec(\tau_{BLP}, \Sigma_{BLP}^I)}$ peuvent s'exprimer directement à partir des niveaux de sécurité.

**Lemme D.7**

$$ 1. \forall o \in \mathcal{O} \ \forall s \in \mathcal{S} \ o \overset{\sim}{\to}^{OS}_{\mathbb{P}'_{BLP}[\rho'_{BLP}]} \ s \Leftrightarrow f_o(o) \leq f_s(s) $$

2. Soit $o_1$ et $o_2$ deux objets.

$$ (a) \ o_1 \hookrightarrow^{OO}_{Exec(\tau_{BLP}, \Sigma_{BLP}^I)} o_2 \Rightarrow f_o(o_1) \leq f_o(o_2) $$

(b) Si il existe un sujet $s \in \mathcal{S}$ tel que $f_o(o_1) \leq f_s(s)$, alors :

$$ f_o(o_1) \leq f_o(o_2) \Rightarrow o_1 \hookrightarrow^{OO}_{Exec(\tau_{BLP}, \Sigma_{BLP}^I)} o_2 $$

Nous montrons également que l'ensemble des exécutions de $(\tau_{BLP}, \Sigma_{BLP}^I)$ est correct et complet pour les politiques de flots $\sim_{\mathbb{P}'_{BLP}[\rho'_{BLP}]}^{OS}$ and $\sim_{\mathbb{P}'_{BLP}[\rho'_{BLP}]}^{SO}$.

**Lemme D.8** $Exec(\tau_{BLP}, \Sigma_{BLP}^I)$ est correct et complet pour $\sim_{\mathbb{P}'_{BLP}[\rho'_{BLP}]}^{OS}$ et $\sim_{\mathbb{P}'_{BLP}[\rho'_{BLP}]}^{SO}$.
Cette propriété n'est pas vérifiée par les exécutions de $(\tau_{HRU}, \Sigma_{HRU}^I)$. En effet, si l'on considère par exemple l'ensemble $m_D$ introduit précédemment, nous avons $o_3 \hookrightarrow_{Exec(\tau_{HRU}, \Sigma_{HRU}^I)}^{OS}$
Bob (car Alice peut lire $o_3$ et écrire dans $o_1$ qui est accessible en lecture par Bob) mais nous n'avons pas $o_3 \rightsquigarrow_{\mathbb{P}'_{HRU}[m_D]}^{OS}$ Bob. De manière similaire, nous avons Bob $\hookrightarrow_{Exec(\tau_{HRU}, \Sigma_{HRU}^I)}^{SO}$ $o_4$
(car Bob peut écrire dans $o_2$ et Charlie peut lire $o_2$ et écrire dans $o_4$) mais nous n'avons pas Bob $\rightsquigarrow_{\mathbb{P}'_{HRU}[m_D]}^{SO}$ $o_4$. Il est toutefois possible de caractériser les paramètres de sécurité
de la politique HRU pour lesquels la propriété de correction est vérifiée.

**Lemme D.9**

1. Exec($\tau_{HRU}, \Sigma_{HRU}^I$) est complet et correct pour $\rightsquigarrow_{\mathbb{P}'_{HRU}[m_D]}^{OS}$ ssi :

$$ \begin{gather*} \forall s_1, s_2 \in \mathcal{S} \quad \forall o_1, o_2 \in \mathcal{O} \\ \{ (s_1, o_1, \mathit{read}), (s_1, o_2, \mathit{write}), (s_2, o_2, \mathit{read}) \} \subseteq m_D \Rightarrow (s_2, o_1, \mathit{read}) \in m_D \end{gather*} $$

2. Exec($\tau_{HRU}, \Sigma_{HRU}^I$) est complet et correct pour $\rightsquigarrow_{\mathbb{P}'_{HRU}[m_D]}^{SO}$ ssi :

$$ \begin{gather*} \forall s_1, s_2 \in \mathcal{S} \quad \forall o_1, o_2 \in \mathcal{O} \\ \{ (s_1, o_1, \mathit{write}), (s_2, o_1, \mathit{read}), (s_2, o_2, \mathit{write}) \} \subseteq m_D \Rightarrow (s_1, o_2, \mathit{write}) \in m_D \end{gather*} $$

**Détection de flots “illégaux”**

Puisque les exécutions de $(\tau_{HRU}, \Sigma_{HRU}^I)$ ne sont pas correctes pour les politiques de
flots $\rightsquigarrow_{\mathbb{P}'_{HRU}[\rho'_{HRU}]}^{OS}$ et $\rightsquigarrow_{\mathbb{P}'_{HRU}[\rho'_{HRU}]}^{SO}$, nous utilisons maintenant le mécanisme de détection
de flots défini dans la section D.3.2 afin que le système lève une alerte dès qu'il détecte un
flot ne respectant pas les politiques $\rightsquigarrow_{\mathbb{P}'_{HRU}[\rho'_{HRU}]}^{OS}$ et $\rightsquigarrow_{\mathbb{P}'_{HRU}[\rho'_{HRU}]}^{SO}$. Ici ces deux politiques
de flots sont exprimées en associant un objet $o_s$ à chaque sujet $s$. Plus formellement, le
mécanisme de détection de flots est obtenu en considérant :

- l'ensemble $m_D$ comme paramètre de sécurité $\rho$,

- l'ensemble $\Sigma_{\Omega_{HRU}}$ comme ensemble d'états observables $E$,

- l'ensemble Exec($\tau_{HRU}, \Sigma_{HRU}^I$), où $\Sigma_{HRU}^I \subseteq \{\sigma \in \Sigma \mid \Lambda(\sigma) = \emptyset\}$, comme ensemble
de séquences d'états observables,

- la relation :

$$ \rightsquigarrow^{OO} = \left\{ \begin{array}{ll} o_1 \hookrightarrow^{OO} o_2 & (o_1 \in \mathcal{O} \wedge o_2 = o_s \in \mathcal{O}_S \wedge o_1 \rightsquigarrow_{\mathbb{P}'_{HRU}[\rho'_{HRU}]}^{OS} (\rho'_{HRU})^s) \\ \vee & (o_1 = o_s \in \mathcal{O}_S \wedge o_2 \in \mathcal{O} \wedge s \rightsquigarrow_{\mathbb{P}'_{HRU}[\rho'_{HRU}]}^{SO} (\rho'_{HRU})^{o_2}) \end{array} \right\} $$

comme politique de flots $\rightsquigarrow^{OO}$.

Les propositions D.8, D.10 et 2.1, nous garantissent alors que les états d'alerte sont exactement les états issus de séquences engendrant un flot ne respectant pas les politiques $\rightsquigarrow_{\mathbb{P}'_{HRU}[\rho'_{HRU}]}^{OS}$ et $\rightsquigarrow_{\mathbb{P}'_{HRU}[\rho'_{HRU}]}^{SO}$.

Par exemple, considérons à nouveau le modèle HRU introduit précédemment. La politique de contrôle d'accès induit la politique de confidentialité et d'intégrité suivante, exprimée par des relations de flots entre objets :

$$ \rightarrow_{HRU} = \left\{ \begin{array}{ll} (\{o_1, o_3, o_A\}, o_1) & (\{o_1, o_2, o_B\}, o_2) \\ (\{o_3\}, o_3) & (\{o_2, o_4, o_c\}, o_4) \\ (\{o_1, o_2, o_B\}, o_B) & (\{o_2, o_c\}, o_c) \end{array} \right\} $$
où $o_A$, $o_B$ et $o_C$ sont les objets respectivement associés aux sujets Alice, Bob et Charlie. Considérons la séquence d'états $(\sigma_1, \sigma_2, \sigma_3, \sigma_4)$ telle que $\sigma_1$ est un état dont l'ensemble des accès courants est vide, $\sigma_2$ est obtenu en ajoutant un accès en lecture sur $o_3$ pour Alice, $\sigma_3$ en ajoutant un accès en écriture sur $o_1$ pour Alice, et $\sigma_4$ en ajoutant un accès en lecture sur $o_1$ pour Bob. Aucun des états $\sigma_1$, $\sigma_2$ et $\sigma_3$ n'est un état d'alerte, mais nous avons :

$$ T_{\sigma_4}^R(o_B) \cap T_{\sigma_4}^W(o_B) = \{(o_1, o_3, o_3), o_1\}, (o_3), o_3\}, \{o_1, o_3, o_A\}, o_A\} \cap \{(o_1, o_2, o_B), o_B\} = \emptyset $$

et donc $\sigma_4$ est un état d'alerte ce qui correspond bien au fait que Bob accède au contenu de l'objet $o_3$ alors que la politique de confidentialité ne l'y autorise pas.