--- layout: fc_discuss_archives title: Message 55 from Frama-C-discuss on December 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] how to abstract the loop



   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>