An Executable Model for JFKrAbout ACL2Diffie-HelmanBasic DH Model PartsKnowledge-state Attempt #1Knowledge-state Attempt #2Onto JFKrJFKr PropertiesWhat I DidCapturing Perfect CryptographyCapturing Perfect CryptographyCapturing Perfect CryptographyCapturing Perfect CryptographyMain FunctionA Simple Honest Step FunctionA Simple Dishonest Step FunctionA More Complex Step Function…ExampleDOS Non-deterministic FunctionMem DoS ThmFuture WorkConclusionsResourcesNovember 29, 2004An Executable Model for JFKrAn ACL2 approach to key-establishmentprotocol verificationPresented by: David RagerNovember 22, 2004November 29, 2004About ACL2 J S Moore and Matt Kaufmann ACL2 - A Computational Logic for Applicative Common Lisp Applicative – functional Hierarchical Prove lemmas to prove larger theorems Doubles as an executable modelNovember 29, 2004Diffie-Helman Model based off a state containing a list of “knowledge” From “knowledge” compute diffie-helmancomponents From diffie-helman components, show: Forward secrecy - yes Authentication - no Replay Attack - yes DoS - no ID Protection - noNovember 29, 2004Basic DH Model Parts1. If an actor has neither of the two nonces used in a DH computation, it can not derive the DH key.2. An intruder does not begin with either of the two relevant nonces.3. Nonces are not released during the communication (requires induction).4. Since nonces are not released during communication and the intruder has neither of the two relevant nonces, the intruder can not obtain the DH key Should be easyNovember 29, 2004Knowledge-state Attempt #1 Contained redundant data Should trim to basic building blocks'((A (nonce a)(exp (nonce g) (nonce a)) (exp (nonce g) (nonce b)) (exp (nonce g) (mult (nonce a) (nonce b))))(B (nonce b) (exp (nonce g) (nonce a)) (exp (nonce g) (nonce b))(exp (nonce g) (mult (nonce a) (nonce b))))(I (exp (nonce g) (nonce a))(exp (nonce g) (nonce b))))November 29, 2004Knowledge-state Attempt #2 The need to move forward preempted developing this more‘( ;; I is for initiator(I (nonce x)(base g)(mod b)(term (mod (exp g y) b))));; R is for Responder(R (nonce y)(base g)(mod b)(term (mod (exp g x) b))));; N is for intruder(N (base g) (mod b)(term (mod (exp g x) b)))(term (mod (exp g y) b)))))November 29, 2004Onto JFKrIRNi, xixi=gdiNi, Nr, xr, gr, trxr=gdrtr=hashKr(xr,Nr,Ni,IPi)Ni, Nr, xi, xr, tr, ei, hiei=encKe(IDi,ID’r,sai,sigKi(Nr,Ni,xr,xi,gr))xidr=xrdi=x Ka,e,v=hashx(Ni,Nr,{a,e,v})hi=hashKa(“i”,ei)er, hr“hint” to responder which identity to usederive a set of keys from shared secret and noncescheck integrity before decryptingSame drforevery connectionDH groupIf initiator knowsgroup g in advanceer=encKe(IDr,sar,sigKr(xr,Nr,xi,Ni)) hr=hashKa(“r”,er)real identity of the responder[Aiello et al.] and ShmatikovNovember 29, 2004JFKr Properties Secrecy (via DH like key agreement) Prevention of DoS (via cookie) Forward secrecy (use of nonce for randomization) Authentication (public/private key signatures) ID Protection (ID not revealed until protocol nearing completion)November 29, 2004What I Did Executable model 1200 lines of ACL2 code Relatively low global constant usageNovember 29, 2004Capturing Perfect Cryptography First idea: Make all knowledge broadcast in previous transmissions a constant > 100 Make all private knowledge < 100 Show that the attacker never gains something < 100November 29, 2004Capturing Perfect Cryptography Second idea: Assign a probability threshold for what is acceptable Requires tracking probability of a “crack”cumulatively Could use to show mathematical weakness in encryption schemesNovember 29, 2004Capturing Perfect Cryptography Third idea: Create generic functions “encapsulated” together with some other functions These functions don’t begin with any definitions Through instantiation of the function set, can prove that there exist functions that satisfy certain properties Useful for specifying mysterious properties like keyed-hash and digital signatures Can specify “perfect” encryption None of these ideas were actually used by meNovember 29, 2004Capturing Perfect Cryptography My Version: Computed a hash of an integer list: Signatures similar Symmetric keys modeled with one + key value Encryption was an addition operation and decryption was a subtraction operation Asymmetric keys modeled with +/- key values Encryption and decryption were same + for encryption - for decryption(defun compute-hash (int-list key acc)(if (atom int-list)acc(compute-hash (cdr int-list)key(* key (+ acc (car int-list))))))November 29, 2004Main Function Uses “honest” participants Chose to make it an explicit calling of recursion instead of a case statement(defun run-honest (network-s initiator-s responder-s)(mv-let (network-s-after-1 initiator-s-after-1)(step1-honest network-s initiator-s)(mv-let (network-s-after-2 responder-s-after-2)(step2-honest network-s-after-1 responder-s)… left out part so it would fit …(mv-let(network-s-after-5 initiator-s-after-5)(step5-honest network-s-after-4 initiator-s-after-3)(mv-let(network-s-after-6 responder-s-after-6)(step6-honest network-s-after-5 responder-s-after-4)(mv network-s-after-6initiator-s-after-5responder-s-after-6))))))))November 29, 2004A Simple Honest Step Function; doesn't matter who responder is(defun step1-honest (network-s my-s); resp-s) ; doesn't matter who responder is(let* ((Ni (nonce-mine my-s))(Xi (compute-public-dh-value *g*(dh-exponent my-s)*b*));; updates are alists(network-update (list (cons 'Ni Ni) (cons 'Xi Xi)(cons 'Src-ip (ip my-s))))(my-update (list (cons 'cost-cpu (+ (cost-cpu my-s) 1))(cons 'cost-mem (+ (cost-mem my-s) 1))(cons 'public-dh-value-mine Xi)(cons 'role 'initiator))))(mv(acons 1 network-update network-s)(append my-update my-s))))November 29, 2004A Simple Dishonest Step Function(defun step1-dishonest (network-s my-s) ; doesn't matter who responder is(let* ((Ni -1)(Xi -1)(Src-ip (ip my-s));; updates are alists(network-update (list (cons 'Ni Ni) (cons 'Xi Xi)(cons 'Src-ip Src-ip)))(my-update(list (cons 'cost-cpu (+ (cost-cpu my-s) 0))(cons 'cost-mem (+ (cost-mem my-s) 0)))))(mv(acons 1 network-update network-s)(append my-update my-s))))November 29, 2004A More Complex Step Function…;; responder is processing and sending message(defun step2-honest (network-s my-s) (let* ((Ni (ni-msg1
View Full Document
Unlocking...