%0 Journal Article
%T Automated analysis of timed security: a case study on web privacy
%A Gorrieri, Roberto
%A Lanotte, Ruggero
%A Maggiolo-Schettini, Andrea
%A Martinelli, Fabio
%A Tini, Simone
%A Tronci, Enrico
%J International Journal of Information Security
%D 2004
%V 2
%N 3-4
%F Gorrieri_etal2004
%O exported from refbase (http://mclab.di.uniroma1.it/publications/show.php?record=33), last updated on Thu, 22 Nov 2012 14:59:18 +0100
%X 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.
%R 10.1007/s10207-004-0037-9
%U http://mclab.di.uniroma1.it/publications/papers/papers/Gorrieri2004.pdf
%U https://doi.org/10.1007/s10207-004-0037-9
%P 168-186