{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,13]],"date-time":"2026-04-13T04:58:16Z","timestamp":1776056296003,"version":"3.50.1"},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2012,1,19]],"date-time":"2012-01-19T00:00:00Z","timestamp":1326931200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2012,2]]},"DOI":"10.1007\/s10703-012-0141-9","type":"journal-article","created":{"date-parts":[[2012,1,18]],"date-time":"2012-01-18T12:13:31Z","timestamp":1326888811000},"page":"88-115","source":"Crossref","is-referenced-by-count":134,"title":["Synthesis of opaque systems with static and dynamic masks"],"prefix":"10.1007","volume":"40","author":[{"given":"Franck","family":"Cassez","sequence":"first","affiliation":[]},{"given":"J\u00e9r\u00e9my","family":"Dubreil","sequence":"additional","affiliation":[]},{"given":"Herv\u00e9","family":"Marchand","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2012,1,19]]},"reference":[{"key":"141_CR1","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1007\/11787006_10","volume-title":"ICALP\u201906: proceedings (Part II) of the 33rd international colloquium on automata, languages and programming","author":"R Alur","year":"2006","unstructured":"Alur R, \u010cern\u00fd P, Zdancewic S (2006) Preserving secrecy under refinement. In: ICALP\u201906: proceedings (Part II) of the 33rd international colloquium on automata, languages and programming. Springer, Berlin, pp 107\u2013118"},{"key":"141_CR2","doi-asserted-by":"crossref","first-page":"425","DOI":"10.1007\/s10626-007-0020-5","volume":"17","author":"E Badouel","year":"2007","unstructured":"Badouel E, Bednarczyk M, Borzyszkowski A, Caillaud B, Darondeau P (2007) Concurrent secrets. Discret Event Dyn Syst 17:425\u2013446","journal-title":"Discret Event Dyn Syst"},{"key":"141_CR3","first-page":"331","volume-title":"20th IEEE symposium on logic in computer science","author":"B Blanchet","year":"2005","unstructured":"Blanchet B, Abadi M, Fournet C (2005) Automated verification of selected equivalences for security protocols. In: 20th IEEE symposium on logic in computer science (LICS 2005), Chicago, IL, June 2005. IEEE Computer Society, Los Alamitos, pp 331\u2013340"},{"issue":"6","key":"141_CR4","doi-asserted-by":"crossref","first-page":"421","DOI":"10.1007\/s10207-008-0058-x","volume":"7","author":"J Bryans","year":"2008","unstructured":"Bryans J, Koutny M, Mazar\u00e9 L, Ryan P (2008) Opacity generalised to transition systems. Int J Inf Secur 7(6):421\u2013435","journal-title":"Int J Inf Secur"},{"issue":"4","key":"141_CR5","first-page":"497","volume":"88","author":"F Cassez","year":"2008","unstructured":"Cassez F, Tripakis S (2008) Fault diagnosis with static or dynamic diagnosers. Fundam Inform 88(4):497\u2013540","journal-title":"Fundam Inform"},{"key":"141_CR6","series-title":"Communications in computer and inform science","first-page":"307","volume-title":"4th int conf on mathematical methods, models and architectures for computer network security (MMM-ACNS\u201907)","author":"F Cassez","year":"2007","unstructured":"Cassez F, Mullins J, Roux OH (2007) Synthesis of non-interferent systems. In: 4th int conf on mathematical methods, models and architectures for computer network security (MMM-ACNS\u201907). Communications in computer and inform science, vol 1. Springer, Berlin, pp 307\u2013321"},{"key":"141_CR7","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"352","DOI":"10.1007\/978-3-642-04761-9_26","volume-title":"7th international symposium on automated technology for verification and analysis","author":"F Cassez","year":"2009","unstructured":"Cassez F, Dubreil J, Marchand H (2009) Dynamic observers for the synthesis of opaque systems. In: Liu Z, Ravn AP (eds) 7th international symposium on automated technology for verification and analysis (ATVA\u201909), Macao SAR, China, October 2009. LNCS, vol\u00a05799. Springer, Berlin, pp 352\u2013367"},{"key":"141_CR8","series-title":"LNCS","volume-title":"TestCom 2006","author":"V Darmaillacq","year":"2006","unstructured":"Darmaillacq V, Fernandez J-C, Groz R, Mounier L, Richier J-L (2006) Test generation for network security rules. In: TestCom 2006. LNCS, vol 3964"},{"key":"141_CR9","first-page":"37","volume-title":"Annual ACM IEEE design automation conference","author":"A Dasdan","year":"1999","unstructured":"Dasdan A, Irani S, Gupta R (1999) Efficient algorithms for optimum cycle mean and optimum cost to time ratio problems. In: Annual ACM IEEE design automation conference, New Orleans, Louisiana, United States. ACM, New York, pp 37\u201342"},{"key":"141_CR10","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1109\/WODES.2008.4605918","volume-title":"Proceedings of the 9th international workshop on discrete event systems","author":"J Dubreil","year":"2008","unstructured":"Dubreil J, Darondeau P, Marchand H (2008) Opacity enforcing control synthesis. In: Proceedings of the 9th international workshop on discrete event systems (WODES\u201908), G\u00f6teborg, Sweden, May 2008, pp\u00a028\u201335"},{"key":"141_CR11","doi-asserted-by":"crossref","first-page":"2584","DOI":"10.23919\/ECC.2009.7074795","volume-title":"European control conference, Budapest, Hungary, August 2009","author":"J Dubreil","year":"2009","unstructured":"Dubreil J, J\u00e9ron T, Marchand H (2009) Monitoring confidentiality by diagnosis techniques. In: European control conference, Budapest, Hungary, August 2009, pp 2584\u20132590"},{"issue":"5","key":"141_CR12","doi-asserted-by":"crossref","first-page":"1089","DOI":"10.1109\/TAC.2010.2042008","volume":"55","author":"J Dubreil","year":"2010","unstructured":"Dubreil J, Darondeau Ph, Marchand H (2010) Supervisory control for opacity. IEEE Trans Autom Control 55(5):1089\u20131100","journal-title":"IEEE Trans Autom Control"},{"key":"141_CR13","doi-asserted-by":"crossref","unstructured":"Falcone Y, Fernandez J-C, Mounier L (2011) What can you verify and enforce at runtime? Int J Softw Tools Technol Transf (STTT)","DOI":"10.1007\/s10009-011-0196-8"},{"key":"141_CR14","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"331","DOI":"10.1007\/3-540-45608-2_6","volume-title":"Foundations of security analysis and design I: FOSAD 2000 tutorial lectures","author":"R Focardi","year":"2001","unstructured":"Focardi R, Gorrieri R (2001) Classification of security properties (part I: Information flow). In: Focardi R, Gorrieri R (eds) Foundations of security analysis and design I: FOSAD 2000 tutorial lectures. Lecture notes in computer science, vol 2171. Springer, Heidelberg, pp 331\u2013396"},{"issue":"5","key":"141_CR15","doi-asserted-by":"crossref","first-page":"948","DOI":"10.1109\/TSMCB.2005.847749","volume":"35","author":"N Hadj-Alouane","year":"2005","unstructured":"Hadj-Alouane N, Lafrance S, Lin F, Mullins J, Yeddes M (2005) On the verification of intransitive noninterference in multilevel security. IEEE Trans Syst Man Cybern, Part B, Cybern 35(5):948\u2013957","journal-title":"IEEE Trans Syst Man Cybern, Part B, Cybern"},{"key":"141_CR16","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1016\/0012-365X(78)90011-0","volume":"23","author":"R Karp","year":"1978","unstructured":"Karp R (1978) A characterization of the minimum mean cycle in a digraph. Discrete Math 23:309\u2013311","journal-title":"Discrete Math"},{"key":"141_CR17","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/978-3-540-76929-3_4","volume-title":"Advances in computer science, ASIAN 2007, Computer and network security","author":"G Guernic Le","year":"2007","unstructured":"Le Guernic G (2007) Information flow testing\u2014the third path towards confidentiality guarantee. In: Advances in computer science, ASIAN 2007, Computer and network security. LNCS, vol 4846, pp\u00a033\u201347"},{"issue":"1\u20132","key":"141_CR18","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/s10207-004-0046-8","volume":"4","author":"J Ligatti","year":"2005","unstructured":"Ligatti J, Bauer L, Walker D (2005) Edit automata: enforcement mechanisms for run-time security policies. Int J Inf Secur 4(1\u20132):2\u201316","journal-title":"Int J Inf Secur"},{"issue":"2\u20133","key":"141_CR19","doi-asserted-by":"crossref","first-page":"89","DOI":"10.3233\/JCS-1999-72-302","volume":"7","author":"G Lowe","year":"1999","unstructured":"Lowe G (1999) Towards a completeness result for model checking of security protocols. J Comput Secur 7(2\u20133):89\u2013146","journal-title":"J Comput Secur"},{"issue":"2","key":"141_CR20","doi-asserted-by":"crossref","first-page":"363","DOI":"10.2307\/1971035","volume":"102","author":"D Martin","year":"1975","unstructured":"Martin D (1975) Borel determinacy. Ann Math 102(2):363\u2013371","journal-title":"Ann Math"},{"key":"141_CR21","first-page":"165","volume-title":"Proceedings of the 4th IFIP WG1.7 workshop on issues in the theory of security","author":"L Mazar\u00e9","year":"2004","unstructured":"Mazar\u00e9 L (2004) Using unification for opacity properties. In: Proceedings of the 4th IFIP WG1.7 workshop on issues in the theory of security (WITS\u201904), Barcelona (Spain), pp 165\u2013176"},{"key":"141_CR22","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1109\/WODES.2006.1678408","volume-title":"8th international workshop on discrete event systems","author":"SL Ricker","year":"2006","unstructured":"Ricker SL (2006) A question of access: decentralized control and communication strategies for security policies. In: 8th international workshop on discrete event systems, June 2006, pp 58\u201363"},{"issue":"1","key":"141_CR23","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1145\/353323.353382","volume":"3","author":"F Schneider","year":"2000","unstructured":"Schneider F (2000) Enforceable security policies. ACM Trans Inf Syst Secur 3(1):30\u201350","journal-title":"ACM Trans Inf Syst Secur"},{"key":"141_CR24","first-page":"1","volume-title":"STOC","author":"L Stockmeyer","year":"1973","unstructured":"Stockmeyer L, Meyer A (1973) Word problems requiring exponential time: Preliminary report. In: STOC. ACM, New York, pp 1\u20139"},{"issue":"4","key":"141_CR25","doi-asserted-by":"crossref","first-page":"307","DOI":"10.9746\/jcmsi.1.307","volume":"1","author":"S Takai","year":"2008","unstructured":"Takai S, Oka Y (2008) A formula for the supremal controllable and opaque sublanguage arising in supervisory control. J Control Meas Syst Integr 1(4):307\u2013312","journal-title":"J Control Meas Syst Integr"},{"key":"141_CR26","first-page":"1","volume-title":"Proc 12th annual symposium on theoretical aspects of computer science (STACS\u201995)","author":"W Thomas","year":"1995","unstructured":"Thomas W (1995) On the synthesis of strategies in infinite games. In: Proc 12th annual symposium on theoretical aspects of computer science (STACS\u201995), vol 900. Springer, Berlin, pp 1\u201313. Invited talk"},{"issue":"1\u20132","key":"141_CR27","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1016\/0304-3975(95)00188-3","volume":"158","author":"U Zwick","year":"1996","unstructured":"Zwick U, Paterson M (1996) The complexity of mean payoff games on graphs. Theor Comput Sci 158(1\u20132):343\u2013359","journal-title":"Theor Comput Sci"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-012-0141-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-012-0141-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-012-0141-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,22]],"date-time":"2019-06-22T13:01:15Z","timestamp":1561208475000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-012-0141-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,1,19]]},"references-count":27,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2012,2]]}},"alternative-id":["141"],"URL":"https:\/\/doi.org\/10.1007\/s10703-012-0141-9","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,1,19]]}}}