{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,3]],"date-time":"2026-10-03T07:59:55Z","timestamp":1791014395776,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540228493","type":"print"},{"value":"9783540278368","type":"electronic"}],"license":[{"start":{"date-parts":[[2004,1,1]],"date-time":"2004-01-01T00:00:00Z","timestamp":1072915200000},"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":[[2004]]},"DOI":"10.1007\/978-3-540-27836-8_7","type":"book-chapter","created":{"date-parts":[[2010,9,15]],"date-time":"2010-09-15T22:53:21Z","timestamp":1284591201000},"page":"46-58","source":"Crossref","is-referenced-by-count":35,"title":["Deciding Knowledge in Security Protocols Under Equational Theories"],"prefix":"10.1007","author":[{"given":"Mart\u00edn","family":"Abadi","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"V\u00e9ronique","family":"Cortier","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"7_CR1","unstructured":"Abadi, M., Cortier, V.: Deciding knowledge in security protocols under equational theories. Technical Report RR-5169, INRIA (April 2004), An up-to-date version will be kept at http:\/\/www.loria.fr\/~cortier\/publis.html"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Proceedings of the 28th ACM Symposium on Principles of Programming Languages (POPL 2001), January 2001, pp. 104\u2013115 (2001)","DOI":"10.1145\/373243.360213"},{"issue":"4","key":"7_CR3","first-page":"267","volume":"5","author":"M. Abadi","year":"1998","unstructured":"Abadi, M., Gordon, A.D.: A bisimulation method for cryptographic protocols. Nordic Journal of Computing\u00a05(4), 267\u2013303 (1998)","journal-title":"Nordic Journal of Computing"},{"issue":"1","key":"7_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1998.2740","volume":"148","author":"M. Abadi","year":"1999","unstructured":"Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: The spi calculus. Information and Computation\u00a0148(1), 1\u201370 (1999)","journal-title":"Information and Computation"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1007\/3-540-44618-4_28","volume-title":"CONCUR 2000 - Concurrency Theory","author":"R.M. Amadio","year":"2000","unstructured":"Amadio, R.M., Lugiez, D.: On the reachability problem in cryptographic protocols. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol.\u00a01877, pp. 380\u2013394. Springer, Heidelberg (2000)"},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: 14th IEEE Computer Security Foundations Workshop (CSFW-14), June 2001, pp. 82\u201396 (2001)","DOI":"10.1109\/CSFW.2001.930138"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/3-540-45789-5_25","volume-title":"Static Analysis","author":"B. Blanchet","year":"2002","unstructured":"Blanchet, B.: From secrecy to authenticity in security protocols. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol.\u00a02477, pp. 342\u2013359. Springer, Heidelberg (2002)"},{"key":"7_CR8","unstructured":"Blanchet, B.: Automatic proof of strong secrecy for security protocols. In: IEEE Symposium on Security and Privacy (May 2004) (to appear)"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Boreale, M., De Nicola, R., Pugliese, R.: Proof techniques for cryptographic processes. In: Proceedings of the Fourteenth Annual IEEE Symposium on Logic in Computer Science, July 1999, pp. 157\u2013166 (1999)","DOI":"10.1109\/LICS.1999.782608"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-540-24597-1_11","volume-title":"FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science","author":"Y. Chevalier","year":"2003","unstructured":"Chevalier, Y., Kuester, R., Rusinowitch, M., Turani, M.: Deciding the security of protocols with Diffie-Hellman exponentiation and products in exponents. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol.\u00a02914, pp. 124\u2013135. Springer, Heidelberg (2003)"},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"Chevalier, Y., Kuester, R., Rusinowitch, M., Turani, M.: An NP decision procedure for protocol insecurity with xor. In: Proceedings of the 18th Annual IEEE Symposium on Logic In Computer Science (LICS 2003), pp. 261\u2013270 (2003)","DOI":"10.1109\/LICS.2003.1210066"},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"Comon-Lundh, H., Shmatikov, V.: Intruder deductions, constraint solving and insecurity decision in presence of exclusive or. In: Proceedings of the 18th Annual IEEE Symposium on Logic In Computer Science (LICS 2003), pp. 271\u2013280 (2003)","DOI":"10.1109\/LICS.2003.1210067"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Comon-Lundh, H., Treinen, R.: Easy intruder deductions. Technical Report LSV-03-8, Laboratoire Sp\u00e9cification et V\u00e9rification, ENS de Cachan, France (2003)","DOI":"10.1007\/978-3-540-39910-0_10"},{"key":"7_CR14","unstructured":"Delaune, S., Jacquemard, F.: Narrowing-based constraint solving for the verification of security protocols. Technical Report LSV-04-8, Laboratoire Sp\u00e9cification et V\u00e9rification, ENS de Cachan, France (April 2004)"},{"issue":"12","key":"7_CR15","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"IT-29","author":"D. Dolev","year":"1983","unstructured":"Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Transactions on Information Theory\u00a0IT-29(12), 198\u2013208 (1983)","journal-title":"IEEE Transactions on Information Theory"},{"key":"7_CR16","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1016\/0022-0000(84)90070-9","volume":"28","author":"S. Goldwasser","year":"1984","unstructured":"Goldwasser, S., Micali, S.: Probabilistic encryption. Journal of Computer and System Sciences\u00a028, 270\u2013299 (1984)","journal-title":"Journal of Computer and System Sciences"},{"issue":"2","key":"7_CR17","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/BF00197942","volume":"7","author":"R. Kemmerer","year":"1994","unstructured":"Kemmerer, R., Meadows, C., Millen, J.: Three system for cryptographic protocol analysis. Journal of Cryptology\u00a07(2), 79\u2013130 (1994)","journal-title":"Journal of Cryptology"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"Lincoln, P., Mitchell, J., Mitchell, M., Scedrov, A.: A probabilistic poly-time framework for protocol analysis. In: Proceedings of the Fifth ACM Conference on Computer and Communications Security, pp. 112\u2013121 (1998)","DOI":"10.1145\/288090.288117"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/3-540-61042-1_43","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Lowe","year":"1996","unstructured":"Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol.\u00a01055, pp. 147\u2013166. Springer, Heidelberg (1996)"},{"issue":"1-2","key":"7_CR20","doi-asserted-by":"crossref","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"6","author":"L.C. Paulson","year":"1998","unstructured":"Paulson, L.C.: The inductive approach to verifying cryptographic protocols. Journal of Computer Security\u00a06(1-2), 85\u2013128 (1998)","journal-title":"Journal of Computer Security"},{"key":"7_CR21","doi-asserted-by":"crossref","unstructured":"Schneider, S.: Security properties and CSP. In: IEEE Symposium on Security and Privacy, pp. 174\u2013187 (1996)","DOI":"10.1109\/SECPRI.1996.502680"}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-27836-8_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,25]],"date-time":"2025-02-25T21:31:04Z","timestamp":1740519064000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-27836-8_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540228493","9783540278368"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-27836-8_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004]]}}}