(line (spec (line (declare (line (type (line "S" 2 8 2 9 "nspriv.eva") (line "principal" 2 12 2 21 "nspriv.eva")) 2 2 2 21 "nspriv.eva") (line (type (line "B" 2 5 2 6 "nspriv.eva") (line "principal" 2 12 2 21 "nspriv.eva")) 2 2 2 21 "nspriv.eva") (line (type (line "A" 2 2 2 3 "nspriv.eva") (line "principal" 2 12 2 21 "nspriv.eva")) 2 2 2 21 "nspriv.eva") (line (type (line "Kab" 3 2 3 5 "nspriv.eva") (line "number" 3 8 3 14 "nspriv.eva")) 3 2 3 14 "nspriv.eva") (line (type (line "Nb" 4 6 4 8 "nspriv.eva") (line "number" 4 11 4 17 "nspriv.eva")) 4 2 4 17 "nspriv.eva") (line (type (line "Na" 4 2 4 4 "nspriv.eva") (line "number" 4 11 4 17 "nspriv.eva")) 4 2 4 17 "nspriv.eva") (line (type (line "nudge" 5 2 5 7 "nspriv.eva") (line (function (line "number" 5 19 5 25 "nspriv.eva") (line "number" 5 9 5 15 "nspriv.eva")) 5 8 5 25 "nspriv.eva")) 5 2 5 25 "nspriv.eva") (line (type (line "S_key_base" 7 2 7 12 "nspriv.eva") (line (one-way-function (line "number" 7 38 7 44 "nspriv.eva") (line "principal" 7 14 7 23 "nspriv.eva") (line "principal" 7 25 7 34 "nspriv.eva")) 7 13 7 49 "nspriv.eva")) 7 2 7 49 "nspriv.eva") (line (knows (line "S" 8 2 8 3 "nspriv.eva") (line "S_key_base" 8 10 8 20 "nspriv.eva")) 8 2 8 20 "nspriv.eva") (line (alias (line "Kas" 9 8 9 11 "nspriv.eva") (line (apply (line "S_key_base" 9 12 9 22 "nspriv.eva") (line "A" 9 23 9 24 "nspriv.eva") (line "S" 9 26 9 27 "nspriv.eva")) 9 12 9 28 "nspriv.eva")) 9 2 9 28 "nspriv.eva") (line (alias (line "Kbs" 10 8 10 11 "nspriv.eva") (line (apply (line "S_key_base" 10 12 10 22 "nspriv.eva") (line "B" 10 23 10 24 "nspriv.eva") (line "S" 10 26 10 27 "nspriv.eva")) 10 12 10 28 "nspriv.eva")) 10 2 10 28 "nspriv.eva") (line (knows (line "A" 12 2 12 3 "nspriv.eva") (line "A" 12 10 12 11 "nspriv.eva")) 12 2 12 22 "nspriv.eva") (line (knows (line "A" 12 2 12 3 "nspriv.eva") (line "B" 12 13 12 14 "nspriv.eva")) 12 2 12 22 "nspriv.eva") (line (knows (line "A" 12 2 12 3 "nspriv.eva") (line "S" 12 16 12 17 "nspriv.eva")) 12 2 12 22 "nspriv.eva") (line (knows (line "A" 12 2 12 3 "nspriv.eva") (line "Kas" 12 19 12 22 "nspriv.eva")) 12 2 12 22 "nspriv.eva") (line (knows (line "B" 13 2 13 3 "nspriv.eva") (line "Kbs" 13 10 13 13 "nspriv.eva")) 13 2 13 13 "nspriv.eva") (line (knows (line "S" 14 2 14 3 "nspriv.eva") (line "Kas" 14 10 14 13 "nspriv.eva")) 14 2 14 18 "nspriv.eva") (line (knows (line "S" 14 2 14 3 "nspriv.eva") (line "Kbs" 14 15 14 18 "nspriv.eva")) 14 2 14 18 "nspriv.eva") (line (knows (line "A" 15 2 15 3 "nspriv.eva") (line "nudge" 15 10 15 15 "nspriv.eva")) 15 2 15 15 "nspriv.eva") (line (knows (line "B" 16 2 16 3 "nspriv.eva") (line "nudge" 16 10 16 15 "nspriv.eva")) 16 2 16 15 "nspriv.eva")) 1 0 16 15 "") (line (line (block (line (comm "1." (line "A" 19 7 19 8 "nspriv.eva") (line "S" 19 12 19 13 "nspriv.eva") (line (tuple (line "A" 19 16 19 17 "nspriv.eva") (line "B" 19 19 19 20 "nspriv.eva") (line "Na" 19 22 19 24 "nspriv.eva")) 19 16 19 24 "nspriv.eva")) 19 4 19 24 "nspriv.eva") (line (comm "2." (line "S" 20 7 20 8 "nspriv.eva") (line "A" 20 12 20 13 "nspriv.eva") (line (crypt (line (tuple (line "Na" 20 17 20 19 "nspriv.eva") (line "B" 20 21 20 22 "nspriv.eva") (line "Kab" 20 24 20 27 "nspriv.eva") (line (crypt (line (tuple (line "Kab" 20 30 20 33 "nspriv.eva") (line "A" 20 35 20 36 "nspriv.eva")) 20 30 20 36 "nspriv.eva") (line "Kbs" 20 38 20 41 "nspriv.eva") (vanilla)) 20 29 20 41 "nspriv.eva")) 20 17 20 41 "nspriv.eva") (line "Kas" 20 43 20 46 "nspriv.eva") (vanilla)) 20 16 20 46 "nspriv.eva")) 20 4 20 46 "nspriv.eva") (line (comm "3." (line "A" 21 7 21 8 "nspriv.eva") (line "B" 21 12 21 13 "nspriv.eva") (line (crypt (line (tuple (line "Kab" 21 17 21 20 "nspriv.eva") (line "A" 21 22 21 23 "nspriv.eva")) 21 17 21 23 "nspriv.eva") (line "Kbs" 21 25 21 28 "nspriv.eva") (vanilla)) 21 16 21 28 "nspriv.eva")) 21 4 21 28 "nspriv.eva") (line (comm "4." (line "B" 22 7 22 8 "nspriv.eva") (line "A" 22 12 22 13 "nspriv.eva") (line (crypt (line "Nb" 22 17 22 19 "nspriv.eva") (line "Kab" 22 21 22 24 "nspriv.eva") (vanilla)) 22 16 22 24 "nspriv.eva")) 22 4 22 24 "nspriv.eva") (line (comm "5." (line "A" 23 7 23 8 "nspriv.eva") (line "B" 23 12 23 13 "nspriv.eva") (line (crypt (line (apply (line "nudge" 23 17 23 22 "nspriv.eva") (line "Nb" 23 24 23 26 "nspriv.eva")) 23 17 23 27 "nspriv.eva") (line "Kab" 23 29 23 32 "nspriv.eva") (vanilla)) 23 16 23 32 "nspriv.eva")) 23 4 23 32 "nspriv.eva")) 18 2 24 3 "nspriv.eva") 18 2 24 3 "nspriv.eva") (line (sessions) 24 2 24 3 "") (line (assume) 24 3 24 3 "") (line (claim) 24 3 24 3 "")) 1 0 24 3 "nspriv.eva")