PT Journal AU Gorrieri, R Lanotte, R Maggiolo-Schettini, A Martinelli, F Tini, S Tronci, E TI Automated analysis of timed security: a case study on web privacy SO International Journal of Information Security PY 2004 BP 168 EP 186 VL 2 IS 3-4 DI 10.1007/s10207-004-0037-9 AB This paper presents a case study on an automated analysis of real-time security models. The case study on a web system (originally proposed by Felten and Schneider) is presented that shows a timing attack on the privacy of browser users. Three different approaches are followed: LH-Timed Automata (analyzed using the model checker HyTech), finite-state automata (analyzed using the model checker NuSMV), and process algebras (analyzed using the model checker CWB-NC). A comparative analysis of these three approaches is given. ER