{"id":155868,"date":"2005-01-01T00:00:00","date_gmt":"2005-01-01T00:00:00","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/msr-research-item\/model-based-testing-of-cryptographic-protocols\/"},"modified":"2018-10-16T20:09:22","modified_gmt":"2018-10-17T03:09:22","slug":"model-based-testing-of-cryptographic-protocols","status":"publish","type":"msr-research-item","link":"https:\/\/www.microsoft.com\/en-us\/research\/publication\/model-based-testing-of-cryptographic-protocols\/","title":{"rendered":"Model-Based Testing of Cryptographic Protocols"},"content":{"rendered":"<div class=\"asset-content\">\n<p>Modeling is a popular way of representing the behavior of a system. A very useful type of model in computing is an abstract state machine which describes transitions over first order structures. The general purpose model-based testing tool SpecExplorer (used within Microsoft, also available externally) uses such a model, written in AsmL or Spec#, to perform a search that checks that all reachable states of the model are safe, and also to check conformance of an arbitrary .NET implementation to the model. Spec Explorer provides a variety of ways to cut down the state space of the model, for instance by finitizing parameter domains or by providing predicate abstraction. It has already found subtle bugs in production software. First order structures and abstract state machines over them are also a useful way to think about cryptographic protocols, since models formulated in these terms arise by natural abstraction from computational cryptography . In this paper we explain this abstraction process, \u2018experiments as structures\u2019, and argue for its faithfulness. We show how the Dolev\u2013Yao intruder model fits into SpecExplorer. In a word, the actions of the Dolev\u2013Yao intruder are the \u2018controllable\u2019 actions of the testing framework, whereas the actions of protocol participants are the \u2018observable\u2019 actions of the model. The unsafe states are the states violating say Lowe\u2019s security guarantees. Under this view, the general purpose software testing tool quickly finds known attacks, such as Lowe\u2019s attack on the Needham Schroeder protocol.<\/p>\n<\/div>\n<p><!-- .asset-content --><\/p>\n","protected":false},"excerpt":{"rendered":"<p>Modeling is a popular way of representing the behavior of a system. A very useful type of model in computing is an abstract state machine which describes transitions over first order structures. The general purpose model-based testing tool SpecExplorer (used within Microsoft, also available externally) uses such a model, written in AsmL or Spec#, to [&hellip;]<\/p>\n","protected":false},"featured_media":0,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"footnotes":""},"msr-content-type":[3],"msr-research-highlight":[],"research-area":[13547],"msr-publication-type":[193716],"msr-product-type":[],"msr-focus-area":[],"msr-platform":[],"msr-download-source":[],"msr-locale":[268875],"msr-field-of-study":[],"msr-conference":[],"msr-journal":[],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-155868","msr-research-item","type-msr-research-item","status-publish","hentry","msr-research-area-systems-and-networking","msr-locale-en_us"],"msr_publishername":"Springer","msr_edition":"TGC","msr_affiliation":"","msr_published_date":"2005-01-01","msr_host":"","msr_duration":"","msr_version":"","msr_speaker":"","msr_other_contributors":"","msr_booktitle":"","msr_pages_string":"33-60","msr_chapter":"","msr_isbn":"3-540-30007-4","msr_journal":"","msr_volume":"3705","msr_number":"","msr_editors":"","msr_series":"Lecture Notes in Computer Science","msr_issue":"","msr_organization":"","msr_how_published":"","msr_notes":"","msr_highlight_text":"","msr_release_tracker_id":"","msr_original_fields_of_study":"","msr_download_urls":"","msr_external_url":"","msr_secondary_video_url":"","msr_longbiography":"","msr_microsoftintellectualproperty":1,"msr_main_download":"223546","msr_publicationurl":"","msr_doi":"","msr_publication_uploader":[{"type":"file","title":"ModelBasedTestingOfCrypto(TGC2005).pdf","viewUrl":"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2005\/01\/ModelBasedTestingOfCryptoTGC2005.pdf","id":223546,"label_id":0}],"msr_related_uploader":"","msr_attachments":[{"id":223546,"url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2005\/01\/ModelBasedTestingOfCryptoTGC2005.pdf"}],"msr-author-ordering":[{"type":"text","value":"Dean Rosenzweig","user_id":0,"rest_url":false},{"type":"text","value":"Davor Runje","user_id":0,"rest_url":false},{"type":"user_nicename","value":"schulte","user_id":33552,"rest_url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/microsoft-research\/v1\/researchers?person=schulte"}],"msr_impact_theme":[],"msr_research_lab":[],"msr_event":[],"msr_group":[],"msr_project":[170116],"publication":[],"video":[],"download":[],"msr_publication_type":"inproceedings","_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/155868"}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-research-item"}],"version-history":[{"count":1,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/155868\/revisions"}],"predecessor-version":[{"id":523426,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/155868\/revisions\/523426"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=155868"}],"wp:term":[{"taxonomy":"msr-content-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-content-type?post=155868"},{"taxonomy":"msr-research-highlight","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-highlight?post=155868"},{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=155868"},{"taxonomy":"msr-publication-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-publication-type?post=155868"},{"taxonomy":"msr-product-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-product-type?post=155868"},{"taxonomy":"msr-focus-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-focus-area?post=155868"},{"taxonomy":"msr-platform","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-platform?post=155868"},{"taxonomy":"msr-download-source","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-download-source?post=155868"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=155868"},{"taxonomy":"msr-field-of-study","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-field-of-study?post=155868"},{"taxonomy":"msr-conference","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-conference?post=155868"},{"taxonomy":"msr-journal","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-journal?post=155868"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=155868"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=155868"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}