{"id":4270,"date":"2021-09-21T10:42:23","date_gmt":"2021-09-21T09:42:23","guid":{"rendered":"https:\/\/cyberschool.univ-rennes.fr\/?page_id=4270"},"modified":"2026-03-12T14:35:50","modified_gmt":"2026-03-12T13:35:50","slug":"formal-modeling-and-verification-of-security-protocols","status":"publish","type":"page","link":"https:\/\/cyberschool.univ-rennes.fr\/en\/education\/masters-and-postgraduate-programmes\/masters-in-mathematics-and-applications-it-mathematics-and-cryptography\/study-programme-of-the-masters-mathematics-and-applications-it-mathematics-and-cryptography\/formal-modeling-and-verification-of-security-protocols\/","title":{"rendered":"S\u00e9curit\u00e9 des protocoles"},"content":{"rendered":"\n<section class=\"txt\">\n    <div class=\"container\">\n        <div class=\"bloc-txt\">\n                            <h2><span class=\"elipse\"><\/span><span class=\"trait\"><\/span>Teaching goals<\/h2>\n                        <p>The objective of this course is to provide students with an in-depth knowledge regarding methods and tools for the specification, design, and symbolic verification of security protocols in various domains.<\/p>\n\n        <\/div>\n    <\/div>\n<\/section>\n\n\n\n<section class=\"txt\">\n    <div class=\"container\">\n        <div class=\"bloc-txt\">\n                            <h2><span class=\"elipse\"><\/span><span class=\"trait\"><\/span>Course description<\/h2>\n                        <div class=\"contain-txt\">\n<ul>\n<li>Introduction to cryptography (if necessary): symmetric and asymmetric cryptography, hash functions<\/li>\n<li>Formal ways of specifying a protocol: Alice &amp; Bob notation, message sequence charts, Horn clauses, constraint systems, applied pi calculus<\/li>\n<li>Attacker models: passive and active attackers, Dolev-Yao adversary, knowledge inference<\/li>\n<li>Formal specification of security properties: weak and strong secrecy, indistinguishability property, authentication (aliveness, agreement, synchronization), anonymity<\/li>\n<li>Man-in-the-middle attacks<\/li>\n<li>Protocol verification with a bounded number of sessions: constraint systems<\/li>\n<li>Protocol verification with an unbounded number of sessions: Horn Clauses<\/li>\n<li>Symbolic versus computational models for protcol verification<\/li>\n<li>Tools for automatic verification of security protocols: ProVerif, Scyther<\/li>\n<\/ul>\n<\/div>\n\n        <\/div>\n    <\/div>\n<\/section>\n\n\n<section class=\"tuiles\">\n    <div class=\"container\">\n                <div class=\"bloc\">\n            <h2><span class=\"elipse\"><\/span><span class=\"trait\"><\/span>Skills to acquire<\/h2>\n            <div class=\"contain-txt\">\n<ul>\n<li>Specify a protocol in a suitable formal framework<\/li>\n<li>Formally define the security property against which the protocol should be checked<\/li>\n<li>Select an appropriate verification tool to analyze the protocol<\/li>\n<li>Detect logical flaws in improperly designed or implemented protocols<\/li>\n<\/ul>\n<\/div>\n\n                    <\/div>\n            <\/div>\n<\/section>\n\n\n\n<section class=\"txt\">\n    <div class=\"container\">\n        <div class=\"bloc-txt\">\n                            <h2><span class=\"elipse\"><\/span><span class=\"trait\"><\/span>Biography<\/h2>\n                        <p><strong>Barbara FILA<\/strong> is an associate professor (Ma\u00eetre de conf\u00e9rences) at Institut National des Sciences Appliqu\u00e9es (INSA Rennes) and a researcher at the Institut de Recherche en Informatique et Syst\u00e8mes Al\u00e9atoires (IRISA) in Rennes. She is a member of the <a href=\"https:\/\/www-spicy.irisa.fr\/\" target=\"_blank\" rel=\"noopener\">Security and Privacy (SPICY) project-team<\/a>.<\/p>\n\n        <\/div>\n    <\/div>\n<\/section>\n","protected":false},"excerpt":{"rendered":"","protected":false},"author":8,"featured_media":0,"parent":11605,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":[],"acf":[],"yoast_head":"<!-- This site is optimized with the Yoast SEO plugin v20.13 - https:\/\/yoast.com\/wordpress\/plugins\/seo\/ -->\n<title>S\u00e9curit\u00e9 des protocoles - CyberSchool<\/title>\n<meta name=\"robots\" content=\"index, follow, max-snippet:-1, max-image-preview:large, max-video-preview:-1\" \/>\n<link rel=\"canonical\" href=\"https:\/\/cyberschool.univ-rennes.fr\/en\/education\/masters-and-postgraduate-programmes\/masters-in-mathematics-and-applications-it-mathematics-and-cryptography\/study-programme-of-the-masters-mathematics-and-applications-it-mathematics-and-cryptography\/formal-modeling-and-verification-of-security-protocols\/\" \/>\n<meta property=\"og:locale\" content=\"en_US\" \/>\n<meta property=\"og:type\" content=\"article\" \/>\n<meta property=\"og:title\" content=\"S\u00e9curit\u00e9 des protocoles - CyberSchool\" \/>\n<meta property=\"og:url\" content=\"https:\/\/cyberschool.univ-rennes.fr\/en\/education\/masters-and-postgraduate-programmes\/masters-in-mathematics-and-applications-it-mathematics-and-cryptography\/study-programme-of-the-masters-mathematics-and-applications-it-mathematics-and-cryptography\/formal-modeling-and-verification-of-security-protocols\/\" \/>\n<meta property=\"og:site_name\" content=\"CyberSchool\" \/>\n<meta property=\"article:publisher\" content=\"https:\/\/www.facebook.com\/CSchoolRennes\/\" \/>\n<meta property=\"article:modified_time\" content=\"2026-03-12T13:35:50+00:00\" \/>\n<meta property=\"og:image\" content=\"https:\/\/cyberschool.univ-rennes.fr\/app\/uploads\/2021\/02\/cover-social-network.jpeg\" \/>\n\t<meta property=\"og:image:width\" content=\"1500\" \/>\n\t<meta property=\"og:image:height\" content=\"500\" \/>\n\t<meta property=\"og:image:type\" content=\"image\/jpeg\" \/>\n<meta name=\"twitter:card\" content=\"summary_large_image\" \/>\n<meta name=\"twitter:site\" content=\"@CSchoolRennes\" \/>\n<script type=\"application\/ld+json\" class=\"yoast-schema-graph\">{\"@context\":\"https:\/\/schema.org\",\"@graph\":[{\"@type\":\"WebPage\",\"@id\":\"https:\/\/cyberschool.univ-rennes.fr\/en\/education\/masters-and-postgraduate-programmes\/masters-in-mathematics-and-applications-it-mathematics-and-cryptography\/study-programme-of-the-masters-mathematics-and-applications-it-mathematics-and-cryptography\/formal-modeling-and-verification-of-security-protocols\/\",\"url\":\"https:\/\/cyberschool.univ-rennes.fr\/en\/education\/masters-and-postgraduate-programmes\/masters-in-mathematics-and-applications-it-mathematics-and-cryptography\/study-programme-of-the-masters-mathematics-and-applications-it-mathematics-and-cryptography\/formal-modeling-and-verification-of-security-protocols\/\",\"name\":\"S\u00e9curit\u00e9 des protocoles - CyberSchool\",\"isPartOf\":{\"@id\":\"https:\/\/cyberschool.univ-rennes.fr\/en\/#website\"},\"datePublished\":\"2021-09-21T09:42:23+00:00\",\"dateModified\":\"2026-03-12T13:35:50+00:00\",\"breadcrumb\":{\"@id\":\"https:\/\/cyberschool.univ-rennes.fr\/en\/education\/masters-and-postgraduate-programmes\/masters-in-mathematics-and-applications-it-mathematics-and-cryptography\/study-programme-of-the-masters-mathematics-and-applications-it-mathematics-and-cryptography\/formal-modeling-and-verification-of-security-protocols\/#breadcrumb\"},\"inLanguage\":\"en-US\",\"potentialAction\":[{\"@type\":\"ReadAction\",\"target\":[\"https:\/\/cyberschool.univ-rennes.fr\/en\/education\/masters-and-postgraduate-programmes\/masters-in-mathematics-and-applications-it-mathematics-and-cryptography\/study-programme-of-the-masters-mathematics-and-applications-it-mathematics-and-cryptography\/formal-modeling-and-verification-of-security-protocols\/\"]}]},{\"@type\":\"BreadcrumbList\",\"@id\":\"https:\/\/cyberschool.univ-rennes.fr\/en\/education\/masters-and-postgraduate-programmes\/masters-in-mathematics-and-applications-it-mathematics-and-cryptography\/study-programme-of-the-masters-mathematics-and-applications-it-mathematics-and-cryptography\/formal-modeling-and-verification-of-security-protocols\/#breadcrumb\",\"itemListElement\":[{\"@type\":\"ListItem\",\"position\":1,\"name\":\"Home\",\"item\":\"https:\/\/cyberschool.univ-rennes.fr\/en\/\"},{\"@type\":\"ListItem\",\"position\":2,\"name\":\"Education\",\"item\":\"https:\/\/cyberschool.univ-rennes.fr\/en\/education\/\"},{\"@type\":\"ListItem\",\"position\":3,\"name\":\"Master\u2019s and postgraduate programmes\",\"item\":\"https:\/\/cyberschool.univ-rennes.fr\/en\/education\/masters-and-postgraduate-programmes\/\"},{\"@type\":\"ListItem\",\"position\":4,\"name\":\"Master\u2019s in Mathematics and Applications \u2013 IT Mathematics and Cryptography\",\"item\":\"https:\/\/cyberschool.univ-rennes.fr\/en\/education\/masters-and-postgraduate-programmes\/masters-in-mathematics-and-applications-it-mathematics-and-cryptography\/\"},{\"@type\":\"ListItem\",\"position\":5,\"name\":\"Study programme of the Master&rsquo;s Mathematics and Applications \u2013 IT Mathematics and Cryptography\",\"item\":\"https:\/\/cyberschool.univ-rennes.fr\/en\/education\/masters-and-postgraduate-programmes\/masters-in-mathematics-and-applications-it-mathematics-and-cryptography\/study-programme-of-the-masters-mathematics-and-applications-it-mathematics-and-cryptography\/\"},{\"@type\":\"ListItem\",\"position\":6,\"name\":\"S\u00e9curit\u00e9 des protocoles\"}]},{\"@type\":\"WebSite\",\"@id\":\"https:\/\/cyberschool.univ-rennes.fr\/en\/#website\",\"url\":\"https:\/\/cyberschool.univ-rennes.fr\/en\/\",\"name\":\"CyberSchool\",\"description\":\"Just another WordPress site\",\"potentialAction\":[{\"@type\":\"SearchAction\",\"target\":{\"@type\":\"EntryPoint\",\"urlTemplate\":\"https:\/\/cyberschool.univ-rennes.fr\/en\/?s={search_term_string}\"},\"query-input\":\"required name=search_term_string\"}],\"inLanguage\":\"en-US\"}]}<\/script>\n<!-- \/ Yoast SEO plugin. -->","yoast_head_json":{"title":"S\u00e9curit\u00e9 des protocoles - CyberSchool","robots":{"index":"index","follow":"follow","max-snippet":"max-snippet:-1","max-image-preview":"max-image-preview:large","max-video-preview":"max-video-preview:-1"},"canonical":"https:\/\/cyberschool.univ-rennes.fr\/en\/education\/masters-and-postgraduate-programmes\/masters-in-mathematics-and-applications-it-mathematics-and-cryptography\/study-programme-of-the-masters-mathematics-and-applications-it-mathematics-and-cryptography\/formal-modeling-and-verification-of-security-protocols\/","og_locale":"en_US","og_type":"article","og_title":"S\u00e9curit\u00e9 des protocoles - CyberSchool","og_url":"https:\/\/cyberschool.univ-rennes.fr\/en\/education\/masters-and-postgraduate-programmes\/masters-in-mathematics-and-applications-it-mathematics-and-cryptography\/study-programme-of-the-masters-mathematics-and-applications-it-mathematics-and-cryptography\/formal-modeling-and-verification-of-security-protocols\/","og_site_name":"CyberSchool","article_publisher":"https:\/\/www.facebook.com\/CSchoolRennes\/","article_modified_time":"2026-03-12T13:35:50+00:00","og_image":[{"width":1500,"height":500,"url":"https:\/\/cyberschool.univ-rennes.fr\/app\/uploads\/2021\/02\/cover-social-network.jpeg","type":"image\/jpeg"}],"twitter_card":"summary_large_image","twitter_site":"@CSchoolRennes","schema":{"@context":"https:\/\/schema.org","@graph":[{"@type":"WebPage","@id":"https:\/\/cyberschool.univ-rennes.fr\/en\/education\/masters-and-postgraduate-programmes\/masters-in-mathematics-and-applications-it-mathematics-and-cryptography\/study-programme-of-the-masters-mathematics-and-applications-it-mathematics-and-cryptography\/formal-modeling-and-verification-of-security-protocols\/","url":"https:\/\/cyberschool.univ-rennes.fr\/en\/education\/masters-and-postgraduate-programmes\/masters-in-mathematics-and-applications-it-mathematics-and-cryptography\/study-programme-of-the-masters-mathematics-and-applications-it-mathematics-and-cryptography\/formal-modeling-and-verification-of-security-protocols\/","name":"S\u00e9curit\u00e9 des protocoles - CyberSchool","isPartOf":{"@id":"https:\/\/cyberschool.univ-rennes.fr\/en\/#website"},"datePublished":"2021-09-21T09:42:23+00:00","dateModified":"2026-03-12T13:35:50+00:00","breadcrumb":{"@id":"https:\/\/cyberschool.univ-rennes.fr\/en\/education\/masters-and-postgraduate-programmes\/masters-in-mathematics-and-applications-it-mathematics-and-cryptography\/study-programme-of-the-masters-mathematics-and-applications-it-mathematics-and-cryptography\/formal-modeling-and-verification-of-security-protocols\/#breadcrumb"},"inLanguage":"en-US","potentialAction":[{"@type":"ReadAction","target":["https:\/\/cyberschool.univ-rennes.fr\/en\/education\/masters-and-postgraduate-programmes\/masters-in-mathematics-and-applications-it-mathematics-and-cryptography\/study-programme-of-the-masters-mathematics-and-applications-it-mathematics-and-cryptography\/formal-modeling-and-verification-of-security-protocols\/"]}]},{"@type":"BreadcrumbList","@id":"https:\/\/cyberschool.univ-rennes.fr\/en\/education\/masters-and-postgraduate-programmes\/masters-in-mathematics-and-applications-it-mathematics-and-cryptography\/study-programme-of-the-masters-mathematics-and-applications-it-mathematics-and-cryptography\/formal-modeling-and-verification-of-security-protocols\/#breadcrumb","itemListElement":[{"@type":"ListItem","position":1,"name":"Home","item":"https:\/\/cyberschool.univ-rennes.fr\/en\/"},{"@type":"ListItem","position":2,"name":"Education","item":"https:\/\/cyberschool.univ-rennes.fr\/en\/education\/"},{"@type":"ListItem","position":3,"name":"Master\u2019s and postgraduate programmes","item":"https:\/\/cyberschool.univ-rennes.fr\/en\/education\/masters-and-postgraduate-programmes\/"},{"@type":"ListItem","position":4,"name":"Master\u2019s in Mathematics and Applications \u2013 IT Mathematics and Cryptography","item":"https:\/\/cyberschool.univ-rennes.fr\/en\/education\/masters-and-postgraduate-programmes\/masters-in-mathematics-and-applications-it-mathematics-and-cryptography\/"},{"@type":"ListItem","position":5,"name":"Study programme of the Master&rsquo;s Mathematics and Applications \u2013 IT Mathematics and Cryptography","item":"https:\/\/cyberschool.univ-rennes.fr\/en\/education\/masters-and-postgraduate-programmes\/masters-in-mathematics-and-applications-it-mathematics-and-cryptography\/study-programme-of-the-masters-mathematics-and-applications-it-mathematics-and-cryptography\/"},{"@type":"ListItem","position":6,"name":"S\u00e9curit\u00e9 des protocoles"}]},{"@type":"WebSite","@id":"https:\/\/cyberschool.univ-rennes.fr\/en\/#website","url":"https:\/\/cyberschool.univ-rennes.fr\/en\/","name":"CyberSchool","description":"Just another WordPress site","potentialAction":[{"@type":"SearchAction","target":{"@type":"EntryPoint","urlTemplate":"https:\/\/cyberschool.univ-rennes.fr\/en\/?s={search_term_string}"},"query-input":"required name=search_term_string"}],"inLanguage":"en-US"}]}},"_links":{"self":[{"href":"https:\/\/cyberschool.univ-rennes.fr\/en\/wp-json\/wp\/v2\/pages\/4270"}],"collection":[{"href":"https:\/\/cyberschool.univ-rennes.fr\/en\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/cyberschool.univ-rennes.fr\/en\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/cyberschool.univ-rennes.fr\/en\/wp-json\/wp\/v2\/users\/8"}],"replies":[{"embeddable":true,"href":"https:\/\/cyberschool.univ-rennes.fr\/en\/wp-json\/wp\/v2\/comments?post=4270"}],"version-history":[{"count":17,"href":"https:\/\/cyberschool.univ-rennes.fr\/en\/wp-json\/wp\/v2\/pages\/4270\/revisions"}],"predecessor-version":[{"id":18484,"href":"https:\/\/cyberschool.univ-rennes.fr\/en\/wp-json\/wp\/v2\/pages\/4270\/revisions\/18484"}],"up":[{"embeddable":true,"href":"https:\/\/cyberschool.univ-rennes.fr\/en\/wp-json\/wp\/v2\/pages\/11605"}],"wp:attachment":[{"href":"https:\/\/cyberschool.univ-rennes.fr\/en\/wp-json\/wp\/v2\/media?parent=4270"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}