A Machine-Checked Formalization of the Generic Model and the Random Oracle Model