Applying Cryptography’s Real/Ideal Paradigm to PL Security


The Real/Ideal Paradigm is the standard approach for defining security in theoretical cryptography. In this paradigm, the real and ideal worlds are parameterized by an adversary with certain powers of observation or corruption. The real world is a model of an actual protocol/system. The ideal world consists of an ideal functionality with the same API as the real world, but which is connected with a simulator whose job is to try to convince the adversary it is interacting with the real world, but where the simulator must work with the limited information leaked to it by the ideal functionality. If the adversary can only tell the difference between the real and ideal worlds with negligible probability, we say the real world is secure.

Beginning with a paper I presented at PLAS'14, I’ve been arguing in favor of using the real/ideal paradigm for defining security in a programming languages context, even when systems are entirely non-probabilistic. E.g., even though a system might be implemented using information flow control, its definition of security could be given using the real/ideal paradigm. I will illustrate this approach using the two party game Battleship, giving a definition of when one player is secure against a possibly malicious opponent, and showing two secure implementations, one using information flow control (Haskell/LIO), and one using access control in Concurrent ML.

Nov 23, 2022 10:30 AM — 11:30 AM
Live talk in EDIT 8103

Alley Stoughton is a research professor at Boston University. She earned her doctorate in computer science from University of Edinburgh in 1987, and has a background in programming language semantics and functional programming. But in recent years her focus has been on security, mainly using the EasyCrypt proof assistant to prove the security of cryptographic protocols.