{"id":6623,"date":"2018-03-05T09:10:42","date_gmt":"2018-03-05T08:10:42","guid":{"rendered":"https:\/\/www.uni.lu\/fr\/events\/srm-research-seminar-how-to-model-e-voting-protocols-in-tamarin\/"},"modified":"2018-03-05T09:10:42","modified_gmt":"2018-03-05T08:10:42","slug":"srm-research-seminar-how-to-model-e-voting-protocols-in-tamarin","status":"publish","type":"events","link":"https:\/\/www.uni.lu\/fr\/events\/srm-research-seminar-how-to-model-e-voting-protocols-in-tamarin\/","title":{"rendered":"SRM Research Seminar: How to model (e-voting) protocols in Tamarin"},"content":{"rendered":"

The Tamarin prover is a tool for the symbolic modeling and analysis of security protocols. It takes as input a protocol model, a specification of the adversary, and a specification of the protocol’s desired properties. Tamarin can then be used to automatically check if the protocol fulfills the properties, given that arbitrarily many instances of the protocol’s roles are run in parallel with the adversary.<\/p>

In addition to trace properties, Tamarin can express observational equivalence properties. Such properties express that an adversary cannot distinguish two systems and are especially useful for modeling privacy.\u00a0<\/p>

In this talk, we present an introduction to the Tamarin tool and explain how a protocol specified in traditional Alice&Bob notation can be translated to the Tamarin protocol model. Furthermore, we explain on the example of a simplified e-voting protocol how properties such as privacy and receipt-freeness can be modeled with Tamarin’s built in observational equivalence theory.<\/p>

Lara Schmid<\/strong> is a PhD student with Prof. David Basin at the Institute of Information Security at ETH Zurich. She received a Master’s degree in Computer Science from ETH Zurich in 2015. In her Master’s thesis she proposed a model for formalizing and reasoning about erroneous human agents in security protocols. She is interested in formal methods for analyzing security protocols. At the moment, her focus is on formally modeling e-voting protocols.<\/p>

The SRM seminars are the joint seminars of the Security and Trust of Software Systems and Applied Security and Information Assurance research groups, supported by the Laboratory of Algorithmics, Cryptology and Security and the Interdisciplinary Centre for Security, Reliability and Trust.<\/strong><\/p><\/div><\/section>","protected":false},"excerpt":{"rendered":"

The Tamarin prover is a tool for the symbolic modeling and analysis of security protocols. It takes as input a protocol model, a specification of the adversary, and a specification of the protocol’s desired properties. Tamarin can then be used to automatically check if the protocol fulfills the properties, given that arbitrarily many instances of the protocol’s roles are run in parallel with the adversary.<\/p>\n","protected":false},"author":0,"featured_media":6624,"parent":0,"menu_order":0,"comment_status":"open","ping_status":"closed","template":"","format":"standard","meta":{"featured_image_focal_point":[],"show_featured_caption":false,"ulux_newsletter_groups":"","uluxPostTitle":"","uluxPrePostTitle":"","_trash_the_other_posts":false,"_price":"","_stock":"","_tribe_ticket_header":"","_tribe_default_ticket_provider":"","_tribe_ticket_capacity":"0","_ticket_start_date":"","_ticket_end_date":"","_tribe_ticket_show_description":"","_tribe_ticket_show_not_going":false,"_tribe_ticket_use_global_stock":"","_tribe_ticket_global_stock_level":"","_global_stock_mode":"","_global_stock_cap":"","_tribe_rsvp_for_event":"","_tribe_ticket_going_count":"","_tribe_ticket_not_going_count":"","_tribe_tickets_list":"[]","_tribe_ticket_has_attendee_info_fields":false,"event_start_date":"2018-03-13 10:30:00","event_end_date":"2018-03-13 11:30:00","event_speaker_name":"Lara Schmid (ETH Zurich)","event_speaker_link":"","event_is_online":false,"event_location":"Room 3.100, Maison du savoir","event_street":"2, avenue de l'Universit\u00e9","event_location_link":"","event_zip_code":"L-4365","event_city":"Esch-sur-Alzette","event_country":"LU"},"events-topic":[],"events-type":[],"organisation":[184,226],"authorship":[],"acf":[],"yoast_head":"\nSRM Research Seminar: How to model (e-voting) protocols in Tamarin - Universit\u00e9 du Luxembourg<\/title>\n<meta name=\"description\" content=\"The Tamarin prover is a tool for the symbolic modeling and analysis of security protocols. It takes as input a protocol model, a specification of the adversary, and a specification of the protocol's desired properties. Tamarin can then be used to automatically check if the protocol fulfills the properties, given that arbitrarily many instances of the protocol's roles are run in parallel with the adversary.\" \/>\n<meta name=\"robots\" content=\"index, follow, max-snippet:-1, max-image-preview:large, max-video-preview:-1\" \/>\n<link rel=\"canonical\" href=\"https:\/\/www.uni.lu\/fr\/events\/srm-research-seminar-how-to-model-e-voting-protocols-in-tamarin\/\" \/>\n<meta property=\"og:locale\" content=\"fr_FR\" \/>\n<meta property=\"og:type\" content=\"article\" \/>\n<meta property=\"og:title\" content=\"SRM Research Seminar: How to model (e-voting) protocols in Tamarin\" \/>\n<meta property=\"og:description\" content=\"The Tamarin prover is a tool for the symbolic modeling and analysis of security protocols. It takes as input a protocol model, a specification of the adversary, and a specification of the protocol's desired properties. Tamarin can then be used to automatically check if the protocol fulfills the properties, given that arbitrarily many instances of the protocol's roles are run in parallel with the adversary.\" \/>\n<meta property=\"og:url\" content=\"https:\/\/www.uni.lu\/fr\/events\/srm-research-seminar-how-to-model-e-voting-protocols-in-tamarin\/\" \/>\n<meta property=\"og:site_name\" content=\"UNI FR\" \/>\n<meta property=\"article:publisher\" content=\"https:\/\/www.facebook.com\/uni.lu\" \/>\n<meta property=\"og:image\" content=\"https:\/\/www.uni.lu\/wp-content\/uploads\/sites\/11\/2026\/03\/03120045\/UNIV_SM-Profile_1600x1600px-scaled.jpg\" \/>\n\t<meta property=\"og:image:width\" content=\"2560\" \/>\n\t<meta property=\"og:image:height\" content=\"2560\" \/>\n\t<meta property=\"og:image:type\" content=\"image\/jpeg\" \/>\n<meta name=\"twitter:card\" content=\"summary_large_image\" \/>\n<meta name=\"twitter:label1\" content=\"Dur\u00e9e de lecture estim\u00e9e\" \/>\n\t<meta name=\"twitter:data1\" content=\"1 minute\" \/>\n<script type=\"application\/ld+json\" class=\"yoast-schema-graph\">{\"@context\":\"https:\/\/schema.org\",\"@graph\":[{\"@type\":\"WebPage\",\"@id\":\"https:\/\/www.uni.lu\/fr\/events\/srm-research-seminar-how-to-model-e-voting-protocols-in-tamarin\/\",\"url\":\"https:\/\/www.uni.lu\/fr\/events\/srm-research-seminar-how-to-model-e-voting-protocols-in-tamarin\/\",\"name\":\"SRM Research Seminar: How to model (e-voting) protocols in Tamarin - Universit\u00e9 du Luxembourg\",\"isPartOf\":{\"@id\":\"https:\/\/www.uni.lu\/fr\/#website\"},\"primaryImageOfPage\":{\"@id\":\"https:\/\/www.uni.lu\/fr\/events\/srm-research-seminar-how-to-model-e-voting-protocols-in-tamarin\/#primaryimage\"},\"image\":{\"@id\":\"https:\/\/www.uni.lu\/fr\/events\/srm-research-seminar-how-to-model-e-voting-protocols-in-tamarin\/#primaryimage\"},\"thumbnailUrl\":\"https:\/\/www.uni.lu\/wp-content\/uploads\/sites\/11\/2018\/03\/srm_research_seminar_how_to_model_e_voting_protocols_in_tamarin.jpg\",\"datePublished\":\"2018-03-05T08:10:42+00:00\",\"dateModified\":\"2018-03-05T08:10:42+00:00\",\"description\":\"The Tamarin prover is a tool for the symbolic modeling and analysis of security protocols. It takes as input a protocol model, a specification of the adversary, and a specification of the protocol's desired properties. Tamarin can then be used to automatically check if the protocol fulfills the properties, given that arbitrarily many instances of the protocol's roles are run in parallel with the adversary.\",\"breadcrumb\":{\"@id\":\"https:\/\/www.uni.lu\/fr\/events\/srm-research-seminar-how-to-model-e-voting-protocols-in-tamarin\/#breadcrumb\"},\"inLanguage\":\"fr-FR\",\"potentialAction\":[{\"@type\":\"ReadAction\",\"target\":[\"https:\/\/www.uni.lu\/fr\/events\/srm-research-seminar-how-to-model-e-voting-protocols-in-tamarin\/\"]}]},{\"@type\":\"ImageObject\",\"inLanguage\":\"fr-FR\",\"@id\":\"https:\/\/www.uni.lu\/fr\/events\/srm-research-seminar-how-to-model-e-voting-protocols-in-tamarin\/#primaryimage\",\"url\":\"https:\/\/www.uni.lu\/wp-content\/uploads\/sites\/11\/2018\/03\/srm_research_seminar_how_to_model_e_voting_protocols_in_tamarin.jpg\",\"contentUrl\":\"https:\/\/www.uni.lu\/wp-content\/uploads\/sites\/11\/2018\/03\/srm_research_seminar_how_to_model_e_voting_protocols_in_tamarin.jpg\",\"width\":800,\"height\":600},{\"@type\":\"BreadcrumbList\",\"@id\":\"https:\/\/www.uni.lu\/fr\/events\/srm-research-seminar-how-to-model-e-voting-protocols-in-tamarin\/#breadcrumb\",\"itemListElement\":[{\"@type\":\"ListItem\",\"position\":1,\"name\":\"Home\",\"item\":\"https:\/\/www.uni.lu\/fr\/\"},{\"@type\":\"ListItem\",\"position\":2,\"name\":\"Events\",\"item\":\"https:\/\/www.uni.lu\/fr\/events\/\"},{\"@type\":\"ListItem\",\"position\":3,\"name\":\"SRM Research Seminar: How to model (e-voting) protocols in Tamarin\"}]},{\"@type\":\"WebSite\",\"@id\":\"https:\/\/www.uni.lu\/fr\/#website\",\"url\":\"https:\/\/www.uni.lu\/fr\/\",\"name\":\"Uni.lu\",\"description\":\"Universit\u00e9 du Luxembourg\",\"publisher\":{\"@id\":\"https:\/\/www.uni.lu\/fr\/#organization\"},\"alternateName\":\"Universit\u00e9 du Luxembourg\",\"potentialAction\":[{\"@type\":\"SearchAction\",\"target\":{\"@type\":\"EntryPoint\",\"urlTemplate\":\"https:\/\/www.uni.lu\/fr\/?s={search_term_string}\"},\"query-input\":\"required name=search_term_string\"}],\"inLanguage\":\"fr-FR\"},{\"@type\":\"Organization\",\"@id\":\"https:\/\/www.uni.lu\/fr\/#organization\",\"name\":\"Universit\u00e9 du Luxembourg\",\"alternateName\":\"Uni.lu\",\"url\":\"https:\/\/www.uni.lu\/fr\/\",\"logo\":{\"@type\":\"ImageObject\",\"inLanguage\":\"fr-FR\",\"@id\":\"https:\/\/www.uni.lu\/fr\/#\/schema\/logo\/image\/\",\"url\":\"https:\/\/www.uni.lu\/wp-content\/uploads\/sites\/11\/2026\/03\/03120045\/UNIV_SM-Profile_1600x1600px-scaled.jpg\",\"contentUrl\":\"https:\/\/www.uni.lu\/wp-content\/uploads\/sites\/11\/2026\/03\/03120045\/UNIV_SM-Profile_1600x1600px-scaled.jpg\",\"width\":2560,\"height\":2560,\"caption\":\"Universit\u00e9 du Luxembourg\"},\"image\":{\"@id\":\"https:\/\/www.uni.lu\/fr\/#\/schema\/logo\/image\/\"},\"sameAs\":[\"https:\/\/www.facebook.com\/uni.lu\",\"https:\/\/www.linkedin.com\/school\/university-of-luxembourg\/\",\"https:\/\/www.instagram.com\/uni.lu\",\"https:\/\/www.youtube.com\/@uni_lu\",\"https:\/\/en.wikipedia.org\/wiki\/University_of_Luxembourg\"]}]}<\/script>\n<!-- \/ Yoast SEO Premium plugin. -->","yoast_head_json":{"title":"SRM Research Seminar: How to model (e-voting) protocols in Tamarin - Universit\u00e9 du Luxembourg","description":"The Tamarin prover is a tool for the symbolic modeling and analysis of security protocols. It takes as input a protocol model, a specification of the adversary, and a specification of the protocol's desired properties. Tamarin can then be used to automatically check if the protocol fulfills the properties, given that arbitrarily many instances of the protocol's roles are run in parallel with the adversary.","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:\/\/www.uni.lu\/fr\/events\/srm-research-seminar-how-to-model-e-voting-protocols-in-tamarin\/","og_locale":"fr_FR","og_type":"article","og_title":"SRM Research Seminar: How to model (e-voting) protocols in Tamarin","og_description":"The Tamarin prover is a tool for the symbolic modeling and analysis of security protocols. It takes as input a protocol model, a specification of the adversary, and a specification of the protocol's desired properties. Tamarin can then be used to automatically check if the protocol fulfills the properties, given that arbitrarily many instances of the protocol's roles are run in parallel with the adversary.","og_url":"https:\/\/www.uni.lu\/fr\/events\/srm-research-seminar-how-to-model-e-voting-protocols-in-tamarin\/","og_site_name":"UNI FR","article_publisher":"https:\/\/www.facebook.com\/uni.lu","og_image":[{"width":2560,"height":2560,"url":"https:\/\/www.uni.lu\/wp-content\/uploads\/sites\/11\/2026\/03\/03120045\/UNIV_SM-Profile_1600x1600px-scaled.jpg","type":"image\/jpeg"}],"twitter_card":"summary_large_image","twitter_misc":{"Dur\u00e9e de lecture estim\u00e9e":"1 minute"},"schema":{"@context":"https:\/\/schema.org","@graph":[{"@type":"WebPage","@id":"https:\/\/www.uni.lu\/fr\/events\/srm-research-seminar-how-to-model-e-voting-protocols-in-tamarin\/","url":"https:\/\/www.uni.lu\/fr\/events\/srm-research-seminar-how-to-model-e-voting-protocols-in-tamarin\/","name":"SRM Research Seminar: How to model (e-voting) protocols in Tamarin - Universit\u00e9 du Luxembourg","isPartOf":{"@id":"https:\/\/www.uni.lu\/fr\/#website"},"primaryImageOfPage":{"@id":"https:\/\/www.uni.lu\/fr\/events\/srm-research-seminar-how-to-model-e-voting-protocols-in-tamarin\/#primaryimage"},"image":{"@id":"https:\/\/www.uni.lu\/fr\/events\/srm-research-seminar-how-to-model-e-voting-protocols-in-tamarin\/#primaryimage"},"thumbnailUrl":"https:\/\/www.uni.lu\/wp-content\/uploads\/sites\/11\/2018\/03\/srm_research_seminar_how_to_model_e_voting_protocols_in_tamarin.jpg","datePublished":"2018-03-05T08:10:42+00:00","dateModified":"2018-03-05T08:10:42+00:00","description":"The Tamarin prover is a tool for the symbolic modeling and analysis of security protocols. It takes as input a protocol model, a specification of the adversary, and a specification of the protocol's desired properties. Tamarin can then be used to automatically check if the protocol fulfills the properties, given that arbitrarily many instances of the protocol's roles are run in parallel with the adversary.","breadcrumb":{"@id":"https:\/\/www.uni.lu\/fr\/events\/srm-research-seminar-how-to-model-e-voting-protocols-in-tamarin\/#breadcrumb"},"inLanguage":"fr-FR","potentialAction":[{"@type":"ReadAction","target":["https:\/\/www.uni.lu\/fr\/events\/srm-research-seminar-how-to-model-e-voting-protocols-in-tamarin\/"]}]},{"@type":"ImageObject","inLanguage":"fr-FR","@id":"https:\/\/www.uni.lu\/fr\/events\/srm-research-seminar-how-to-model-e-voting-protocols-in-tamarin\/#primaryimage","url":"https:\/\/www.uni.lu\/wp-content\/uploads\/sites\/11\/2018\/03\/srm_research_seminar_how_to_model_e_voting_protocols_in_tamarin.jpg","contentUrl":"https:\/\/www.uni.lu\/wp-content\/uploads\/sites\/11\/2018\/03\/srm_research_seminar_how_to_model_e_voting_protocols_in_tamarin.jpg","width":800,"height":600},{"@type":"BreadcrumbList","@id":"https:\/\/www.uni.lu\/fr\/events\/srm-research-seminar-how-to-model-e-voting-protocols-in-tamarin\/#breadcrumb","itemListElement":[{"@type":"ListItem","position":1,"name":"Home","item":"https:\/\/www.uni.lu\/fr\/"},{"@type":"ListItem","position":2,"name":"Events","item":"https:\/\/www.uni.lu\/fr\/events\/"},{"@type":"ListItem","position":3,"name":"SRM Research Seminar: How to model (e-voting) protocols in Tamarin"}]},{"@type":"WebSite","@id":"https:\/\/www.uni.lu\/fr\/#website","url":"https:\/\/www.uni.lu\/fr\/","name":"Uni.lu","description":"Universit\u00e9 du Luxembourg","publisher":{"@id":"https:\/\/www.uni.lu\/fr\/#organization"},"alternateName":"Universit\u00e9 du Luxembourg","potentialAction":[{"@type":"SearchAction","target":{"@type":"EntryPoint","urlTemplate":"https:\/\/www.uni.lu\/fr\/?s={search_term_string}"},"query-input":"required name=search_term_string"}],"inLanguage":"fr-FR"},{"@type":"Organization","@id":"https:\/\/www.uni.lu\/fr\/#organization","name":"Universit\u00e9 du Luxembourg","alternateName":"Uni.lu","url":"https:\/\/www.uni.lu\/fr\/","logo":{"@type":"ImageObject","inLanguage":"fr-FR","@id":"https:\/\/www.uni.lu\/fr\/#\/schema\/logo\/image\/","url":"https:\/\/www.uni.lu\/wp-content\/uploads\/sites\/11\/2026\/03\/03120045\/UNIV_SM-Profile_1600x1600px-scaled.jpg","contentUrl":"https:\/\/www.uni.lu\/wp-content\/uploads\/sites\/11\/2026\/03\/03120045\/UNIV_SM-Profile_1600x1600px-scaled.jpg","width":2560,"height":2560,"caption":"Universit\u00e9 du Luxembourg"},"image":{"@id":"https:\/\/www.uni.lu\/fr\/#\/schema\/logo\/image\/"},"sameAs":["https:\/\/www.facebook.com\/uni.lu","https:\/\/www.linkedin.com\/school\/university-of-luxembourg\/","https:\/\/www.instagram.com\/uni.lu","https:\/\/www.youtube.com\/@uni_lu","https:\/\/en.wikipedia.org\/wiki\/University_of_Luxembourg"]}]}},"_links":{"self":[{"href":"https:\/\/www.uni.lu\/fr\/wp-json\/wp\/v2\/events\/6623"}],"collection":[{"href":"https:\/\/www.uni.lu\/fr\/wp-json\/wp\/v2\/events"}],"about":[{"href":"https:\/\/www.uni.lu\/fr\/wp-json\/wp\/v2\/types\/events"}],"replies":[{"embeddable":true,"href":"https:\/\/www.uni.lu\/fr\/wp-json\/wp\/v2\/comments?post=6623"}],"version-history":[{"count":0,"href":"https:\/\/www.uni.lu\/fr\/wp-json\/wp\/v2\/events\/6623\/revisions"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.uni.lu\/fr\/wp-json\/wp\/v2\/media\/6624"}],"wp:attachment":[{"href":"https:\/\/www.uni.lu\/fr\/wp-json\/wp\/v2\/media?parent=6623"}],"wp:term":[{"taxonomy":"events-topic","embeddable":true,"href":"https:\/\/www.uni.lu\/fr\/wp-json\/wp\/v2\/events-topic?post=6623"},{"taxonomy":"events-type","embeddable":true,"href":"https:\/\/www.uni.lu\/fr\/wp-json\/wp\/v2\/events-type?post=6623"},{"taxonomy":"organisation","embeddable":true,"href":"https:\/\/www.uni.lu\/fr\/wp-json\/wp\/v2\/organisation?post=6623"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}