
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Ruggero Lanotte, Andrea MaggioloSchettini, Angelo Troina, "Time and ProbabilityBased Information Flow Analysis," IEEE Transactions on Software Engineering, vol. 36, no. 5, pp. 719734, September/October, 2010.  
BibTex  x  
@article{ 10.1109/TSE.2010.4, author = {Ruggero Lanotte and Andrea MaggioloSchettini and Angelo Troina}, title = {Time and ProbabilityBased Information Flow Analysis}, journal ={IEEE Transactions on Software Engineering}, volume = {36}, number = {5}, issn = {00985589}, year = {2010}, pages = {719734}, doi = {http://doi.ieeecomputersociety.org/10.1109/TSE.2010.4}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  Time and ProbabilityBased Information Flow Analysis IS  5 SN  00985589 SP719 EP734 EPD  719734 A1  Ruggero Lanotte, A1  Andrea MaggioloSchettini, A1  Angelo Troina, PY  2010 KW  Probabilistic timed automata KW  multilevel security KW  information flow analysis KW  weak bisimulation. VL  36 JA  IEEE Transactions on Software Engineering ER   
[1] J. Agat, "Transforming Out Timing Leaks," Proc. Symp. Principles of Programming Languages, pp. 4053, 2000.
[2] A. Aldini, M. Bravetti, and R. Gorrieri, "A ProcessAlgebraic Approach for the Analysis of Probabilistic Non Interference," J. Computer Security, vol. 12, pp. 191245, 2004.
[3] A. Aldini and A. Di Pierro, "Estimating the Maximum Information Leakage," Int'l J. Information Security, vol. 7, pp. 219242, 2008.
[4] R. Alur, C. Courcoubetis, and D.L. Dill, "Verifying Automata Specifications of Probabilistic RealTime Systems," Proc. Workshop RealTime: Theory in Practice, pp. 2844, 1992.
[5] R. Alur and D.L. Dill, "A Theory of Timed Automata," Theoretical Computer Science, vol. 126, pp. 183235, 1994.
[6] C. Baier and H. Hermanns, "Weak Bisimulation for Fully Probabilistic Processes," Proc. Int'l Conf. Computer Aided Verification, pp. 119130, 1997.
[7] R. Barbuti and L. Tesei, "A Decidable Notion of Timed NonInterference," Fundamenta Informaticae, vol. 54, pp. 137150, 2003.
[8] D. Beauquier, "On Probabilistic Timed Automata," Theoretical Computer Science, vol. 292, pp. 6584, 2003.
[9] R.E. Bellman, Dynamic Programming. Princeton Univ. Press, 1957.
[10] M. Boreale, "Quantifying Information Leakage in Process Calculi," Information and Computation, vol. 207, pp. 699725, 2009.
[11] P. Bouyer, "Timed Automata May Cause Some Troubles," BRICS Research Report RS0235, 2002.
[12] F. van Breugel and J. Worrel, "Towards Quantitative Verification of Probabilistic Systems (Extended Abstract)," Proc. Int'l Colloquium Automata, Languages, and Programming, pp. 421432, 2001.
[13] S. Cattani and R. Segala, "Decision Algorithm for Probabilistic Bisimulation," Proc. Int'l Conf. Concurrency Theory, pp. 371385, 2002.
[14] K. Cerans, "Decidability of Bisimulation Equivalences for Parallel Timer Processes," Proc. Int'l Conf. Computer Aided Verification, pp. 302315, 1992.
[15] D. Clark, S. Hunt, and P. Malacaria, "Quantitative Information Flow, Relations and Polymorphic Types," J. Logic and Computation, vol. 18, pp. 181199, 2005.
[16] K. Chatzikokolakis, G. Norman, and D. Parker, "Bisimulation for Demonic Schedulers," Proc. Int'l Conf. Foundations of Software Science and Computational Structures, pp. 318332, 2009.
[17] K. Chatzikokolakis and C. Palamidessi, "Making Random Choices Invisible to the Scheduler," Proc. Int'l Conf. Concurrency Theory, pp. 4258, 2007.
[18] D. Chaum, "The Dining Cryptographers Problem: Unconditional Sender and Recipient Untraceability," J. Cryptology, vol. 1, pp. 6575, 1988.
[19] J. Desharnais, V. Gupta, R. Jagadeesan, and P. Panangaden, "The Metric Analogue of Weak Bisimulation for Probabilistic Processes," Proc. Ann. IEEE Symp. Logic in Computer Science, 2002.
[20] A. Di Pierro, C. Hankin, I. Siveroni, and H. Wiklicky, "Tempus Fugit: How to Plug It," J. Logic and Algebraic Programming, vol. 72, pp. 173190, 2007.
[21] A. Di Pierro, C. Hankin, and H. Wiklicky, "Quantitative Relations and Approximate Process Equivalences," Proc. Int'l Conf. Concurrency Theory, pp. 508522, 2003.
[22] A. Di Pierro, C. Hankin, and H. Wiklicky, "Approximate Non Interference," J. Computer Security, vol. 12, pp. 3782, 2004.
[23] A. Di Pierro, C. Hankin, and H. Wiklicky, "Measuring the Confinement of Probabilistic Systems," Theoretical Computer Science, vol. 340, pp. 356, 2005.
[24] A. Di Pierro, C. Hankin, and H. Wiklicky, "Quantifying Timing Leaks and Cost Optimisation," Proc. Int'l Conf. Information and Comm. Security, pp. 8196, 2008.
[25] N. Evans and S. Schneider, "Analysing Time Dependent Security Properties in CSP Using PVS," Proc. Symp. Research in Computer Security, pp. 222237, 2000.
[26] R. Focardi and R. Gorrieri, "A Classification of Security Properties," J. Computer Security, vol. 3, pp. 533, 1995.
[27] R. Focardi, R. Gorrieri, R. Lanotte, A. MaggioloSchettini, F. Martinelli, S. Tini, and E. Tronci, "Formal Models of Timing Attacks on Web Privacy," Electronic Notes in Theoretical Computer Science, vol. 62, pp. 229243, 2001.
[28] R. Focardi, R. Gorrieri, and F. Martinelli, "Information Flow Analysis in a DiscreteTime Process Algebra," Proc. 13th IEEE Computer Security Foundations Workshop, pp. 170184, 2000.
[29] J.A. Goguen and J. Meseguer, "Security Policy and Security Models," Proc. Symp. Research in Security and Privacy, pp. 1120, 1982.
[30] J.W. GrayIII, "Toward a Mathematical Foundation for Information Flow Security," J. Computer Security, vol. 1, pp. 255294, 1992.
[31] P.R. Halmos, Measure Theory. SpringerVerlag, 1950.
[32] T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, "Symbolic Model Checking for RealTime Systems," Information and Computation, vol. 111, pp. 193244, 1994.
[33] H. Howard, Dynamic Programming and Markov Processes. MIT Press, 1960.
[34] M. Kwiatkowska, G. Norman, R. Segala, and J. Sproston, "Automatic Verification of RealTime Systems with Discrete Probability Distribution," Theoretical Computer Science, vol. 282, pp. 101150, 2002.
[35] M. Kwiatkowska, R. Norman, and J. Sproston, "Symbolic Model Checking of Probabilistic Timed Automata Using Backwards Reachability," Technical Report CSR0310, Univ. of Birmingham, 2003.
[36] R. Lanotte and D. Beauquier, A Decidable Probability Logic for Timed Probabilistic Systems, CoRR cs.LO/0411100, 2004.
[37] R. Lanotte, A. MaggioloSchettini, and A. Troina, "Information Flow Analysis for Probabilistic Timed Automata," Proc. Int'l Workshop Formal Aspects in Security and Trust, Aug. 2004.
[38] R. Lanotte, A. MaggioloSchettini, and A. Troina, Weak Bisimulation for Probabilistic Timed Automata, http://www.di.unito.it/~troinaPTA_WB.pdf , 2008.
[39] F. Laroussinie, K.G. Larsen, and C. Weise, "From Timed Automata to Logic—And Back," Proc. Int'l Symp. Math. Foundations of Computer Science, pp. 2741, 1995.
[40] K.G. Larsen and Y. Wang, "Time Abstracted Bisimulation: Implicit Specifications and Decidability," Information and Computation, vol. 134, pp. 75101, 1997.
[41] D. McCullough, "Noninterference and the Composability of Security Properties," Proc. Symp. Research in Security and Privacy, pp. 177186, 1988.
[42] J.K. Millen, "Hookup Security for Synchronous Machines," Proc. IEEE Computer Security Foundations Workshop, pp. 8490, 1990.
[43] R. Milner, Communication and Concurrency. Prentice Hall, 1989.
[44] A. Troina, "Probabilistic Timed Automata for Security Analysis and Design," PhD thesis, Univ. of Pisa, 2006.
[45] Y. Wang, "RealTime Behaviour of Asynchronous Agents," Proc. Int'l Conf. Concurrency Theory, pp. 502520, 1990.