2024/08/30 by Ugo Dal Lago, Lago, Ugo Dal, Zeinab Galal +3 · 1 citation
Computer Science · #Advanced Algebra and Logic #Cryptography and Security (cs.CR) #FOS: Computer and information sciences #Logic, Reasoning, and Knowledge #Programming Languages (cs.PL)
paper · pdf · doi:10.48550/arxiv.2408.17340
openalex publication_date 2024/08/30 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/01
A λ-calculus is introduced in which all programs can be evaluated in probabilistic polynomial time and in which there is sufficient structure to represent sequential cryptographic constructions and adversaries for them, even when the latter are oracle-based. A notion of observational equivalence capturing computational indistinguishability and a class of approximate logical relations are then presented, showing that the latter represent a sound proof technique for the former. The work concludes with the presentation of an example of a security proof in which the encryption scheme induced by a pseudorandom function is proven secure against active adversaries in a purely equational style.