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.
Lago, U.D., Galal, Z., Giusti, G. (2024). On Computational Indistinguishability and Logical Relations. 152 BEACH ROAD, #21-01/04 GATEWAY EAST, SINGAPORE, 189721, SINGAPORE : Springer Science and Business Media Deutschland GmbH [10.1007/978-981-97-8943-6_12].
On Computational Indistinguishability and Logical Relations
Lago, Ugo Dal
;Galal, Zeinab;
2024
Abstract
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
