Probabilistic Functions and Cryptographic Oracles in Higher Order Logic