{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,13]],"date-time":"2025-02-13T00:40:09Z","timestamp":1739407209647,"version":"3.37.0"},"reference-count":31,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2010,9,1]],"date-time":"2010-09-01T00:00:00Z","timestamp":1283299200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2010,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We model security protocols as games using concepts of game semantics. Using this model we ascribe semantics to protocols written in the standard simple arrow notation. According to the semantics, a protocol is interpreted as a set of strategies over a game tree that represents the type of the protocol. The model uses abstract computation functions and message frames in order to model internal computations and knowledge of agents and the intruder. Moreover, in order to specify properties of the model, a logic that deals with games and strategies is developed. A tableau-based proof system is given for the logic, which can serve as a basis for a model checking algorithm. This approach allows us to model a wide range of security protocol types and verify different properties instead of using a variety of methods as is currently the practice. Furthermore, the analyzed protocols are specified using only the simple arrow notation heavily used by protocol designers and by practitioners.<\/jats:p>","DOI":"10.1007\/s00165-009-0129-4","type":"journal-article","created":{"date-parts":[[2009,10,29]],"date-time":"2009-10-29T15:56:01Z","timestamp":1256831761000},"page":"585-609","source":"Crossref","is-referenced-by-count":1,"title":["A game-theoretic framework for specification and verification of cryptographic protocols"],"prefix":"10.1145","volume":"22","author":[{"given":"Mohamed","family":"Saleh","sequence":"first","affiliation":[{"name":"Computer Security Laboratory, Concordia Institute for Information Systems Engineering, Concordia University, Montr\u00e9al, QC, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mourad","family":"Debbabi","sequence":"additional","affiliation":[{"name":"Computer Security Laboratory, Concordia Institute for Information Systems Engineering, Concordia University, Montr\u00e9al, QC, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","first-page":"39","volume-title":"Foundations of secure computation, 20th Int. Summer School, Marktoberdorf, Germany","author":"Abadi M","year":"2000"},{"volume-title":"Proceedings of the 1996 CLiCS Summer School, Isaac Newton Institute","year":"1997","author":"Abramsky S","key":"e_1_2_1_2_2_2"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Abadi M Cortier V (2005) Deciding knowledge in security protocols under (many more) equational theories. In: Proceedings of the 18th IEEE Computer Security Foundations Workshop","DOI":"10.1007\/978-3-540-27836-8_7"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00364-X"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Abadi M Fournet C (2001) Mobile values new names and secure communication. In: POPL pp 104\u2013115","DOI":"10.1145\/373243.360213"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Abadi M Gordon A (1997) A calculus for cryptographic protocols: the SPI calculus. In: Proceedings of the 4th ACM conference on computer and communications security","DOI":"10.1145\/266420.266432"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Alur R Henzinger T Kupferman O (2002) Alternating-time temporal logic. JACM: J ACM 49","DOI":"10.1145\/585265.585270"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Abramsky S Malacaria P Jagadeesan R (1994) Full abstraction for PCF. In: Theoretical Aspects of Computer Software pp 1\u201315","DOI":"10.1007\/3-540-57887-0_87"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00145-001-0014-7"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Blanchet B Abadi M Fournet C (2005) Automated verification of selected equivalences for security protocols. In: LICS pp 331\u2013340. IEEE Computer Society New York","DOI":"10.1109\/LICS.2005.8"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Burrows M Abadi M Needham R (1989) A logic of authentication. Technical report Digital Systems Research Center","DOI":"10.1145\/74850.74852"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Boreale M Buscemi M (2005) A method for symbolic analysis of security protocols. TCS: Theoretical Computer Science vol 338","DOI":"10.1016\/j.tcs.2005.03.044"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(92)90073-9"},{"key":"e_1_2_1_2_14_2","unstructured":"Cervesato I Durgin N Lincoln P Mitchell J Scedrov A (1999) A meta-notation for protocol analysis. In: CSFW: Proceedings of The 12th Computer Security Foundations Workshop. IEEE Computer Society Press New York"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Clarke E Jha S Marrero W (1998) Using state space exploration and a natural deduction style message derivation engine to verify security protocols. In: International Conference on Programming Concepts and Methods pp 87\u2013106","DOI":"10.1007\/978-0-387-35358-6_10"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-005-9019-5"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00264284"},{"key":"e_1_2_1_2_18_2","unstructured":"Delaune S (2006) V\u00e9rification des protocoles cryptographiques et propri\u00e9t\u00e9s alg\u00e9briques. Th\u00e8se de doctorat Laboratoire Sp\u00e9cification et V\u00e9rification ENS Cachan France"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2917"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"J\u00fcrjens J (2002) Games in the semantics of programming languages. Synthese (Elsevier) 133(1\u20132) October\/November 2002","DOI":"10.1023\/A:1020883810034"},{"key":"e_1_2_1_2_22_2","unstructured":"Kremer S Raskin J (2000) A game approach to the verification of exchange protocols\u2014application to non-repudiation protocols. In: Proceedings of the workshop on issues in the theory of security (WITS \u201900) 2000"},{"key":"e_1_2_1_2_23_2","unstructured":"Lorenz K (2001) Basic objectives of dialogue logic in historical perspective. Synthese (Elsevier) 127(1\u20132) April\/May"},{"issue":"3","key":"e_1_2_1_2_24_2","first-page":"93","article-title":"Breaking and fixing the Needham\u2013Schroeder public-key protocol using FDR","volume":"17","author":"Lowe G","year":"1996","journal-title":"Software\u2014concepts and tools"},{"key":"e_1_2_1_2_25_2","unstructured":"Lowe G (1997) A hierarchy of authentication specification. In: CSFW pp 31\u201344. IEEE Computer Society New York"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Needham R Schroeder M (1978) Using encryption for authentication in large networks of computers. Commun ACM 21(12)","DOI":"10.1145\/359657.359659"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Paulson LC (1998) The inductive approach to verifying cryptographic protocols. J Comp Secur 85\u2013128 (1998)","DOI":"10.3233\/JCS-1998-61-205"},{"key":"e_1_2_1_2_28_2","unstructured":"Rivest RL Shamir A Adleman L (1978) Mental poker. Technical report TM-125 MIT Nov"},{"key":"e_1_2_1_2_29_2","volume-title":"Applied cryptography","author":"Schneier B","year":"2001","edition":"2"},{"key":"e_1_2_1_2_30_2","first-page":"317","volume-title":"Handbook of logic in computer science, vol 5","author":"Tucker JV","year":"2000"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Woo TYC Lam SS (1994) A lesson on authentication protocol design. Oper Syst Rev 24\u201337","DOI":"10.1145\/182110.182113"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-009-0129-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-009-0129-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-009-0129-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,13]],"date-time":"2025-02-13T00:01:09Z","timestamp":1739404869000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-009-0129-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,9]]},"references-count":31,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2010,9]]}},"alternative-id":["10.1007\/s00165-009-0129-4"],"URL":"https:\/\/doi.org\/10.1007\/s00165-009-0129-4","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2010,9]]}}}