### Abstract

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 paper, 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.

Original language | English (US) |
---|---|

Title of host publication | PLDI 2019 - Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation |

Editors | Kathryn S. McKinley, Kathleen Fisher |

Publisher | Association for Computing Machinery |

Pages | 640-654 |

Number of pages | 15 |

ISBN (Electronic) | 9781450367127 |

DOIs | |

State | Published - Jun 8 2019 |

Event | 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019 - Phoenix, United States Duration: Jun 22 2019 → Jun 26 2019 |

### Publication series

Name | Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) |
---|

### Conference

Conference | 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019 |
---|---|

Country | United States |

City | Phoenix |

Period | 6/22/19 → 6/26/19 |

### Fingerprint

### Keywords

- Process calculus
- Provable security
- Type systems
- Universal composability

### ASJC Scopus subject areas

- Software

### Cite this

*PLDI 2019 - Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation*(pp. 640-654). (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)). Association for Computing Machinery. https://doi.org/10.1145/3314221.3314607

**ILC : A calculus for composable, computational cryptography.** / Liao, Kevin; Hammer, Matthew A.; Miller, Andrew.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

*PLDI 2019 - Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation.*Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Association for Computing Machinery, pp. 640-654, 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, United States, 6/22/19. https://doi.org/10.1145/3314221.3314607

}

TY - GEN

T1 - ILC

T2 - A calculus for composable, computational cryptography

AU - Liao, Kevin

AU - Hammer, Matthew A.

AU - Miller, Andrew

PY - 2019/6/8

Y1 - 2019/6/8

N2 - 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 paper, 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.

AB - 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 paper, 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.

KW - Process calculus

KW - Provable security

KW - Type systems

KW - Universal composability

UR - http://www.scopus.com/inward/record.url?scp=85067645049&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85067645049&partnerID=8YFLogxK

U2 - 10.1145/3314221.3314607

DO - 10.1145/3314221.3314607

M3 - Conference contribution

AN - SCOPUS:85067645049

T3 - Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)

SP - 640

EP - 654

BT - PLDI 2019 - Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation

A2 - McKinley, Kathryn S.

A2 - Fisher, Kathleen

PB - Association for Computing Machinery

ER -