4.5 Framework logique pour les systèmes de réputation
Dans cette section, nous détaillons le fonctionnement du framework logique défini pour le mécanisme de réputation proposé par Karl Krukow et al. [59]. Ce système de réputation a été conçu pour les applications en ligne qui ont besoin de la confiance pour contrôler les interactions entre les différentes entités du système. K. Krukow a proposé un modèle d’application qui repose sur une structure d’événement qui formalise le système par son utilisation des événements et des politiques pour chaque entité.
Le contenu de cette section est un résumé du travail de K. Krukow et al. [59] auquel nous avons ajouté les détails qui permettront au lecteur de mieux comprendre de quelle manière nous l’avons adapté à notre système de négociation de la confiance. Pour finir ce préambule, nous rappelons que le mécanisme de recommandation proposé par K. Krukow n’est en aucun cas un mécanisme de négociation.
Le principe qui à été mis en œuvre lors de la conception du framework de recommandation de K. Krukow est le suivant : utiliser les informations sur les comportements passés du principal pour évaluer de futures interactions avec lui.
Dans ce modèle, les informations sur les comportements passés et futurs des participants sont spécifiées dans le langage de politique. Tous les comportements passés d’un principal sont conservés dans un historique des transactions.
Toute action future entreprise par un principal sera validée si nous avons la conformité de la politique et de l’historique des transactions. Le contrôle d’accès aux ressources est réalisé de la manière suivante : « si le principal p a le droit d’accéder à la ressource r à l’instant t, alors les comportements passés de p jusqu’à l’instant t satisfont la politique d’accès à r ».
Le principal observe les comportements passés de son partenaire sous la forme d’événements. L’historique qui contient les informations sur ces comportements est donc un ensemble d’événements respectant les règles de relation entre événements. La modélisation de ces relations entre événements est réalisée a l’aide de la structure d’événements (event structure) [71].
Le langage proposé pour exprimer la politique d’interaction des entités est une variante de la logique LTL [74], appelée PP-LTL (Pure-Past LTL). Cette logique est restreinte à l’expression des faits survenus dans le passé par l’usage des quantificateurs G−1 , F −1 et X −1 dont la sémantique est définie en logique LTL. Dans ce modèle, le comportement est modélisé comme un ensemble d’événements et chaque structure linéaire peut être modélisée par une structure d’événements que nous allons présenter ci-dessous.
Chaque entité dans le système a sa propre politique pour protéger ses ressources. Nous pouvons proposer la politique de l’entité en utilisant un modèle d’autorisation d’accès à la ressource. Ce modèle d’autorisation d’accès nous permet de définir les conditions, les contraintes pour avoir accès à la ressource. C’est une base pour définir la politique de l’entité.
De manière à contrôler l’accès aux ressources, la politique de sécurité doit être évaluée en fonction de l’historique des comportements de l’entité. Cela se ramène à un problème de vérification de la satisfaction d’une formule logique PP-LTL auprès de l’historique de l’entité.
Les auteurs ont utilisés les algorithmes proposés par Havelund et Roçu [40] pour résoudre ce problème de vérification. Il s’agit d’un algorithme basé sur les techniques de la programmation dynamique et qui, bien qu’efficace n’en reste pas moins de complexité exponentielle (il s’agit d’un problème NP-complet ).
4.5.1 Observation des événements
Le système est composé de plusieurs entités en interaction. Ces entités s’échangent des informations sous la forme de messages. L’observation de ces messages permet aux entités de déterminer les événements qui seront à prendre en compte et à rajouter à l’historique.
Si une entité a des interactions avec plusieurs autres entités au même moment, les observations doivent permettre de répartir les événement dans les historiques concernés (notion de sessions indépendantes).
Voici un exemple de ce fonctionnement appliqué à un scénario d’enchères sur le site eBay [38].
Lorsqu’un vendeur décide de vendre un produit aux enchères, il commence par publier une annonce sur le site. Á partir de ce moment, les clients potentiellement intéressés par ce produit peuvent commencer à enchérir et à sur-enchérir.
Lorsque la période d’enchère est terminée (en général une ou deux semaines selon les préférences du vendeur), le client qui a fait l’offre la plus élevée remporte l’enchère. Ce client va maintenant avoir à effectuer la transaction avec le vendeur du produit pour concrétiser son achat. Le module de gestion de la confiance est réalisé de manière à lui permettre d’observer les événements et de prendre des décisions pour chacune des étapes de la transaction.
Maintenant que l’enchère est terminée, nous spécifions la transaction par l’ordre des différents échanges entre le client et le vendeur sous la forme du protocole suivant :
-Le vendeur envoie la confirmation de la vente du produit objet de l’enchère et en demande de paiement.
Lorsque le client reçoit la demande de paiement, il a deux choix possibles : payer pour continuer la transaction et disposer du produit ou ne pas payer. Si le client ne paie pas le vendeur, la transaction se termine. Si le client paie, la transaction se poursuit.
Lorsque le vendeur reçoit le paiement, il envoie une confirmation de paiement au client et lui envoie le produit. À ce stade de la transaction, le vendeur peut être malhonnête et ne pas envoyer la confirmation de paiement ni le produit au client.
Enfin, le vendeur et le client peuvent évaluer mutuellement la transaction (positive, neutral, negative ).
Le client peut observer les événements suivants concernant le comportement du vendeur : la demande de paiement, le paiement au vendeur, la confirmation du paiement par le vendeur (et bien sûr l’envoi du produit) ou bien le fait d’ignorer la demande de paiement et enfin, l’évaluation de la transaction.
Le scénario sera modélisé dans un framework de la structure d’événements expliqué en détail dans les sections suivantes. Cela donnera différents éléments du scénario : des événements observés possibles, l’historique de la transaction et la politique de sécurité appliquée.
4.5.2 Framework de structure des événements
Quand une interaction a lieu, nous voyons apparaître les événements dans un certain ordre et il existe des relations entre eux qui sont liées au type de transaction qui est en train de se dérouler. Certains événements ne peuvent pas se produire si d’autres se sont déjà produit. Nous dirons que ces événements sont en conflit et qu’il y aura une exclusion mutuelle entre ces événements.
Par exemple, dans le scénario de l’application eBay, si le client a généré l’événement positive (l’évaluation du vendeur sur la transaction), on ne peut pas observer l’événement neutral ou l’événement negative sur cette transaction. Un événement peut dépendre d’un autre dans le sens où ce deuxième événement ne pourrait pas avoir lieu si le premier n’avait pas été déjà observé (relation de causalité).
Dans le scénario eBay, l’événement de confirmation de paiement ne peut pas avoir lieu si l’événement paiement n’a pas eu lieu au préalable. Les événements sont dits indépendants s’ils ne sont ni en conflit ni dépendant d’autres événements. Par exemple les événements paiement et négative (évaluation de la transaction) sont indépendants.
Un événement ne peut être rajouté à l’historique d’une transaction que s’il n’entre pas en conflit avec un événement déjà observé et qu’il respecte les conditions de dépendances imposées par l’application. La notion de structure d’événements va nous permettre de spécifier ces contraintes.
Structure d’événements
Une structure d’événement est un triplet ES = (E, ≤, #) qui se compose d’un ensemble d’événements E et de deux relations binaires sur E : ≤ et #. Chaque élément e ∈ E est un événement. La relation # est la relation de conflit, et ≤ est la relation de causalité.
-Relation de causalité (≤) : étant donné un événement e′ ∈ E, pour tout e ∈ E, si e ≤ e′ (e′ dépend/est une conséquence de e) alors e′ ne peut apparaître qu’après e; pour chaque e ∈ E, l’ensemble ⌈e⌉ = { e′ ∈ E | e′ ≤ e} est fini. Cette relation est symétrique et non-réflexive.
Relation de conflit (#) : cette relation doit satisfaire l’axiome de transitivité suivant : pour tout événement e, e′, e” ∈ E, (e#e′ et e′ ≤ e”) implique e#e”.
Événements indépendants : deux événements sont indépendants s’ils n’ont pas de relation de causalité et ne sont pas en conflit.
La figure 4.3 présente une structure d’événements utilisable dans le cadre du scénario de l’application eBay que nous venons de décrire dans le paragraphe précédent.
________ caucality relation
—————conflict relation
Fig. 4.3 Structure d’événements observée par l’acheteur
Les evénements observés par l’acheteur représentent les différents comportements que peut avoir l’entité. Ils ont le sens suivant :
-positive, negative, neutral : il s’agit des valeurs possibles que peut prendre l’évaluation d’une transaction. Lorsque la transaction est terminée (par un échec ou pas), l’acheteur peut donner une évaluation sur la transaction.
pay/ignore : l’événement pay indique que l’acheteur paie pour la transaction après avoir reçu la demande de paiement du vendeur. Par contre, ignore indique que l’acheteur ignore, la transaction sera interrompue.
confirm/time-out : les événements indiquant le comportement du vendeur après que l’acheteur a payé pour sa demande de paiement. Soit le vendeur confirme avoir reçu le paiement (confirm ), soit il ne le confirme pas (time-out ). Dans ce cas de time-out, le client considère que le vendeur est malhonnête et la transaction échoue.
Configuration
Avec les relations de causalité et de conflit, nous pouvons construire un sous-ensemble des événements observables. Les événements observés respectant ces relations représentent une session de la transaction et sont désignés sous le nom de configuration :
Soit une structure d’événements ES = (E, ≤, #). Un sous-ensemble d’événements X ∈ E est une configuration, si et seulement si, il satisfait les conditions d’absence de conflit et de causalité fermée (clôture de E par ≤). Les propriétés suivantes doivent être vérifiées : Pour tout d, d′ ∈ X et e ∈ E
-absence de conflit : d¬#d′
causalité fermée : e ≤ d ⇒ e ∈ X
La notation CE S désigne l’ensemble des configurations de ES, et C 0 ⊆ CE S signifie un ensemble fini des configurations. Une configuration est maximale si son ordre partiel (CE S , ⊆) est maximal. Une configuration finie permet de modéliser une transaction. La configuration maximale présente l’information complète d’une transaction. L’entité peut avoir plusieurs transactions et elle doit observer et prendre en compte l’information de toutes ces transactions.
Historique
Pour une structure d’événements ES, l’historique local des transactions est un ensemble fini de configurations, h = x1x2 . . . xn ⊆ C 0 ∗. Chaque élément xi dans l’historique h est une session qui correspond à l’exécution d’une transaction.
Dans le cas du scénario eBay et en utilisant la structure d’événements présentée figure 4.3, nous pourrions avoir l’historique suivant :
{pay,confirm,positive}{pay,confirm,neutral}{pay}
Cet exemple nous montre l’historique d’un client qui a eu trois transactions avec un même vendeur. Les deux premières transactions sont terminées, la troisième en est à l’étape du paiement et en attente de sa confirmation.
Les deux opérations suivantes sont définies pour manipuler l’historique : new et update.
4.5.3 Langage de politique
Le fait de disposer d’informations sur le comportement passé de l’acteur nous permettra d’en tenir compte lorsqu’il sera nécessaire de prendre des décisions lors d’interactions futures. Les décisions qui seront à prendre dans ce contexte sont de type binaire, elles indiqueront si l’interaction pourra avoir lieu ou non. la décision de continuer la transaction sera prise si la politique locale peut être satisfaite en utilisant l’historique des interactions.
Dans ce système, l’auteur a utilisé un langage d’expression de la politique qui est une variante de LTL [74], variante qui ne s’applique qu’aux seuls faits passés, logique PP-LTL. Dans ce langage, l’historique des transactions est basé sur la structure d’événements et est utilisé comme un système de transitions pour tirer le meilleur parti des algorithmes issus du model-checking.
La politique est représentée par une formule de logique PP-LTL. On définit la relation de satisfaction |= entre une politique ψ et un historique H : H |= ψ (l’historique H satisfait aux exigences de la politique ψ).
La politique utilisée dans ce système est construite de manière à assurer le contrôle d’accès aux ressources. Pour construire leur modèle, les auteurs se sont inspirés du modèle de contrôle d’accès utilisant l’historique des comportements de Edjlali et al. [24].
Syntaxe
Le langage est défini pour une structure d’événements ES = (E, ≤, #). Supposons que e, e′ , ei soient des événements appartenant à E. La syntaxe du langage, donnée sous sa forme BNF est la suivante :
ψ ::= e | ⋄e | ψ0 ∨ ψ1 | ψ0 ∧ ψ1 | ¬e | X −1 ψ | ψ0 S ψ1
Pour cette définition, e et ⋄e sont des propositions atomiques. Un événement e est vrai dans une session si e y est observé. La proposition ⋄e (e est possible ) est vrai si l’événement e est encore observable dans cette session. Les opérateurs X −1 (à l’étape précédente last time ) et S (depuis since ) sont les opérateurs standards concernant
les actions passées. La formule logique X −1 ψ est vraie si ψ est vraie dans la session précédente. La formule logique ψ0 S ψ1 est vraie si ψ1 a été vraie dans une session antérieure et si ψ0 est vraie dans toutes les sessions depuis ce moment là.
Sémantique
La sémantique du langage est présentée ici de façon inductive en utilisant la relation de satisfaction. L’historique contient plusieurs sessions H = x1x2 . . . xN ⊆ C 0 ∗ avec N > 0. La sémantique n’est considéré que pour les historiques non-vides 
. La relation de satisfaction H |= ψ implique que l’historique H satisfait les exigences de la politique ψ pour toutes les sessions de H .
Nous noterons (H, i) |= ψ le fait que H restreint à ses i premières sessions satisfait ψ. Nous avons donc H |= ψ si et seulement si (H, | H |) |= ψ (ssi ψ est vérifiée pour tous les éléments de H , | H | est le cardinal de H ). Nous donnons ici la définition inductive de cette relation de satisfaction :
La vérification de (H, 1) |= ψ est définie la manière suivante :
| (H, 1) |= e | ssi | e ∈ x1 | ||
| (H, 1) |= ⋄e | ssi | e¬#x1 | ||
| (H, 1) |= ψ0 | ∧ | ψ1 | ssi | (H, 1) |= ψ0 and (H, 1) |= ψ1 |
| (H, 1) |= ψ0 | ∨ | ψ1 | ssi | (H, 1) |= ψ0 ou (H, 1) |= ψ1 |
| (H, 1) |= ¬ψ(H, 1) |= X −1 ψ | ssissi | (H, 1) 2 ψf alse | ||
| (H, 1) |= ψ0 S ψ1 | ssi | (H, 1) |= ψ1 |
Si 1 < i ≤ N et si (H, i − 1) |= ψ est définie pour ψ, alors on peut définir (H, i) |= ψ
de la manière suivante :
Ces définitions inductives de la sémantique sont équivalentes à la sémantique courante de la logique LTL. Cette sémantique est définie seulement pour les historiques non-vides, . Cela veut dire que la politique ne peut pas être interprétée correctement si nous n’avons jamais eu de transaction. En pratique, l’acteur aura besoin
de prendre explicitement une décision s’il se trouve dans cette situation.
Voici quelques formes équivalentes utiles à la rédaction de politiques :
Exemples
Nous considérons à nouveau le scénario d’enchères sur eBay qui a été présenté dans la section précédente. En utilisant la structure d’événement présentée figure 4.3, nous pouvons exprimer les politiques suivantes :
-Politique 1 : le client ne participe qu’à des enchères proposées par les vendeurs qui ont toujours envoyé les produits payés.
ψbid ≡ ¬F −1 (time − out)
-Politique 2 : le client indique en plus que le vendeur n’a jamais émis d’avis
«négatif» sur une enchère dont le paiement a été réalisé.
ψbid ≡ ¬F −1 (time − out) ∧ G−1(negative → ignore)
4.5.4 Vérification de la satisfaction des politiques
L’observation des interactions permet au système de construire l’historique H . Nous avons besoin de savoir si cet historique respecte la politique ψ. Nous avons donc à vérifier que H satisfait bien la politique 
D’un point de vue dynamique, lors de chaque décision, il est nécessaire de vérifier que notre politique
est toujours satisfaite. Pour cette raison il est nécessaire de disposer d’un mécanisme de vérification efficace.
Dans le cas général, la complexité associée à la vérification et à la satisfiabilité d’une formule de logique LTL est un problème NP-complet [80] (PSPACE-complete pour être précis). Par contre, dans le cas de la logique LTL restreinte aux faits passés, nous allons voir qu’il existe des algorithmes efficaces pour vérifier la satisfiabilité d’une solution partielle.
Krukow et al. [59] ont proposé un modèle de vérification dynamique appelé DMC (Dynamic Model Checking). Les implémentations proposées utilisent l’algorithme récursif proposés par Havelund et Ro su[40].
Le principe de cet algorithme est le suivant : la vérification de la satisfaction de ψ pour la session (H, m) ((H, m) |= ψ) peut se transformer en un processus récursif
1. par la vérification de toutes les sous-formules ψj de ψ, pour la session précédente ((H, m − 1) |= ψj ),
2. et par la vérification de toutes les sous-formules propres ψi de ψ de la session courante, ((H, m) |= ψi ). Une sous-formule de ψ est dite propre s’il ne s’agit pas de ψ elle-même.
Les auteurs ont proposé deux implémentations de cet algorithme qui sont basées soit sur l’utilisation d’un tableau, soit sur l’utilisation d’un automate.
La complexité de chacun de ces algorithmes est calculée en fonction de la taille de la politique (| ψ |), de la taille de la structure d’événements utilisée (| CE S |) et du nombre de sessions actives dans l’historique (K ).
Implémentation utilisant un tableau
-Initialisation de la structure de données : O(| ψ |),
vérification : O(1),
création d’une session : O(| ψ |),
mise à jour d’une session : O((K − i + 1). | ψ |),
complexité en espace : O(K.(| ψ | + | E |).
Implémentation utilisant un automate à états fini
-Initialisation de la structure de données : O(2|ψ| . | CE S | . | ψ |),
vérification : O(1),
création d’une session : O(| ψ |),
mise à jour d’une session : O((K − i + 1)),
complexité en espace : O(K. | E | +2|ψ|. | CE S |).
4.5.5 Discussions
Ce langage d’expression de politique peut être rendu plus flexible; deux quantificateurs supplémentaires ont été suggérés par l’auteur : ∃ et ∀. À l’aide de ces deux quantificateurs, les politiques pourront être spécifiées de façon plus simple.
Considérons l’exemple suivant : soit deux événements open_f et create_f qui représentent respectivement les actions ouvrir et créer le fichier f. La formule G−1(open_f → F −1create_f ) exprime le fait que le fichier f doit être créé avant de pouvoir être ou-vert. Si nous voulons pouvoir utiliser cette politique pour n’importe quel fichier, nous pourrions l’indiquer avec le quantificateur ∀ si nous en disposions :
G−1(∀x.[open(x) → F −1 create(x)])
4.6 Synthèse
Dans ce chapitre, nous avons présenté les principes de conception de notre infrastructure de gestion de la confiance. Nous avons d’abord indiqué quels étaient les critères que nous avons retenus dans notre approche : décentralisation, utilisation de plusieurs sources d’informations, expression de la politique . . .
Nous avons également présenté l’architecture globale de notre système de gestion de la confiance.
Par la suite, nous avons présenté les éléments principaux qui constituent les bases qui nous permettront de construire notre système de confiance : le modèle formel de confiance de SECURE, la logique LTL et le modèle de la structure des événements.
