{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T21:12:19Z","timestamp":1743109939637,"version":"3.40.3"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319175805"},{"type":"electronic","value":"9783319175812"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-17581-2_11","type":"book-chapter","created":{"date-parts":[[2015,4,15]],"date-time":"2015-04-15T12:22:36Z","timestamp":1429100556000},"page":"159-173","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Key-Secrecy of PACE with OTS\/CafeOBJ"],"prefix":"10.1007","author":[{"given":"Dominik","family":"Klein","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,4,16]]},"reference":[{"key":"11_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1007\/978-3-540-30580-4_6","volume-title":"Public key cryptography","author":"M Abdalla","year":"2005","unstructured":"Abdalla, M., Fouque, P.-A., Pointcheval, D.: Password-based authenticated key exchange in the three-party setting. In: Vaudenay, S. (ed.) PKC 2005. LNCS, vol. 3386, pp. 65\u201384. Springer, Heidelberg (2005)"},{"key":"11_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-642-04474-8_3","volume-title":"Information security","author":"J Bender","year":"2009","unstructured":"Bender, J., Fischlin, M., K\u00fcgler, D.: Security analysis of the PACE key-agreement protocol. In: Samarati, P., Yung, M., Martinelli, F., Ardagna, C.A. (eds.) ISC 2009. LNCS, vol. 5735, pp. 33\u201348. Springer, Heidelberg (2009)"},{"key":"11_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-642-28641-4_2","volume-title":"Principles of security trust","author":"B Blanchet","year":"2012","unstructured":"Blanchet, B.: Security protocol verification: symbolic and computational models. In: Degano, P., Guttman, J.D. (eds.) POST 2012. LNCS, vol. 7215, pp. 3\u201329. Springer, Heidelberg (2012)"},{"key":"11_CR4","unstructured":"BSI: Advanced security mechanisms for machine readable travel documents (2012)"},{"key":"11_CR5","unstructured":"Cheikhrouhou, L., Stephan, W.: Meilensteinreport: inductive verification of PACE. Technical report, DFKI GmbH (2010)"},{"key":"11_CR6","unstructured":"Cheikhrouhou, L., Stephan, W., Dagdelen, \u00d6., Fischlin, M., Ullmann, M.: Merging the cryptographic security analysis and the algebraic-logic security proof of PACE. Sicherheit. LNI, vol. 195, 83\u201394 (2012)"},{"key":"11_CR7","unstructured":"Clark, J., Jacob, J.: A survey of authentication protocol literature (1997)"},{"key":"11_CR8","series-title":"AMAST Series in Computing","doi-asserted-by":"crossref","DOI":"10.1142\/3831","volume-title":"CafeOBJ Report: The Language, Proof Techniques and Methodologies for Object-oriented Algebraic Specification","author":"R Diaconescu","year":"1998","unstructured":"Diaconescu, R., Futatsugi, K.: CafeOBJ Report: The Language, Proof Techniques and Methodologies for Object-oriented Algebraic Specification. AMAST Series in Computing, vol. 6. World Scientific, Singapore (1998)"},{"issue":"6","key":"11_CR9","doi-asserted-by":"publisher","first-page":"644","DOI":"10.1109\/TIT.1976.1055638","volume":"22","author":"W Diffie","year":"1976","unstructured":"Diffie, W., Hellman, M.E.: New directions in cryptography. IEEE Trans. Inf. Theory 22(6), 644\u2013654 (1976)","journal-title":"IEEE Trans. Inf. Theory"},{"issue":"2","key":"11_CR10","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"29","author":"D Dolev","year":"1983","unstructured":"Dolev, D., Yao, A.C.C.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198\u2013208 (1983)","journal-title":"IEEE Trans. Inf. Theory"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-03829-7_1","volume-title":"Foundations of Security Analysis and Design V","author":"S Escobar","year":"2009","unstructured":"Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA: Cryptographic protocol analysis modulo equational properties. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007. LNCS, vol. 5705, pp. 1\u201350. Springer, Heidelberg (2009)"},{"key":"11_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/978-3-642-40206-7_26","volume-title":"Algebra and coalgebra in computer science","author":"D G\u0103in\u0103","year":"2013","unstructured":"G\u0103in\u0103, D., Zhang, M., Chiba, Y., Arimoto, Y.: Constructor-based inductive theorem prover. In: Heckel, R., Milius, S. (eds.) CALCO 2013. LNCS, vol. 8089, pp. 328\u2013333. Springer, Heidelberg (2013)"},{"key":"11_CR13","unstructured":"ICAO: Doc 9303 - Machine readable travel documents"},{"key":"11_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"454","DOI":"10.1007\/3-540-61474-5_101","volume-title":"Computer aided verification","author":"FA Koch","year":"1996","unstructured":"Koch, F.A., Ullmann, M., Wittmann, S.: Verification support environment. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 454\u2013457. Springer, Heidelberg (1996)"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"K\u00fcsters, R., Truderung, T.: Using proverif to analyze protocols with Diffie-Hellman exponentiation. In: proceedings of the 22nd CSF (2009)","DOI":"10.1109\/CSF.2009.17"},{"issue":"3","key":"11_CR16","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. Inf. Process. Lett. 56(3), 131\u2013133 (1995)","journal-title":"Inf. Process. Lett."},{"key":"11_CR17","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1016\/S1571-0661(05)82536-8","volume":"71","author":"K Ogata","year":"2002","unstructured":"Ogata, K., Futatsugi, K.: Rewriting-based verification of authentication protocols. Electron. Notes Theor. Comput. Sci. 71, 208\u2013222 (2002)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"2","key":"11_CR18","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1016\/S0020-0190(02)00480-5","volume":"86","author":"K Ogata","year":"2003","unstructured":"Ogata, K., Futatsugi, K.: Flaw and modification of the iKP electronic payment protocols. Inf. Process. Lett. 86(2), 57\u201362 (2003)","journal-title":"Inf. Process. Lett."},{"key":"11_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/978-3-540-39958-2_12","volume-title":"Formal methods for open object-based distributed systems","author":"K Ogata","year":"2003","unstructured":"Ogata, K., Futatsugi, K.: Proof scores in the OTS\/cafeOBJ method. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol. 2884, pp. 170\u2013184. Springer, Heidelberg (2003)"},{"key":"11_CR20","unstructured":"Ogata, K., Futatsugi, K.: Equational approach to formal analysis of TLS. In: Proceedings of the 25th ICDCS. IEEE Computer Society (2005)"},{"issue":"2","key":"11_CR21","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1142\/S0218194010004712","volume":"20","author":"K Ogata","year":"2010","unstructured":"Ogata, K., Futatsugi, K.: Proof score approach to analysis of electronic commerce protocols. Int. J. Softw. Eng. Knowl. Eng. 20(2), 253\u2013287 (2010)","journal-title":"Int. J. Softw. Eng. Knowl. Eng."},{"key":"11_CR22","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky, P.C., Grimeland, M.: Formal analysis of time-dependent cryptographic protocols in real-time maude. In: Proceedings of the 21st IPDPS (2007)","DOI":"10.1109\/IPDPS.2007.370355"},{"key":"11_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-642-34032-1_15","volume-title":"Leveraging applications of formal methods, verification and validation","author":"I Ouranos","year":"2012","unstructured":"Ouranos, I., Ogata, K., Stefaneas, P.: Formal analysis of tesla protocol in the timed OTS\/cafeOBJ method. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part II. LNCS, vol. 7610, pp. 126\u2013142. Springer, Heidelberg (2012)"},{"key":"11_CR24","doi-asserted-by":"crossref","unstructured":"Schmidt, B., Meier, S., Cremers, C.J.F., Basin, D.A.: Automated analysis of Diffie-Hellman protocols and advanced security properties. In: Proceedings of the 25th CSF (2012)","DOI":"10.1109\/CSF.2012.25"}],"container-title":["Communications in Computer and Information Science","Formal Techniques for Safety-Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-17581-2_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,24]],"date-time":"2023-01-24T11:56:50Z","timestamp":1674561410000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-17581-2_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319175805","9783319175812"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-17581-2_11","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"type":"print","value":"1865-0929"},{"type":"electronic","value":"1865-0937"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"16 April 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}