@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}
}

{"_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.&nbsp;J.; and Guttman, J.&nbsp;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 &nbsp;\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 &nbsp;\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 &nbsp;\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"]}