Symbolic Protocol Analysis for Diffie-Hellman. Dougherty, D. J. & Guttman, J. D. *CoRR*, 2012.

Link Paper abstract bibtex

Link Paper abstract bibtex

We extend symbolic protocol analysis to apply to protocols using Diffie-Hellman operations. Diffie-Hellman operations act on a cyclic group of prime order, together with an exponentiation operator. The exponents form a finite field. This rich algebraic structure has resisted previous symbolic approaches. We work in an algebra defined by the normal forms of a rewriting theory (modulo associativity and commutativity). These normal forms allow us to define our crucial notion of indicator, a vector of integers that summarizes how many times each secret exponent appears in a message. We prove that the adversary can never construct a message with a new indicator in our adversary model. Using this invariant, we prove the main security goals achieved by several different protocols that use Diffie-Hellman operators in subtle ways. We also give a model-theoretic justification of our rewriting theory: the theory proves all equations that are uniformly true as the order of the cyclic group varies.

@article{ DBLP:journals/corr/abs-1202-2168, author = {Daniel J. Dougherty and Joshua D. Guttman}, title = {Symbolic Protocol Analysis for {Diffie-Hellman}}, journal = {CoRR}, volume = {abs/1202.2168}, year = {2012}, ee = {http://arxiv.org/abs/1202.2168}, bibsource = {DBLP, http://dblp.uni-trier.de}, abstract = {We extend symbolic protocol analysis to apply to protocols using Diffie-Hellman operations. Diffie-Hellman operations act on a cyclic group of prime order, together with an exponentiation operator. The exponents form a finite field. This rich algebraic structure has resisted previous symbolic approaches. We work in an algebra defined by the normal forms of a rewriting theory (modulo associativity and commutativity). These normal forms allow us to define our crucial notion of indicator, a vector of integers that summarizes how many times each secret exponent appears in a message. We prove that the adversary can never construct a message with a new indicator in our adversary model. Using this invariant, we prove the main security goals achieved by several different protocols that use Diffie-Hellman operators in subtle ways. We also give a model-theoretic justification of our rewriting theory: the theory proves all equations that are uniformly true as the order of the cyclic group varies.}, url = {iadh-arxiv.pdf} }

Downloads: 0

{"_id":{"_str":"51f6934359ced8df44000e49"},"__v":1,"authorIDs":[],"author_short":["Dougherty, D.<nbsp>J.","Guttman, J.<nbsp>D."],"bibbaseid":"dougherty-guttman-symbolicprotocolanalysisfordiffiehellman-2012","bibdata":{"html":"<div class=\"bibbase_paper\"> \n\n\n<span class=\"bibbase_paper_titleauthoryear\">\n\t<span class=\"bibbase_paper_title\"><a name=\"DBLP:journals/corr/abs-1202-2168\"> </a>Symbolic Protocol Analysis for Diffie-Hellman.</span>\n\t<span class=\"bibbase_paper_author\">\nDougherty, D. J.; and Guttman, J. D.</span>\n\t<!-- <span class=\"bibbase_paper_year\">2012</span>. -->\n</span>\n\n\n\n<i>CoRR</i>,\n\nabs/1202.2168.\n\n 2012.\n\n\n\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content\">\n \n \n <!-- <i -->\n <!-- onclick=\"javascript:log_download('dougherty-guttman-symbolicprotocolanalysisfordiffiehellman-2012', 'http://web.cs.wpi.edu/~dd/publications/iadh-arxiv.pdf')\">DEBUG -->\n <!-- </i> -->\n\n <a href=\"http://web.cs.wpi.edu/~dd/publications/iadh-arxiv.pdf\"\n onclick=\"javascript:log_download('dougherty-guttman-symbolicprotocolanalysisfordiffiehellman-2012', 'http://web.cs.wpi.edu/~dd/publications/iadh-arxiv.pdf')\">\n <img src=\"http://bibbase.org/img/filetypes/pdf.png\"\n\t alt=\"Symbolic Protocol Analysis for Diffie-Hellman [.pdf]\" \n\t class=\"bibbase_icon\"\n\t style=\"width: 24px; height: 24px; border: 0px; vertical-align: text-top\" ><span class=\"bibbase_icon_text\">Paper</span></a> \n \n \n <!-- <i -->\n <!-- onclick=\"javascript:log_download('dougherty-guttman-symbolicprotocolanalysisfordiffiehellman-2012', 'http://arxiv.org/abs/1202.2168')\">DEBUG -->\n <!-- </i> -->\n\n <a href=\"http://arxiv.org/abs/1202.2168\"\n onclick=\"javascript:log_download('dougherty-guttman-symbolicprotocolanalysisfordiffiehellman-2012', 'http://arxiv.org/abs/1202.2168')\">\n <img src=\"http://bibbase.org/img/filetypes/blank.png\"\n\t alt=\"Symbolic Protocol Analysis for Diffie-Hellman [.2168]\" \n\t class=\"bibbase_icon\"\n\t style=\"width: 24px; height: 24px; border: 0px; vertical-align: text-top\" ><span class=\"bibbase_icon_text\">Link</span></a> \n \n \n \n <a href=\"javascript:showBib('DBLP:journals/corr/abs-1202-2168')\"\n class=\"bibbase link\">\n <!-- <img src=\"http://bibbase.org/img/filetypes/bib.png\" -->\n\t<!-- alt=\"Symbolic Protocol Analysis for Diffie-Hellman [bib]\" -->\n\t<!-- class=\"bibbase_icon\" -->\n\t<!-- style=\"width: 24px; height: 24px; border: 0px; vertical-align: text-top\"><span class=\"bibbase_icon_text\">Bibtex</span> -->\n BibTeX\n <i class=\"fa fa-caret-down\"></i></a>\n \n \n \n <a class=\"bibbase_abstract_link bibbase link\"\n href=\"javascript:showAbstract('DBLP:journals/corr/abs-1202-2168')\">\n Abstract\n <i class=\"fa fa-caret-down\"></i></a>\n \n \n \n\n \n \n \n</span>\n\n<div class=\"well well-small bibbase\" id=\"bib_DBLP_journals_corr_abs_1202_2168\"\n style=\"display:none\">\n <pre>@article{ DBLP:journals/corr/abs-1202-2168,\n author = {Daniel J. Dougherty and Joshua D. Guttman},\n title = {Symbolic Protocol Analysis for {Diffie-Hellman}},\n journal = {CoRR},\n volume = {abs/1202.2168},\n year = {2012},\n ee = {http://arxiv.org/abs/1202.2168},\n bibsource = {DBLP, http://dblp.uni-trier.de},\n abstract = {We extend symbolic protocol analysis to apply to\n protocols using Diffie-Hellman\n operations. Diffie-Hellman operations act on a cyclic\n group of prime order, together with an exponentiation\n operator. The exponents form a finite field. This rich\n algebraic structure has resisted previous symbolic\n approaches. We work in an algebra defined by the\n normal forms of a rewriting theory (modulo\n associativity and commutativity). These normal forms\n allow us to define our crucial notion of indicator, a\n vector of integers that summarizes how many times each\n secret exponent appears in a message. We prove that\n the adversary can never construct a message with a new\n indicator in our adversary model. Using this\n invariant, we prove the main security goals achieved\n by several different protocols that use Diffie-Hellman\n operators in subtle ways. We also give a\n model-theoretic justification of our rewriting theory:\n the theory proves all equations that are uniformly\n true as the order of the cyclic group varies.},\n url = {iadh-arxiv.pdf}\n}</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" id=\"abstract_DBLP_journals_corr_abs_1202_2168\"\n style=\"display:none\">\n We extend symbolic protocol analysis to apply to protocols using Diffie-Hellman operations. Diffie-Hellman operations act on a cyclic group of prime order, together with an exponentiation operator. The exponents form a finite field. This rich algebraic structure has resisted previous symbolic approaches. We work in an algebra defined by the normal forms of a rewriting theory (modulo associativity and commutativity). These normal forms allow us to define our crucial notion of indicator, a vector of integers that summarizes how many times each secret exponent appears in a message. We prove that the adversary can never construct a message with a new indicator in our adversary model. Using this invariant, we prove the main security goals achieved by several different protocols that use Diffie-Hellman operators in subtle ways. We also give a model-theoretic justification of our rewriting theory: the theory proves all equations that are uniformly true as the order of the cyclic group varies.\n</div>\n\n\n</div>\n","downloads":0,"bibbaseid":"dougherty-guttman-symbolicprotocolanalysisfordiffiehellman-2012","urls":{"Link":"http://arxiv.org/abs/1202.2168","Paper":"http://web.cs.wpi.edu/~dd/publications/iadh-arxiv.pdf"},"role":"author","abstract":"We extend symbolic protocol analysis to apply to protocols using Diffie-Hellman operations. Diffie-Hellman operations act on a cyclic group of prime order, together with an exponentiation operator. The exponents form a finite field. This rich algebraic structure has resisted previous symbolic approaches. We work in an algebra defined by the normal forms of a rewriting theory (modulo associativity and commutativity). These normal forms allow us to define our crucial notion of indicator, a vector of integers that summarizes how many times each secret exponent appears in a message. We prove that the adversary can never construct a message with a new indicator in our adversary model. Using this invariant, we prove the main security goals achieved by several different protocols that use Diffie-Hellman operators in subtle ways. We also give a model-theoretic justification of our rewriting theory: the theory proves all equations that are uniformly true as the order of the cyclic group varies.","author":["Dougherty, Daniel J.","Guttman, Joshua D."],"author_short":["Dougherty, D.<nbsp>J.","Guttman, J.<nbsp>D."],"bibsource":"DBLP, http://dblp.uni-trier.de","bibtex":"@article{ DBLP:journals/corr/abs-1202-2168,\n author = {Daniel J. Dougherty and Joshua D. Guttman},\n title = {Symbolic Protocol Analysis for {Diffie-Hellman}},\n journal = {CoRR},\n volume = {abs/1202.2168},\n year = {2012},\n ee = {http://arxiv.org/abs/1202.2168},\n bibsource = {DBLP, http://dblp.uni-trier.de},\n abstract = {We extend symbolic protocol analysis to apply to\n protocols using Diffie-Hellman\n operations. Diffie-Hellman operations act on a cyclic\n group of prime order, together with an exponentiation\n operator. The exponents form a finite field. This rich\n algebraic structure has resisted previous symbolic\n approaches. We work in an algebra defined by the\n normal forms of a rewriting theory (modulo\n associativity and commutativity). These normal forms\n allow us to define our crucial notion of indicator, a\n vector of integers that summarizes how many times each\n secret exponent appears in a message. We prove that\n the adversary can never construct a message with a new\n indicator in our adversary model. Using this\n invariant, we prove the main security goals achieved\n by several different protocols that use Diffie-Hellman\n operators in subtle ways. We also give a\n model-theoretic justification of our rewriting theory:\n the theory proves all equations that are uniformly\n true as the order of the cyclic group varies.},\n url = {iadh-arxiv.pdf}\n}","bibtype":"article","ee":"http://arxiv.org/abs/1202.2168","id":"DBLP:journals/corr/abs-1202-2168","journal":"CoRR","key":"DBLP:journals/corr/abs-1202-2168","title":"Symbolic Protocol Analysis for Diffie-Hellman","type":"article","url":"iadh-arxiv.pdf","volume":"abs/1202.2168","year":"2012"},"bibtype":"article","biburl":"http://web.cs.wpi.edu/~dd/publications/index.bib","downloads":0,"search_terms":["symbolic","protocol","analysis","diffie","hellman","dougherty","guttman"],"title":"Symbolic Protocol Analysis for Diffie-Hellman","year":2012,"dataSources":["HB5RrPb3Y5aikRoLH"]}