How to Specify and How to Prove Correctness of Secure Routing Protocols for MANET