1(herald "Yahalom Protocol with Forwarding Removed") 2 3(defprotocol yahalom basic 4 (defrole init 5 (vars (a b c name) (n-a n-b text) (k skey)) 6 (trace (send (cat a n-a)) 7 (recv (enc b k n-a n-b (ltk a c))) 8 (send (enc n-b k)))) 9 (defrole resp 10 (vars (b a c name) (n-a n-b text) (k skey)) 11 (trace (recv (cat a n-a)) 12 (send (cat b (enc a n-a n-b (ltk b c)))) 13 (recv (enc a k (ltk b c))) 14 (recv (enc n-b k)))) 15 (defrole serv 16 (vars (c a b name) (n-a n-b text) (k skey)) 17 (trace (recv (cat b (enc a n-a n-b (ltk b c)))) 18 (send (enc b k n-a n-b (ltk a c))) 19 (send (enc a k (ltk b c)))) 20 (uniq-orig k))) 21 22(defskeleton yahalom 23 (vars (a b c name) (n-b text)) 24 (defstrand resp 4 (a a) (b b) (c c) (n-b n-b)) 25 (non-orig (ltk b c) (ltk a c)) 26 (uniq-orig n-b)) 27 28;;; Ensure encryption key remains secret. 29(defskeleton yahalom 30 (vars (a b c name) (n-b text) (k skey)) 31 (defstrand resp 4 (a a) (b b) (c c) (n-b n-b) (k k)) 32 (deflistener k) 33 (non-orig (ltk b c) (ltk a c)) 34 (uniq-orig n-b)) 35