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