{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,7]],"date-time":"2026-07-07T15:41:29Z","timestamp":1783438889546,"version":"3.54.6"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540242970","type":"print"},{"value":"9783540305798","type":"electronic"}],"license":[{"start":{"date-parts":[[2005,1,1]],"date-time":"2005-01-01T00:00:00Z","timestamp":1104537600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-30579-8_24","type":"book-chapter","created":{"date-parts":[[2010,12,20]],"date-time":"2010-12-20T11:45:34Z","timestamp":1292845534000},"page":"363-379","source":"Crossref","is-referenced-by-count":64,"title":["Cryptographic Protocol Analysis on Real C Code"],"prefix":"10.1007","author":[{"given":"Jean","family":"Goubault-Larrecq","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Fabrice","family":"Parrennes","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"24_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1007\/3-540-45694-5_33","volume-title":"CONCUR 2002 - Concurrency Theory","author":"R.M. Amadio","year":"2002","unstructured":"Amadio, R.M., Charatonik, W.: On name generation and set-based analysis in the Dolev- Yao model. In: Brim, L., Jan\u010dar, P., K\u0159et\u00ednsk\u00fd, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol.\u00a02421, pp. 499\u2013514. Springer, Heidelberg (2002)"},{"key":"24_CR2","unstructured":"Andersen, L.O.: Program Analysis and Specialization for the C Programming Language. PhD thesis, DIKU, University of Copenhagen (DIKU report 94\/19) (1994)"},{"key":"24_CR3","first-page":"82","volume-title":"14th IEEE Computer Security Foundations Workshop (CSFW-14)","author":"B. Blanchet","year":"2001","unstructured":"Blanchet, B.: An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In: 14th IEEE Computer Security Foundations Workshop (CSFW-14), Cape Breton, Nova Scotia, Canada, June, pp. 82\u201396. IEEE Computer Society Press, Los Alamitos (2001)"},{"key":"24_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/3-540-36377-7_5","volume-title":"The Essence of Computation","author":"B. Blanchet","year":"2002","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: Design and Implementation of a Special-Purpose Static Program Analyzer for Safety- Critical Real-Time Embedded Software. In: Mogensen, T.\u00c6., Schmidt, D.A., Sudborough, I.H. (eds.) The Essence of Computation. LNCS, vol.\u00a02566, pp. 85\u2013108. Springer, Heidelberg (2002)"},{"key":"24_CR5","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1145\/781131.781153","volume-title":"ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (PLD 2003)","author":"B. Blanchet","year":"2003","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: A Static Analyzer for Large Safety-Critical Software. In: ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (PLD 2003), San Diego, California, June, pp. 196\u2013207. ACM Press, New York (2003)"},{"key":"24_CR6","unstructured":"Boury, P., Elkhadi, N.: Static Analysis of Java Cryptographic Applets. In: ECOOP 2001 Workshop on Formal Techniques for Java Programs. Fern Universit\u00e4t Hagen (2001)"},{"key":"24_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/3-540-36575-3_8","volume-title":"Programming Languages and Systems","author":"H. Comon-Lundh","year":"2003","unstructured":"Comon-Lundh, H., Cortier, V.: Security properties: Two agents are sufficient. In: Degano, P. (ed.) ESOP 2003. LNCS, vol.\u00a02618, pp. 99\u2013113. Springer, Heidelberg (2003)"},{"key":"24_CR8","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"30","author":"D. Dolev","year":"1983","unstructured":"Dolev, D., Yao, A.C.: On security of public key protocols. IEEE trans. on Information Theory, IT\u00a030, 198\u2013208 (1983)","journal-title":"IEEE trans. on Information Theory, IT"},{"key":"24_CR9","unstructured":"Durgin, N., Lincoln, P., Mitchell, J., Scedrov, A.: Undecidability of bounded security protocols. In: Heintze, N., Clarke, E. (eds.) Proceedings of the Workshop on Formal Methods and Security Protocols \u2013 FMSP, Trento, Italy (July 1999)"},{"key":"24_CR10","unstructured":"Freier, A., Karlton, P., Kocher, P.: The SSL protocol. Version 3.0 (1996), \n                    \n                      http:\/\/home.netscape.com\/eng\/ssl3\/"},{"key":"24_CR11","unstructured":"Gay, O.: Exploitation avanc\u00e9e de buffer overflows. Technical report, LASEC, Ecole Polytechnique F\u00e9d\u00e9rale de Lausanne (June 2002), \n                    \n                      http:\/\/diwww.epfl.ch\/~ogay\/advbof\/advbof.pdf"},{"key":"24_CR12","unstructured":"Goubault-Larrecq, J. (ed.): Special Issue on Models and Methods for Cryptographic Protocol Verification, Warsaw, Poland, December. Instytut \u0141\u0105csno\u015bci (Institute of Telecommunications), vol.\u00a04 (2002)"},{"key":"24_CR13","unstructured":"Goubault-Larrecq, J.: Une fois qu\u2019on n\u2019a pas trouv\u00e9 de preuve, comment le faire comprendre \u00e0 un assistant de preuve? In: Actes 15\u00e8mes journ\u00e9es francophones sur les langages applicatifs (JFLA 2004), Sainte-Marie-de-R\u00e9 France, Janvier (2004) INRIA"},{"key":"24_CR14","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1145\/378795.378855","volume-title":"Proc. of the ACM SIGPLAN 2001 conference on Programming language design and implementation","author":"N. Heintze","year":"2001","unstructured":"Heintze, N., Tardieu, O.: Ultra-fast aliasing analysis using cla: a million lines of c code in a second. In: Proc. of the ACM SIGPLAN 2001 conference on Programming language design and implementation, pp. 254\u2013263. ACM Press, New York (2001)"},{"key":"24_CR15","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1145\/379605.379665","volume-title":"Proceedings of the 2001 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering","author":"M. Hind","year":"2001","unstructured":"Hind, M.: Pointer analysis: haven\u2019t we solved this problem yet? In: Proceedings of the 2001 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, pp. 54\u201361. ACM Press, New York (2001)"},{"key":"24_CR16","unstructured":"Kadhi, N.E.: Automatic verification of confidentiality properties of cryptographic programs. Networking and Information Systems\u00a03(6) (2001)"},{"issue":"3","key":"24_CR17","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1016\/0020-0190(95)00144-2","volume":"56","author":"G. Lowe","year":"1995","unstructured":"Lowe, G.: An attack on the needham-schroeder public-key authentication protocol. Information Processing Letters\u00a056(3), 131\u2013133 (1995)","journal-title":"Information Processing Letters"},{"key":"24_CR18","volume-title":"Communication and concurrency","author":"R. Milner","year":"1995","unstructured":"Milner, R.: Communication and concurrency. Prentice Hall International (UK) Ltd., Englewood Cliffs (1995)"},{"key":"24_CR19","doi-asserted-by":"crossref","unstructured":"Needham, R., Schroeder, M.: Using encryption for authentification in large networks of computers. Communications of the ACM\u00a021(12) (December 1978)","DOI":"10.1145\/359657.359659"},{"key":"24_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/3-540-45789-5_5","volume-title":"Static Analysis","author":"F. Nielson","year":"2002","unstructured":"Nielson, F., Riis Nielson, H., Seidl, H.: Normalizable horn clauses, strongly recognizable relations, and spi. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol.\u00a02477, pp. 20\u201335. Springer, Heidelberg (2002)"},{"key":"24_CR21","unstructured":"Parrennes, F.: The CSur project (2004), \n                    \n                      http:\/\/www.lsv.ens-cachan.fr\/csur\/"},{"issue":"3","key":"24_CR22","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"S. Sagiv","year":"2002","unstructured":"Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Prog. Lang. Sys.\u00a024(3), 217\u2013298 (2002)","journal-title":"ACM Trans. Prog. Lang. Sys."},{"key":"24_CR23","unstructured":"Selinger, P.: Models for an adversary-centric protocol logic. Electronic Notes in Theoretical Computer Science\u00a055(1), 73\u201387 (2001): Goubault-Larrecq, J. (ed.) Proceedings of the 1st Workshop on Logical Aspects of Cryptographic Protocol Verification, LACPV 2001 (2001)"},{"key":"24_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/3-540-45719-4_25","volume-title":"Algebraic Methodology and Software Technology","author":"A. Simon","year":"2002","unstructured":"Simon, A., King, A.: Analyzing string buffers in C. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol.\u00a02422, pp. 365\u2013379. Springer, Heidelberg (2002)"},{"key":"24_CR25","unstructured":"Wagner, D., Foster, J.S., Brewer, E.A., Aiken, A.: A first step towards automated detection of buffer overrun vulnerabilities. In: Network and Distributed System Security Symposium, San Diego, CA, February, pp. 3\u201317 (2000)"},{"key":"24_CR26","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1007\/3-540-48660-7_29","volume-title":"Automated Deduction - CADE-16","author":"C. Weidenbach","year":"1999","unstructured":"Weidenbach, C.: Towards an automatic analysis of security protocols. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 314\u2013328. Springer, Heidelberg (1999)"},{"key":"24_CR27","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/3-540-45620-1_22","volume-title":"Automated Deduction - CADE-18","author":"C. Weidenbach","year":"2002","unstructured":"Weidenbach, C., Brahm, U., Hillenbrand, T., Keen, E., Theobald, C., Topic, D.: SPASS version 2.0. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 275\u2013279. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30579-8_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T19:30:33Z","timestamp":1558294233000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30579-8_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540242970","9783540305798"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30579-8_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}