A Machine-Checked Formalization of the Generic Model and the Random Oracle Model. - Gilles Barthe; Jan Cederquist; Sabrina Tarento (IJCAR, 2004)

A Machine-Checked Formalization of the Random Oracle Model. - Gilles Barthe; Sabrina Tarento (TYPES, 2004)

Machine-Checked Security Proofs of Cryptographic Signature Schemes. - Sabrina Tarento (ESORICS, 2005)