https:\/\/webconf.imt.fr\/frontend\/rooms\/4oc-jdn-ghh-dhb\/join<\/a><\/p>\n\n\n\nMembres du jury :<\/strong><\/p>\n\n\n\n
M. Thomas CLAUSEN<\/strong>, Professeur, Ecole Polytechnique, FRANCE – Examinateur
M. Luca HIRSCHI<\/strong>, Charg\u00e9 de recherche, Loria, FRANCE – Examinateur
M. Vincent NICOMETTE<\/strong>, Professeur, INSA Toulouse, FRANCE – Examinateur<\/p>\n\n\n\nM. Erik POLL<\/strong>, Full professor, Radboud University, PAYS-BAS – Rapporteur
Mme Val\u00e9rie VIET TRIEM TONG<\/strong>, Professeure, Centrale Sup\u00e9lec, FRANCE – Rapporteur<\/p>\n\n\n\nM. Herv\u00e9 DEBAR<\/strong>, Professeur, T\u00e9l\u00e9com SudParis, FRANCE – Directeur de th\u00e8se
M. Olivier LEVILLAIN<\/strong>, Ma\u00eetre de conf\u00e9rences, T\u00e9l\u00e9com SudParis, FRANCE – Co-encadrant de th\u00e8se<\/p>\n\n\n\n\u00ab Am\u00e9lioration de l\u2019impl\u00e9mentation des protocoles cryptographiques gr\u00e2ce \u00e0 l\u2019inf\u00e9rence grammaticale \u00bb<\/h2>\n\n\n\npr\u00e9sent\u00e9 par Monsieur Arthur TRAN VAN<\/h2>\n\n\n\n
R\u00e9sum\u00e9 :<\/strong><\/p>\n\n\n\nLes protocoles r\u00e9seaux cryptographiques, tels que SSH et OPC UA, sont essentiels dans la s\u00e9curisation des communications. Cependant, leurs sp\u00e9cifications sont souvent longues, ambigu\u00ebs et incompl\u00e8tes, entra\u00eenant des erreurs d\u2019impl\u00e9mentation et des vuln\u00e9rabilit\u00e9s exploitables. Sans acc\u00e8s au code source, la v\u00e9rification de la conformit\u00e9 d\u2019une impl\u00e9mentation \u00e0 sa sp\u00e9cification devient particuli\u00e8rement complexe et se limite \u00e0 l\u2019analyse des \u00e9changes avec l\u2019impl\u00e9mentation. L\u2019apprentissage actif d\u2019automates (Active Automata Learning, AAL) permet de construire un automate pour la v\u00e9rification formelle, via des interrogations dynamiques de l\u2019impl\u00e9mentation. Toutefois, le co\u00fbt \u00e9lev\u00e9 de cette m\u00e9thode limite son adoption pratique. Cette th\u00e8se propose plusieurs contributions visant \u00e0 am\u00e9liorer l\u2019efficacit\u00e9 et l\u2019applicabilit\u00e9 de l\u2019analyse de protocoles bas\u00e9e sur les automates. Tout d\u2019abord, elle introduit un cadre unifi\u00e9 pour l\u2019apprentissage actif adaptatif, permettant d\u2019exploiter des sp\u00e9cifications partielles ou des mod\u00e8les issus de versions ant\u00e9rieures afin de guider le processus d\u2019apprentissage. Ce cadre g\u00e9n\u00e9ralise les strat\u00e9gies adaptatives existantes et facilite l\u2019int\u00e9gration de nouvelles, aboutissant \u00e0 un nouvel algorithme adaptatif, AL\u03bb, qui r\u00e9alise \u00e0 la fois des gains de performance et permet d\u2019\u00e9tudier les limites de l\u2019apprentissage actif adaptatif. Ensuite, elle s\u2019attaque aux limites de la phase de v\u00e9rification en pr\u00e9sentant le Mealy Verifier, un outil sp\u00e9cialis\u00e9 capable de fournir rapidement des ensembles exhaustifs de contre-exemples pour des propri\u00e9t\u00e9s sp\u00e9cifiques aux protocoles. Cet outil r\u00e9duit le besoin d’it\u00e9ration d’extraction de mod\u00e8le et de v\u00e9rification. La m\u00e9thode propos\u00e9e est valid\u00e9e au travers d\u2019\u00e9tudes de cas sur OPC UA et SSH, permettant la d\u00e9couverte de vuln\u00e9rabilit\u00e9s in\u00e9dites. Enfin, dans un projet de recherche distinct men\u00e9 durant la th\u00e8se, un protocole de stockage multi-cloud s\u00e9curis\u00e9 est con\u00e7u et impl\u00e9ment\u00e9 sous forme de preuve de concept, offrant des garanties renforc\u00e9es en mati\u00e8re de confidentialit\u00e9, d\u2019int\u00e9grit\u00e9 et de r\u00e9cup\u00e9rabilit\u00e9 des fichiers. Dans l\u2019ensemble, ces travaux contribuent \u00e0 rendre les m\u00e9thodes formelles plus pratiques et plus \u00e9volutives pour la v\u00e9rification des protocoles dans des environnements r\u00e9els.<\/p>\n\n\n\n
Abstract :<\/strong><\/p>\n\n\n\nCryptographic network protocols, such as SSH and OPC UA, are critical to secure communications. However, their specifications are often lengthy, ambiguous, and incomplete, leading to implementation inconsistencies and security vulnerabilities. Without access to the source code, verifying that an implementation complies with its specification becomes particularly complex and is limited to analyzing its interactions. Active automata learning (AAL) builds an automaton for verification by actively interrogating the protocol implementation. However, the high learning costs limit the adoption of this method in practice. This thesis introduces several contributions to improve the efficiency and applicability of automata-based protocol analysis. First, it presents a unified framework for adaptive AAL, allowing learners to leverage partial specifications or legacy models to guide the learning process. The framework generalizes existing adaptive strategies and supports the development of new ones, culminating in the novel adaptive learning algorithm AL\u03bb, which both achieves performance gains and facilitates analysis of adaptive AAL\u2019s limits. Second, the thesis addresses limitations in verification by introducing the Mealy Verifier, a specialized tool that rapidly identifies exhaustive sets of counterexamples for protocol-specific properties, reducing the number of costly model extraction and verification iterations. This method is validated through case studies on OPC UA and SSH, uncovering previously unknown vulnerabilities. Finally, although independent from the main line of contributions, the thesis presents the design and proof-of-concept implementation of a secure multi-cloud storage protocol, offering enhanced guarantees for privacy, integrity, and file retrievability. Overall, this thesis contributes to the broader objective of making formal methods more practical and scalable for real-world protocol verification.<\/p>\n","protected":false},"excerpt":{"rendered":"
L’Ecole doctorale : Ecole Doctorale de l’Institut Polytechnique de Paris et le Laboratoire de recherche SAMOVAR – Services r\u00e9partis, Architectures, Mod\u00e9lisation, Validation, Administration des R\u00e9seaux pr\u00e9sentent l\u2019AVIS DE SOUTENANCE de Monsieur Arthur TRAN VAN Autoris\u00e9 \u00e0 pr\u00e9senter ses travaux en vue de l\u2019obtention du Doctorat de l’Institut Polytechnique de Paris, pr\u00e9par\u00e9 \u00e0 T\u00e9l\u00e9com SudParis en […]<\/p>\n","protected":false},"author":4,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"ocean_post_layout":"","ocean_both_sidebars_style":"","ocean_both_sidebars_content_width":0,"ocean_both_sidebars_sidebars_width":0,"ocean_sidebar":"","ocean_second_sidebar":"","ocean_disable_margins":"enable","ocean_add_body_class":"","ocean_shortcode_before_top_bar":"","ocean_shortcode_after_top_bar":"","ocean_shortcode_before_header":"","ocean_shortcode_after_header":"","ocean_has_shortcode":"","ocean_shortcode_after_title":"","ocean_shortcode_before_footer_widgets":"","ocean_shortcode_after_footer_widgets":"","ocean_shortcode_before_footer_bottom":"","ocean_shortcode_after_footer_bottom":"","ocean_display_top_bar":"default","ocean_display_header":"default","ocean_header_style":"","ocean_center_header_left_menu":"","ocean_custom_header_template":"","ocean_custom_logo":0,"ocean_custom_retina_logo":0,"ocean_custom_logo_max_width":0,"ocean_custom_logo_tablet_max_width":0,"ocean_custom_logo_mobile_max_width":0,"ocean_custom_logo_max_height":0,"ocean_custom_logo_tablet_max_height":0,"ocean_custom_logo_mobile_max_height":0,"ocean_header_custom_menu":"","ocean_menu_typo_font_family":"","ocean_menu_typo_font_subset":"","ocean_menu_typo_font_size":0,"ocean_menu_typo_font_size_tablet":0,"ocean_menu_typo_font_size_mobile":0,"ocean_menu_typo_font_size_unit":"px","ocean_menu_typo_font_weight":"","ocean_menu_typo_font_weight_tablet":"","ocean_menu_typo_font_weight_mobile":"","ocean_menu_typo_transform":"","ocean_menu_typo_transform_tablet":"","ocean_menu_typo_transform_mobile":"","ocean_menu_typo_line_height":0,"ocean_menu_typo_line_height_tablet":0,"ocean_menu_typo_line_height_mobile":0,"ocean_menu_typo_line_height_unit":"","ocean_menu_typo_spacing":0,"ocean_menu_typo_spacing_tablet":0,"ocean_menu_typo_spacing_mobile":0,"ocean_menu_typo_spacing_unit":"","ocean_menu_link_color":"","ocean_menu_link_color_hover":"","ocean_menu_link_color_active":"","ocean_menu_link_background":"","ocean_menu_link_hover_background":"","ocean_menu_link_active_background":"","ocean_menu_social_links_bg":"","ocean_menu_social_hover_links_bg":"","ocean_menu_social_links_color":"","ocean_menu_social_hover_links_color":"","ocean_disable_title":"default","ocean_disable_heading":"default","ocean_post_title":"","ocean_post_subheading":"","ocean_post_title_style":"","ocean_post_title_background_color":"","ocean_post_title_background":0,"ocean_post_title_bg_image_position":"","ocean_post_title_bg_image_attachment":"","ocean_post_title_bg_image_repeat":"","ocean_post_title_bg_image_size":"","ocean_post_title_height":0,"ocean_post_title_bg_overlay":0.5,"ocean_post_title_bg_overlay_color":"","ocean_disable_breadcrumbs":"default","ocean_breadcrumbs_color":"","ocean_breadcrumbs_separator_color":"","ocean_breadcrumbs_links_color":"","ocean_breadcrumbs_links_hover_color":"","ocean_display_footer_widgets":"default","ocean_display_footer_bottom":"default","ocean_custom_footer_template":"","ocean_post_oembed":"","ocean_post_self_hosted_media":"","ocean_post_video_embed":"","ocean_link_format":"","ocean_link_format_target":"self","ocean_quote_format":"","ocean_quote_format_link":"post","ocean_gallery_link_images":"on","ocean_gallery_id":[],"footnotes":""},"categories":[286,603],"tags":[],"class_list":["post-6966","post","type-post","status-publish","format-standard","hentry","category-fractualites-ennews-fr","category-seminaire-scn","entry"],"_links":{"self":[{"href":"https:\/\/samovar.telecom-sudparis.eu\/index.php\/wp-json\/wp\/v2\/posts\/6966","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/samovar.telecom-sudparis.eu\/index.php\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/samovar.telecom-sudparis.eu\/index.php\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/samovar.telecom-sudparis.eu\/index.php\/wp-json\/wp\/v2\/users\/4"}],"replies":[{"embeddable":true,"href":"https:\/\/samovar.telecom-sudparis.eu\/index.php\/wp-json\/wp\/v2\/comments?post=6966"}],"version-history":[{"count":2,"href":"https:\/\/samovar.telecom-sudparis.eu\/index.php\/wp-json\/wp\/v2\/posts\/6966\/revisions"}],"predecessor-version":[{"id":6968,"href":"https:\/\/samovar.telecom-sudparis.eu\/index.php\/wp-json\/wp\/v2\/posts\/6966\/revisions\/6968"}],"wp:attachment":[{"href":"https:\/\/samovar.telecom-sudparis.eu\/index.php\/wp-json\/wp\/v2\/media?parent=6966"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/samovar.telecom-sudparis.eu\/index.php\/wp-json\/wp\/v2\/categories?post=6966"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/samovar.telecom-sudparis.eu\/index.php\/wp-json\/wp\/v2\/tags?post=6966"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}