X-IronPort-MID: 56718504 X-SBRS: 5.5 X-BrightmailFiltered: true X-Brightmail-Tracker: AAAAAQAAA+k= X-IronPort-AV: i="4.01,233,1136181600"; d="scan'208"; a="56718504:sNHT16084288" From: "David L. Rager" To: Cc: "'David L. Rager'" Subject: This Week in ACL2: A model for JFKr, a shared-key establishment protocol Date: Mon, 30 Jan 2006 05:59:27 -0600 X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.2180 Thread-Index: AcX6SiwrSH9KitcRTIKKk3Qxv8gdXArSO1tg In-Reply-To: <200512060948.jB69mBrO006223@mail.cs.utexas.edu> Reply-To: acl2-mtg@lists.cc.utexas.edu Sender: owner-acl2-mtg@lists.cc.utexas.edu X-Listprocessor-Version: 8.2.10/020311/17:52 -- ListProc(tm) by CREN X-SpamAssassin-Status: No, hits=-2.6 required=5.0 X-UTCS-Spam-Status: No, hits=-152 required=180 Hello All, This week during the ACL2 meeting I will present my work on shared-key establishment protocol JFKr. While the model has been through revision, there is still work to do, and I encourage those with ideas to voice them. I have included an abstract below the signature. The meeting is scheduled this Wednesday (2/1) from 4:00 to 5:45 pm in ACES 3.116. Hope to see and hear you there, David Abstract JFKr is a security protocol that establishes a shared key between two participants. Its roots stem from the original Diffie-Hellman protocol which takes advantage of the mathematical properties of modular exponentiation to allow two parties to create a secret key from one private piece of information and one public piece of information. Since the original Diffie-Hellman protocol had no method for authenticating users, no notion of protecting identity (since there was no identity in the first place), and was vulnerable to denial of service attacks, it has evolved over time into ISO 9798-3, Internet Key Exchange (IKE), and finally Just Fast Keying (JFK). This talk will describe briefly the different security components of JFKr and the security property each component is supposed to provide us with. I will then describe my executable model, interleaving pieces of code to help the audience understand how my model represents the protocol specification. Finally, I will present my proof of each party's identity and describe my future strategy for proving key agreement.