{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T05:17:11Z","timestamp":1740115031085,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":39,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642124587"},{"type":"electronic","value":"9783642124594"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-12459-4_19","type":"book-chapter","created":{"date-parts":[[2010,4,29]],"date-time":"2010-04-29T06:49:38Z","timestamp":1272523778000},"page":"263-278","source":"Crossref","is-referenced-by-count":2,"title":["A User Interface for a Game-Based Protocol Verification Tool"],"prefix":"10.1007","author":[{"given":"Peeter","family":"Laud","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ilja","family":"T\u0161ahhirov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"19_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/11924661_16","volume-title":"Programming Languages and Systems","author":"M. Abadi","year":"2006","unstructured":"Abadi, M., Corin, R., Fournet, C.: Computational secrecy by typing for the pi calculus. In: Kobayashi, N. (ed.) APLAS 2006. LNCS, vol.\u00a04279, pp. 253\u2013269. Springer, Heidelberg (2006)"},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: POPL 2001, pp. 104\u2013115 (2001)","DOI":"10.1145\/373243.360213"},{"key":"19_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-45500-0_4","volume-title":"Theoretical Aspects of Computer Software","author":"M. Abadi","year":"2001","unstructured":"Abadi, M., J\u00fcrjens, J.: Formal eavesdropping and its computational interpretation. In: Kobayashi, N., Pierce, B.C. (eds.) TACS 2001. LNCS, vol.\u00a02215, pp. 82\u201394. Springer, Heidelberg (2001)"},{"issue":"2","key":"19_CR4","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/s00145-001-0014-7","volume":"15","author":"M. Abadi","year":"2002","unstructured":"Abadi, M., Rogaway, P.: Reconciling two views of cryptography (the computational soundness of formal encryption). J. Cryptology\u00a015(2), 103\u2013127 (2002)","journal-title":"J. Cryptology"},{"key":"19_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/978-3-540-89439-1_26","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M. Backes","year":"2008","unstructured":"Backes, M., Berg, M., Unruh, D.: A formal language for cryptographic pseudocode. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol.\u00a05330, pp. 353\u2013376. Springer, Heidelberg (2008)"},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"Backes, M., Laud, P.: Computationally sound secrecy proofs by mechanized flow analysis. In: ACM\u00a0CCS\u00a0 2006, pp. 370\u2013379 (2006)","DOI":"10.1145\/1180405.1180450"},{"key":"19_CR7","doi-asserted-by":"crossref","unstructured":"Backes, M., Pfitzmann, B., Waidner, M.: A composable cryptographic library with nested operations. In: ACM CCS 2003, pp. 220\u2013230 (2003)","DOI":"10.1145\/948109.948140"},{"key":"19_CR8","doi-asserted-by":"crossref","unstructured":"Ballance, R.A., Maccabe, A.B., Ottenstein, K.J.: The program dependence web: A representation supporting control, data, and demand-driven interpretation of imperative languages. In: PLDI 1990, pp. 257\u2013271 (1990)","DOI":"10.1145\/93548.93578"},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"Barthe, G., Gr\u00e9goire, B., B\u00e9guelin, S.Z.: Formal certification of code-based cryptographic proofs. In: POPL 2009, pp. 90\u2013101 (2009)","DOI":"10.1145\/1594834.1480894"},{"key":"19_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"531","DOI":"10.1007\/3-540-44448-3_41","volume-title":"Advances in Cryptology - ASIACRYPT 2000","author":"M. Bellare","year":"2000","unstructured":"Bellare, M., Namprempre, C.: Authenticated encryption: Relations among notions and analysis of the generic composition paradigm. In: Okamoto, T. (ed.) ASIACRYPT 2000. LNCS, vol.\u00a01976, pp. 531\u2013535. Springer, Heidelberg (2000)"},{"key":"19_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/11761679_25","volume-title":"Advances in Cryptology - EUROCRYPT 2006","author":"M. Bellare","year":"2006","unstructured":"Bellare, M., Rogaway, P.: The security of triple encryption and a framework for code-based game-playing proofs. In: Vaudenay, S. (ed.) EUROCRYPT 2006. LNCS, vol.\u00a04004, pp. 409\u2013426. Springer, Heidelberg (2006)"},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: A computationally sound mechanized prover for security protocols. In: IEEE\u00a0S&P\u00a02006, pp. 140\u2013154 (2006)","DOI":"10.1109\/SP.2006.1"},{"key":"19_CR13","unstructured":"Blanchet, B.: A Computationally Sound Mechanized Prover for Security Protocols. Cryptology ePrint Archive, Report 2005\/401 (February 2, 2007)"},{"key":"19_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/11787006_22","volume-title":"Automata, Languages and Programming","author":"R. Corin","year":"2006","unstructured":"Corin, R., den Hartog, J.: A probabilistic hoare-style logic for game-based cryptographic proofs. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol.\u00a04052, pp. 252\u2013263. Springer, Heidelberg (2006)"},{"key":"19_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/11944836_18","volume-title":"FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science","author":"V. Cortier","year":"2006","unstructured":"Cortier, V., Kremer, S., K\u00fcsters, R., Warinschi, B.: Computationally sound symbolic secrecy in the presence of hash functions. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol.\u00a04337, pp. 176\u2013187. Springer, Heidelberg (2006)"},{"key":"19_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1007\/978-3-540-31987-0_12","volume-title":"Programming Languages and Systems","author":"V. Cortier","year":"2005","unstructured":"Cortier, V., Warinschi, B.: Computationally sound, automated proofs for security protocols. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 157\u2013171. Springer, Heidelberg (2005)"},{"key":"19_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"16","DOI":"10.1007\/11523468_2","volume-title":"Automata, Languages and Programming","author":"A. Datta","year":"2005","unstructured":"Datta, A., Derek, A., Mitchell, J.C., Shmatikov, V., Turuani, M.: Probabilistic polynomial-time semantics for a protocol security logic. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol.\u00a03580, pp. 16\u201329. Springer, Heidelberg (2005)"},{"key":"19_CR18","doi-asserted-by":"crossref","unstructured":"Datta, A., Derek, A., Mitchell, J.C., Warinschi, B.: Computationally sound compositional logic for key exchange protocols. In: CSFW\u00a02006, pp. 321\u2013334 (2006)","DOI":"10.1109\/CSFW.2006.9"},{"issue":"3","key":"19_CR19","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1145\/24039.24041","volume":"9","author":"J. Ferrante","year":"1987","unstructured":"Ferrante, J., Ottenstein, K.J., Warren, J.D.: The program dependence graph and its use in optimization. ACM Trans. Program. Lang. Syst.\u00a09(3), 319\u2013349 (1987)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"19_CR20","doi-asserted-by":"crossref","unstructured":"Fournet, C., Rezk, T.: Cryptographically sound implementations for typed information-flow security. In: POPL 2008, pp. 323\u2013335 (2008)","DOI":"10.1145\/1328897.1328478"},{"key":"19_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"266","DOI":"10.1007\/3-540-58950-3_379","volume-title":"Graph Drawing","author":"M. Fr\u00f6hlich","year":"1995","unstructured":"Fr\u00f6hlich, M., Werner, M.: Demonstration of the interactive graph-visualization system vinci. In: Tamassia, R., Tollis, I.G. (eds.) GD 1994. LNCS, vol.\u00a0894, pp. 266\u2013269. Springer, Heidelberg (1995)"},{"key":"19_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1007\/978-3-540-31987-0_13","volume-title":"Programming Languages and Systems","author":"R. Janvier","year":"2005","unstructured":"Janvier, R., Lakhnech, Y., Mazar\u00e9, L.: Completing the picture: Soundness of formal encryption in the presence of active adversaries. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 172\u2013185. Springer, Heidelberg (2005)"},{"key":"19_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/3-540-45309-1_6","volume-title":"Programming Languages and Systems","author":"P. Laud","year":"2001","unstructured":"Laud, P.: Semantics and program analysis of computationally secure information flow. In: Sands, D. (ed.) ESOP 2001. LNCS, vol.\u00a02028, pp. 77\u201391. Springer, Heidelberg (2001)"},{"key":"19_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/3-540-36575-3_12","volume-title":"Programming Languages and Systems","author":"P. Laud","year":"2003","unstructured":"Laud, P.: Handling encryption in an analysis for secure information flow. In: Degano, P. (ed.) ESOP 2003. LNCS, vol.\u00a02618, pp. 159\u2013173. Springer, Heidelberg (2003)"},{"key":"19_CR25","doi-asserted-by":"crossref","unstructured":"Laud, P.: Symmetric encryption in automatic analyses for confidentiality against active adversaries. In: IEEE\u00a0S&P\u00a02004, pp. 71\u201385 (2004)","DOI":"10.1109\/SECPRI.2004.1301316"},{"key":"19_CR26","doi-asserted-by":"crossref","unstructured":"Laud, P.: Secrecy types for a simulatable cryptographic library. In: ACM\u00a0CCS\u00a02005, pp. 26\u201335 (2005)","DOI":"10.1145\/1102120.1102126"},{"key":"19_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/11537311_32","volume-title":"Fundamentals of Computation Theory","author":"P. Laud","year":"2005","unstructured":"Laud, P., Vene, V.: A type system for computationally secure information flow. In: Li\u015bkiewicz, M., Reischuk, R. (eds.) FCT 2005. LNCS, vol.\u00a03623, pp. 365\u2013377. Springer, Heidelberg (2005)"},{"key":"19_CR28","doi-asserted-by":"crossref","unstructured":"Lincoln, P., Mitchell, J.C., Mitchell, M., Scedrov, A.: A probabilistic poly-time framework for protocol analysis. In: ACM\u00a0CCS\u00a01998, pp. 112\u2013121 (1998)","DOI":"10.1145\/288090.288117"},{"key":"19_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1007\/978-3-540-24638-1_8","volume-title":"Theory of Cryptography","author":"D. Micciancio","year":"2004","unstructured":"Micciancio, D., Warinschi, B.: Soundness of formal encryption in the presence of active adversaries. In: Naor, M. (ed.) TCC 2004. LNCS, vol.\u00a02951, pp. 133\u2013151. Springer, Heidelberg (2004)"},{"key":"19_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/978-3-540-77048-0_25","volume-title":"Information and Communications Security","author":"D. Nowak","year":"2007","unstructured":"Nowak, D.: A framework for game-based security proofs. In: Qing, S., Imai, H., Wang, G. (eds.) ICICS 2007. LNCS, vol.\u00a04861, pp. 319\u2013333. Springer, Heidelberg (2007)"},{"key":"19_CR31","doi-asserted-by":"crossref","unstructured":"Pingali, K., Beck, M., Johnson, R., Moudgill, M., Stodghill, P.: Dependence flow graphs: An algebraic approach to program dependencies. In: POPL 1991, pp. 67\u201378 (1991)","DOI":"10.1145\/99583.99595"},{"key":"19_CR32","unstructured":"Shoup, V.: Sequences of games: a tool for taming complexity in security proofs. Cryptology ePrint Archive, Report 2004\/332 (2004), http:\/\/eprint.iacr.org\/"},{"key":"19_CR33","doi-asserted-by":"crossref","unstructured":"Smith, G.: Secure information flow with random assignment and encryption. In: FMSE 2006, pp. 33\u201344 (2006)","DOI":"10.1145\/1180337.1180341"},{"key":"19_CR34","doi-asserted-by":"crossref","unstructured":"Sprenger, C., Backes, M., Basin, D.A., Pfitzmann, B., Waidner, M.: Cryptographically sound theorem proving. In: CSFW\u00a02006, pp. 153\u2013166 (2006)","DOI":"10.1109\/CSFW.2006.10"},{"key":"19_CR35","doi-asserted-by":"crossref","unstructured":"Sprenger, C., Basin, D.A.: Cryptographically-sound protocol-model abstractions. In: CSF 2008, pp. 115\u2013129 (2008)","DOI":"10.1109\/CSF.2008.19"},{"key":"19_CR36","unstructured":"T\u0161ahhirov, I.: Security Protocols Analysis in the Computational Model \u2014 Dependency Flow Graphs-Based Approach. PhD thesis, Tallinn University of Technology (2008)"},{"key":"19_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-540-78663-4_20","volume-title":"Trustworthy Global Computing","author":"I. T\u0161ahhirov","year":"2008","unstructured":"T\u0161ahhirov, I., Laud, P.: Application of dependency graphs to security protocol analysis. In: Barthe, G., Fournet, C. (eds.) TGC 2007 and FODO 2008. LNCS, vol.\u00a04912, pp. 294\u2013311. Springer, Heidelberg (2008)"},{"key":"19_CR38","unstructured":"uDraw(Graph) graph visualizer (2005), http:\/\/www.informatik.uni-bremen.de\/uDrawGraph\/en\/index.html"},{"key":"19_CR39","doi-asserted-by":"crossref","unstructured":"Volpano, D.M.: Secure introduction of one-way functions. In: CSFW 2000, pp. 246\u2013254 (2000)","DOI":"10.1109\/CSFW.2000.856941"}],"container-title":["Lecture Notes in Computer Science","Formal Aspects in Security and Trust"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-12459-4_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,20]],"date-time":"2025-02-20T08:19:06Z","timestamp":1740039546000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-12459-4_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642124587","9783642124594"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-12459-4_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}