Les deux tiers de la population mondiale, soit environ cinq milliards de personnes, utilisent quotidiennement un téléphone mobile. Ils se connectent au réseau via leurs cartes SIM, passent des appels, envoient des SMS, échangent des images ou effectuent des achats. Le réseau est, bien entendu, vulnérables aux attaques. À maintes reprises, des délinquants ont pu accéder à des communications lors de la connexion de l’appareil au réseau afin d’intercepter des conversations ou de voler des données.
Comment progresser en matière de sécurité ? La cinquième et dernière génération de communications mobiles (5G) prévue pour un déploiement d’ici 2020 devrait offrir plus de garanties aux utilisateurs. Afin de soutenir la sécurité, le périphérique et le réseau doivent pouvoir s’authentifier l’un et l’autre au moment de la connexion. En même temps, les échanges de données, l’identité et la localisation de l’utilisateur doivent rester confidentiels. Pour cela un protocole de communication appelé Authentification and Key Agreement (AKA) est mis en œuvre depuis l’introduction de la norme 3G.
Protocole 5G AKA
La norme de communication mobile 5G s’appuie donc sur le protocole 5G AKA. Le nouveau protocole améliorera considérablement la protection des données par rapport aux technologies 3G et 4G. Notamment, grâce à lui, un problème a été résolu concernant une faille auparavant exploitée par les intercepteurs IMSI (International Mobile Subscriber Identity). Avec ces appareils, l’identité internationale d’abonné mobile d’une carte de téléphone portable pouvait être lue pour déterminer l’emplacement d’un appareil mobile et suivre un utilisateur. Pour ce faire, l’appareil avait seulement besoin d’écouter les transmissions entre le téléphone mobile et l’antenne du réseau mobile. Cela n’est plus possible désormais avec le 5G AKA.
Comment évaluer globalement la sécurité offerte par le protocole 5G AKA ? Pour le vérifier, notre équipe du laboratoire d’informatique Loria, en collaboration avec des chercheurs de l’École Polytechnique Fédérale de Zurich, l’Université de Dundee et le Centre National sur la Cybersécurité de Sarrebruck a utilisé l’outil de vérification de protocoles de sécurité Tamarin. Il a permis d’identifier automatiquement les hypothèses de sécurité minimale requises pour atteindre les objectifs de sécurité définis par le standard proposé par l’organisme de standardisation 3GPP. L’analyse a montré que le protocole était insuffisant pour atteindre tous les objectifs de sécurité critiques avec les hypothèses énoncées dans le standard. En particulier, une mise en œuvre trop rapide, mais respectant la norme, pourrait aboutir à une situation où un utilisateur est facturé pour les appels d’un autre utilisateur.
Nous avons montré que le protocole permettait également d’autres types d’attaques, notamment des attaques de traçabilité. Lors de ces attaques, le téléphone mobile n’envoie pas l’identité complète de l’utilisateur, mais un attaquant peut identifier un téléphone, et le tracer. Vu les faiblesses identifiées, si la nouvelle technologie de communication mobile est introduite avec ces spécifications, cela peut entraîner de nombreuses cyberattaques avec des conséquences sur la protection de la vie privée.
Vérification formelle
Pour aboutir à ce résultat, nous nous sommes appuyés sur la vérification formelle. Il s’agit de vérifier que tout standard assure des propriétés de sécurité suffisantes pour être commercialisé. Tout système ou programme grand public possède un document de spécification technique que nous appelons un standard. Ce document est en général public et décrit avec précision le contenu et fonctionnement du système. C’est à partir de ce document de spécification que nos chercheurs ont pu faire ces vérifications.
L’avantage de l’approche permet de tester différentes propriétés comme l’authentification, la confidentialité, la traçabilité avant la commercialisation du système. Le logiciel « Tamarin » permet de bâtir des modèles mathématiques précis du système à partir du standard et d’y insérer des scénarios d’intrusion pour ainsi construire des preuves de ce qui est garanti ou non. Comme par exemple l’authentification afin d’être sûr qu’on s’adresse à la bonne personne. Tamarin est également un outil d’aide à la décision car il permet d’évaluer rapidement des solutions alternatives pour parer aux failles détectées.
La vérification formelle est utilisée en particulier pour la sécurité dans l’automobile et l’aéronautique. Il est évidemment crucial que les standards utilisés dans les avions ne contiennent pas de bugs. L’objectif de la vérification n’est donc pas seulement de trouver des failles mais au contraire d’assurer leur absence, donc d’améliorer le système en proposant des alternatives et des corrections.
Il faut toujours se préoccuper des brèches pour éviter des conséquences graves. Dans les protocoles de communication 3G et 4G, il y a une faille permettant à une personne malveillante de suivre un autre individu, et cette faille est effectivement exploité en pratique par les intercepteurs d’IMSI. Nous sommes en contact avec le 3GPP pour résoudre les problèmes identifiés dans la norme 5G, mais le problème de la traçabilité est complexe et nécessite une importante remise à niveau.
Jannik Dreier, Maître de Conférences cryptographie et informatique théorique, Université de Lorraine
Cet article est republié à partir de The Conversation sous licence Creative Commons. Lire l’article original.
Comment pouvez-vous nous aider à vous tenir informés ?
Epoch Times est un média libre et indépendant, ne recevant aucune aide publique et n’appartenant à aucun parti politique ou groupe financier. Depuis notre création, nous faisons face à des attaques déloyales pour faire taire nos informations portant notamment sur les questions de droits de l'homme en Chine. C'est pourquoi, nous comptons sur votre soutien pour défendre notre journalisme indépendant et pour continuer, grâce à vous, à faire connaître la vérité.
