Probabilistic Functions and Cryptographic Oracles in Higher Order Logic

8 years 18 days ago

Download www.infsec.ethz.ch

This paper presents a shallow embedding of a probabilistic functional programming language in higher order logic. The language features monadic sequencing, recursion, random sampling, failures and failure handling, and black-box access to oracles. Oracles are probabilistic functions which maintain hidden state between diﬀerent invocations. To that end, we propose generative probabilistic systems as the semantic domain in which the operators of the language are deﬁned. We prove that these operators are parametric and derive a relational program logic for reasoning about programs from parametricity. Several examples demonstrate that our language is suitable for conducting cryptographic proofs.

Andreas Lochbihler

Real-time Traffic