“system with formal proof” vs “system without formal proof but extensively tested by cryptographers in real-world settings”
Well this is saying formal proof is bad because testing is better. I think in this situation it depends on exactly what was proved, and how extensive the testing is.
One time pads always work, so long as no one else knows the key. This is the best you can ask for from any symmetric encryption. The only advantage AES gives you is a key that is smaller than the message. (Which is more helpful for saving bandwidth than for security.) If you were sending out a drone, you could give it a hard drive full of random nonsense, keeping a similar hard drive in your base, and encrypt everything with a one time pad. Idealy the drone should delete the one time pad as it uses it. But if you want to send more than a hard drive full of data, suddenly you can’t without breaking all the security. AES can use a small key to send lots of data.
Well this is saying formal proof is bad because testing is better. I think in this situation it depends on exactly what was proved, and how extensive the testing is.
One time pads always work, so long as no one else knows the key. This is the best you can ask for from any symmetric encryption. The only advantage AES gives you is a key that is smaller than the message. (Which is more helpful for saving bandwidth than for security.) If you were sending out a drone, you could give it a hard drive full of random nonsense, keeping a similar hard drive in your base, and encrypt everything with a one time pad. Idealy the drone should delete the one time pad as it uses it. But if you want to send more than a hard drive full of data, suddenly you can’t without breaking all the security. AES can use a small key to send lots of data.