{"id":15120,"date":"2022-06-18T19:40:39","date_gmt":"2022-06-18T23:40:39","guid":{"rendered":"https:\/\/carleton.ca\/scs\/?page_id=15120"},"modified":"2026-06-08T14:49:06","modified_gmt":"2026-06-08T18:49:06","slug":"tr-241-extending-cryptographic-logics-of-belief-to-key-agreement-protocols","status":"publish","type":"page","link":"https:\/\/carleton.ca\/scs\/research\/scs-technical-reports\/technical-reports-1994\/tr-241-extending-cryptographic-logics-of-belief-to-key-agreement-protocols\/","title":{"rendered":"TR-241: Extending Cryptographic Logics of Belief to Key Agreement Protocols"},"content":{"rendered":"\n<section class=\"w-screen px-6 cu-section cu-section--white ml-offset-center md:px-8 lg:px-14\">\n    <div class=\"space-y-6 cu-max-w-child-5xl  md:space-y-10 cu-prose-first-last\">\n\n            <div class=\"cu-textmedia flex flex-col lg:flex-row mx-auto gap-6 md:gap-10 my-6 md:my-12 first:mt-0 max-w-5xl\">\n        <div class=\"justify-start cu-textmedia-content cu-prose-first-last\" style=\"flex: 0 0 100%;\">\n            <header class=\"font-light prose-xl cu-pageheader md:prose-2xl cu-component-updated cu-prose-first-last\">\n                                    <h1 class=\"cu-prose-first-last font-semibold !mt-2 mb-4 md:mb-6 relative after:absolute after:h-px after:bottom-0 after:bg-cu-red after:left-px text-3xl md:text-4xl lg:text-5xl lg:leading-[3.5rem] pb-5 after:w-10 text-cu-black-700 not-prose\">\n                        TR-241: Extending Cryptographic Logics of Belief to Key Agreement Protocols\n                    <\/h1>\n                \n                                \n                            <\/header>\n\n                    <\/div>\n\n            <\/div>\n\n    <\/div>\n<\/section>\n\n\n\n<p>Carleton University<br><a href=\"https:\/\/carleton.ca\/scs\/research\/scs-technical-reports\/technical-reports-1994\/\">Technical Report<\/a>&nbsp;<strong>TR-241<\/strong><br>May 1994<\/p>\n\n\n\n<h2 id=\"extending-cryptographic-logics-of-belief-to-key-agreement-protocols\" class=\"wp-block-heading\">Extending Cryptographic Logics of Belief to Key Agreement Protocols<\/h2>\n\n\n\n<p>Paul C. van Oorschot<\/p>\n\n\n\n<h3 id=\"abstract\" class=\"wp-block-heading\">Abstract<\/h3>\n\n\n\n<p>The authentication logic of Burrows, Abadi and Needham (BAN) provided an important step towards rigourous analysis of authentication protocols, and has motivated several subsequent refinements. We propose extensions to BAN-like log\u00adics which facilitate, for the first time, examination of public-key based authenticated key establishment protocols in which both par\u00adties contribute to the derived key (i.e. key agreement protocols). Attention is focussed on six distinct generic goals for authenticated key establishment protocols. The extended logic is used to analyze three Diffie-Hellman based key agreement protocols, facilitating direct comparison of these protocols with respect to formal goals reached and formal assumptions required.<\/p>\n\n\n\n<p><a href=\"https:\/\/carleton.ca\/scs\/wp-content\/uploads\/sites\/260\/TR-241.pdf\">TR-241.pdf<\/a><\/p>\n","protected":false},"excerpt":{"rendered":"<p>Carleton UniversityTechnical Report&nbsp;TR-241May 1994 Extending Cryptographic Logics of Belief to Key Agreement Protocols Paul C. van Oorschot Abstract The authentication logic of Burrows, Abadi and Needham (BAN) provided an important step towards rigourous analysis of authentication protocols, and has motivated several subsequent refinements. We propose extensions to BAN-like log\u00adics which facilitate, for the first time, [&hellip;]<\/p>\n","protected":false},"author":2,"featured_media":0,"parent":11914,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"_acf_changed":false,"_cu_dining_location_slug":"","footnotes":"","_links_to":"","_links_to_target":""},"cu_page_type":[],"class_list":["post-15120","page","type-page","status-publish","hentry"],"acf":{"cu_post_thumbnail":""},"_links":{"self":[{"href":"https:\/\/carleton.ca\/scs\/wp-json\/wp\/v2\/pages\/15120","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/carleton.ca\/scs\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/carleton.ca\/scs\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/carleton.ca\/scs\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/carleton.ca\/scs\/wp-json\/wp\/v2\/comments?post=15120"}],"version-history":[{"count":2,"href":"https:\/\/carleton.ca\/scs\/wp-json\/wp\/v2\/pages\/15120\/revisions"}],"predecessor-version":[{"id":24438,"href":"https:\/\/carleton.ca\/scs\/wp-json\/wp\/v2\/pages\/15120\/revisions\/24438"}],"up":[{"embeddable":true,"href":"https:\/\/carleton.ca\/scs\/wp-json\/wp\/v2\/pages\/11914"}],"wp:attachment":[{"href":"https:\/\/carleton.ca\/scs\/wp-json\/wp\/v2\/media?parent=15120"}],"wp:term":[{"taxonomy":"cu_page_type","embeddable":true,"href":"https:\/\/carleton.ca\/scs\/wp-json\/wp\/v2\/cu_page_type?post=15120"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}