Formal definition of "explicit" algorithm? A long time ago, I read that the definition of "cryptographic hash function" is "collision-resistant one-way function". (A similar definition shows up in the FIPS standards for SHA-1 etc.)

But this is not a sufficient property for many of the modern uses of cryptographic hash functions, like Bitcoin. What they really want is for hash functions to act like a "random oracle".

Of course, no deterministic function can be random.

I am taking Dan Boneh's Coursera cryptography class. Most cryptographic primitives we cover assume some sort of secret, and then the definition of "secure" involves probabilities over the space of possible secrets. For example, a secure RNG has a secret seed, and if I (a) pick a seed at random and generate a long pseudo-random string, and (b) pick a long truly random string, then no efficient algorithm should be able to tell them apart with noticeably better than even odds. (With those odds computed over the space of keys and truly random strings.)

In the intro lecture to hash functions (see here or here if you do not want to register), Boneh gives the following definition of "collision resistant" hash function:


  A function $H$ is collision resistant if for all (explicit) "effective"
  algorithms $A$, $$\mathrm{ADV}_\mathrm{CR}[A,H] = \mathrm{Pr}[A\ \mathrm{outputs\ a\ collision\ for\ } H]$$ is "negligible".


Now, obviously, a very simple algorithm exists to output a collision for, say, SHA-256; we just do not know what that algorithm is. And there is no indication in this definition of the space over which we are calculating the probability.

So my question is twofold:


What is the formal definition of "explicit" algorithm? (I assume this is meant to rule out algorithms that we know exist but cannot explicitly describe.)
Over what space is the probability being computed in Boneh's definition?


To clarify: I am aware of the dictionary definition of "explicit". I am asking for a formal definition. I know how to translate a statement like "There exists an algorithm such that..." into (say) the language of ZF set theory, at least in principle. I do not know how to translate "...but nobody knows what it is" into any formal language at all. So I am wondering how a mathematician would think about this sort of definition.
What Dan Boneh says is not a formal definition as you want it. Let me quote Rogaway on this:


  In cryptographic practice, a collision-resistant hash-function (also
  called a collision-free or collision-intractable hash-function) maps
  arbitrary-length strings to fixed-length ones; it’s an algorithm
  $H:\{0,1\}^*\rightarrow \{0,1\}^n$  for some fixed  $n$ (we
  momentarily assume a message space of $\{0,1\}^*$. But in
  cryptographic theory, a collision-resistant hash-function is always
  keyed; now $H:\,\mathcal{K}\times\{0,1\}^*\rightarrow \{0,1\}^n$,
  where each $K\in\mathcal{K}$ names a function $H_K = H(K,\cdot)$ (This
  formalization assumes a concrete-security framework.) In this case $H$
  can be thought of as a collection or family of hash functions
  $\mathcal{H} = \{H_K:\:K\in\mathcal{K}\}$, each key (or index)
  $K\in\mathcal{K}$ naming one. (Note that we call $K$ a key but it is
  not secret; it will be chosen from $\mathcal{K}$ and then made
  public.)
  
  Why should theoretical treatments be keyed when practical
  constructions are not? The traditional answer is that a rigorous
  treatment of collision resistance for unkeyed hash-functions just
  doesn’t work. At issue is the fact that for any function
  $H:\{0,1\}^*\rightarrow \{0,1\}^n$ there is always a simple and
  compact algorithm that outputs a collision: the algorithm that has one
  “hardwired in.” That is, by the pigeonhole principle there must be
  distinct strings $X$ and $X_0$ of length at most $n$ such that $H(X) = H(X_0)$, and so there’s a short and fast program that outputs such an
  $(X, X_0)$. The difficulty, of course, is that us human beings might
  not know any such pair $(X, X_0)$, so no one can actually write the
  program down.
  
  Because of the above, what is meant when someone says that a hash
  function $H:\{0,1\}^*\rightarrow \{0,1\}^n$ is collision resistant
  cannot be that there is no efficient adversary that outputs a
  collision in $H$. What is meant is that there is no efficient
  algorithm known to man that outputs a collision in $H$. But such a
  statement would seem to be unformalizable — outside the realm of
  mathematics. One cannot hope to construct a meaningful theory based on
  what humankind currently does or does not know. Regarding a hash
  function like SHA-1 as a random element from a family of hash
  functions has been the traditional way out of this quandary.


Rogaway then demonstrates that even though it is not possible to formally define the collision resistance, it is possible to formally define the requirement for a collision resistant hash function by a higher-level protocol or a construction. This is done by a reduction that shows that if someone can break the protocol in a certain way, then he is able to find a collision for the underlying hash function. This allows to consider the protocol secure as long as collisions have not been explicitly found.