Adresse mail : dima
at univ-paris12 dot fr La logique temporelle de la connaissance (voir le cours ici) permet d'exprimer des propriétés de connaissance dans des systèmes multi-agents. En particulier, elle permet de spécifier des propriétés comme la fuite d'information, l'authenticité, l'anonymat etc.
Le but de ce stage est d'évaluer l'expressivité des propriétés de transfert de confiance dans un réseau de pairs. Le contexte est celui d'un protocole de communication pair-à-pair dans lequel chaque pair peut déléguer des serveurs à faire certaines opérations à sa place. Le protocole est sous développement dans le cadre du projet ANR SPREADS, dirigé par UbiStorage, PME basée à Amiens, et dans lequel le LACL est impliqué dans la partie vérification des propriétés de sécurité.
Le travail demandé est de modéliser, dans un modèle multi-agent, le protocole du projet SPREADS, de spécifier certaines propriétés de transfert de confiance et de vérifier ces propriétés sur le modèle construit. Le point de départ est l'article [1] et le document [3] ci-dessous. L'étape de vérification impliquerait le choix et l'utilisation d'un outil de model-checking existant, ou se ferait, le cas échéant, en corrélation avec le travail dans le cadre d'un autre sujet proposé au LACL.
Possibilité de rémunération du stage sur le projet ANR SPREADS.
Références :
[1] C.
Dima : Revisiting satisfiability and model-checking for CTLK with
synchrony and perfect recall, Proceedings of CLIMA 2008, disponible
sur la page web personnelle.
[2]
R. Fagin, J. Halpern, Y. Moses, M. Vardi : Reasoning
about knowledge, MIT Press (disponible à la bibliothèque
du LACL).
[3] Descriptif du protocôle
de communication P2P utilisé dans le cadre du projet SPREADS,
document non-public.