Narjes Ben Rajeb : Décider la connaissance d'un intrus pour des théories de vote électronique (travaux réalisés en collaboration avec M. Berrima et V. Cortier)

Les méthodes formelles jouent un rôle important dans l'analyse des protocoles de sécurité. Ces derniers requièrent souvent un raisonnement sur la connaissance d'un attaquant (intrus). Deux notions standards sont souvent considérées dans les approches formelles: la déductibilité et l'indistinguabilité. La première notion exprime si un attaquant peut connaître la valeur d'un secret, alors que la seconde permet de savoir si un attaquant peut observer une différence entre les exécutions d'un protocole avec différentes valeurs du secret. Plusieurs procédures de décision ont été proposées pour ces deux notions, mais aucune ne s'applique dans le contexte des protocoles de vote électronique qui font appel à des primitives cryptographiques spécifiques. Dans cet exposé, nous montrons que la déduction et l'indistinguabilité sont décidables en temps polynomial pour deux théories modélisant des protocoles de vote électronique : le protocole d'Okamoto et celui de Lee et al.

Bibliographie : · M. Abadi and V. Cortier. Deciding knowledge in security protocols under equational theories.Theoretical Computer Science, 367(1-2):2-32, 2006. · M. Berrima, N. Ben Rajeb et V. Cortier. Deciding knowledge in security protocols under some e-voting protocols. Rapport de recherche inria-00375784, 2009.

Riadh ROBBANA : Test des Systèmes de Durées (Tavaux réalisés avec Saddek Bensalem, Lotfi Majdoub, Moez Krichen et Stavros Tripakis [1,2, 4] )

Dans cet exposé, nous considérons le problème de test des systèmes à durées et plus précisément au test de conformité de ces systèmes. Les systèmes à durées constituent un extension des systèmes temporisés dans le sens où ils permettent de raisonner sur l'accumulation du temps écoulé durant certaines phases du système, cette accumulation de temps est appelée durée, alors que pour les systèmes temporisés il n'est possible de raisonner que sur des différences de temps séparant des paires d'événements. L'activité de test de conformité consiste à examiner si une implémentation sous test considérée comme un boîtier noir dont le testeur ne connaît pas son code est conforme à sa spécification. L'approche de test que nous considérons est basée sur le concept d'objectif de test. L'objectif de test peut être vu comme un ensemble de propriétés qui doivent être satisfaites par le système considéré, et faire du test par objectif, consiste à générer seulement les cas de test conformes à l'objectif considéré. Nous verrons à travers cet exposé, l'algorithme de test des systèmes à durées que nous proposons, qui combine la génération et l'exécution de test sur l'implémentation en respectant une relation de conformité inspirée de la relation de conformité ioco proposée par Tretmans [3].

[1] L.Majdoub and R.Robbana, "Automatic Test of Duration Systems with an approximation method", in STV'07 System Testing and Validation Workshop, Paris, December 2007. [2] S. Bensalem, M. Krichen, L. Majdoub, R. Robbana et S. Tripakis. "Test Generation for Duration Systems". Dans le workshop VECoS 2007, mai 2007, Alger, Algérie. [3] J. Tretmans, Testing Concurrent Systems : A Formal Approach, CONCUR'99 , 10th Int, conference on Concurrency Theory, LNCS 1664, pages 46-65, Springer -Verlag, 1999. [4] L. Majdoub and R. Robbana : Testing Duration Systems, Journal Européen des Systèmes Automatisés numéro spécial JESA les méthodes formelles temps-réel, Vol 42/9 2008, pp 1111- 1134..