{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T13:20:44Z","timestamp":1742995244893,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642014642"},{"type":"electronic","value":"9783642014659"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-01465-9_15","type":"book-chapter","created":{"date-parts":[[2009,4,4]],"date-time":"2009-04-04T00:56:06Z","timestamp":1238806566000},"page":"226-241","source":"Crossref","is-referenced-by-count":0,"title":["Verifying Multi-party Authentication Using Rank Functions and PVS"],"prefix":"10.1007","author":[{"given":"Rob","family":"Verhoeven","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Francien","family":"Dechesne","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"15_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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)"},{"key":"15_CR2","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: Prototype Verification System, \n                  \n                    http:\/\/www.csl.sri.com\/"},{"key":"15_CR3","unstructured":"Cremers, C., Mauw, S.: A Family of Multi-Party Authentication Protocols. In: First Benelux Workshop on Information and System Security (WISSec) (2006)"},{"issue":"1-2","key":"15_CR4","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1016\/j.tcs.2006.08.034","volume":"367","author":"C.J.F. Cremers","year":"2006","unstructured":"Cremers, C.J.F., Mauw, S., de Vink, E.P.: Injective Synchronisation: an Extension of the Authentication Hierarchy. Theor. Comput. Sci.\u00a0367(1-2), 139\u2013161 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"15_CR5","unstructured":"Cremers, C.: Scyther tool, \n                  \n                    http:\/\/people.inf.ethz.ch\/cremersc\/scyther\/"},{"key":"15_CR6","unstructured":"Cremers, C.: Scyther \u2013 Semantics and Verification of Security Protocols. PhD thesis, Technische Universiteit Eindhoven (November 2006)"},{"key":"15_CR7","first-page":"3","volume-title":"CSFW 10","author":"S. Schneider","year":"1997","unstructured":"Schneider, S.: Verifying Authentication Protocols with CSP. In: CSFW 10, pp. 3\u201317. IEEE Computer Society Press, Los Alamitos (1997)"},{"issue":"2","key":"15_CR8","doi-asserted-by":"publisher","first-page":"317","DOI":"10.3233\/JCS-2005-13204","volume":"13","author":"J. Heather","year":"2005","unstructured":"Heather, J., Schneider, S.: A Decision Procedure for the Existence of a Rank Function. Journal of Computer Security\u00a013(2), 317\u2013344 (2005)","journal-title":"Journal of Computer Security"},{"key":"15_CR9","volume-title":"Modelling and Analysis of Security Protocols","author":"P. Ryan","year":"2001","unstructured":"Ryan, P., Schneider, S.: Modelling and Analysis of Security Protocols. Addison-Wesley, Reading (2001)"},{"key":"15_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/11423348_14","volume-title":"Communicating Sequential Processes. The First 25 Years","author":"S. Schneider","year":"2005","unstructured":"Schneider, S., Delicata, R.: Verifying Security Protocols: An Application of CSP. In: Abdallah, A.E., Jones, C.B., Sanders, J.W. (eds.) Communicating Sequential Processes. LNCS, vol.\u00a03525, pp. 243\u2013263. Springer, Heidelberg (2005)"},{"issue":"2","key":"15_CR11","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/j.jlap.2004.09.005","volume":"64","author":"N. Evans","year":"2005","unstructured":"Evans, N., Schneider, S.: Verifying Security Protocols with PVS: Widening the Rank Function Approach. Journal of Logic and Algebraic Programming\u00a064(2), 253\u2013284 (2005)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"15_CR12","unstructured":"Verhoeven, R.: PVS-code for this paper, \n                  \n                    http:\/\/www.win.tue.nl\/~fdechesn\/"},{"issue":"1","key":"15_CR13","first-page":"19","volume":"38","author":"S. Shaikh","year":"2006","unstructured":"Shaikh, S., Bush, V.: Analysing the Woo-Lam Protocol Using CSP and Rank Functions. Journal of Research and Practice in Information Technology\u00a038(1), 19\u201329 (2006)","journal-title":"Journal of Research and Practice in Information Technology"},{"key":"15_CR14","unstructured":"Delicata, R., Schneider, S.A.: A Formal Model of Diffie-Hellman Using CSP and Rank Functions. Technical Report CSD-TR-03-05, Department of Computer Science, Royal Holloway, University of London (2003)"},{"key":"15_CR15","first-page":"16","volume-title":"CSFW 17","author":"O. Pereira","year":"2004","unstructured":"Pereira, O., Quisquater, J.J.: Generic Insecurity of Cliques-Type Authenticated Group Key Agreement Protocols. In: CSFW 17, pp. 16\u201319. IEEE Computer Society Press, Los Alamitos (2004)"},{"key":"15_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-540-39724-3_21","volume-title":"Correct Hardware Design and Verification Methods","author":"M. Layouni","year":"2003","unstructured":"Layouni, M., Hooman, J., Tahar, S.: On the correctness of an intrusion-tolerant group communication protocol. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol.\u00a02860, pp. 231\u2013246. Springer, Heidelberg (2003)"},{"issue":"1-2","key":"15_CR17","doi-asserted-by":"publisher","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":"15_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/11599548_6","volume-title":"Information Security and Cryptology","author":"S.A. Shaikh","year":"2005","unstructured":"Shaikh, S.A., Bush, V.J., Schneider, S.A.: Specifying authentication using signal events in CSP. In: Feng, D., Lin, D., Yung, M. (eds.) CISC 2005. LNCS, vol.\u00a03822, pp. 63\u201374. Springer, Heidelberg (2005)"},{"key":"15_CR19","volume-title":"The Theory and Practice of Concurrency","author":"A.W. Roscoe","year":"1997","unstructured":"Roscoe, A.W., Hoare, C.A.R., Bird, R.: The Theory and Practice of Concurrency. Prentice Hall, NJ (1997)"},{"key":"15_CR20","unstructured":"Verhoeven, R.: Proving Correctness of a Multi-Party Authentication Protocol with Rank Functions. Master\u2019s thesis, Technische Universiteit Eindhoven (2007)"},{"issue":"1-2","key":"15_CR21","first-page":"87","volume":"22","author":"S. Mauw","year":"2001","unstructured":"Mauw, S., Bos, V.: Drawing Message Sequence Charts with LaTeX. TUGBoat\u00a022(1-2), 87\u201392 (2001)","journal-title":"TUGBoat"},{"key":"15_CR22","first-page":"255","volume-title":"CSFW 13","author":"J. Heather","year":"2000","unstructured":"Heather, J., Lowe, G., Schneider, S.: How to prevent type flaw attacks on security protocols. In: CSFW 13, pp. 255\u2013268. IEEE Computer Society Press, Los Alamitos (2000)"},{"issue":"2","key":"15_CR23","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.: On the Security of Public Key Protocols. IEEE Transactions on Information Theory\u00a029(2), 198\u2013208 (1983)","journal-title":"IEEE Transactions on Information Theory"},{"key":"15_CR24","first-page":"31","volume-title":"CSFW 10","author":"G. Lowe","year":"1997","unstructured":"Lowe, G.: A Hierarchy of Authentication Specifications. In: CSFW 10, pp. 31\u201344. IEEE Computer Society Press, Los Alamitos (1997)"},{"key":"15_CR25","unstructured":"Meier, S.: A Formalization of an Operational Semantics of Security Protocols. Diploma thesis, ETH Zurich (August 2007)"}],"container-title":["Lecture Notes in Computer Science","Formal Aspects in Security and Trust"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-01465-9_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,7]],"date-time":"2019-03-07T04:42:51Z","timestamp":1551933771000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-01465-9_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642014642","9783642014659"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-01465-9_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}