{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,15]],"date-time":"2025-08-15T00:16:50Z","timestamp":1755217010263,"version":"3.43.0"},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1999,3,1]],"date-time":"1999-03-01T00:00:00Z","timestamp":920246400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1999,3,1]],"date-time":"1999-03-01T00:00:00Z","timestamp":920246400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Formal Methods in System Design"],"published-print":{"date-parts":[[1999,3]]},"DOI":"10.1023\/a:1008683519655","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T10:12:40Z","timestamp":1040551960000},"page":"171-191","source":"Crossref","is-referenced-by-count":9,"title":["Model-Based Verification of a Security Protocol for Conditional Access to Services"],"prefix":"10.1007","volume":"14","author":[{"given":"G.","family":"Leduc","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"O.","family":"Bonaventure","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"L.","family":"L\u00e9onard","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"E.","family":"Koerner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"C.","family":"Pecheur","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"200089_CR1","doi-asserted-by":"crossref","unstructured":"M. Abadi and A. Gordon, \u201cA calculus for cryptographic protocols\u2014The spi calculus,\u201d in Proc. of the 4th ACM Conference on Computer and Communications Security, 1997.","DOI":"10.1145\/266420.266432"},{"key":"200089_CR2","doi-asserted-by":"crossref","unstructured":"D. Bolignano, \u201cFormal verification of cryptographic protocols,\u201d in Proc. of the 3rd ACM Conference on Computer and Communication Security, 1996.","DOI":"10.1145\/238168.238196"},{"key":"200089_CR3","doi-asserted-by":"crossref","unstructured":"D. Bolignano, \u201cTowards a mechanization of cryptographic protocol verification,\u201d in Proc. of CAV 97, LNCS 1254, Springer-Verlag, 1997.","DOI":"10.1007\/3-540-63166-6_15"},{"issue":"1","key":"200089_CR4","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1016\/0169-7552(87)90085-7","volume":"14","author":"T. Bolognesi","year":"1987","unstructured":"T. Bolognesi and E. Brinksma, \u201cIntroduction to the ISO specification language LOTOS,\u201d Computer Networks and ISDN Systems, Vol. 14,No. 1, pp. 25\u201359, 1987.","journal-title":"Computer Networks and ISDN Systems"},{"key":"200089_CR5","volume-title":"18th ICALP","author":"A. Bouajjani","year":"1991","unstructured":"A. Bouajjani, J.-C. Fernandez, S. Graf, C. Rodriguez, and J. Sifakis, \u201cSafety for branching time semantics,\u201d in 18th ICALP, Springer-Verlag, Berlin, July 1991."},{"key":"200089_CR6","doi-asserted-by":"crossref","unstructured":"M. Burrows, M. Abadi, and R. Needham, \u201cAlogic of authentication,\u201d ACM Transactions on Computer Systems, Vol. 8, 1990.","DOI":"10.1145\/77648.77649"},{"key":"200089_CR7","doi-asserted-by":"crossref","unstructured":"P. Chen and V. Gligor, \u201cOn the formal specification and verification of a multiparty session protocol,\u201d in Proc. of the IEEE Symposium on Research in Security and Privacy, 1990.","DOI":"10.1109\/RISP.1990.63853"},{"key":"200089_CR8","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1016\/S0019-9958(82)90401-6","volume":"55","author":"D. Dolev","year":"1982","unstructured":"D. Dolev, S. Even, and R. Karp, \u201cOn the security of ping-pong protocols,\u201d Information and Control, Vol. 55, pp. 57\u201368, 1982.","journal-title":"Information and Control"},{"issue":"2","key":"200089_CR9","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"29","author":"D. Dolev","year":"1983","unstructured":"D. Dolev and A. Yao, \u201cOn the security of public key protocols,\u201d IEEE Transactions on Information Theory, Vol. 29,No. 2, pp. 198\u2013208, March 1983.","journal-title":"IEEE Transactions on Information Theory"},{"key":"200089_CR10","unstructured":"H. Ehrig and B. Mahr, \u201cFundamentals of algebraic specification 1, equations and initial semantics,\u201d in W. Brauer, B. Rozenberg, and A. Salomaa (Eds.), EATCS, Monographs on Theoretical Computer Science, Springer Verlag, 1985."},{"key":"200089_CR11","doi-asserted-by":"crossref","unstructured":"J.-C. Fernandez, H. Garavel, A. Kerbrat, R. Mateescu, L. Mounier, and M. Sighireanu, \u201cCADP (C\u00c6SAR\/ALDEBARAN development package): A protocol validation and verification toolbox,\u201d in R. Alur and T. Henzinger (Eds.), in Proc. of the 8th Conference on Computer-Aided Verification, New Brunswick, New Jersey, USA, Aug. 1996.","DOI":"10.1007\/3-540-61474-5_97"},{"key":"200089_CR12","unstructured":"H. Garavel, \u201cAn overview of the eucalyptus toolbox, in Proc. of the COST247 Workshop,\u201d Maribor, Slovenia, June 1996."},{"key":"200089_CR13","volume-title":"Proc. of the DIMACS Workshop on Design and Formal Verification of Security Protocols","author":"F. Germeau","year":"1997","unstructured":"F. Germeau and G. Leduc, \u201cModel-based design and verification of security protocols using LOTOS,\u201d in Proc. of the DIMACS Workshop on Design and Formal Verification of Security Protocols, Rutgers University, NJ, USA, Sept. 1997."},{"key":"200089_CR14","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1007\/978-0-387-35271-8_9","volume-title":"Formal Description Techniques and Protocol Specification, Testing and Verification, FORTE\/PSTV' 97","author":"F. Germeau","year":"1997","unstructured":"F. Germeau and G. Leduc, \u201cA computer-aided design of a secure registration protocol,\u201d Formal Description Techniques and Protocol Specification, Testing and Verification, FORTE\/PSTV' 97, Chapman & Hall, London, pp. 145\u2013160, 1997."},{"key":"200089_CR15","doi-asserted-by":"crossref","unstructured":"L. Guillou and J.-J. Quisquater, \u201cA practical zero-knowledge protocol fitted to security microprocessor minimizing both transmission and memory,\u201d in Proc. of Eurocrypt'88, LNCS 330, Springer-Verlag, pp. 123\u2013128.","DOI":"10.1007\/3-540-45961-8_11"},{"key":"200089_CR16","unstructured":"J. Guimaraes, J.-M. Boucqueau, and B. Macq, \u201cOKAPI: A Kernel for access control to multimedia services based on trusted third parties,\u201d in Proc. of ECMAST 96\u2014European Conference on Multimedia Applications, Services and Techniques, Louvain-la-Neuve, Belgium, pp. 783\u2013798, May 1996."},{"key":"200089_CR17","unstructured":"C.A.R. Hoare, Communicating Sequential Processes, Prentice-Hall International, 1985."},{"key":"200089_CR18","unstructured":"ISO\/IEC, Information Processing Systems\u2014Open Systems Interconnection\u2014LOTOS, a Formal Description Technique Based on the Temporal Ordering of Observational Behaviour. IS 8807, Feb. 1989."},{"issue":"4","key":"200089_CR19","doi-asserted-by":"crossref","first-page":"448","DOI":"10.1109\/49.17707","volume":"7","author":"R. Kemmerer","year":"1989","unstructured":"R. Kemmerer, \u201cUsing formal methods to analyse encryption protocols,\u201d IEEE Journal on Selected Areas in Communications, Vol. 7,No. 4, pp. 448\u2013457, 1989.","journal-title":"IEEE Journal on Selected Areas in Communications"},{"issue":"2","key":"200089_CR20","first-page":"14","volume":"7","author":"R. Kemmerer","year":"1989","unstructured":"R. Kemmerer, C. Meadows, and J. Millen, \u201cThree systems for cryptographic protocol analysis,\u201d Journal of Cryptology, Vol. 7,No. 2, pp. 14\u201318, 1989.","journal-title":"Journal of Cryptology"},{"key":"200089_CR21","unstructured":"S. Lacroix, J.-M. Boucqueau, J.-J. Quisquater, and B. Macq, \u201cProviding equitable conditional access by use of trusted third parties,\u201d in Proc. of ECMAST 96\u2014European Conference on Multimedia Applications, Services and Techniques, Louvain-la-Neuve, Belgium, pp. 763\u2013782, May 1996."},{"key":"200089_CR22","unstructured":"G. Leduc, O. Bonaventure, E. Koerner, L. L\u00e9onard, C. Pecheur, and D. Zanetti, \u201cSpecification and verification of a TTP protocol for the conditional access to services,\u201d in Proc. of 12th J. Cartier Workshop on Formal Methods and their Applications: Telecommunications, VLSI and Real-Time Computerized Control System, Montreal, Canada, Oct. 1996."},{"key":"200089_CR23","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1016\/0020-0190(95)00144-2","volume":"56","author":"G. Lowe","year":"1995","unstructured":"G. Lowe, \u201cAn attack on the Needham-Schroeder public-key authentication protocol,\u201d Information Processing Letters, Vol. 56, pp. 131\u2013133, 1995.","journal-title":"Information Processing Letters"},{"key":"200089_CR24","doi-asserted-by":"crossref","unstructured":"G. Lowe, \u201cBreaking and fixing the Needham-Schroeder public-key protocol using FDR,\u201d in T. Margaria and B. Steffen (Eds.), Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1055, Springer-Verlag, 1996.","DOI":"10.1007\/3-540-61042-1_43"},{"key":"200089_CR25","doi-asserted-by":"crossref","unstructured":"C. Meadows, \u201cApplying formal methods to the analysis of a key management protocol,\u201d Journal of Computer Security, 1992.","DOI":"10.3233\/JCS-1992-1102"},{"issue":"8","key":"200089_CR26","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1016\/0743-1066(95)00095-X","volume":"26","author":"C. Meadows","year":"1996","unstructured":"C. Meadows, \u201cThe NRL protocol analyser: An overview,\u201d Journal of Logic Programming, Vol. 26,No. 8, pp. 113\u2013131, 1996.","journal-title":"Journal of Logic Programming"},{"key":"200089_CR27","doi-asserted-by":"crossref","unstructured":"C. Meadows, \u201cFormal verification of cryptographic protocols: A survey,\u201d in Proc. of Asiacrypt 94, LNCS 917, pp. 133\u2013150, 1995.","DOI":"10.1007\/BFb0000430"},{"key":"200089_CR28","doi-asserted-by":"crossref","unstructured":"J. Millen, S. Clark, and S. Freedman, \u201cThe interrogator: Protocol security analysis,\u201d IEEE Transactions on Software Engineering, Vol. SE-13,No. 2, 1987.","DOI":"10.1109\/TSE.1987.233151"},{"key":"200089_CR29","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"R. Milner, Communication and Concurrency, Prentice-Hall Intern., London, 1989."},{"key":"200089_CR30","unstructured":"C. Pecheur, \u201cImproving the specification of data types in LOTOS,\u201d Doctoral Dissertation, University of Li\u00e8ge, July 1996."},{"key":"200089_CR31","doi-asserted-by":"crossref","first-page":"120","DOI":"10.1145\/359340.359342","volume":"21","author":"R. Rivest","year":"1978","unstructured":"R. Rivest, A. Shamir, and L. Adleman, \u201cOn a method for obtaining digital signatures and public key cryptosystems,\u201d Communication of the ACM, Vol. 21, pp. 120\u2013126, Feb. 1978.","journal-title":"Communication of the ACM"},{"key":"200089_CR32","unstructured":"B. Stepien, J. Tourrilhes, and J. Sincennes, \u201cELUDO: The University of Ottawa Toolkit,\u201d Technical Report, University of Ottawa, 1994. Obtainable by FTP at lotos.csi.uottawa.ca."},{"key":"200089_CR33","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1016\/0920-5489(89)90022-6","volume":"9","author":"V. Varadharajan","year":"1989","unstructured":"V. Varadharajan, \u201cUse of formal technique in the specification of authentication protocols,\u201d Computer Standards and Interfaces, Vol. 9, pp. 203\u2013215, 1989.","journal-title":"Computer Standards and Interfaces"},{"key":"200089_CR34","unstructured":"T. Woo and S. Lam, \u201cA semantic model for authentication protocols,\u201d in Proc. of IEEE Symposium on Research in Security and Privacy, 1993."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008683519655.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1008683519655\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008683519655.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T03:57:22Z","timestamp":1754366242000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1008683519655"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,3]]},"references-count":34,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1999,3]]}},"alternative-id":["200089"],"URL":"https:\/\/doi.org\/10.1023\/a:1008683519655","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[1999,3]]}}}