Symbolic Protocol Analysis for Diffie-Hellman. Dougherty, D. J. & Guttman, J. D. CoRR, 2012. 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"]}