Provably secure block ciphers

Question

I have read the paper by Anderson and Biham [0] describing the ciphers Bear and Lion, which combine a PRG and a hash function (each cipher does that in a different way). the authors proved that a key recovery attack on the ciphers would imply breaking the PRG and hash function used. I also read the paper by Morin [1] in which he shows a man-in-the-middle attack on Bear and Lion, and also proposes a new cipher (Aardvark) of the same kind, immune to such attack.

Was there any attack on Aardvark?

And are there other block ciphers with proof of security?

The references are the following (sorry, I couldn't find exactly the publication years and conference names)

[0] Ross Anderson and Eli Biham. Two Practical and Provably Secure Block Ciphers: BEAR and LION.

[1] Pat Morin (1996). Provably Secure and Efficient Block Ciphers.

Answer 1

Construction of provably-secure block ciphers are considered in the following papers:

• Pseudo-Random Permutation Generators and Cryptographic Composition by Luby & Rackoff. Full version of this paper can be found in How to Construct Pseudorandom Permutations from Pseudorandom Functions.
• On the Construction of Pseudo-Random Permutations: Luby-Rackoff Revisited by Naor & Reingold. This is in fact a revised version of the above ideas by Luby & Rackoff. Full version can be found in here.

The construct by Pat Morin and many others are reviewed in Building Secure Block Ciphers on Generic Attacks Assumptions.