{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:27:41Z","timestamp":1761596861182},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2004,8,1]],"date-time":"2004-08-01T00:00:00Z","timestamp":1091318400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IJIS"],"published-print":{"date-parts":[[2004,8]]},"DOI":"10.1007\/s10207-004-0037-9","type":"journal-article","created":{"date-parts":[[2004,7,21]],"date-time":"2004-07-21T23:12:55Z","timestamp":1090451575000},"page":"168-186","source":"Crossref","is-referenced-by-count":10,"title":["Automated analysis of timed security: a case study on web privacy"],"prefix":"10.1007","volume":"2","author":[{"given":"Roberto","family":"Gorrieri","sequence":"first","affiliation":[]},{"given":"Ruggero","family":"Lanotte","sequence":"additional","affiliation":[]},{"given":"Andrea","family":"Maggiolo-Schettini","sequence":"additional","affiliation":[]},{"given":"Fabio","family":"Martinelli","sequence":"additional","affiliation":[]},{"given":"Simone","family":"Tini","sequence":"additional","affiliation":[]},{"given":"Enrico","family":"Tronci","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2004,8,1]]},"reference":[{"key":"37_CRabadi","doi-asserted-by":"publisher","first-page":"749","DOI":"10.1145\/324133.324266","volume":"46","author":"Abadi","year":"1999","unstructured":"Abadi M (1999) Secrecy by typing in security protocols. J ACM 46(5):749\u2013786","journal-title":"J ACM"},{"key":"37_CRalurdill","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"Alur","year":"1994","unstructured":"Alur R, Dill DL (1994) A THEORY OF TIMED AUTOMATA. Theor Comput Sci 126(2):183\u2013235","journal-title":"Theor Comput Sci"},{"key":"37_CRHytech1","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1109\/32.489079","volume":"22","author":"Alur","year":"1996","unstructured":"Alur R, Henzinger TA, Ho PH (1996) Automatic symbolic verification of embedded systems. IEEE Trans Softw Eng 22(3):181\u2013201","journal-title":"IEEE Trans Softw Eng"},{"key":"37_CRAMP98","doi-asserted-by":"crossref","unstructured":"Asarin E, Maler O, Pnueli A (1998) On discretization of delays in timed automata and digital circuits. In: Proceedings of the international conference on concurrency theory. Lecture notes in computer science, vol 1466. Springer, Berlin Heidelberg New York, pp 470\u2013484","DOI":"10.1007\/BFb0055642"},{"key":"37_CResterel","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0167-6423(92)90005-V","volume":"19","author":"Berry","year":"1992","unstructured":"Berry G, Gonthier G (1992) The Esterel Synchronous Programming Language: design, semantics, implementation. Sci Comput Programm 19(2):87\u2013152","journal-title":"Sci Comput Programm"},{"key":"37_CRchiara","unstructured":"Bodei C, Degano P, Nielson F, Nielson HR (1998) Control flow analysis for the pi-calculus. In: Proceedings of the international conference on concurrency theory. Lecture notes in computer science, vol 1466. Springer, Berlin Heidelberg New York, pp 84\u201398"},{"key":"37_CRBMT99","doi-asserted-by":"crossref","unstructured":"Bozga M, Maler O, Tripakis S (1999) Efficient verification of timed automata using dense and discrete time semantics. In: Proceedings of the international conference on correct hardware design and verification methods. Lecture notes in computer science, vol 1703. Springer, Berlin Heidelberg New York, pp 125\u2013141","DOI":"10.1007\/3-540-48153-2_11"},{"key":"37_CRBry86","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"Bryant","year":"1986","unstructured":"Bryant RE (1986) Graph-based algorithms for Boolean function manipulation. IEEE Trans Comput 35(8):677\u2013691","journal-title":"IEEE Trans Comput"},{"key":"37_CRBCMDH92","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"Burch","year":"1992","unstructured":"Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang LJ (1992) Symbolic model checking: 1020 states and beyond. Inf Comput 98(2):142\u2013170","journal-title":"Inf Comput"},{"key":"37_CRNuSMVpaper","unstructured":"Cimatti A, Clarke EM, Giunchiglia E, Giunchiglia F, Pistore M, Roveri M, Sebastiani R, Tacchella A (2002) NuSMV 2: An open source tool for symbolic model checking. In: Proceedings of the international conference on computer aided verification. Lecture notes in computer science, vol 2404. Springer, Berlin Heidelberg New York, pp 359\u2013364"},{"key":"37_CRfelten","doi-asserted-by":"crossref","unstructured":"Felten EW, Schneider MA (2000) Timing attacks on Web privacy. In: Proceedings of the ACM conference on computer and communications security. ACM Press, New York, pp 25\u201332","DOI":"10.1145\/352600.352606"},{"key":"37_CRf2","doi-asserted-by":"publisher","first-page":"5","DOI":"10.3233\/JCS-1994\/1995-3103","volume":"3","author":"Focardi","year":"1995","unstructured":"Focardi R, Gorrieri R (1995) A classification of security properties for process algebras. J Comput Secur 3(1):5\u201333","journal-title":"J Comput Secur"},{"key":"37_CRf1","doi-asserted-by":"publisher","first-page":"550","DOI":"10.1109\/32.629493","volume":"23","author":"Focardi","year":"1997","unstructured":"Focardi R, Gorrieri R (1997) The compositional security checker: a tool for the verification of information flow security properties. IEEE Trans Softw Eng 23(9):550\u2013571","journal-title":"IEEE Trans Softw Eng"},{"key":"37_CRfabio","doi-asserted-by":"crossref","unstructured":"Focardi R, Gorrieri R, Martinelli F (2000) Information flow analysis in a discrete-time process algebra. In: Proceedings of the IEEE Computer Security Foundation workshop. IEEE Press, Los Alamitos, pp 170\u2013184","DOI":"10.1109\/CSFW.2000.856935"},{"key":"37_CRJSAC","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1109\/JSAC.2002.806122","volume":"21","author":"Focardi","year":"2003","unstructured":"Focardi R, Gorrieri R, Martinelli F (2003) Real-time information flow analysis. IEEE J Select Areas Commun 21(1):20\u201335","journal-title":"IEEE J Select Areas Commun"},{"key":"37_CRgroote","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1016\/0304-3975(93)90111-6","volume":"118","author":"Groote","year":"1993","unstructured":"Groote JF (1993) Transition system specifications with negative premises. Theor Comput Sci 118(2):263\u2013299","journal-title":"Theor Comput Sci"},{"key":"37_CRHH99","doi-asserted-by":"crossref","unstructured":"Handschuh H, Howard Heys M (1999) A timing attack on RC5. In: Proceedings of the international workshop on selected areas in cryptography. Lecture notes in computer science, vol 1556. Springer, Berlin Heidelberg New York, pp 306\u2013318","DOI":"10.1007\/3-540-48892-8_24"},{"key":"37_CRHytech2","doi-asserted-by":"crossref","unstructured":"Henzinger TA, Ho PH, Wong-Toi H (1997) HyTech: A model checker for hybrid systems. Int J Softw Tools Technol Transfer 1(1\u20132):110\u2013122","DOI":"10.1007\/s100090050008"},{"key":"37_CRKS90","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/0890-5401(90)90025-D","volume":"86","author":"Kanellakis","year":"1990","unstructured":"Kanellakis PC, Smolka SA (1990) CCS expressions, finite-state processes, and three problems of equivalence. Inf Comput 86(1):43\u201368","journal-title":"Inf Comput"},{"key":"37_CRKo96","doi-asserted-by":"crossref","unstructured":"Kocher PC (1996) Timing attacks on implementations of Diffie-Hellman, RSA, DSS and other systems. In: Proceedings of the international conference on advances in cryptology. Lecture notes in computer science, vol 1109. Springer, Berlin Heidelberg New York, pp 104\u2013113","DOI":"10.1007\/3-540-68697-5_9"},{"key":"37_CRkozen","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"Kozen","year":"1983","unstructured":"Kozen D (1983) Results on the propositional \u03bc-calculus. Theor Comput Sci 27(3):333\u2013354","journal-title":"Theor Comput Sci"},{"key":"37_CRLMT01","doi-asserted-by":"crossref","unstructured":"Lanotte R, Maggiolo-Schettini A, Tini S (2001) Privacy in real-time systems. In: Proceedings of the workshop on models for timed critical systems. Electronic notes in theoretical computer science, vol 52, Elsevier, Amsterdam","DOI":"10.1016\/S1571-0661(04)00229-4"},{"key":"37_CRfabio98","doi-asserted-by":"crossref","unstructured":"Martinelli F (1998) Partial model checking and theorem proving for ensuring security properties. In: Proceedings of the IEEE Computer Security Foundations workshop. IEEE Press, Los Alamitos, pp 44\u201352","DOI":"10.1109\/CSFW.1998.683154"},{"key":"37_CRMcM93","doi-asserted-by":"crossref","unstructured":"McMillan KL (1993) Symbolic model checking. Kluwer, Norwell, Massachusetts","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"37_CRmeadows","doi-asserted-by":"crossref","unstructured":"Meadows C (1997): Languages for formal specification of security protocols. In: Proceedings of the IEEE Computer Security Foundations workshop. IEEE Press, Los Alamitos, CA, pp 96\u201397","DOI":"10.1109\/CSFW.1997.596792"},{"key":"37_CRccs","unstructured":"Milner R (1989) Communication and concurrency. Prentice Hall, London"},{"key":"37_CRmitchell","unstructured":"Mitchell JC, Mitchell M, Stern U (1997) Automated analysis of cryptographic protocols using Murphi. In: Proceedings of the IEEE symposium on security and privacy. IEEE Press, Los Alamitos, CA, pp 141\u2013153"},{"key":"37_CRclock","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1109\/9.52290","volume":"35","author":"Ostroff","year":"1990","unstructured":"Ostroff JS, Wonham WS (1990) A framework for real-time discrete event control. IEEE Trans Automat Control 35(4):386\u2013397","journal-title":"IEEE Trans Automat Control"},{"key":"37_CRPSP94","unstructured":"Panda S, Somenzi F, Plessier BF (1994) Symmetry detection and dynamic variable ordering of decision diagrams. In: Proceedings of the IEEE International conference on computer-aided design. IEEE Press, Los Alamitos, CA, pp 628\u2013631"},{"key":"37_CRPV94","unstructured":"Puri A, Varaiya P (1994) Decidability of hybrid systems with rectangular differential equations. In: Proceedings of the international conference on computer aided verification. Lecture notes in computer science, vol 818. Springer, Berlin Heidelberg New York, pp 95\u2013104"},{"key":"37_CRv2","doi-asserted-by":"crossref","unstructured":"Smith G, Volpano D (1998) Secure information flow in a multi-threaded imperative language. In: Proceedings of the ACM symposium on principles of programming languages. ACM Press, New York, pp 355\u2013364","DOI":"10.1145\/268946.268975"},{"key":"37_CRSWT01","unstructured":"Song D, Wagner D, Tian X (2001) Timing analysis of Keystrokes and SSH timing attacks. In: Proceedings of the 10th USENIX security symposium, 2001"},{"key":"37_CRv1","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1145\/300307.300311","volume":"29","author":"Volpano","year":"1998","unstructured":"Volpano D, Smith G (1998) Confinement properties for programming languages. SIGACT News 29(3):33\u201342","journal-title":"SIGACT News"},{"key":"37_CRCUDDweb","unstructured":"CUDD Web Page: http:\/\/vlsi.colorado.edu\/\u223cfabio\/CUDD\/"},{"key":"37_CRNuSMVweb","unstructured":"NuSMV Web Page: http:\/\/nusmv.irst.itc.it\/"},{"key":"37_CRsmvweb","unstructured":"URL: http:\/\/www.cs.cmu.edu\/\u223cmodelcheck\/"},{"key":"37_CRhyweb","unstructured":"URL: http:\/\/www-cad.eecs.berkeley.edu\/\u223ctah\/HyTech\/"},{"key":"37_CRcwbMINUSnc","unstructured":"URL: http:\/\/www.cs.sunysb.edu\/\u223ccwb\/"}],"container-title":["International Journal of Information Security"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10207-004-0037-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10207-004-0037-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10207-004-0037-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,2]],"date-time":"2020-04-02T20:32:54Z","timestamp":1585859574000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10207-004-0037-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,8]]},"references-count":38,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2004,8]]}},"alternative-id":["37"],"URL":"https:\/\/doi.org\/10.1007\/s10207-004-0037-9","relation":{},"ISSN":["1615-5262","1615-5270"],"issn-type":[{"value":"1615-5262","type":"print"},{"value":"1615-5270","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,8]]}}}