{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T08:14:24Z","timestamp":1725869664462},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319490991"},{"type":"electronic","value":"9783319491004"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-49100-4_2","type":"book-chapter","created":{"date-parts":[[2016,11,1]],"date-time":"2016-11-01T14:41:42Z","timestamp":1478011302000},"page":"32-61","source":"Crossref","is-referenced-by-count":1,"title":["Cross-Tool Semantics for Protocol Security Goals"],"prefix":"10.1007","author":[{"given":"Joshua D.","family":"Guttman","sequence":"first","affiliation":[]},{"given":"John D.","family":"Ramsdell","sequence":"additional","affiliation":[]},{"given":"Paul D.","family":"Rowe","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,11,2]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: 28th ACM Symposium on Principles of Programming Languages (POPL 2001), pp. 104\u2013115, January 2001","DOI":"10.1145\/360204.360213"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-3-319-25527-9_7","volume-title":"Programming Languages with Applications to Biology and Security","author":"O Almousa","year":"2015","unstructured":"Almousa, O., M\u00f6dersheim, S., Vigan\u00f2, L.: Alice and Bob: reconciling formal models and implementation. In: Bodei, C., Ferrari, G.-L., Priami, C. (eds.) Programming Languages with Applications to Biology and Security. LNCS, vol. 9465, pp. 66\u201385. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-25527-9_7"},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/11513988_27","volume-title":"Computer Aided Verification","author":"A Armando","year":"2005","unstructured":"Armando, A., et al.: The AVISPA tool for the automated validation of internet security protocols and applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 281\u2013285. Springer, Heidelberg (2005). doi: 10.1007\/11513988_27"},{"key":"2_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-642-28756-5_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Armando","year":"2012","unstructured":"Armando, A., et al.: The AVANTSSAR platform for the automated validation of trust and security of service-oriented architectures. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 267\u2013282. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-28756-5_19"},{"issue":"3","key":"2_CR5","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1109\/MSP.2013.162","volume":"13","author":"DA Basin","year":"2015","unstructured":"Basin, D.A., Cremers, C.J.F., Miyazaki, K., Radomirovic, S., Watanabe, D.: Improving the security of cryptographic protocol standards. IEEE Secur. Priv. 13(3), 24\u201331 (2015)","journal-title":"IEEE Secur. Priv."},{"issue":"1","key":"2_CR6","doi-asserted-by":"crossref","first-page":"3","DOI":"10.3233\/JCS-2005-13102","volume":"13","author":"S Bistarelli","year":"2005","unstructured":"Bistarelli, S., Cervesato, I., Lenzini, G., Martinelli, F.: Relating multiset rewriting and process algebras for security protocol analysis. J. Comput. Secur. 13(1), 3\u201347 (2005)","journal-title":"J. Comput. Secur."},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: An efficient protocol verifier based on Prolog rules. In: 14th Computer Security Foundations Workshop, pp. 82\u201396. IEEE CS Press, June 2001","DOI":"10.1109\/CSFW.2001.930138"},{"key":"2_CR8","unstructured":"Blanchet, B.: V\u00e9rification automatique de protocoles cryptographiques: mod\u00e8le formel et mod\u00e8le calculatoire. Automatic verification of security protocols: formal model and computational model. M\u00e9moire d\u2019habilitation \u00e0 diriger des recherches, Universit\u00e9 Paris-Dauphine, November 2008"},{"key":"2_CR9","unstructured":"Blanchet, B., Smyth, B., Cheval, V.: ProVerif 1.93: Automatic Cryptographic Protocol Verifier. User Manual and Tutorial (2016)"},{"issue":"1871","key":"2_CR10","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1098\/rspa.1989.0125","volume":"426","author":"M Burrows","year":"1989","unstructured":"Burrows, M., Abadi, M., Needham, R.: A logic of authentication. Proc. R. Soc. Ser. A 426(1871), 233\u2013271 (1989)","journal-title":"Proc. R. Soc. Ser. A"},{"issue":"2","key":"2_CR11","doi-asserted-by":"crossref","first-page":"265","DOI":"10.3233\/JCS-2005-13203","volume":"13","author":"I Cervesato","year":"2005","unstructured":"Cervesato, I., Durgin, N.A., Lincoln, P.: A comparison between strand spaces and multiset rewriting for security protocol analysis. J. Comput. Secur. 13(2), 265\u2013316 (2005)","journal-title":"J. Comput. Secur."},{"issue":"1\u20133","key":"2_CR12","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/j.scico.2003.12.002","volume":"50","author":"H Comon","year":"2004","unstructured":"Comon, H., Cortier, V.: Security properties: two agents are sufficient. Sci. Comput. Program. 50(1\u20133), 51\u201371 (2004)","journal-title":"Sci. Comput. Program."},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/978-3-662-49635-0_11","volume-title":"Principles of Security and Trust","author":"V Cortier","year":"2016","unstructured":"Cortier, V., Dallon, A., Delaune, S.: Bounding the number of agents, for\u00a0equivalence too. In: Piessens, F., Vigan\u00f2, L. (eds.) POST 2016. LNCS, vol. 9635, pp. 211\u2013232. Springer, Heidelberg (2016). doi: 10.1007\/978-3-662-49635-0_11"},{"key":"2_CR14","unstructured":"Cortier, V., Kremer, S. (eds.): Formal Models and Techniques for Analyzing Security Protocols. Cryptology and Information Security Series. IOS Press (2011)"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Crazzolara, F., Winskel, G.: Events in security protocols. In: Proceedings of the 8th ACM Conference on Computer and Communications Security, CCS 2001, 6\u20138 November 2001, Philadelphia, Pennsylvania, USA, pp. 96\u2013105 (2001)","DOI":"10.7146\/brics.v8i13.20470"},{"key":"2_CR16","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-540-78636-8","volume-title":"Operational Semantics and Verification of Security Protocols","author":"C Cremers","year":"2012","unstructured":"Cremers, C., Mauw, S.: Operational Semantics and Verification of Security Protocols. Springer, Heidelberg (2012)"},{"key":"2_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/978-3-642-23822-2_18","volume-title":"Computer Security \u2013 ESORICS 2011","author":"C Cremers","year":"2011","unstructured":"Cremers, C.: Key exchange in IPsec revisited: formal analysis of IKEv1 and IKEv2. In: Atluri, V., Diaz, C. (eds.) ESORICS 2011. LNCS, vol. 6879, pp. 315\u2013334. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-23822-2_18"},{"key":"2_CR18","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1016\/j.entcs.2007.02.012","volume":"172","author":"A Datta","year":"2007","unstructured":"Datta, A., Derek, A., Mitchell, J.C., Roy, A.: Protocol composition logic (PCL). Electron. Notes Theoret. Comput. Sci. 172, 311\u2013358 (2007)","journal-title":"Electron. Notes Theoret. Comput. Sci."},{"issue":"2","key":"2_CR19","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1016\/0304-3975(92)90302-V","volume":"105","author":"JA Goguen","year":"1992","unstructured":"Goguen, J.A., Meseguer, J.: Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theoret. Comput. Sci. 105(2), 217\u2013273 (1992)","journal-title":"Theoret. Comput. Sci."},{"issue":"3\u20134","key":"2_CR20","doi-asserted-by":"crossref","first-page":"435","DOI":"10.3233\/JCS-2004-123-406","volume":"12","author":"AD Gordon","year":"2004","unstructured":"Gordon, A.D., Jeffrey, A.: Types, effects for asymmetric cryptographic protocols. J. Comput. Secur. 12(3\u20134), 435\u2013484 (2004)","journal-title":"J. Comput. Secur."},{"key":"2_CR21","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/9946.001.0001","volume-title":"Modeling and Analysis of Communicating Systems","author":"JF Groote","year":"2014","unstructured":"Groote, J.F., Mousavi, M.R.: Modeling and Analysis of Communicating Systems. MIT Press, Cambridge (2014)"},{"issue":"2","key":"2_CR22","doi-asserted-by":"crossref","first-page":"201","DOI":"10.3233\/JCS-140497","volume":"22","author":"JD Guttman","year":"2014","unstructured":"Guttman, J.D.: Establishing and preserving protocol security goals. J. Comput. Secur. 22(2), 201\u2013267 (2014)","journal-title":"J. Comput. Secur."},{"key":"2_CR23","unstructured":"ISO\/IEC 29128: Information Technology-Security techniques\u2013Verification of Cryptographic Protocols (2011)"},{"key":"2_CR24","doi-asserted-by":"crossref","unstructured":"Kremer, S., K\u00fcnnemann, R.: Automated analysis of security protocols with global state. In: 2014 IEEE Symposium on Security and Privacy, SP 2014, 18\u201321 May 2014, Berkeley, CA, USA, pp. 163\u2013178 (2014)","DOI":"10.1109\/SP.2014.18"},{"issue":"1","key":"2_CR25","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1016\/j.entcs.2004.05.018","volume":"125","author":"C Lynch","year":"2005","unstructured":"Lynch, C., Meadows, C.A.: On the relative soundness of the free algebra model for public key encryption. Electron. Notes Theoret. Comput. Sci. 125(1), 43\u201354 (2005)","journal-title":"Electron. Notes Theoret. Comput. Sci."},{"key":"2_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/978-3-642-14992-4_16","volume-title":"Financial Cryptography and Data Security","author":"S Matsuo","year":"2010","unstructured":"Matsuo, S., Miyazaki, K., Otsuka, A., Basin, D.: How to evaluate the security of real-life cryptographic protocols? In: Sion, R., Curtmola, R., Dietrich, S., Kiayias, A., Miret, J.M., Sako, K., Seb\u00e9, F. (eds.) FC 2010. LNCS, vol. 6054, pp. 182\u2013194. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-14992-4_16"},{"issue":"2","key":"2_CR27","doi-asserted-by":"crossref","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. J. Logic Program. 26(2), 113\u2013131 (1996)","journal-title":"J. Logic Program."},{"key":"2_CR28","doi-asserted-by":"crossref","unstructured":"Meadows, C: Analysis of the internet key exchange protocol using the NRL protocol analyzer. In: Proceedings of the 1999 IEEE Symposium on Security and Privacy. IEEE CS Press, May 1999","DOI":"10.1109\/SECPRI.1999.766916"},{"key":"2_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1007\/978-3-642-39799-8_48","volume-title":"Computer Aided Verification","author":"S Meier","year":"2013","unstructured":"Meier, S., Schmidt, B., Cremers, C., Basin, D.: The TAMARIN prover for the symbolic analysis of security protocols. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 696\u2013701. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39799-8_48"},{"issue":"6","key":"2_CR30","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1016\/S0020-0190(03)00211-4","volume":"86","author":"JK Millen","year":"2003","unstructured":"Millen, J.K.: On the freedom of encryption. Inf. Process. Lett. 86(6), 329\u2013333 (2003)","journal-title":"Inf. Process. Lett."},{"key":"2_CR31","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1016\/S1571-0661(04)80841-7","volume":"84","author":"D Miller","year":"2003","unstructured":"Miller, D.: Encryption as an abstract data type. Electron. Notes Theoret. Comput. Sci. 84, 18\u201329 (2003)","journal-title":"Electron. Notes Theoret. Comput. Sci."},{"key":"2_CR32","unstructured":"Ramsdell, J.D., Guttman, J.D.: CPSA: a cryptographic protocol shapes analyzer (2009). http:\/\/hackage.haskell.org\/package\/cpsa"},{"key":"2_CR33","doi-asserted-by":"crossref","unstructured":"Rowe, P.D., Guttman, J.D., Liskov, M.D.: Measuring protocol strength with security goals. International Journal of Information Security (Accepted, Forthcoming)","DOI":"10.1007\/s10207-016-0319-z"},{"key":"2_CR34","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1145\/182110.182113","volume":"28","author":"TYC Woo","year":"1994","unstructured":"Woo, T.Y.C., Lam, S.S.: A lesson on authentication protocol design. Oper. Syst. Rev. 28, 24\u201337 (1994)","journal-title":"Oper. Syst. Rev."}],"container-title":["Lecture Notes in Computer Science","Security Standardisation Research"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-49100-4_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,15]],"date-time":"2019-09-15T05:46:59Z","timestamp":1568526419000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-49100-4_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319490991","9783319491004"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-49100-4_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}