2026-09-19T19:43:00Z https://www.ideals.illinois.edu/oai-pmh

oai:www.ideals.illinois.edu:2142/106266 2023-07-11 col_2142_5131 col_2142_10761 com_2142_5130 com_2142_10755 com_2142_234

Miller, Andrew Liao, Kevin 2020-03-02T21:58:29Z 2020-03-02T21:58:29Z 2019-12-09 2019-12 The universal composability (UC) framework is the established standard for analyzing cryptographic protocols in a modular way, such that security is preserved under concurrent composition with arbitrary other protocols. However, although UC is widely used for on-paper proofs, prior attempts at systemizing it have fallen short, either by using a symbolic model (thereby ruling out computational reduction proofs), or by limiting its expressiveness. In this thesis, we lay the groundwork for building a concrete, executable implementation of the UC framework. Our main contribution is a process calculus, dubbed the Interactive Lambda Calculus (ILC). ILC faithfully captures the computational model underlying UC—interactive Turing machines (ITMs)—by adapting ITMs to a subset of the π-calculus through an affine typing discipline. In other words, well-typed ILC programs are expressible as ITMs. In turn, ILC’s strong confluence property enables reasoning about cryptographic security reductions. We use ILC to develop a simplified implementation of UC called SaUCy. Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2020-02-28 without embargo terms The student, Kevin Liao, accepted the attached license on 2019-12-07 at 17:57. The student, Kevin Liao, submitted this Thesis for approval on 2019-12-07 at 18:01. This Thesis was approved for publication on 2019-12-09 at 09:33. DSpace SAF Submission Ingestion Package generated from Vireo submission #14751 on 2020-02-28 at 17:16:17 Made available in DSpace on 2020-03-02T21:58:29Z (GMT). No. of bitstreams: 2 LIAO-THESIS-2019.pdf: 1588290 bytes, checksum: 972109e343af6cc1f24851cf6edb7f94 (MD5) LICENSE.txt: 4207 bytes, checksum: ac19ebe344d957af93249c508b259a66 (MD5) Previous issue date: 2019-12-09 application/pdf http://hdl.handle.net/2142/106266 en Copyright 2019 Kevin Liao universal composability affine types process calculus A calculus for composable, computational cryptography text text Computer Science Computer Science University of Illinois at Urbana-Champaign Thesis M.S.