--- layout: fc_discuss_archives title: Message 55 from Frama-C-discuss on December 2011 ---
I thought the prover could not understand the iteration without loop invariants ,no matter which properties I want to verify. If without loop invariants, some corresponding VCs would not be discharged, right? I am using frama-c/jessie/why to verify the safety of AES. After that , I plan to verify information flow security. However , I have no idea about how to formalize this property. But the loop invariant is a must in my mind. > It does not simplify (or Rijndael would be a very bad cipher indeed). Do you mean Frama-c is not suitable to verify the properties of Rijndael, for its source code is complicated? I want to verify the security of some cryptographic software with frama-c/jessie/why. I have seen someone verified RC4 with frama-c/jessie/why. Rijndael is popular and I want to try , but it seems to be not easy . Would you give me some advice about some other cryptographic software easier to be verified with frama-c/jessie/why. Thanks! -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20111229/4cf0b674/attachment.htm>