%PDF-1.4 % 4 0 obj << /S /GoTo /D (section.1) >> endobj 7 0 obj (Introduction) endobj 8 0 obj << /S /GoTo /D (subsection.1.1) >> endobj 11 0 obj (Problem Context) endobj 12 0 obj << /S /GoTo /D (subsection.1.2) >> endobj 15 0 obj (Our Solution) endobj 16 0 obj << /S /GoTo /D (subsection.1.3) >> endobj 19 0 obj (Contributions) endobj 20 0 obj << /S /GoTo /D (subsection.1.4) >> endobj 23 0 obj (Structure) endobj 24 0 obj << /S /GoTo /D (section.2) >> endobj 27 0 obj (Background) endobj 28 0 obj << /S /GoTo /D (subsection.2.1) >> endobj 31 0 obj (CryptHOL) endobj 32 0 obj << /S /GoTo /D (subsection.2.2) >> endobj 35 0 obj (Constructive Cryptography) endobj 36 0 obj << /S /GoTo /D (section.3) >> endobj 39 0 obj (Running example) endobj 40 0 obj << /S /GoTo /D (section.4) >> endobj 43 0 obj (Formalizing Resources and Converters) endobj 44 0 obj << /S /GoTo /D (subsection.4.1) >> endobj 47 0 obj (Resources) endobj 48 0 obj << /S /GoTo /D (subsubsection.4.1.1) >> endobj 51 0 obj (Defining Concrete Resources) endobj 52 0 obj << /S /GoTo /D (subsubsection.4.1.2) >> endobj 55 0 obj (A type system for interfaces) endobj 56 0 obj << /S /GoTo /D (subsubsection.4.1.3) >> endobj 59 0 obj (Parallel composition) endobj 60 0 obj << /S /GoTo /D (subsection.4.2) >> endobj 63 0 obj (Converters) endobj 64 0 obj << /S /GoTo /D (subsection.4.3) >> endobj 67 0 obj (Constructing Systems) endobj 68 0 obj << /S /GoTo /D (section.5) >> endobj 71 0 obj (Equivalence of Resources) endobj 72 0 obj << /S /GoTo /D (section.6) >> endobj 75 0 obj (Secure Constructions) endobj 76 0 obj << /S /GoTo /D (subsection.6.1) >> endobj 79 0 obj (Distinguishers) endobj 80 0 obj << /S /GoTo /D (subsection.6.2) >> endobj 83 0 obj (Security model) endobj 84 0 obj << /S /GoTo /D (subsection.6.3) >> endobj 87 0 obj (Composability) endobj 88 0 obj << /S /GoTo /D (section.7) >> endobj 91 0 obj (Wrapping-up the Running Example) endobj 92 0 obj << /S /GoTo /D (section.8) >> endobj 95 0 obj (Discussion and Related Work) endobj 96 0 obj << /S /GoTo /D (section.9) >> endobj 99 0 obj (Conclusion and Future Work) endobj 100 0 obj << /S /GoTo /D (section*.15) >> endobj 103 0 obj (References) endobj 104 0 obj << /S /GoTo /D (section*.16) >> endobj 107 0 obj (Appendix) endobj 108 0 obj << /S /GoTo /D (subsection.Appendix.A.1) >> endobj 111 0 obj (Guide to the source theory files) endobj 112 0 obj << /S /GoTo /D [113 0 R /Fit] >> endobj 142 0 obj << /Length 4787 /Filter /FlateDecode >> stream xZK㶵Whv GMcO<)N*^)v5)_ER]un$