(line (spec (line (declare (line (type (line "S" 4 8 4 9 "nspub1.eva") (line "principal" 4 12 4 21 "nspub1.eva")) 4 2 4 21 "nspub1.eva") (line (type (line "B" 4 5 4 6 "nspub1.eva") (line "principal" 4 12 4 21 "nspub1.eva")) 4 2 4 21 "nspub1.eva") (line (type (line "A" 4 2 4 3 "nspub1.eva") (line "principal" 4 12 4 21 "nspub1.eva")) 4 2 4 21 "nspub1.eva") (line (type (line "Nb" 5 6 5 8 "nspub1.eva") (line "number" 5 11 5 17 "nspub1.eva")) 5 2 5 17 "nspub1.eva") (line (type (line "Na" 5 2 5 4 "nspub1.eva") (line "number" 5 11 5 17 "nspub1.eva")) 5 2 5 17 "nspub1.eva") (line (keypair (vanilla) (line "PK" 6 10 6 12 "nspub1.eva") (line "SK" 6 14 6 16 "nspub1.eva") (line (one-way-function (line "number" 6 2 6 9 "nspub1.eva") (line "principal" 6 18 6 27 "nspub1.eva")) 6 2 6 28 "nspub1.eva")) 6 2 6 16 "nspub1.eva") (line (knows (line "A" 7 2 7 3 "nspub1.eva") (line "A" 7 10 7 11 "nspub1.eva")) 7 2 7 35 "nspub1.eva") (line (knows (line "A" 7 2 7 3 "nspub1.eva") (line "B" 7 13 7 14 "nspub1.eva")) 7 2 7 35 "nspub1.eva") (line (knows (line "A" 7 2 7 3 "nspub1.eva") (line (apply (line "SK" 7 16 7 18 "nspub1.eva") (line "A" 7 19 7 20 "nspub1.eva")) 7 16 7 21 "nspub1.eva")) 7 2 7 35 "nspub1.eva") (line (knows (line "A" 7 2 7 3 "nspub1.eva") (line (apply (line "PK" 7 23 7 25 "nspub1.eva") (line "B" 7 26 7 27 "nspub1.eva")) 7 23 7 28 "nspub1.eva")) 7 2 7 35 "nspub1.eva") (line (knows (line "A" 7 2 7 3 "nspub1.eva") (line (apply (line "PK" 7 30 7 32 "nspub1.eva") (line "S" 7 33 7 34 "nspub1.eva")) 7 30 7 35 "nspub1.eva")) 7 2 7 35 "nspub1.eva") (line (knows (line "B" 8 2 8 3 "nspub1.eva") (line "B" 8 10 8 11 "nspub1.eva")) 8 2 8 25 "nspub1.eva") (line (knows (line "B" 8 2 8 3 "nspub1.eva") (line (apply (line "SK" 8 13 8 15 "nspub1.eva") (line "B" 8 16 8 17 "nspub1.eva")) 8 13 8 18 "nspub1.eva")) 8 2 8 25 "nspub1.eva") (line (knows (line "B" 8 2 8 3 "nspub1.eva") (line (apply (line "PK" 8 20 8 22 "nspub1.eva") (line "S" 8 23 8 24 "nspub1.eva")) 8 20 8 25 "nspub1.eva")) 8 2 8 25 "nspub1.eva") (line (knows (line "S" 9 2 9 3 "nspub1.eva") (line (apply (line "PK" 9 10 9 12 "nspub1.eva") (line "A" 9 13 9 14 "nspub1.eva")) 9 10 9 15 "nspub1.eva")) 9 2 9 29 "nspub1.eva") (line (knows (line "S" 9 2 9 3 "nspub1.eva") (line (apply (line "PK" 9 17 9 19 "nspub1.eva") (line "B" 9 20 9 21 "nspub1.eva")) 9 17 9 22 "nspub1.eva")) 9 2 9 29 "nspub1.eva") (line (knows (line "S" 9 2 9 3 "nspub1.eva") (line (apply (line "SK" 9 24 9 26 "nspub1.eva") (line "S" 9 27 9 28 "nspub1.eva")) 9 24 9 29 "nspub1.eva")) 9 2 9 29 "nspub1.eva") (line (type (line "I" 12 11 12 12 "nspub1.eva") (line "principal" 12 15 12 24 "nspub1.eva")) 12 2 12 24 "nspub1.eva") (line (type (line "s" 12 8 12 9 "nspub1.eva") (line "principal" 12 15 12 24 "nspub1.eva")) 12 2 12 24 "nspub1.eva") (line (type (line "b" 12 5 12 6 "nspub1.eva") (line "principal" 12 15 12 24 "nspub1.eva")) 12 2 12 24 "nspub1.eva") (line (type (line "a" 12 2 12 3 "nspub1.eva") (line "principal" 12 15 12 24 "nspub1.eva")) 12 2 12 24 "nspub1.eva")) 3 0 12 24 "") (line (line (block (line (comm "1." (line "A" 15 7 15 8 "nspub1.eva") (line "S" 15 12 15 13 "nspub1.eva") (line (tuple (line "A" 15 16 15 17 "nspub1.eva") (line "B" 15 19 15 20 "nspub1.eva")) 15 16 15 20 "nspub1.eva")) 15 4 15 20 "nspub1.eva") (line (comm "2." (line "S" 16 7 16 8 "nspub1.eva") (line "A" 16 12 16 13 "nspub1.eva") (line (crypt (line (tuple (line (apply (line "PK" 16 17 16 19 "nspub1.eva") (line "B" 16 21 16 22 "nspub1.eva")) 16 17 16 23 "nspub1.eva") (line "B" 16 25 16 26 "nspub1.eva")) 16 17 16 26 "nspub1.eva") (line (apply (line "SK" 16 29 16 31 "nspub1.eva") (line "S" 16 33 16 34 "nspub1.eva")) 16 29 16 35 "nspub1.eva") (vanilla)) 16 16 16 36 "nspub1.eva")) 16 4 16 36 "nspub1.eva") (line (comm "3." (line "A" 17 7 17 8 "nspub1.eva") (line "B" 17 12 17 13 "nspub1.eva") (line (crypt (line (tuple (line "Na" 17 17 17 19 "nspub1.eva") (line "A" 17 21 17 22 "nspub1.eva")) 17 17 17 22 "nspub1.eva") (line (apply (line "PK" 17 25 17 27 "nspub1.eva") (line "B" 17 28 17 29 "nspub1.eva")) 17 25 17 30 "nspub1.eva") (vanilla)) 17 16 17 31 "nspub1.eva")) 17 4 17 31 "nspub1.eva") (line (comm "4." (line "B" 18 7 18 8 "nspub1.eva") (line "S" 18 12 18 13 "nspub1.eva") (line (tuple (line "B" 18 16 18 17 "nspub1.eva") (line "A" 18 19 18 20 "nspub1.eva")) 18 16 18 20 "nspub1.eva")) 18 4 18 20 "nspub1.eva") (line (comm "5." (line "S" 19 7 19 8 "nspub1.eva") (line "B" 19 12 19 13 "nspub1.eva") (line (crypt (line (tuple (line (apply (line "PK" 19 17 19 19 "nspub1.eva") (line "A" 19 21 19 22 "nspub1.eva")) 19 17 19 23 "nspub1.eva") (line "A" 19 25 19 26 "nspub1.eva")) 19 17 19 26 "nspub1.eva") (line (apply (line "SK" 19 29 19 31 "nspub1.eva") (line "S" 19 33 19 34 "nspub1.eva")) 19 29 19 35 "nspub1.eva") (vanilla)) 19 16 19 36 "nspub1.eva")) 19 4 19 36 "nspub1.eva") (line (comm "6." (line "B" 20 7 20 8 "nspub1.eva") (line "A" 20 12 20 13 "nspub1.eva") (line (crypt (line (tuple (line "Na" 20 17 20 19 "nspub1.eva") (line "Nb" 20 21 20 23 "nspub1.eva")) 20 17 20 23 "nspub1.eva") (line (apply (line "PK" 20 26 20 28 "nspub1.eva") (line "A" 20 30 20 31 "nspub1.eva")) 20 26 20 32 "nspub1.eva") (vanilla)) 20 16 20 33 "nspub1.eva")) 20 4 20 33 "nspub1.eva") (line (comm "7." (line "A" 21 7 21 8 "nspub1.eva") (line "B" 21 12 21 13 "nspub1.eva") (line (crypt (line "Nb" 21 17 21 19 "nspub1.eva") (line (apply (line "PK" 21 22 21 24 "nspub1.eva") (line "B" 21 26 21 27 "nspub1.eva")) 21 22 21 28 "nspub1.eva") (vanilla)) 21 16 21 29 "nspub1.eva")) 21 4 21 29 "nspub1.eva")) 14 2 22 3 "nspub1.eva") 14 2 22 3 "nspub1.eva") (line (sessions (line (session "'a." (line (principals-except) 21 12 21 13 "nspub1.eva") (line (bind (line "A" 23 10 23 11 "nspub1.eva") (line "a" 23 12 23 13 "nspub1.eva")) 23 10 23 13 "nspub1.eva") (line (bind (line "B" 23 15 23 16 "nspub1.eva") (line "I" 23 17 23 18 "nspub1.eva")) 23 15 23 18 "nspub1.eva") (line (bind (line "S" 23 20 23 21 "nspub1.eva") (line "s" 23 22 23 23 "nspub1.eva")) 23 20 23 23 "nspub1.eva")) 23 2 23 23 "nspub1.eva") (line (session "'b." (line (principals-except) 23 10 23 9 "") (line (bind (line "A" 24 10 24 11 "nspub1.eva") (line "a" 24 12 24 13 "nspub1.eva")) 24 10 24 13 "nspub1.eva") (line (bind (line "B" 24 15 24 16 "nspub1.eva") (line "b" 24 17 24 18 "nspub1.eva")) 24 15 24 18 "nspub1.eva") (line (bind (line "S" 24 20 24 21 "nspub1.eva") (line "s" 24 22 24 23 "nspub1.eva")) 24 20 24 23 "nspub1.eva")) 24 2 24 23 "nspub1.eva")) 22 2 24 23 "") (line (assume) 26 2 24 23 "") (line (claim (line (A (line (G (line (implies (line (at "s2." (line "B" 26 19 26 20 "nspub1.eva") "end.") 26 16 26 26 "nspub1.eva") (line (and (line (at "s2." (line "A" 26 34 26 35 "nspub1.eva") "end.") 26 31 26 41 "nspub1.eva") (line (prop (line "equals" 26 45 26 51 "nspub1.eva") (line (locate "s2." (line "A" 26 62 26 63 "nspub1.eva") (line "Na" 26 54 26 56 "nspub1.eva")) 26 54 26 63 "nspub1.eva") (line (locate "s2." (line "B" 26 76 26 77 "nspub1.eva") (line "Nb" 26 67 26 69 "nspub1.eva")) 26 67 26 77 "nspub1.eva")) 26 45 26 79 "nspub1.eva")) 26 31 26 79 "nspub1.eva")) 26 16 26 79 "nspub1.eva")) 26 10 26 80 "nspub1.eva")) 26 8 26 80 "nspub1.eva")) 26 2 26 80 "nspub1.eva")) 3 0 24 23 "nspub1.eva")