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