(line (spec (line (declare (line (type (line "S" 2 8 2 9 "yahalom6.eva") (line "principal" 2 12 2 21 "yahalom6.eva")) 2 2 2 21 "yahalom6.eva") (line (type (line "B" 2 5 2 6 "yahalom6.eva") (line "principal" 2 12 2 21 "yahalom6.eva")) 2 2 2 21 "yahalom6.eva") (line (type (line "A" 2 2 2 3 "yahalom6.eva") (line "principal" 2 12 2 21 "yahalom6.eva")) 2 2 2 21 "yahalom6.eva") (line (type (line "Kbs" 3 7 3 10 "yahalom6.eva") (line "number" 3 13 3 19 "yahalom6.eva")) 3 2 3 19 "yahalom6.eva") (line (type (line "Kas" 3 2 3 5 "yahalom6.eva") (line "number" 3 13 3 19 "yahalom6.eva")) 3 2 3 19 "yahalom6.eva") (line (basetype (line "key" 5 11 5 14 "yahalom6.eva")) 5 2 5 14 "yahalom6.eva") (line (type (line "Kab" 7 10 7 13 "yahalom6.eva") (line "key" 7 16 7 19 "yahalom6.eva")) 7 2 7 19 "yahalom6.eva") (line (type (line "Nb" 7 6 7 8 "yahalom6.eva") (line "key" 7 16 7 19 "yahalom6.eva")) 7 2 7 19 "yahalom6.eva") (line (type (line "Na" 7 2 7 4 "yahalom6.eva") (line "key" 7 16 7 19 "yahalom6.eva")) 7 2 7 19 "yahalom6.eva") (line (type-shared (line "shr" 9 2 9 5 "yahalom6.eva") (line (secret-function (line "number" 9 20 9 26 "yahalom6.eva") (line "principal" 9 7 9 16 "yahalom6.eva")) 9 6 9 33 "yahalom6.eva")) 9 2 9 33 "yahalom6.eva") (line (knows (line "A" 11 2 11 3 "yahalom6.eva") (line (apply (line "shr" 11 10 11 13 "yahalom6.eva") (line "A" 11 14 11 15 "yahalom6.eva")) 11 10 11 16 "yahalom6.eva")) 11 2 11 16 "yahalom6.eva") (line (knows (line "B" 12 2 12 3 "yahalom6.eva") (line (apply (line "shr" 12 10 12 13 "yahalom6.eva") (line "B" 12 14 12 15 "yahalom6.eva")) 12 10 12 16 "yahalom6.eva")) 12 2 12 16 "yahalom6.eva") (line (knows (line "A" 16 2 16 3 "yahalom6.eva") (line "A" 16 10 16 11 "yahalom6.eva")) 16 2 16 14 "yahalom6.eva") (line (knows (line "A" 16 2 16 3 "yahalom6.eva") (line "B" 16 13 16 14 "yahalom6.eva")) 16 2 16 14 "yahalom6.eva") (line (knows (line "B" 17 2 17 3 "yahalom6.eva") (line "B" 17 10 17 11 "yahalom6.eva")) 17 2 17 14 "yahalom6.eva") (line (knows (line "B" 17 2 17 3 "yahalom6.eva") (line "S" 17 13 17 14 "yahalom6.eva")) 17 2 17 14 "yahalom6.eva") (line (type (line "s" 19 8 19 9 "yahalom6.eva") (line "principal" 19 12 19 21 "yahalom6.eva")) 19 2 19 21 "yahalom6.eva") (line (type (line "b" 19 5 19 6 "yahalom6.eva") (line "principal" 19 12 19 21 "yahalom6.eva")) 19 2 19 21 "yahalom6.eva") (line (type (line "a" 19 2 19 3 "yahalom6.eva") (line "principal" 19 12 19 21 "yahalom6.eva")) 19 2 19 21 "yahalom6.eva")) 1 0 19 21 "") (line (line (block (line (comm "1." (line "A" 21 6 21 7 "yahalom6.eva") (line "B" 21 11 21 12 "yahalom6.eva") (line (tuple (line "A" 21 15 21 16 "yahalom6.eva") (line "Na" 21 18 21 20 "yahalom6.eva")) 21 15 21 20 "yahalom6.eva")) 21 3 21 20 "yahalom6.eva") (line (comm "2." (line "B" 22 6 22 7 "yahalom6.eva") (line "S" 22 11 22 12 "yahalom6.eva") (line (tuple (line "B" 22 15 22 16 "yahalom6.eva") (line (crypt (line (tuple (line "A" 22 19 22 20 "yahalom6.eva") (line "Na" 22 22 22 24 "yahalom6.eva") (line "Nb" 22 26 22 28 "yahalom6.eva")) 22 19 22 28 "yahalom6.eva") (line (apply (line "shr" 22 30 22 33 "yahalom6.eva") (line "B" 22 34 22 35 "yahalom6.eva")) 22 30 22 36 "yahalom6.eva") (vanilla)) 22 18 22 36 "yahalom6.eva")) 22 15 22 36 "yahalom6.eva")) 22 3 22 36 "yahalom6.eva") (line (comm "3." (line "S" 23 6 23 7 "yahalom6.eva") (line "A" 23 11 23 12 "yahalom6.eva") (line (tuple (line (crypt (line (tuple (line "B" 23 16 23 17 "yahalom6.eva") (line "Kab" 23 19 23 22 "yahalom6.eva") (line "Na" 23 24 23 26 "yahalom6.eva") (line "Nb" 23 28 23 30 "yahalom6.eva")) 23 16 23 30 "yahalom6.eva") (line (apply (line "shr" 23 32 23 35 "yahalom6.eva") (line "A" 23 36 23 37 "yahalom6.eva")) 23 32 23 38 "yahalom6.eva") (vanilla)) 23 15 23 38 "yahalom6.eva") (line (crypt (line (tuple (line "A" 23 41 23 42 "yahalom6.eva") (line "Kab" 23 44 23 47 "yahalom6.eva")) 23 41 23 47 "yahalom6.eva") (line (apply (line "shr" 23 49 23 52 "yahalom6.eva") (line "B" 23 53 23 54 "yahalom6.eva")) 23 49 23 55 "yahalom6.eva") (vanilla)) 23 40 23 55 "yahalom6.eva")) 23 15 23 55 "yahalom6.eva")) 23 3 23 55 "yahalom6.eva") (line (comm "4." (line "A" 24 6 24 7 "yahalom6.eva") (line "B" 24 11 24 12 "yahalom6.eva") (line (tuple (line (crypt (line (tuple (line "A" 24 16 24 17 "yahalom6.eva") (line "Kab" 24 19 24 22 "yahalom6.eva")) 24 16 24 22 "yahalom6.eva") (line (apply (line "shr" 24 24 24 27 "yahalom6.eva") (line "B" 24 28 24 29 "yahalom6.eva")) 24 24 24 30 "yahalom6.eva") (vanilla)) 24 15 24 30 "yahalom6.eva") (line (crypt (line "Nb" 24 33 24 35 "yahalom6.eva") (line "Kab" 24 37 24 40 "yahalom6.eva") (vanilla)) 24 32 24 40 "yahalom6.eva")) 24 15 24 40 "yahalom6.eva")) 24 3 24 40 "yahalom6.eva")) 20 2 25 3 "yahalom6.eva") 20 2 25 3 "yahalom6.eva") (line (sessions (line (session-repeat (line (private (line "A" 27 16 27 17 "yahalom6.eva") (line "B" 27 19 27 20 "yahalom6.eva")) 27 15 27 21 "yahalom6.eva") "s1." (line (principals-except) 27 15 27 16 "yahalom6.eva") (line (bind (line "A" 27 22 27 23 "yahalom6.eva") (line "a" 27 24 27 25 "yahalom6.eva")) 27 22 27 25 "yahalom6.eva") (line (bind (line "B" 27 27 27 28 "yahalom6.eva") (line "b" 27 29 27 30 "yahalom6.eva")) 27 27 27 30 "yahalom6.eva") (line (bind (line "S" 27 32 27 33 "yahalom6.eva") (line "s" 27 34 27 35 "yahalom6.eva")) 27 32 27 35 "yahalom6.eva")) 27 2 27 35 "yahalom6.eva")) 25 2 27 35 "") (line (assume (line (secret (line (locate "s1." (line "A" 29 27 29 28 "yahalom6.eva") (line (apply (line "shr" 29 17 29 20 "yahalom6.eva") (line "A" 29 21 29 22 "yahalom6.eva")) 29 17 29 23 "yahalom6.eva")) 29 17 29 28 "yahalom6.eva")) 29 9 29 29 "yahalom6.eva") (line (secret (line (locate "s1." (line "B" 30 27 30 28 "yahalom6.eva") (line (apply (line "shr" 30 17 30 20 "yahalom6.eva") (line "B" 30 21 30 22 "yahalom6.eva")) 30 17 30 23 "yahalom6.eva")) 30 17 30 28 "yahalom6.eva")) 30 9 30 29 "yahalom6.eva") (line (secret (line (apply (line "shr" 30 39 30 42 "yahalom6.eva") (line (locate "s1." (line "B" 30 48 30 49 "yahalom6.eva") (line "A" 30 43 30 44 "yahalom6.eva")) 30 43 30 49 "yahalom6.eva")) 30 39 30 50 "yahalom6.eva")) 30 31 30 51 "yahalom6.eva") (line (secret (line (locate "s1." (line "S" 31 20 31 21 "yahalom6.eva") (line (apply (line "shr" 31 10 31 13 "yahalom6.eva") (line "A" 31 14 31 15 "yahalom6.eva")) 31 10 31 16 "yahalom6.eva")) 31 10 31 21 "yahalom6.eva")) 31 2 31 22 "yahalom6.eva") (line (secret (line (locate "s1." (line "S" 31 42 31 43 "yahalom6.eva") (line (apply (line "shr" 31 32 31 35 "yahalom6.eva") (line "B" 31 36 31 37 "yahalom6.eva")) 31 32 31 38 "yahalom6.eva")) 31 32 31 43 "yahalom6.eva")) 31 24 31 44 "yahalom6.eva")) 29 2 31 44 "yahalom6.eva") (line (claim (line (A (line (G (line (secret (line (locate "s1." (line "A" 33 31 33 32 "yahalom6.eva") (line (apply (line "shr" 33 21 33 24 "yahalom6.eva") (line "A" 33 25 33 26 "yahalom6.eva")) 33 21 33 27 "yahalom6.eva")) 33 21 33 32 "yahalom6.eva")) 33 13 33 33 "yahalom6.eva")) 33 10 33 33 "yahalom6.eva")) 33 8 33 33 "yahalom6.eva") (line (A (line (G (line (secret (line (locate "s1." (line "B" 34 24 34 25 "yahalom6.eva") (line (apply (line "shr" 34 14 34 17 "yahalom6.eva") (line "B" 34 18 34 19 "yahalom6.eva")) 34 14 34 20 "yahalom6.eva")) 34 14 34 25 "yahalom6.eva")) 34 6 34 26 "yahalom6.eva")) 34 3 34 26 "yahalom6.eva")) 34 1 34 26 "yahalom6.eva") (line (A (line (G (line (secret (line (locate "s1." (line "S" 35 24 35 25 "yahalom6.eva") (line (apply (line "shr" 35 14 35 17 "yahalom6.eva") (line "A" 35 18 35 19 "yahalom6.eva")) 35 14 35 20 "yahalom6.eva")) 35 14 35 25 "yahalom6.eva")) 35 6 35 26 "yahalom6.eva")) 35 3 35 26 "yahalom6.eva")) 35 1 35 26 "yahalom6.eva") (line (A (line (G (line (secret (line (locate "s1." (line "S" 36 24 36 25 "yahalom6.eva") (line (apply (line "shr" 36 14 36 17 "yahalom6.eva") (line "B" 36 18 36 19 "yahalom6.eva")) 36 14 36 20 "yahalom6.eva")) 36 14 36 25 "yahalom6.eva")) 36 6 36 26 "yahalom6.eva")) 36 3 36 26 "yahalom6.eva")) 36 1 36 26 "yahalom6.eva") (line (A (line (G (line (secret (line (locate "s1." (line "S" 37 21 37 22 "yahalom6.eva") (line "Kab" 37 14 37 17 "yahalom6.eva")) 37 14 37 22 "yahalom6.eva")) 37 6 37 23 "yahalom6.eva")) 37 3 37 23 "yahalom6.eva")) 37 1 37 23 "yahalom6.eva") (line (A (line (G (line (secret (line (locate "s1." (line "B" 38 27 38 28 "yahalom6.eva") (line "Nb" 38 21 38 23 "yahalom6.eva")) 38 21 38 28 "yahalom6.eva")) 38 13 38 29 "yahalom6.eva")) 38 10 38 29 "yahalom6.eva")) 38 8 38 29 "yahalom6.eva")) 33 2 38 29 "yahalom6.eva")) 1 0 31 44 "yahalom6.eva")