An Algebra for Symbolic Diffie-Hellman Protocol Analysis

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

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\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 \n \n \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 \n\t\n\t\n\t\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"]}