R. Alur, S. Pavol?ern´ypavol?pavol?ern´pavol?ern´y, and . Zdancewic, Preserving Secrecy Under Refinement, ICALP '06 : Proceedings (Part II) of the 33rd International Colloquium on Automata, Languages and Programming, pp.107-118
DOI : 10.1007/11787006_10

B. Blanchet, M. Abadi, and C. Fournet, Automated Verification of Selected Equivalences for Security Protocols, 20th Annual IEEE Symposium on Logic in Computer Science (LICS' 05), pp.331-340, 2005.
DOI : 10.1109/LICS.2005.8

B. Blanchet, M. Abadi, and C. Fournet, Automated Verification of Selected Equivalences for Security Protocols, 20th Annual IEEE Symposium on Logic in Computer Science (LICS' 05), pp.331-340, 2005.
DOI : 10.1109/LICS.2005.8

. Bbb-+-07-]-e, M. Badouel, A. Bednarczyk, B. Borzyszkowski, P. Caillaud et al., Concurrent secrets. Discrete Event Dynamic Systems, pp.425-446, 2007.

]. A. Belinfante, J. Feenstra, R. De-vries, J. Tretmans, N. Goga et al., Formal Test Automation: A Simple Experiment, International Workshop on the Testing of Communicating Systems (IWTCS'99), pp.179-196, 1999.
DOI : 10.1007/978-0-387-35567-2_12

J. Bryans, M. Koutny, L. Mazaré, and P. Y. Ryan, Opacity Generalised to Transition Systems, Revised Selected Papers of the 3rd International Workshop on Formal Aspects in Security and Trust (FAST'05), pp.81-95, 2006.
DOI : 10.1007/11679219_7

W. Jeremy, M. Bryans, L. Koutny, P. Y. Mazaré, and . Ryan, Opacity generalised to transition systems, International Journal of Information Security, vol.7, issue.6, pp.421-435, 2008.

D. E. David, L. J. Bell, and . Padula, Secure computer system : Mathematical foundations, MITRE, 1973.

C. Constant, T. Jéron, H. Marchand, and V. Rusu, Integrating formal verification and conformance testing for reactive systems, IEEE Transactions on Software Engineering, vol.33, issue.8, pp.558-574, 2007.
DOI : 10.1109/TSE.2007.70707

URL : https://hal.archives-ouvertes.fr/inria-00422904

S. [. Cassandras and . Lafortune, Introduction to Discrete Event Systems, 1999.

J. Dubreil, . Ph, H. Darondeau, and . Marchand, Opacity enforcing control synthesis, 2008 9th International Workshop on Discrete Event Systems, 2008.
DOI : 10.1109/WODES.2008.4605918

URL : https://hal.archives-ouvertes.fr/inria-00344269

J. Dubreil, . Ph, H. Darondeau, and . Marchand, Supervisory Control for Opacity, IEEE Transactions on Automatic Control, vol.55, issue.5, 1921.
DOI : 10.1109/TAC.2010.2042008

URL : https://hal.archives-ouvertes.fr/inria-00483891

. Dfg-+-06-]-v, J. Darmaillacq, R. Fernandez, L. Groz, J. Mounier et al., Test generation for network security rules, LNCS, vol.3964, 2006.

T. [. Dubreil, H. Jéron, and . Marchand, Construction de moniteurs pour la surveillance de propriétés de sécurité, 6` eme Colloque Francophone sur la Modélisation des Systèmes Réactifs, 2007.

T. [. Dubreil, H. Jéron, and . Marchand, Monitoring information flow by diagnosis techniques, 1901.
URL : https://hal.archives-ouvertes.fr/inria-00312747

R. [. Focardi and . Gorrieri, Classification of security properties : Information flow, Foundations of Security Analysis and Design, pp.331-396, 2000.

]. T. Jé02 and . Jéron, Tgv : théorie, principes et algorithmes, Techniques et Sciences Informatiques, numéro spécial Test de Logiciels, pp.1265-1294, 2002.

J. Ligatti, L. Bauer, and D. Walker, Edit automata: enforcement mechanisms for run-time security policies, International Journal of Information Security, vol.3, issue.1-2, pp.2-16, 2005.
DOI : 10.1007/s10207-004-0046-8

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

[. Guernic, Information flow testing -the third path towards confidentiality guarantee, Advances in Computer Science, ASIAN 2007. Computer and Network Security, pp.33-47, 2007.

]. G. Low99 and . Lowe, Towards a completeness result for model checking of security protocols, Journal of Computer Security, vol.7, issue.2-3, pp.89-146, 1999.

L. Mazaré, Using unification for opacity properties, Proceedings of the 4th IFIP WG1.7 Workshop on Issues in the Theory of Security, pp.165-176, 2004.

W. [. Ramadge and . Wonham, The control of discrete event systems, Proceedings of the IEEE, vol.77, issue.1, pp.81-98, 1989.
DOI : 10.1109/5.21072

F. B. Schneider, Enforceable security policies, ACM Transactions on Information and System Security, vol.3, issue.1, pp.30-50, 2000.
DOI : 10.1145/353323.353382

A. [. Schneider and . Sidiropoulos, CSP and anonymity, Computer Security SORICS 96, pp.198-218, 1146.
DOI : 10.1007/3-540-61770-1_38

]. J. Tre96 and . Tretmans, Test generation with inputs, outputs and repetitive quiescence. Software?Concepts and Tools, pp.103-120, 1996.

]. J. Tre99 and . Tretmans, Testing concurrent systems : A formal approach, Concurrency Theory (CONCUR'99), number 1664 in LNCS, pp.46-65, 1999.