An Algebra for Symbolic Diffie-Hellman Protocol Analysis. Dougherty, D. J. & Guttman, J. D. 2012.

Paper abstract bibtex

Paper abstract bibtex

We study the algebra underlying symbolic protocol analysis for 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 define an algebra that validates precisely the equations that hold almost always as the order of the cyclic group varies. We realize this algebra as the set of normal forms of a particular rewriting theory. The 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 UM, a protocol using Diffie-Hellman for implicit authentication.

@conference{ DG12, author = {Daniel J. Dougherty and Joshua D. Guttman}, title = {An Algebra for Symbolic {Diffie-Hellman} Protocol Analysis}, booktitle = {Proceedings of the 7th International Symposium on Trustworthy Global Computing}, year = {2012}, abstract = {We study the algebra underlying symbolic protocol analysis for 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 define an algebra that validates precisely the equations that hold almost always as the order of the cyclic group varies. We realize this algebra as the set of normal forms of a particular rewriting theory. The 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 UM, a protocol using Diffie-Hellman for implicit authentication.}, url = {tgc12.pdf} }

Downloads: 0

{"_id":{"_str":"51f6934359ced8df44000e3d"},"__v":1,"authorIDs":[],"author_short":["Dougherty, D.<nbsp>J.","Guttman, J.<nbsp>D."],"bibbaseid":"dougherty-guttman-analgebraforsymbolicdiffiehellmanprotocolanalysis-2012","bibdata":{"html":"<div class=\"bibbase_paper\"> \n\n\n<span class=\"bibbase_paper_titleauthoryear\">\n\t<span class=\"bibbase_paper_title\"><a name=\"DG12\"> </a>An Algebra for Symbolic Diffie-Hellman Protocol Analysis.</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 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-analgebraforsymbolicdiffiehellmanprotocolanalysis-2012', 'http://web.cs.wpi.edu/~dd/publications/tgc12.pdf')\">DEBUG -->\n <!-- </i> -->\n\n <a href=\"http://web.cs.wpi.edu/~dd/publications/tgc12.pdf\"\n onclick=\"javascript:log_download('dougherty-guttman-analgebraforsymbolicdiffiehellmanprotocolanalysis-2012', 'http://web.cs.wpi.edu/~dd/publications/tgc12.pdf')\">\n <img src=\"http://bibbase.org/img/filetypes/pdf.png\"\n\t alt=\"An Algebra for Symbolic Diffie-Hellman Protocol Analysis [.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 \n <a href=\"javascript:showBib('DG12')\"\n class=\"bibbase link\">\n <!-- <img src=\"http://bibbase.org/img/filetypes/bib.png\" -->\n\t<!-- alt=\"An Algebra for Symbolic Diffie-Hellman Protocol Analysis [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('DG12')\">\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_DG12\"\n style=\"display:none\">\n <pre>@conference{ DG12,\n author = {Daniel J. Dougherty and Joshua D. Guttman},\n title = {An Algebra for Symbolic {Diffie-Hellman} Protocol\n Analysis},\n booktitle = {Proceedings of the 7th International Symposium on\n Trustworthy Global Computing},\n year = {2012},\n abstract = {We study the algebra underlying symbolic protocol\n analysis for 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 define an algebra that validates\n precisely the equations that hold almost always as the\n order of the cyclic group varies. We realize this\n algebra as the set of normal forms of a particular\n rewriting theory. The normal forms allow us to define\n our crucial notion of indicator, a vector of integers\n that summarizes how many times each secret exponent\n appears in a message. We prove that the adversary can\n never construct a message with a new indicator in our\n adversary model. Using this invariant, we prove the\n main security goals achieved by UM, a protocol using\n Diffie-Hellman for implicit authentication.},\n url = {tgc12.pdf}\n}</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" id=\"abstract_DG12\"\n style=\"display:none\">\n We study the algebra underlying symbolic protocol analysis for 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 define an algebra that validates precisely the equations that hold almost always as the order of the cyclic group varies. We realize this algebra as the set of normal forms of a particular rewriting theory. The 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 UM, a protocol using Diffie-Hellman for implicit authentication.\n</div>\n\n\n</div>\n","downloads":0,"bibbaseid":"dougherty-guttman-analgebraforsymbolicdiffiehellmanprotocolanalysis-2012","urls":{"Paper":"http://web.cs.wpi.edu/~dd/publications/tgc12.pdf"},"role":"author","abstract":"We study the algebra underlying symbolic protocol analysis for 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 define an algebra that validates precisely the equations that hold almost always as the order of the cyclic group varies. We realize this algebra as the set of normal forms of a particular rewriting theory. The 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 UM, a protocol using Diffie-Hellman for implicit authentication.","author":["Dougherty, Daniel J.","Guttman, Joshua D."],"author_short":["Dougherty, D.<nbsp>J.","Guttman, J.<nbsp>D."],"bibtex":"@conference{ DG12,\n author = {Daniel J. Dougherty and Joshua D. Guttman},\n title = {An Algebra for Symbolic {Diffie-Hellman} Protocol\n Analysis},\n booktitle = {Proceedings of the 7th International Symposium on\n Trustworthy Global Computing},\n year = {2012},\n abstract = {We study the algebra underlying symbolic protocol\n analysis for 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 define an algebra that validates\n precisely the equations that hold almost always as the\n order of the cyclic group varies. We realize this\n algebra as the set of normal forms of a particular\n rewriting theory. The normal forms allow us to define\n our crucial notion of indicator, a vector of integers\n that summarizes how many times each secret exponent\n appears in a message. We prove that the adversary can\n never construct a message with a new indicator in our\n adversary model. Using this invariant, we prove the\n main security goals achieved by UM, a protocol using\n Diffie-Hellman for implicit authentication.},\n url = {tgc12.pdf}\n}","bibtype":"conference","booktitle":"Proceedings of the 7th International Symposium on Trustworthy Global Computing","id":"DG12","key":"DG12","title":"An Algebra for Symbolic Diffie-Hellman Protocol Analysis","type":"conference","url":"tgc12.pdf","year":"2012"},"bibtype":"conference","biburl":"http://web.cs.wpi.edu/~dd/publications/index.bib","downloads":0,"search_terms":["algebra","symbolic","diffie","hellman","protocol","analysis","dougherty","guttman"],"title":"An Algebra for Symbolic Diffie-Hellman Protocol Analysis","year":2012,"dataSources":["HB5RrPb3Y5aikRoLH"]}