I'm currently working on a proof in the Random Oracle model, and could not find the formal argument on why the random oracle is one-way (i.e. for an Oracle $O$, it is easy to calculate $x=O(n)$, but not efficiently possible to compute $n = O^{-1}(x)$).
Now, I know that the random oracle has that property, and it is intuitively obvious why (as the output is randomly chosen, it is independent from the input and does not contain any information about it). However, as it is not part of the formal specification of a random oracle as per Bellare and Rogaway (as far as I know), I'd like to know how you would formally prove it, based only on the formal specification of a random oracle.