]. J. Aga00 and . Agat, Transforming out timing leaks, POPL, pp.40-53, 2000.

A. Bossi, R. Focardi, C. Piazza, S. [. Rossi, R. Beauquier et al., Bisimulation and unwinding for verifying possibilistic security properties Hiding information in multi level security systems, Proc. Int. Conf. on Verication , Model Checking, and Abstract Interpretation Proc. 4th Int. Workshop on Formal Aspect in Security and Trust (LNCS 4691), pp.223-237, 2003.

R. Dhk-+-08-]-d.-d-'souza, J. Holla, R. K. Kulkarni, B. Ramesh, and . Sprick, On the decidability of model-checking information flow properties, Proc. Int. Conf. on Information Systems Security, pp.26-40, 2008.

]. R. Fg95a, R. Focardi, and . Gorrieri, A classification of security properties for process algebras, In Journal of Computer Security, vol.1, pp.5-33, 1995.

R. Focardi, R. Gorrierifg96-]-r, R. Focardi, and . Gorrieri, A classification of security properties for process algebras The compositional security checker: A tool for the verification of information flow security properties, In Journal of Computer Security, vol.1, pp.5-33, 1995.

R. Focardi, R. Gorrieri, F. [. Martinelli, J. Goguen, . [. Meseguer et al., Information flow analysis in a discrete-time process algebra Unwinding and inference control Timing-sensitive information flow analysis for synchronous systems, CSFW Proc. IEEE Symp. on Security and Privacy ESORICSKoc96] P. C. Kocher. Timing attacks on implementations of Diffie-Hellman, RSA, DSS, and other systems Kanellakis and S. A. Smolka. CCS expressions, finite state processes, and three problems of equivalence Proc. 2nd Annual ACM Symp. on Principles of Distributed Computing, pp.170-184, 1983.

D. J. Mcculloughsc79-]-l, A. K. Stockmeyer, and . Chandra, Reif. The complexity of two-player games of incomplete information [Rus92] J. Rushby. Noninterference, transitivity, and channel-control security policies Provably difficult combinatorial games Word problems requiring exponential time (preliminary report) A comparison of semantic models for noninterference, Proc. IEEE Symp. on Security and Privacy Proc. ACM symp. on Theory of computing Proc. 4th Int. Workshop on Formal Aspect in Security and Trust (LNCS 4691), pp.177-186274, 1973.

R. Van-der-meyden and C. Zhang, Algorithmic Verification of Noninterference Properties, ENTCS, pp.61-75, 2007.
DOI : 10.1016/j.entcs.2006.11.002

R. Van-der-meyden, C. M. Zhang-[-vs97-]-d, G. Volpano, . J. Smith, D. M. Wittbold et al., Information flow in systems with schedulers A type-based approach to program security Information flow in nondeterministic systems, Proc. Computer Security Foundation Symp. TAPSOFT, volume 1214 of Lecture Notes in Computer Science Proc. IEEE Symp. on Security and Privacy, pp.301-312, 1990.