(line (spec (line (declare (line (type (line "aa" 2 1 2 3 "kpf6.eva") (line "asym_algo" 2 17 2 26 "kpf6.eva")) 2 1 2 26 "kpf6.eva") (line (type (line "S" 3 7 3 8 "kpf6.eva") (line "principal" 3 17 3 26 "kpf6.eva")) 3 1 3 26 "kpf6.eva") (line (type (line "B" 3 4 3 5 "kpf6.eva") (line "principal" 3 17 3 26 "kpf6.eva")) 3 1 3 26 "kpf6.eva") (line (type (line "A" 3 1 3 2 "kpf6.eva") (line "principal" 3 17 3 26 "kpf6.eva")) 3 1 3 26 "kpf6.eva") (line (keypair (line "aa" 4 9 4 11 "kpf6.eva") (line "PK" 4 12 4 14 "kpf6.eva") (line "SK" 4 16 4 18 "kpf6.eva") (line (one-way-function (line "number" 4 1 4 8 "kpf6.eva") (line "principal" 4 20 4 29 "kpf6.eva")) 4 1 4 30 "kpf6.eva")) 4 1 4 18 "kpf6.eva") (line (knows (line "A" 5 1 5 2 "kpf6.eva") (line "A" 5 9 5 10 "kpf6.eva")) 5 1 5 41 "kpf6.eva") (line (knows (line "A" 5 1 5 2 "kpf6.eva") (line (apply (line "PK" 5 12 5 14 "kpf6.eva") (line "A" 5 15 5 16 "kpf6.eva")) 5 12 5 17 "kpf6.eva")) 5 1 5 41 "kpf6.eva") (line (knows (line "A" 5 1 5 2 "kpf6.eva") (line (apply (line "SK" 5 19 5 21 "kpf6.eva") (line "A" 5 22 5 23 "kpf6.eva")) 5 19 5 24 "kpf6.eva")) 5 1 5 41 "kpf6.eva") (line (knows (line "A" 5 1 5 2 "kpf6.eva") (line "B" 5 26 5 27 "kpf6.eva")) 5 1 5 41 "kpf6.eva") (line (knows (line "A" 5 1 5 2 "kpf6.eva") (line "S" 5 29 5 30 "kpf6.eva")) 5 1 5 41 "kpf6.eva") (line (knows (line "A" 5 1 5 2 "kpf6.eva") (line (apply (line "PK" 5 32 5 34 "kpf6.eva") (line "S" 5 35 5 36 "kpf6.eva")) 5 32 5 37 "kpf6.eva")) 5 1 5 41 "kpf6.eva") (line (knows (line "A" 5 1 5 2 "kpf6.eva") (line "aa" 5 39 5 41 "kpf6.eva")) 5 1 5 41 "kpf6.eva") (line (knows (line "S" 6 1 6 2 "kpf6.eva") (line "S" 6 9 6 10 "kpf6.eva")) 6 1 6 25 "kpf6.eva") (line (knows (line "S" 6 1 6 2 "kpf6.eva") (line (apply (line "SK" 6 12 6 14 "kpf6.eva") (line "S" 6 15 6 16 "kpf6.eva")) 6 12 6 17 "kpf6.eva")) 6 1 6 25 "kpf6.eva") (line (knows (line "S" 6 1 6 2 "kpf6.eva") (line "PK" 6 19 6 21 "kpf6.eva")) 6 1 6 25 "kpf6.eva") (line (knows (line "S" 6 1 6 2 "kpf6.eva") (line "aa" 6 23 6 25 "kpf6.eva")) 6 1 6 25 "kpf6.eva") (line (type (line "s" 7 7 7 8 "kpf6.eva") (line "principal" 7 11 7 20 "kpf6.eva")) 7 1 7 20 "kpf6.eva") (line (type (line "b" 7 4 7 5 "kpf6.eva") (line "principal" 7 11 7 20 "kpf6.eva")) 7 1 7 20 "kpf6.eva") (line (type (line "a" 7 1 7 2 "kpf6.eva") (line "principal" 7 11 7 20 "kpf6.eva")) 7 1 7 20 "kpf6.eva")) 1 0 7 20 "") (line (line (block (line (comm "1." (line "A" 9 5 9 6 "kpf6.eva") (line "S" 9 10 9 11 "kpf6.eva") (line (tuple (line "A" 9 14 9 15 "kpf6.eva") (line "B" 9 17 9 18 "kpf6.eva")) 9 14 9 18 "kpf6.eva")) 9 2 9 18 "kpf6.eva") (line (comm "2." (line "S" 10 5 10 6 "kpf6.eva") (line "A" 10 10 10 11 "kpf6.eva") (line (crypt (line (tuple (line (apply (line "PK" 10 16 10 18 "kpf6.eva") (line "B" 10 19 10 20 "kpf6.eva")) 10 16 10 21 "kpf6.eva") (line "B" 10 23 10 24 "kpf6.eva")) 10 16 10 24 "kpf6.eva") (line (apply (line "SK" 10 27 10 29 "kpf6.eva") (line "S" 10 30 10 31 "kpf6.eva")) 10 27 10 32 "kpf6.eva") (line "aa" 10 33 10 35 "kpf6.eva")) 10 14 10 35 "kpf6.eva")) 10 2 10 35 "kpf6.eva")) 8 1 11 2 "kpf6.eva") 8 1 11 2 "kpf6.eva") (line (sessions (line (session "s." (line (principals-except) 10 10 10 11 "kpf6.eva") (line (bind (line "A" 12 12 12 13 "kpf6.eva") (line "a" 12 14 12 15 "kpf6.eva")) 12 12 12 15 "kpf6.eva") (line (bind (line "B" 12 17 12 18 "kpf6.eva") (line "b" 12 19 12 20 "kpf6.eva")) 12 17 12 20 "kpf6.eva") (line (bind (line "S" 12 22 12 23 "kpf6.eva") (line "s" 12 24 12 25 "kpf6.eva")) 12 22 12 25 "kpf6.eva")) 12 1 12 25 "kpf6.eva")) 11 1 12 25 "") (line (assume) 12 25 12 25 "") (line (claim) 12 25 12 25 "")) 1 0 12 25 "kpf6.eva")