VALIDATIONS DES SOLUTIONS DE SECURITE DU PROTOCOLE SIP

Validation des solutions de sécurité du protocole SIP

Méthodes et outils de validation

. Les méthodes A l’heure où les systèmes d’informations sont de plus en plus complexes et par là même plus vulnérables, le besoin d’assurer la sécurité s’est généralisé à tous les niveaux dans les réseaux [BOI07]. La sécurité des communications repose sur l’utilisation de fonctions mathématiques et sur l’emploi de protocoles, appelés « protocole de sécurité ». Ces derniers établissent les règles d’échanges entre les différents acteurs d’un ou des réseaux. C’est bien ces mécanismes que nous avons contribué à renforcer avec nos solutions. Pour s’assurer que ces dernières répondaient bien aux attentes, les trois contributions ont été validées soit pratiquement, soit formellement. Les deux méthodes retenues sont donc : – la validation pratique basée sur l’implémentation et l’observation ; – la validation formelle : cette méthode repose sur le modèle d’attaque de Dolev Yao [DOL83]. Pour ce fait, deux hypothèses fortes sont posées : les algorithmes de cryptologie sont considérés comme sûrs, et l’attaquant contrôle le réseau. Ce modèle est à la base du logiciel AVISPA [AVISPA] qui a été utilisé pour cette validation. 

AVISPA

AVISPA (Automated Validation of Internet Security  Protocols and Applications) est un projet européen dédié au développement de techniques de validation de protocoles de sécurité [ARM05]. Cet outil permet de mettre à disposition ces techniques aux ingénieurs en charge des développements : l’architecture d’AVISPA est présentée dans la figure 47. VALIDATIONS DES SOLUTIONS DE SECURITE DU PROTOCOLE SIP Page 84 sur 134 Figure 47. Architecture de fonctionnement d’AVISPA L’outil AVISPA permet quatre méthodes d’analyse : – l’outil On-the-fly Model Checking (OFMC) repose sur l’emploi de structures symbolisant plusieurs exécutions similaires d’un même protocole, réduisant ainsi le champ d’investigation ; – l’outil Constraint-Logic-based Attack Searcher (CLATSE) utilisant des techniques classiques et spécifiques de résolution de contraintes, permet d’obtenir des résultats avec différents modèles de protocoles ; – l’outil SAT-based Model-Checker (SATMC) consiste à savoir si une formule de logique propositionnelle (c’est-à-dire une formule construite avec les opérateurs et, ou, non) peut être vraie si l’on choisie convenablement les valeurs des variables. – l’outil Tree Automata based on Automatic Approximations for the Analysis of Security Protocols (TA4SP) fournit un diagnostic moins précis que les trois autres outils mais sa spécificité est d’analyser les protocoles dans le cadre non borné du nombre de sessions. Pour utiliser ces modules, il faut spécifier la solution de sécurité à valider dans un langage appelé HLPSL. AVISPA existe sous la forme d’un portail Web ou sous la forme d’applicatif comme [SPAN] qui a été utilisé dans les validations. L’analyse présentée plus tard s’appuie sur les modules OFMC et CLATSE qui selon [BOI07] apportent le niveau d’analyse correspondant à notre validation. 

Les équipements et les logiciels

Description de la plate-forme

Pour les validations pratiques, une plate forme a été mise en place pour vérifier le bon fonctionnement des contributions envisagées dans ce mémoire. Elle a permis d’implémenter les différentes solutions et de dérouler les tests de validations. Le dispositif est décrit d’une manière générique dans la figure 48