{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T17:10:03Z","timestamp":1746292203740,"version":"3.40.4"},"reference-count":48,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2014,7,3]],"date-time":"2014-07-03T00:00:00Z","timestamp":1404345600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int. J. Inf. Secur."],"published-print":{"date-parts":[[2015,6]]},"DOI":"10.1007\/s10207-014-0243-z","type":"journal-article","created":{"date-parts":[[2014,7,2]],"date-time":"2014-07-02T11:12:40Z","timestamp":1404299560000},"page":"221-247","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Analysis of two authorization protocols using Colored Petri Nets"],"prefix":"10.1007","volume":"14","author":[{"given":"Younes","family":"Seifi","sequence":"first","affiliation":[]},{"given":"Suriadi","family":"Suriadi","sequence":"additional","affiliation":[]},{"given":"Ernest","family":"Foo","sequence":"additional","affiliation":[]},{"given":"Colin","family":"Boyd","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,7,3]]},"reference":[{"issue":"1\u20132","key":"243_CR1","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.scico.2005.02.002","volume":"58","author":"M Abadi","year":"2005","unstructured":"Abadi, M., Blanchet, B.: Computer-assisted verification of a protocol for certified email. Sci. Comput. Program. 58(1\u20132), 3\u201327 (2005)","journal-title":"Sci. Comput. Program."},{"key":"243_CR2","unstructured":"Al-Azzoni, I.: The verification of cryptographic protocols using Coloured Petri Nets. Master\u2019s thesis, Department of Software Engineering (2004)"},{"issue":"3","key":"243_CR3","first-page":"200","volume":"12","author":"Issam Al-Azzoni","year":"2005","unstructured":"Al-Azzoni, Issam, Down, Douglas G., Kh\u00e9dri, Ridha: Modeling and verification of cryptographic protocols using Coloured Petri Nets and Design\/CPN. Nord. J. Comput. 12(3), 200\u2013228 (2005)","journal-title":"Nord. J. Comput."},{"key":"243_CR4","unstructured":"Aly, S., Mustafa, K.: Protocol verification and analysis using Colored Petri Nets. Depaul University (2003)"},{"key":"243_CR5","doi-asserted-by":"crossref","unstructured":"Bellare, M., Canetti, R., Krawczyk. H.: A modular approach to the design and analysis of authentication and key exchange protocols. In: Proceedings of the Thirtieth Annual ACM Symposium on Theory of Computing, pp. 419\u2013428. ACM (1998)","DOI":"10.1145\/276698.276854"},{"key":"243_CR6","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In CSFW, number 0\u20137695-1146-5, pp. 82\u201396. IEEE Computer Society (2001)","DOI":"10.1109\/CSFW.2001.930138"},{"key":"243_CR7","doi-asserted-by":"crossref","unstructured":"Bozga, L., Lakhnech, Y., P\u00e9rin, M.: Hermes: An automatic tool for verification of secrecy in security protocols. In: Computer Aided Verification, pp. 219\u2013222. Springer (2003)","DOI":"10.1007\/978-3-540-45069-6_23"},{"key":"243_CR8","unstructured":"Brackin, S.H.: A HOL extension of GNY for automatically analyzing cryptographic protocols. In: Computer Security Foundations Workshop, 1996. Proceedings., 9th IEEE, pp. 62\u201376. IEEE (1996)"},{"issue":"1","key":"243_CR9","doi-asserted-by":"crossref","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 Trans. Comput. Syst. 8(1), 18\u201336 (1990)","journal-title":"ACM Trans. Comput. Syst."},{"key":"243_CR10","doi-asserted-by":"crossref","unstructured":"Chen, L., Ryan, M.: Attack, solution and verification for shared authorisation data in TCG TPM. In: Formal Aspects in Security and Trust, pp. 201\u2013216 (2010)","DOI":"10.1007\/978-3-642-12459-4_15"},{"key":"243_CR11","doi-asserted-by":"crossref","unstructured":"Chen, L., Ryan, M.: Offline dictionary attack on TCG TPM weak authorisation data, and solution. In: Gawrock, D., Reimer, H., Sadeghi, A.-R., Vishik, C. (eds.) Future of Trust in Computing, pp. 193\u2013196 . Vieweg+Teubner (2009)","DOI":"10.1007\/978-3-8348-9324-6_20"},{"key":"243_CR12","doi-asserted-by":"crossref","unstructured":"Cheng, A., Christensen, S., Mortensen, K.H.: Model checking Coloured Petri Nets exploiting strongly connected components. Citeseer (1997)","DOI":"10.7146\/dpb.v26i519.7048"},{"key":"243_CR13","unstructured":"Christensen, S., Mortensen, K.H.: Design\/CPN ASK-CTL Manual (1996)"},{"key":"243_CR14","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8(2), 244\u2013263 (1986)","DOI":"10.1145\/5397.5399"},{"key":"243_CR15","doi-asserted-by":"crossref","unstructured":"Cremers, C.J.F.: The Scyther Tool: verification, falsification, and analysis of security protocols. In: Computer Aided Verification, pp. 414\u2013418. Springer (2008)","DOI":"10.1007\/978-3-540-70545-1_38"},{"key":"243_CR16","unstructured":"Doyle, E.M.: Automated security analysis of cryptographic protocols using Coloured Petri Net specifications (1997)"},{"key":"243_CR17","doi-asserted-by":"crossref","unstructured":"Dutertre, B., Schneider, S.: Using a PVS embedding of CSP to verify authentication protocols. In: Theorem Proving in Higher Order Logics, pp. 121\u2013136 (1997)","DOI":"10.1007\/BFb0028390"},{"key":"243_CR18","doi-asserted-by":"crossref","unstructured":"Fontan, B., Mota, S., Villemur, T., Saqui-Sannes, P., Courtiat, J.P.: UML-based modeling and formal verification of authentication protocols (2006)","DOI":"10.1145\/1095921.1095981"},{"key":"243_CR19","doi-asserted-by":"crossref","unstructured":"Gong, L., Needham, R., Yahalom, R.: Reasoning about belief in cryptographic protocols. In: Research in Security and Privacy, 1990. Proceedings., 1990 IEEE Computer Society Symposium on, pp. 234\u2013248. IEEE (1990)","DOI":"10.1109\/RISP.1990.63854"},{"key":"243_CR20","unstructured":"Hollestelle, G., Mauw, S., Cremers, C. J. F.: Systematic analysis of attacks on security protocols. Master\u2019s Thesis, Technical University of Eindhover, Department of Mathematics and Computer Science (2005)"},{"key":"243_CR21","unstructured":"ISO\/IEC 18033\u20132.: Information technology\u2014Security techni- ques\u2014Encryption algorithms\u2014part 2: Asymetric ciphers (2006) http:\/\/www.iso.org\/iso\/home\/store\/catalogue_tc\/catalogue_detail.htm?csnumber=37971"},{"key":"243_CR22","unstructured":"ISO\/IEC 18033\u20133.: Information technology\u2014Security techni- ques\u2014Encryption algorithms\u2014part 3: Block ciphers (2005) http:\/\/www.iso.org\/iso\/home\/store\/catalogue_ics\/catalogue_detail_ics.htm?csnumber=37972"},{"key":"243_CR23","unstructured":"ISO\/IEC 19772.: Information technology\u2014Security techniques\u2014 Authenticated encryption (2009) http:\/\/www.iso.org\/iso\/catalogue_detail?csnumber=46345"},{"key":"243_CR24","unstructured":"ISO\/IEC 9797\u20132.: Information technology\u2014security techniques\u2014Message Authentication Codes (MACs)\u2014part 2: Mechanisms using a dedicated hash-function (2002)"},{"key":"243_CR25","doi-asserted-by":"crossref","unstructured":"Jensen, K.: A brief introduction to Coloured Petri Nets. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 203\u2013208. Springer, Berlin, Heidelberg (1997)","DOI":"10.1007\/BFb0035389"},{"key":"243_CR26","unstructured":"Jensen, K.: Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use, volume 1, Basic Concepts. Monographs in Theoretical Computer Science. Springer, New York, 2nd corrected printing 1997, ISBN: 3-540-60943-1 (1997)"},{"key":"243_CR27","doi-asserted-by":"crossref","unstructured":"Jensen, K.: Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use., volume 2, Analysis Methods. Monographs in Theoretical Computer Science. Springer, New York, 2nd corrected printing 1997, ISBN: 3-540-58276-2 (1997)","DOI":"10.1007\/978-3-642-60794-3"},{"key":"243_CR28","doi-asserted-by":"crossref","unstructured":"Jensen, K.: Special section on Coloured Petri Nets. Int. J. Softw. Tools Technol. Transf. (STTT) 9(3), 209\u2013212 (2007)","DOI":"10.1007\/s10009-007-0039-9"},{"issue":"3","key":"243_CR29","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/s10009-007-0038-x","volume":"9","author":"K Jensen","year":"2007","unstructured":"Jensen, K., Kristensen, L.M., Wells, L.: Coloured Petri Nets and CPN tools for modelling and validation of concurrent systems. Int. J. Softw. Tools Technol. Transf. (STTT) 9(3), 213\u2013254 (2007)","journal-title":"Int. J. Softw. Tools Technol. Transf. (STTT)"},{"key":"243_CR30","doi-asserted-by":"crossref","DOI":"10.1007\/b95112","volume-title":"Coloured Petri Nets\u2014Modelling and Validation of Concurrent Systems","author":"K Jensen","year":"2009","unstructured":"Jensen, K., Kristensen, L.M.: Coloured Petri Nets\u2014Modelling and Validation of Concurrent Systems. Springer, Berlin (2009)"},{"issue":"3","key":"243_CR31","doi-asserted-by":"crossref","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":"243_CR32","doi-asserted-by":"crossref","unstructured":"Meadows, C.A.: Formal verification of cryptographic protocols: A survey. Advances in Cryptology\u2014ASIACRYPT\u201994, pp. 133\u2013150 (1995)","DOI":"10.1007\/BFb0000430"},{"issue":"2","key":"243_CR33","doi-asserted-by":"crossref","first-page":"274","DOI":"10.1109\/TSE.1987.233151","volume":"SE\u201313","author":"JK Millen","year":"1987","unstructured":"Millen, J.K., Clark, S.C., Freedman, S.B.: The interrogator: Protocol security analysis. IEEE Trans. Softw. Eng. SE\u201313(2), 274\u2013288 (1987)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"243_CR34","doi-asserted-by":"crossref","unstructured":"Mitchell, C.: Trusted computing, volume 6. Iet (2005)","DOI":"10.1049\/PBPC006E"},{"key":"243_CR35","unstructured":"Rubin, A.D., Honeyman, P.: Formal Methods for the Analysis of Authentication Protocols. Technical report, Citeseer (1993)"},{"issue":"9","key":"243_CR36","doi-asserted-by":"crossref","first-page":"741","DOI":"10.1109\/32.713329","volume":"24","author":"S Schneider","year":"1998","unstructured":"Schneider, S.: Verifying authentication protocols in CSP. IEEE Trans. Softw. Eng. 24(9), 741\u2013758 (1998)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"243_CR37","unstructured":"Seifi, Y., Suriadi, S., Foo, E., Boyd, C.: Analysis of Object-Specific Authorization Protocol (OSAP) using Coloured Petri Net. In: AISC2012 Proceedings (2012)"},{"key":"243_CR38","unstructured":"Seifi, Y., Suriadi, S., Foo, E., Boyd, C.: Analysis of Object-Specific Authorization Protocol (OSAP) using Coloured Petri Nets\u2014version 1.0. Technical report, Queensland University of Technology (2011)"},{"key":"243_CR39","unstructured":"Tarigan, A. et al.: Survey in Formal Analysis of Security Properties of Cryptographic Protocol. Universit\u00e4t Bielefeld (2002)"},{"key":"243_CR40","unstructured":"TCG.: TCG Specification Architecture Overview Revision 1.4 (2007)"},{"key":"243_CR41","unstructured":"TCG.: TCG TPM specification 1.2, http:\/\/www.trustedcomputinggroup.org (2003)"},{"key":"243_CR42","unstructured":"TCG.: TCG TPM specification 2.0, http:\/\/www.trustedcomputinggroup.org\/resources\/-trusted_platform_module_specifications_in_public_review (2013)"},{"key":"243_CR43","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1016\/j.entcs.2005.11.052","volume":"155","author":"Luca Vigan\u00f2","year":"2006","unstructured":"Vigan\u00f2, Luca: Automated security protocol analysis with the AVISPA tool. Electron. Notes Theor. Comput. Sci. 155, 61\u201386 (2006)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"243_CR44","doi-asserted-by":"crossref","unstructured":"Westergaard, M., Evangelista, S., Kristensen, L.: ASAP: An extensible platform for state space analysis. Applications and theory of petri nets, pp. 303\u2013312 (2009)","DOI":"10.1007\/978-3-642-02424-5_18"},{"key":"243_CR45","doi-asserted-by":"crossref","unstructured":"Westergaard, M., Maggi, F.M.: Modeling and verification of a protocol for operational support using coloured petri nets. Applications and Theory of Petri Nets. volume 6709 of Lecture Notes in Computer Science, pp. 169\u2013188. Springer, Berlin\/Heidelberg (2011)","DOI":"10.1007\/978-3-642-21834-7_10"},{"key":"243_CR46","doi-asserted-by":"crossref","unstructured":"Woo, T.Y.C., Lam, S.S.: A semantic model for authentication protocols. In: Research in Security and Privacy, 1993. Proceedings., 1993 IEEE Computer Society Symposium on, pp. 178\u2013194. IEEE (1993)","DOI":"10.1109\/RISP.1993.287633"},{"key":"243_CR47","doi-asserted-by":"crossref","unstructured":"Woo, T.Y.C., Lam, S.S.: Verifying authentication protocols: Methodology and example. In Network Protocols, 1993. Proceedings., 1993 International Conference on, pp. 36\u201345. IEEE (1993)","DOI":"10.1109\/ICNP.1993.340904"},{"issue":"2","key":"243_CR48","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"29","author":"A Yao","year":"1983","unstructured":"Yao, A.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198\u2013208 (1983)","journal-title":"IEEE Trans. Inf. Theory"}],"container-title":["International Journal of Information Security"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10207-014-0243-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10207-014-0243-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10207-014-0243-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T16:55:59Z","timestamp":1746291359000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10207-014-0243-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,7,3]]},"references-count":48,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2015,6]]}},"alternative-id":["243"],"URL":"https:\/\/doi.org\/10.1007\/s10207-014-0243-z","relation":{},"ISSN":["1615-5262","1615-5270"],"issn-type":[{"type":"print","value":"1615-5262"},{"type":"electronic","value":"1615-5270"}],"subject":[],"published":{"date-parts":[[2014,7,3]]}}}