Towards mechanized correctness proofs for cryptographic algorithms

M. Bellare, P. Rogaway, The game-playing technique, 2004, At http://www.cs.ucdavis.edu/~rogaway/papers/games.html Boneh, 1998, The decisional diffie-hellman problem, 1998, vol. 1423 Boneh, 2001, Identity-based encryption from the weil pairing, 213 Chadha, 2007, Reasoning about probabilistic sequential programs, Theoret. Comput. Sci., 379, 142, 10.1016/j.tcs.2007.02.040 Corin, 2006, A probabilistic hoare-style logic for game-based cryptographic proofs, vol. 4052, 252 ElGamal, 1985, A public-key cryptosystem and a signature scheme based on discrete logarithms, IEEE Transactions on Information Theory, IT-31, 469, 10.1109/TIT.1985.1057074 D. Galindo, Boneh-franklin identity based encryption revisited, in: ICALP, 2005, pp. 791–802 S. Halevi, A plausible approach to computer-aided cryptographic proofs, 2005, At http://eprint.iacr.org/2005/181/ den Hartog, 2002, Verifying probabilistic programs using a Hoare like logic, International Journal of Foundations of Computer Science, 13, 315, 10.1142/S012905410200114X Hoare, 1969, An axiomatic basis for computer programming, Communications of the ACM, 12, 576, 10.1145/363235.363259 Impagliazzo, 2006, Logics for reasoning about cryptographic constructions, Journal of Computer and Systems Sciences, 72, 10.1016/j.jcss.2005.06.008 Morgan, 1996, Probabilistic predicate transformers, ACM Transactions on Programming Languages and Systems, 18, 325, 10.1145/229542.229547 V. Shoup, Sequences of games: A tool for taming complexity in security proofs, May 2005, At http://www.shoup.net/papers/games.pdf