{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T12:20:17Z","timestamp":1725538817687},"publisher-location":"Berlin, Heidelberg","reference-count":54,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642049033"},{"type":"electronic","value":"9783642049040"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-04904-0_11","type":"book-chapter","created":{"date-parts":[[2009,10,6]],"date-time":"2009-10-06T10:21:49Z","timestamp":1254824509000},"page":"62-84","source":"Crossref","is-referenced-by-count":0,"title":["Cordial Security Protocol Programming"],"prefix":"10.1007","author":[{"given":"Per Harald","family":"Myrvang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tage","family":"Stabell-Kul\u00f8","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"11_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"426","DOI":"10.1007\/3-540-61996-8","volume-title":"Computer Science Today - Recent Trends and Developments","author":"R. Anderson","year":"1996","unstructured":"Anderson, R., Needham, R.: Programming satan\u2019s computer. In: van Leeuwen, J. (ed.) Computer Science Today. LNCS, vol.\u00a01000, pp. 426\u2013440. Springer, Heidelberg (1996)"},{"key":"11_CR2","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1145\/343477.343534","volume-title":"Proceedings of the nineteenth annual ACM symposium on Principles of distributed computing","author":"B. Barak","year":"2000","unstructured":"Barak, B., Halevi, S., Herzberg, A., Naor, D.: Clock synchronization with faults and recoveries (extended abstract). In: Proceedings of the nineteenth annual ACM symposium on Principles of distributed computing, pp. 133\u2013142. ACM Press, New York (2000)"},{"issue":"4","key":"11_CR3","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1145\/571637.571638","volume":"20","author":"L. Zhou","year":"2002","unstructured":"Zhou, L., Schneider, F.B., Renesse, R. V.: Coca: A secure distributed online certification authority. ACM Trans. Comput. Syst.\u00a020(4), 329\u2013368 (2002)","journal-title":"ACM Trans. Comput. Syst."},{"key":"11_CR4","unstructured":"Department of Defense: DoD 5200.28-STD: Department of defense (DoD) Trusted Computer System Evaluation Criteria (TCSEC), The Orange Book (1985)"},{"issue":"4","key":"11_CR5","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1145\/138873.138874","volume":"10","author":"B. Lampson","year":"1992","unstructured":"Lampson, B., Abadi, M., Burrows, M., Wobber, E.: Authentication in distribued systems: theory and practice. ACM Transactions on Computer Systems\u00a010(4), 265\u2013310 (1992)","journal-title":"ACM Transactions on Computer Systems"},{"key":"#cr-split#-11_CR6.1","doi-asserted-by":"crossref","unstructured":"Thompson, K.: Reflections on trusting trust. Communications of the ACM\u00a027(8), 761-763 (1984)","DOI":"10.1145\/358198.358210"},{"key":"#cr-split#-11_CR6.2","unstructured":"Also appears in ACM Turing Award Lectures: The First Twenty Years 1965-1985. ACM press, New York (1987), and Computers Under Attack: Intruders, Worms, and Viruses. ACM press, New York (1990)"},{"issue":"11","key":"11_CR7","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1145\/188280.188298","volume":"37","author":"G.J. Simmons","year":"1994","unstructured":"Simmons, G.J.: Cryptanalysis and protocol failures. Communications of the ACM\u00a037(11), 56\u201365 (1994)","journal-title":"Communications of the ACM"},{"issue":"2","key":"11_CR8","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1145\/996943.996948","volume":"7","author":"A. Stubblefield","year":"2004","unstructured":"Stubblefield, A., Ioannidis, J., Rubin, A.D.: A key recovery attack on the 802.11b wired equivalent privacy protocol (wep). ACM Transactions of Information Systems Security\u00a07(2), 319\u2013332 (2004)","journal-title":"ACM Transactions of Information Systems Security"},{"issue":"1","key":"11_CR9","doi-asserted-by":"crossref","first-page":"6","DOI":"10.1109\/32.481513","volume":"22","author":"M. Abadi","year":"1996","unstructured":"Abadi, M., Needham, R.: Prudent engineering practice for cryptographic protocols. IEEE Transactions on Software Engineering\u00a022(1), 6\u201315 (1996); A preliminery version appeared in the Proceedings of the 1994 IEEE Computer Society Symposium on Research in Security and Privacy (1994)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"Harris, J., Henderson, D.: A better mythology for system design. In: ACM Conference on Human Factors in Computing Systems, pp. 88\u201395 (1999)","DOI":"10.1145\/302979.303003"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1007\/3-540-44750-4_19","volume-title":"Advances in Cryptology - CRYPTO 1995","author":"R. Anderson","year":"1995","unstructured":"Anderson, R., Needham, R.: Robustness principles for public key protocols. In: Coppersmith, D. (ed.) CRYPTO 1995. LNCS, vol.\u00a0963, pp. 236\u2013247. Springer, Heidelberg (1995)"},{"issue":"1","key":"11_CR12","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1145\/77648.77649","volume":"8","author":"M. Burrows","year":"1990","unstructured":"Burrows, M., Abadi, M., Needham, R.: A logic of authentication. ACM Transactions on Computer Systems\u00a08(1), 18\u201336 (1990)","journal-title":"ACM Transactions on Computer Systems"},{"issue":"1","key":"11_CR13","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1109\/90.222903","volume":"1","author":"M.B. Abbott","year":"1993","unstructured":"Abbott, M.B., Peterson, L.L.: A language-based approach to protocol implementation. IEEE\/ACM Transactions on Networking\u00a01(1), 4\u201319 (1993)","journal-title":"IEEE\/ACM Transactions on Networking"},{"key":"11_CR14","unstructured":"Durgin, N., Lincoln, P., Mitchell, J., Scedro, A.: Undevidability of bounded security protocols. In: Heintze, N., Clark, E. (eds.) Proceedings of the Workshop on Formal Methods and Security Protocols, Trento, Italy (1999)"},{"issue":"3","key":"11_CR15","doi-asserted-by":"crossref","first-page":"317","DOI":"10.3233\/JCS-1992-13-407","volume":"1","author":"P.F. Syverson","year":"1992","unstructured":"Syverson, P.F.: Knowledge, belief, and semantics in the analysis of cryptographic protocols. Journal of Computer Security\u00a01(3), 317\u2013334 (1992)","journal-title":"Journal of Computer Security"},{"key":"11_CR16","unstructured":"Parnas, D.: Software aging. In: Proceedings of the 16th international conference on Software engineering, Sorrento, Italy, pp. 279\u2013287 (1994)"},{"key":"11_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/3-540-39568-7_23","volume-title":"Advances in Cryptology","author":"J.R. Blum","year":"1985","unstructured":"Blum, J.R., Goldwasser, S.: An efficient probabilistic public-key encryption scheme which hides all partial information. In: Blakely, G.R., Chaum, D. (eds.) CRYPTO 1984. LNCS, vol.\u00a0196, pp. 289\u2013302. Springer, Heidelberg (1985)"},{"key":"11_CR18","unstructured":"Goldwasser, S., Micali, S.: Probabilistic encryption and hos to play mental poker. In: Proceedings of the 14th ACM Symposium on the Theory of Computing (1982)"},{"issue":"4","key":"11_CR19","doi-asserted-by":"crossref","first-page":"581","DOI":"10.3233\/JCS-2003-11405","volume":"11","author":"J.Y. Halpern","year":"2004","unstructured":"Halpern, J.Y., van der Meyden, R.: A logical reconstruction of spki. Journal of Computer Security\u00a011(4), 581\u2013613 (2004)","journal-title":"Journal of Computer Security"},{"issue":"1","key":"11_CR20","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1109\/32.481513","volume":"22","author":"M. Abadi","year":"1996","unstructured":"Abadi, M., Needham, R.: Prudent engineering practice for cryptographic protocols. IEEE Transactions on Software Engineering\u00a022(1), 6\u201315 (1996)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"11_CR21","volume-title":"PCSFW: Proceedings of The 12th Computer Security Foundations Workshop","author":"J.Y. Halpern","year":"1999","unstructured":"Halpern, J.Y., van der Meyden, R.: A logic for SDSI\u2019s linked local name spaces. In: PCSFW: Proceedings of The 12th Computer Security Foundations Workshop. IEEE Computer Society Press, Los Alamitos (1999)"},{"key":"11_CR22","unstructured":"Myrvang, P.H.: An infrastructure for authentication, authorization and delegation. Cand. scient. thesis, Dept. Computer Science, University of Troms\u00f8, Norway (2000)"},{"key":"11_CR23","doi-asserted-by":"crossref","unstructured":"Abadi, M., Tuttle, M.: A Semantics for a Logic of Authentication. In: Proceedings of the 10th Annual ACM Symposium on Principles of Distributed Computing, pp. 201\u2013216 (1991)","DOI":"10.1145\/112600.112618"},{"key":"11_CR24","unstructured":"Andersen, A., Blair, G.S., Eliassen, F.: A reflective component-based middleware with quality of service management. In: PROMS 2000, Protocols for Multimedia Systems, Cracow, Poland (2000)"},{"key":"11_CR25","volume-title":"Practical Cryptography for Data Internetworks","author":"M. Burrows","year":"1989","unstructured":"Burrows, M., Abadi, M., Needham, R.: A logic of authentication, from proceedings of the royal society. In: Stallings, W. (ed.) Practical Cryptography for Data Internetworks, vol.\u00a0426(1871). IEEE Computer Society Press, Los Alamitos (1989)"},{"key":"11_CR26","doi-asserted-by":"crossref","unstructured":"Bellovin, S., Merritt, M.: Encrypted key exchange: Password-based protocols secure against dictionary attacks. In: Proceedings of the IEEE Symposium on Research in Security and Privacy, Oakland (1992)","DOI":"10.1145\/168588.168618"},{"key":"11_CR27","volume-title":"Smart Card Handbook","author":"W. Rankl","year":"2000","unstructured":"Rankl, W., Effing, W.: Smart Card Handbook, 2nd edn. John Wiley & Sons, Chichester (2000), ISBN 0-471-98875-8","edition":"2"},{"issue":"2","key":"11_CR28","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1016\/0167-6423(93)90002-7","volume":"21","author":"M. Abadi","year":"1993","unstructured":"Abadi, M., Burrows, M., Kaufman, C., Lampson, B.: Authentication and delegation with smart-cards. Science of Computer Programming\u00a021(2), 93\u2013113 (1993)","journal-title":"Science of Computer Programming"},{"key":"11_CR29","unstructured":"Stabell-Kul\u00f8, T., Arild, R., Myrvang, P.H.: Providing authentication to messages signed with a smart card in hostile environments. In: Proceedings from the USENIX Workshop on Smartcard Technology, pp. 93\u201399 (1999)"},{"key":"11_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/BFb0000430","volume-title":"Advances in Cryptology \u2013 Asiacrypt\u201994","author":"C. Meadows","year":"1995","unstructured":"Meadows, C.: Formal Verification of Cryptographic Protocols: A Survey. In: Safavi-Naini, R., Pieprzyk, J.P. (eds.) ASIACRYPT 1994. LNCS, vol.\u00a0917, pp. 133\u2013150. Springer, Heidelberg (1995)"},{"issue":"2","key":"11_CR31","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/0743-1066(95)00095-X","volume":"26","author":"C. Meadows","year":"1996","unstructured":"Meadows, C.: The NRL Protocol Analyzer: An Overview. The Journal of Logic Programming\u00a026(2), 113\u2013131 (1996)","journal-title":"The Journal of Logic Programming"},{"key":"11_CR32","doi-asserted-by":"crossref","unstructured":"Gong, L., Needham, R., Yahalom, R.: Reasoning about Belief in Cryptographic Protocols. In: Proceedings of the IEEE 1990 Symposium on Security and Privacy, Oakland, California, pp. 234\u2013248 (1990)","DOI":"10.1109\/RISP.1990.63854"},{"key":"11_CR33","doi-asserted-by":"crossref","unstructured":"Syverson, P.F., van Oorschot, P.C.: A unified cryptographic protocol logic. CHACS Report 5540-227, Naval Research Laboratory, Washington, USA (1996); Parts of this paper appeared in preliminary form in [52] and [53]","DOI":"10.21236\/ADA464967"},{"key":"11_CR34","unstructured":"Brickin, S.H.: Automatically detecting most vulnerabilities in cryptographic protocols. In: DARPA Information Survivability Conference and Exposition, Hilton Head Island, SC, USA (2000)"},{"key":"11_CR35","first-page":"23","volume-title":"The formal description technique LOTOS","author":"T. Bolognesi","year":"1989","unstructured":"Bolognesi, T., Brinksma, E.: Introduction to the ISO specification language LOTOS. In: van Eijk, P.H.J., Visser, C.A., Diaz, M. (eds.) The formal description technique LOTOS, pp. 23\u201373. North-Holland, Amsterdam (1989)"},{"key":"11_CR36","unstructured":"ISO: Information processing systems \u2014 Open systems interconnection \u2014 Estelle \u2014 a formal description technique based on an extended state transition model (1989)"},{"key":"11_CR37","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-69962-7","volume-title":"Fundamentals of Algebraic Specification 1: Equations and Initial Semantics","author":"H. Ehrig","year":"1985","unstructured":"Ehrig, H., Mahr, B.: Fundamentals of Algebraic Specification 1: Equations and Initial Semantics. Springer, Heidelberg (1985)"},{"key":"11_CR38","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)"},{"issue":"79","key":"11_CR39","first-page":"1293","volume":"9","author":"F. Boussinot","year":"1991","unstructured":"Boussinot, F., de Simone, R.: The ESTEREL language. IEEE Transactions on Software Engineering\u00a09(79), 1293\u20131304 (1991)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"11_CR40","doi-asserted-by":"crossref","unstructured":"Berry, G., Gonthier, G.: The ESTREL synchronous programming language: Design, semantics, implementation. Science of Computer Programming\u00a02(19) (1992)","DOI":"10.1016\/0167-6423(92)90005-V"},{"key":"11_CR41","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1109\/ISCC.2002.1021701","volume-title":"Proceedings of the Seventh IEEE Symposium on Computers and Communications","author":"L. Mengual","year":"2002","unstructured":"Mengual, L., Barcia, N., Jim\u00e9nez, E., Menasalvas, E., Seti\u00e9n, J., Y\u00e1g\u00fcez, J.: Automatic implementation system of security protocols based on formal description techniques. In: Corradi, A., Daneshmand, M. (eds.) Proceedings of the Seventh IEEE Symposium on Computers and Communications, pp. 355\u2013360. IEEE Computer Society, Los Alamitos (2002)"},{"key":"11_CR42","first-page":"64","volume-title":"Proceedings of the Symposium on Application - Specific Systems and Software Engineering and Technology","author":"S. Brackin","year":"1999","unstructured":"Brackin, S., Meadows, C., Millen, J.: Capsl interface for the nrl protocol analyzer. In: Proceedings of the Symposium on Application - Specific Systems and Software Engineering and Technology, pp. 64\u201373. IEEE, Los Alamitos (1999)"},{"key":"11_CR43","unstructured":"Millen, J., Muller, F.: Cryptograpic protocol generation from capsl. SRI Techical Report SRI-CSL-07-01, Computer Science Laboratory, SRI international (2001)"},{"key":"11_CR44","unstructured":"Perrig, A., Phan, D., Song, D.X.: ACG-automatic code generation. Automatic implementation of a security protocol. Techical Report 00-1120, UC Berkeley (2000); This technical report was never issued"},{"key":"11_CR45","unstructured":"Perrig, A., Song, D.: A first step towards the automatic generation of security protocols. In: Network and Distributed System Security Symposium, NDSS\u00a02000, pp. 73\u201384 (2000)"},{"key":"11_CR46","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1109\/DISCEX.2003.1194888","volume-title":"DISCEX III, DARPA Information Survivability Conference and Exposition","author":"J. Millen","year":"2003","unstructured":"Millen, J., Denker, G.: Mucapsl. In: DISCEX III, DARPA Information Survivability Conference and Exposition, pp. 238\u2013249. IEEE Computer Society, Los Alamitos (2003)"},{"key":"11_CR47","doi-asserted-by":"crossref","unstructured":"Kohler, E., Kaashoek, M.F., Montgomery, D.R.: A readable TCP in the Prolac protocol language. In: ACM SIGCOMM, pp. 3\u201313 (1999)","DOI":"10.1145\/316194.316200"},{"key":"11_CR48","doi-asserted-by":"crossref","unstructured":"MacKenzie, P., Oprea, A., Reiter, M.K.: Automatic generation of two-party computations. In: Proceedings of the 10th ACM conference on Computer and communication security, Washington D.C., USA, pp. 210\u2013219 (2003)","DOI":"10.1145\/948109.948139"},{"issue":"4","key":"11_CR49","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1145\/227210.227229","volume":"39","author":"R. van Renesse","year":"1996","unstructured":"van Renesse, R., Birman, K.P., Maffeis, S.: Horus: A flexible group communication system. Communications of the ACM\u00a039(4), 76\u201383 (1996)","journal-title":"Communications of the ACM"},{"key":"11_CR50","unstructured":"McDaniel, P.D., Prakash, A., Honeyman, P.: Antigone: A flexible framework for secure group communication. In: Proceedings of the 8th USENIX Security Symposium, pp. 99\u2013114 (1999)"},{"issue":"9","key":"11_CR51","first-page":"1614","volume":"17","author":"B. Stiller","year":"1999","unstructured":"Stiller, B., Class, C., Waldvogel, M., Caronni, G., Bauer, D., Plattner, B.: A flexible middleware for multimedia communication: Design implementation, and experience. IEEE JSAC: Special Issue on Middleware\u00a017(9), 1614\u20131631 (1999)","journal-title":"IEEE JSAC: Special Issue on Middleware"},{"key":"11_CR52","doi-asserted-by":"crossref","unstructured":"van Oorschot, P.C.: Extending cryptographic logics of beliefs to key agreement protocols (extended abstract). In: Proceedings of the First ACM Conference on Computer and Communication Security, pp. 232\u2013243 (1993)","DOI":"10.1145\/168588.168617"},{"key":"11_CR53","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1109\/RISP.1994.296595","volume-title":"Proceedings of the 1994 IEEE Computer Society Symposium on Research in Security and Privacy","author":"P.F. Syverson","year":"1994","unstructured":"Syverson, P.F., van Oorschot, P.C.: On unifying some cryptographic protocol logics. In: Proceedings of the 1994 IEEE Computer Society Symposium on Research in Security and Privacy, Los Alamitos, California, USA, pp. 14\u201328. IEEE Computer Society Press, Los Alamitos (1994)"}],"container-title":["Lecture Notes in Computer Science","Security Protocols"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-04904-0_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,9]],"date-time":"2020-01-09T00:34:34Z","timestamp":1578530074000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-04904-0_11"}},"subtitle":["The Obol Protocol Language"],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642049033","9783642049040"],"references-count":54,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-04904-0_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}