
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Bruno Blanchet, "A Computationally Sound Mechanized Prover for Security Protocols," IEEE Transactions on Dependable and Secure Computing, vol. 5, no. 4, pp. 193207, OctoberDecember, 2008.  
BibTex  x  
@article{ 10.1109/TDSC.2007.1005, author = {Bruno Blanchet}, title = {A Computationally Sound Mechanized Prover for Security Protocols}, journal ={IEEE Transactions on Dependable and Secure Computing}, volume = {5}, number = {4}, issn = {15455971}, year = {2008}, pages = {193207}, doi = {http://doi.ieeecomputersociety.org/10.1109/TDSC.2007.1005}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Dependable and Secure Computing TI  A Computationally Sound Mechanized Prover for Security Protocols IS  4 SN  15455971 SP193 EP207 EPD  193207 A1  Bruno Blanchet, PY  2008 KW  C.2.2.c Protocol verification KW  F.3.1.d Mechanical verification KW  D.2.4.d Formal methods VL  5 JA  IEEE Transactions on Dependable and Secure Computing ER   
[1] M. Abadi and P. Rogaway, “Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption),” J.Cryptology, vol. 15, no. 2, pp. 103127, 2002.
[2] M. Abadi and J. Jürjens, “Formal Eavesdropping and its Computational Interpretation,” Proc. Fourth Int'l Symp. Theoretical Aspects of Computer Software (TACS '01), pp. 8294, Oct. 2001.
[3] M. Backes, B. Pfitzmann, and M. Waidner, “A Composable Cryptographic Library with Nested Operations,” Proc. 10th ACM Conf. Computer and Comm. Security (CCS '03), pp. 220230, Oct. 2003.
[4] J. Herzog, “A Computational Interpretation of DolevYao Adversaries,” Theoretical Computer Science, vol. 340, pp. 5781, June 2005.
[5] D. Micciancio and B. Warinschi, “Completeness Theorems for the AbadiRogaway Logic of Encrypted Expressions,” J. Computer Security, vol. 12, no. 1, pp. 99129, 2004.
[6] D. Micciancio and B. Warinschi, “Soundness of Formal Encryption in the Presence of Active Adversaries,” Proc. First Theory of Cryptography Conf. (TCC '04), pp. 133151, Feb. 2004.
[7] V. Cortier and B. Warinschi, “Computationally Sound Automated Proofs for Security Protocols,” Proc. 14th European Symp. Programming (ESOP '05), pp. 157171, Apr. 2005.
[8] R. Janvier, Y. Lakhnech, and L. Mazaré, “Completing the Picture: Soundness of Formal Encryption in the Presence of Active Adversaries,” Proc. 14th European Symp. Programming (ESOP '05), pp. 172185, Apr. 2005.
[9] M. Baudet, V. Cortier, and S. Kremer, “Computationally Sound Implementations of Equational Theories against Passive Adversaries,” Proc. 32nd Int'l Colloquium Automata, Languages and Programming (ICALP '05), pp. 652663, July 2005.
[10] P. Adão, G. Bana, J. Herzog, and A. Scedrov, “Soundness of Formal Encryption in the Presence of KeyCycles,” Proc. 10th European Symp. Research in Computer Security (ESORICS '05), pp.374396, Sept. 2005.
[11] V. Shoup, “A Proposal for an ISO Standard for PublicKey Encryption,” ISO/IEC JTC 1/SC27, Dec. 2001.
[12] V. Shoup, “OAEP Reconsidered,” J. Cryptology, vol. 15, no. 4, pp.223249, Sept. 2002.
[13] M. Bellare and P. Rogaway, “The Security of Triple Encryption and a Framework for CodeBased GamePlaying Proofs,” Advances in Cryptology—Proc. 25th Int'l Conf. Theory and Applications of Cryptographic Techniques (EUROCRYPT '06), pp. 409426, May 2006.
[14] P.D. Lincoln, J.C. Mitchell, M. Mitchell, and A. Scedrov, “A Probabilistic PolyTime Framework for Protocol Analysis,” Proc. Fifth ACM Conf. Computer and Comm. Security (CCS '98), pp. 112121, Nov. 1998.
[15] P.D. Lincoln, J.C. Mitchell, M. Mitchell, and A. Scedrov, “Probabilistic PolynomialTime Equivalence and Security Protocols,” Proc. World Congress on Formal Methods in the Development of Computing Systems (FM '99), pp. 776793, Sept. 1999.
[16] J.C. Mitchell, A. Ramanathan, A. Scedrov, and V. Teague, “A Probabilistic PolynomialTime Calculus for the Analysis of Cryptographic Protocols,” Theoretical Computer Science, vol. 353, nos. 13, pp. 118164, Mar. 2006.
[17] P. Laud, “Secrecy Types for a Simulatable Cryptographic Library,” Proc. 12th ACM Conf. Computer and Comm. Security (CCS '05), pp. 2635, Nov. 2005.
[18] M. Bellare, J. Kilian, and P. Rogaway, “The Security of the Cipher Block Chaining Message Authentication Code,” J. Computer and System Sciences, vol. 61, no. 3, pp. 362399, Dec. 2000.
[19] M. Bellare, A. Desai, E. Jokipii, and P. Rogaway, “A Concrete Security Treatment of Symmetric Encryption,” Proc. 38th Symp. Foundations of Computer Science (FOCS '97), pp. 394403, Oct. 1997.
[20] D.E. Knuth and P.B. Bendix, “Simple Word Problems in Universal Algebras,” Computational Problems in Abstract Algebra, pp. 263297, 1970.
[21] M. Abdalla, P.A. Fouque, and D. Pointcheval, “PasswordBased Authenticated Key Exchange in the ThreeParty Setting,” Proc. IEE Information Security, vol. 153, no. 1, pp. 2739, Mar. 2006.
[22] B. Blanchet, “Computationally Sound Mechanized Proofs of Correspondence Assertions,” Proc. 20th IEEE Computer Security Foundations Symp. (CSF '07), pp. 97111, July 2007.
[23] T.Y.C. Woo and S.S. Lam, “A Semantic Model for Authentication Protocols,” Proc. 14th IEEE Symp. Security and Privacy (SP '93), pp.178194, May 1993.
[24] M. Bellare, A. Desai, D. Pointcheval, and P. Rogaway, “Relations among Notions of Security for PublicKey Encryption Schemes,” Advances in Cryptology—Proc. 18th Ann. Int'l Cryptology Conf. (CRYPTO '98), pp. 2645, Aug. 1998.
[25] D. Otway and O. Rees, “Efficient and Timely Mutual Authentication,” Operating Systems Rev., vol. 21, no. 1, pp. 810, 1987.
[26] M. Burrows, M. Abadi, and R. Needham, “A Logic of Authentication,” Proc. Royal Soc. of London A, vol. 426, pp. 233271, 1989.
[27] R.M. Needham and M.D. Schroeder, “Using Encryption for Authentication in Large Networks of Computers,” Comm. ACM, vol. 21, no. 12, pp. 993999, Dec. 1978.
[28] R.M. Needham and M.D. Schroeder, “Authentication Revisited,” Operating Systems Rev., vol. 21, no. 1, p. 7, 1987.
[29] D.E. Denning and G.M. Sacco, “Timestamps in Key Distribution Protocols,” Comm. ACM, vol. 24, no. 8, pp. 533536, Aug. 1981.
[30] M. Abadi and R. Needham, “Prudent Engineering Practice for Cryptographic Protocols,” IEEE Trans. Software Eng., vol. 22, no. 1, pp. 615, Jan. 1996.
[31] G. Lowe, “Breaking and Fixing the NeedhamSchroeder PublicKey Protocol Using FDR,” Proc. Second Int'l Workshop Tools and Algorithms for the Construction and Analysis of Systems (TACAS '96), pp. 147166, 1996.
[32] M. Backes, B. Pfitzmann, and M. Waidner, “Symmetric Authentication Within a Simulatable Cryptographic Library,” Computer Security—Proc. Eighth European Symp. Research in Computer Security (ESORICS '03), pp. 271290, Oct. 2003.
[33] M. Backes and B. Pfitzmann, “Symmetric Encryption in a Simulatable DolevYao Style Cryptographic Library,” Proc. 17th IEEE Computer Security Foundations Workshop (CSFW17), June 2004.
[34] M. Backes and B. Pfitzmann, “Relating Symbolic and Cryptographic Secrecy,” IEEE Trans. Dependable and Secure Computing, vol. 2, no. 2, pp. 109123, Apr.June 2005.
[35] C. Sprenger, M. Backes, D. Basin, B. Pfitzmann, and M. Waidner, “Cryptographically Sound Theorem Proving,” Proc. 19th IEEE Computer Security Foundations Workshop (CSFW19), pp. 153166, July 2006.
[36] R. Canetti, “Universally Composable Security: A New Paradigm for Cryptographic Protocols,” Proc. 42nd Ann. Symp. Foundations of Computer Science (FOCS '01), pp. 136145, Oct. 2001.
[37] R. Canetti and J. Herzog, “Universally Composable Symbolic Analysis of Mutual Authentication and Key Exchange Protocols,” Proc. Third Theory of Cryptography Conf. (TCC '06), Mar. 2006.
[38] B. Blanchet, “Automatic Proof of Strong Secrecy for Security Protocols,” Proc. 25th IEEE Symp. Security and Privacy (SP '04), pp.86100, May 2004.
[39] P. Mateus, J. Mitchell, and A. Scedrov, “Composition of Cryptographic Protocols in a Probabilistic PolynomialTime Process Calculus,” Proc. 14th Int'l Conf. Concurrency Theory (CONCUR '03), pp. 327349, Sept. 2003.
[40] A. Ramanathan, J. Mitchell, A. Scedrov, and V. Teague, “Probabilistic Bisimulation and Equivalence for Security Analysis of Network Protocols,” Proc. Seventh Int'l Conf. Foundations of Software Science and Computation Structures (FOSSACS '04), pp.468483, Mar. 2004.
[41] A. Datta, A. Derek, J.C. Mitchell, V. Shmatikov, and M. Turuani, “Probabilistic PolynomialTime Semantics for a Protocol Security Logic,” Proc. 32nd Int'l Colloquium Automata, Languages and Programming (ICALP '05), pp. 1629, July 2005.
[42] P. Laud, “Handling Encryption in an Analysis for Secure Information Flow,” Programming Languages and Systems—Proc. 12th European Symp. Programming (ESOP '03), pp. 159173, Apr. 2003.
[43] P. Laud, “Symmetric Encryption in Automatic Analyses for Confidentiality against Active Adversaries,” Proc. 25th IEEE Symp. Security and Privacy (SP '04), pp. 7185, May 2004.
[44] M. Backes and P. Laud, “Computationally Sound Secrecy Proofs by Mechanized Flow Analysis,” Proc. 13th ACM Conf. Computer and Comm. Security (CCS '06), pp. 370379, Nov. 2006.
[45] G. Barthe, J. Cederquist, and S. Tarento, “A MachineChecked Formalization of the Generic Model and the Random Oracle Model,” Proc. Second Int'l Joint Conf. Automated Reasoning (IJCAR '04), pp. 385399, July 2004.
[46] S. Tarento, “MachineChecked Security Proofs of Cryptographic Signature Schemes,” Proc. 10th European Symp. Research in Computer Security (ESORICS '05), pp. 140158, Sept. 2005.
[47] S. Halevi, “A Plausible Approach to ComputerAided Cryptographic Proofs,” Cryptology ePrint Archive, Report 2005/181, http://eprint.iacr.org/2005181, June 2005.
[48] B. Blanchet and D. Pointcheval, “Automated Security Proofs with Sequences of Games,” Advances in Cryptology—Proc. 26th Ann. Int'l Cryptology Conf. (CRYPTO '06), pp. 537554, Aug. 2006.