@string{csp = "Computer Science Press, New York"} %@string{lnai = "Lecture Notes in Artificial Intelligence"} %@string{lncs = "Lecture Notes in Computer Science"} @string{lncs = "LNCS"} %@string{mit = "The MIT Press, Cambridge, Mass."} @string{mit = "The MIT Press"} %@string{springer = "Springer-Verlag, Berlin"} @string{springer = "Springer-Verlag"} @string{addison = "Addison-Wesley"} @string{holland = {North Holland, Amsterdam}} @string{kluwer = {Kluwer Academic Publishers}} @string{morgan = {Morgan Kaufman, San Mateo, CA}} @string{ cpam = "Comm. Pure App. Math. "} @string{ jar = "Journal of Automated Reasoning"} @string{jsl = "Journal of Symbolic Logic" } @string{ cpam = "Comm. Pure App. Math. "} @string{ jsc = "Journal of Symbolic Computation" } @string{ jlc = "Journal of Logic and Computation" } @string{ jlp = "Journal of Logic Programming" } @string{ jacm = "Journal of the Association for Computing Machinery"} @string{lemat = "Matematiche"} @string{sl ="Studia Logica"} @string{joacm = "Journal of the ACM"} @string{tcs = "Theoretical Computer Science"} @string{toplas = "ACM Transactions on Programming Languages and Systems"} @string{infocom = "Information and Computation"} @string{ngc = "New generation Computing"} @string{funda = {Fundamenta Informaticae}} @Article{BSS, author = {Blum, L. and Shub, M. and Smale, S.}, title = {{On a Theory of Computation and Complexity over the Real Numbers: NP-completeness, recursive functions and universal machines}}, journal = {Bull. Amer. Math. Soc.}, year = {1989}, volume = {21}, pages = {1--46} } @inproceedings{csfw04, author = {A. Bossi and C. Piazza and S. Rossi}, title = {Modelling {D}owngrading in {I}nformation {F}low {S}ecurity}, booktitle = {Proc. of the 17th IEEE Computer Security Foundations Workshop (CSFW'04)}, year = {2004}, pages = {187-201}, publisher = {IEEE Computer Society Press}, } @inproceedings{BAR04, author = {Barthe, G. and D'Argenio, P. and Rezk, T.}, title = {Secure {I}nformation {F}low by {S}elf {C}omposition}, booktitle = {Proc. of the 17th IEEE Computer Security Foundations Workshop (CSFW'04)}, year = {2004}, pages = {100--114}, publisher = {IEEE Computer Society Press}, } @inproceedings{csfw03, author = {A. Bossi and D. Macedonio and C. Piazza and S. Rossi}, title = {Secure {C}ontexts for {C}onfidential {D}ata}, booktitle = {Proc. of the 16th IEEE Computer Security Foundations Workshop (CSFW'03)}, year = {2003}, pages = {14--25}, publisher = {IEEE Computer Society Press}, } @inproceedings{ICTCS03, author = {A. Bossi and D. Macedonio and C. Piazza and S. Rossi}, title = {Information {F}low {S}ecurity and {R}ecursive {S}ystems}, booktitle = {Proc. of the Italian Conference on Theoretical Computer Science ({ICTCS}'03)}, year = {2003}, pages = {369--382}, volume = {2841}, series = "LNCS", publisher = "Springer-Verlag", } @inproceedings{SEFM03, author = {A. Bossi and R. Focardi and C. Piazza and S. Rossi}, title = {Refinement {O}perators and {I}nformation {F}low {S}ecurity}, booktitle = {Proc. of the 1st IEEE Int. Conference on Software Engineering and Formal Methods (SEFM'03)}, year = {2003}, pages = {44--53}, publisher = {IEEE Computer Society Press}, } @inproceedings{RG99, author = "Roscoe, A. W. and Goldsmith, M. H.", title = "What Is Intransitive Noninterference?", booktitle = {Proc. of the IEEE Computer Security Foundations Workshop (CSFW'99)}, pages = {228--238}, year = {1999}, publisher = {IEEE Computer Society Press}, } @manual{orange, organization = "{US} {Departement} {of} Defence", TITLE = "DoD {T}rusted {C}omputer {S}ystem {E}valuation {C}riteria", YEAR = "1985", note = "DOD 5200.28-STD", } @ARTICLE{Shields89, AUTHOR = "M.W. Shields", TITLE = "Implicit {S}ystem {V}erification and the {I}nterface {E}quation", JOURNAL = "The {C}omputer {J}ournal", YEAR = "1989", volume = "32", number = "5", pages = "399--412", } @INPROCEEDINGS{RMMG01, AUTHOR = "P.Y.A. Ryan and J. McLean and J. Millen and V. Gilgor", TITLE = "Non-interference, {W}ho {N}eeds {I}t?", BOOKTITLE = "Proc. of the IEEE Computer Security Foundations Workshop (CSFW'01)", pages = "237--238", YEAR = "2001", publisher = "IEEE Computer Society Press", } @INPROCEEDINGS{NDS, AUTHOR = "J. T. Wittbold and D. M. Johnson", TITLE = "{``Information Flow in Non\-deterministic Systems''}", BOOKTITLE = "Proceedings of the 1990 IEEE Symposium on Research in Security and Privacy", PUBLISHER = "IEEE Computer Society Press", YEAR = "1990", PAGES = "144-161" } @INPROCEEDINGS{PHW02, author = {A. {Di Pierro} and C. Hankin and H.Wiklicky}, title = {Approximate {N}on-{I}nterference}, booktitle = {Proc. of the IEEE Computer Security Foundations Workshop (CSFW'02)}, pages = {3--17}, year = {2002}, publisher = {IEEE Computer Society Press}, } @inproceedings{BDNN01, author = "Bodei, C. and Degano, P. and Nielson, F. and Riis Nielson, H.", title = "Static Analysis for Secrecy and Non-interference in Networks of Processes", booktitle = {Proc. of International Conference on Parallel Computing Technologies}, series = "Lecture Notes in Computer Science", publisher = springer, editor = "Victor E. Malyshkin", volume = "2127", pages = "27--41", year = "2001", } @INPROCEEDINGS{Low02, author = {G. Lowe}, title = {Quantifying {I}nformation {F}low}, booktitle = {Proc. of the IEEE Computer Security Foundations Workshop (CSFW'02)}, pages = {18--31}, year = {2002}, publisher = {IEEE Computer Society Press}, } @InProceedings{SM02, author = "A. Sabelfeld and H. Mantel", title = "Static {C}onfidentiality {E}nforcement for {D}istributed {P}rograms", booktitle = "Proc. of Int. Static Analysis Symposium (SAS'02)", series = lncs, publisher = springer, year = "2002", editor = {Hermenegildo, M. V. and G. Puebla}, volume = {2477}, pages = "376--394 ", } @inproceedings{Ryan01, author = {P.Y.A Ryan}, title = {{M}athematical {M}odels of {C}omputer {S}ecurity}, booktitle = {Foundations of Security Analysis and Design}, year = {2001}, pages = "1--62", editor = {R. Focardi and R. Gorrieri}, volume = {2171}, series = lncs, publisher = springer, } @PHDTHESIS{TesiMart, author = {F. Martinelli}, title = {Formal {M}ethods for the {A}nalysis of {O}pen {S}ystems with {A}pplications to {S}ecurity {P}roperties}, school = {University of Siena}, year = {1999}, month = {December}, type = {PhD Thesis}, } @TECHREPORT{Rush92, AUTHOR = "J. Rushby", TITLE = "Noninterference, Transitivity, and Channel-Control Security Policies", INSTITUTION = "SRI International", YEAR = "1992", number = "CSL-92-02", month = "December", source = "http://www.csl.sri.com/papers/csl-92-2/", } @ARTICLE{Mar03, author = {F. Martinelli}, title = {Analysis of {S}ecurity {P}rotocols as \emph{open} {S}ystems }, journal = tcs, year = {2003}, volume = {290}, number = {1}, pages = {1057--1106}, } @article{FG95, author = "R. Focardi and R. Gorrieri", title = " A {C}lassification of {S}ecurity {P}roperties for {P}rocess {A}lgebras", journal = "Journal of Computer Security", volume = "3", number = "1", pages = "5--33", year = "1994/1995", } @article{ABG04, author = "Aldini, A. and Bravetti, M. and Gorrieri, R.", title = "A {P}rocess-algebraic {A}pproach for the {A}nalysis of {P}robabilistic {N}on-interference", journal = "Journal of Computer Security", year = "2004", note = "To appear", } @ARTICLE{AA99, author = {M. Abadi}, title = {{S}ecrecy by {T}yping in {S}ecurity {P}rotocols}, journal = joacm, year = {1999}, volume = {46}, number = {5}, pages = {749--786}, } @ARTICLE{spiin, author = {M. Abadi and Gordon, A. D.}, title = {A {C}alculus for {C}ryptographic {P}rotocols: {T}he {S}pi {C}alculus}, journal = infocom, year = {1999}, volume = {148}, number = {1}, pages = {1--70}, } @TECHREPORT{BLP, author = {D.~E. Bell and L.~J.~La Padula}, title = {Secure Computer Systems: Unified Exposition and Multics Interpretation}, institution = {MITRE MTR-2997}, year = {1975}, type = {Technical Report}, number = {ESD-TR-75-306}, } @ARTICLE{MuTracce, author = {J. Mullins}, title = {Nondeterministic {A}dmissible {I}nterference}, journal = {Journal of Universal Computer Science}, year = {2000}, volume = {11}, pages = {1054--1070}, } @ARTICLE{MuBisi, author = {S. Lafrance and J. Mullins}, title = {{B}isimulation-based {N}on-deterministic {A}dmissible {I}nterference and its {A}pplication to the {A}nalysis of {C}ryptographic {P}rotocols}, journal = {Electronic Notes in Theoretical Computer Science}, year = {2002}, volume = {61}, pages = {1--24}, } @ARTICLE{BDFP01, author = {C. Bodei and P. Degano and R. Focardi and C. Priami}, title = {{P}rimitives for {A}uthentication in {P}rocess {A}lgebras}, journal = tcs, year = {2002}, volume = {283}, number = {2}, pages = {271--304}, } @TECHREPORT{BDFP02tr, author = {C. Bodei and P. Degano and R. Focardi and C. Priami}, title = {{P}rimitives for {A}uthentication in {P}rocess {A}lgebras}, institution = {Dipartimento di Informatica e Telecomunicazioni, Universit\`a degli Studi di Trento, Italy}, year = {2002}, type = {Technical Report}, number = {DIT-02-019} } @inproceedings{LOPSTR02, author = {A. Bossi and R. Focardi and C. Piazza and S. Rossi}, title = {A {P}roof {S}ystem for {I}nformation {F}low {S}ecurity}, booktitle = {Logic Based Program Development and Transformation}, year = {2003}, editor = {M. Leuschel}, series = lncs, pages = {199--218}, publisher = springer, volume = {2664}, } @inproceedings{AMAST02, author = "A. Bossi and R. Focardi and C. Piazza and S. Rossi", title = "Transforming {P}rocesses to {E}nsure and {C}heck {I}nformation {F}low {S}ecurity", editor = "H. Kirchner and C. Ringeissen", booktitle = "Int. Conference on Algebraic Methodology and Software Technology ({AMAST}'02)", series = lncs, pages = "271--286", volume = "2422", publisher = springer, year = "2002" } @inproceedings{DMP01, author = {Durgin, N. A. and Mitchell, J. C. and Pavlovic, D.}, title = {A {C}ompositional {L}ogic for {P}rotocol {C}orrectness}, booktitle = {Proc. of the IEEE Computer Security Foundations Workshop (CSFW'01)}, pages ={241--260}, publisher = {IEEE Computer Society Press}, year = 2001, } @ARTICLE{FG97, author = {R. Focardi and R. Gorrieri}, title = {The {C}ompositional {S}ecurity {C}hecker: A {T}ool for the {V}erification of {I}nformation {F}low {S}ecurity {P}roperties}, journal = {IEEE Transactions on Software Engineering}, year = {1997}, volume = {23}, number = {9}, pages = {550--571}, } @inproceedings{FG01, author = {R. Focardi and R. Gorrieri}, title = {Classification of {S}ecurity {P}roperties ({P}art {I}: {I}nformation {F}low)}, booktitle = {Proc. of Foundations of Security Analysis and Design (FOSAD'01)}, year = {2001}, pages = {331--396}, editor = {R. Focardi and R. Gorrieri}, volume = {2171}, series = lncs, publisher = springer, } @inproceedings{FGM-ICALP, author = {R. Focardi and R. Gorrieri and F. Martinelli}, title = {{N}on {I}nterference for the {A}nalysis of {C}ryptographic {P}rotocols}, booktitle = {Proc. of Int. Colloquium on Automata, Languages and Programming (ICALP'00)}, year = {2000}, editor = {Montanari, U. and Rolim, J. D. P. and Welzl, E.}, volume = {1853}, pages = {744--755}, series = lncs, publisher = springer, } @inproceedings{VMCAI02, author = {R. Focardi and C. Piazza and S. Rossi}, title = {{P}roof {M}ethods for {B}isimulation based {I}nformation {F}low {S}ecurity}, booktitle = {Proc. of Int. Workshop on Verification, Model Checking and Abstract Interpretation (VMCAI'02)}, year = {2002}, editor = {A. Cortesi}, volume = {2294}, pages = {16--31}, series = lncs, publisher = springer, } @inproceedings{FM99, author = {R. Focardi and F. Martinelli}, title = {A {U}niform {A}pproach for the {D}efinition of {S}ecurity {P}roperties}, booktitle = {Proc. of World Congress on Formal Methods (FM'99)}, year = {1999}, editor = {Wing, J.M. and Woodcook, J. and Davies, J.}, volume = {1708}, pages = {794--813}, series = lncs, publisher = springer, } @inproceedings{Fol87, author = {Foley, S. N.}, title = {A {U}niversal {T}heory of {I}nformation {F}low}, booktitle = {Proc. of the IEEE Symposium on Security and Privacy (SSP'87)}, year = {1987}, pages = {116--122}, publisher = {IEEE Computer Society Press}, } @inproceedings{Pinsky95, author = {Pinsky, S.}, title = {Absorbing {C}overs and {I}ntransitive {N}oninterference}, booktitle = {Proc. of the IEEE Symposium on Security and Privacy (SSP'95)}, year = {1995}, pages = {102--113}, publisher = {IEEE Computer Society Press}, } @PHDTHESIS{For99, author = {R. Forster}, title = {Non-{I}nterference {P}roperties for {N}ondeterministic {P}rocesses}, school = {Oxford University Computing Laboratory}, year = {1999}, } @inproceedings{GCS91, author = {Graham-Cumming, J. and Sanders, J. W.}, title = {On the {R}efinement of {N}on-{I}nterference}, booktitle = {Proc. of the IEEE Computer Security Foundations Workshop (CSFW'91)}, year = {1991}, pages = {35--42}, publisher = {IEEE Computer Society Press}, } @inproceedings{GM82, author = {Goguen, J. A. and Meseguer, J.}, title = {{S}ecurity {P}olicies and {S}ecurity {M}odels}, booktitle = {Proc. of the IEEE Symposium on Security and Privacy (SSP'82)}, year = {1982}, pages = {11--20}, publisher = {IEEE Computer Society Press}, } @inproceedings{GM84, author = {Goguen, J. A. and Meseguer, J.}, title = {{U}nwinding and {I}nference {C}ontrol}, booktitle = {Proc. of the IEEE Symposium on Security and Privacy (SSP'84)}, year = {1984}, pages = {75--86}, publisher = {IEEE Computer Society Press}, } @inproceedings{Jac89, author = {Jacob, J.}, title = {On the {D}erivation of {S}ecure {C}omponents}, booktitle = {Proc. of the IEEE Symposium on Security and Privacy (SSP'89)}, year = {1989}, pages = {242--247}, publisher = {IEEE Computer Society Press}, } @inproceedings{JT88, author = {Johnson, D. M. and Thayer, F. J.}, title = {Security and the {C}omposition of {M}achines}, booktitle = {Proc. of the IEEE Computer Security Foundations Workshop (CSFW'88)}, publisher = {IEEE Computer Society Press}, year = 1988, pages = {72--89}, } @inproceedings{Man00, author = {Mantel, H.}, title = {Possibilistic {D}efinitions of {S}ecurity - {A}n {A}ssembly {K}it -}, booktitle = {Proc. of the IEEE Computer Security Foundations Workshop (CSFW'00)}, year = {2000}, pages = {185--199}, publisher = {IEEE Computer Society Press}, } @inproceedings{Man00b, author = {Mantel, H.}, title = {Unwinding {P}ossibilistic {S}ecurity {P}roperties}, booktitle = {Proc. of the European Symposium on Research in Computer Security (ESoRiCS'00)}, year = {2000}, series = lncs, publisher = springer, pages = {238--254}, volume = {2895}, } @inproceedings{Man01, author = {Mantel, H.}, title = {Preserving {I}nformation {F}low {P}roperties under {R}efinement}, booktitle = {Proc. of the IEEE Symposium on Security and Privacy (SSP'01)}, year = {2001}, pages = {78--91}, publisher = {IEEE Computer Society Press}, } @inproceedings{Man02, author = {Mantel, H.}, title = {On the {C}omposition of {S}ecure {S}ystems}, booktitle = {Proc. of the IEEE Symposium on Security and Privacy (SSP'02)}, year = {2002}, pages = {88--101}, publisher = {IEEE Computer Society Press}, } @inproceedings{McC87, author = {McCullough, D.}, title = {Specifications for {M}ulti-{L}evel {S}ecurity and a {H}ook-{U}p {P}roperty}, booktitle = {Proc. of the IEEE Symposium on Security and Privacy (SSP'87)}, year = {1987}, pages = {161--166}, publisher = {IEEE Computer Society Press}, } @inproceedings{McL90, author = {McLean, J.}, title = {Security {M}odels and {I}nformation {F}low}, booktitle = {Proc. of the IEEE Symposium on Security and Privacy (SSP'90)}, year = {1990}, pages = {180--187}, publisher = {IEEE Computer Society Press}, } @inproceedings{McL94, author = {McLean, J.}, title = {A {G}eneral {T}heory of {C}omposition for {T}race {S}ets {C}losed under {S}elective {I}nterleaving {F}unctions}, booktitle = {Proc. of the IEEE Symposium on Security and Privacy (SSP'94)}, year = {1994}, pages = {79--93}, publisher = {IEEE Computer Society Press}, } @article{McL94b, author = {McLean, J.}, title = {Security {M}odels}, journal = {Encyclopedia of Software Engineering}, year = {1994}, publisher = {Wiley & Sons}, } @ARTICLE{McL96, author = {McLean, J.}, title = {A {G}eneral {T}heory of {C}omposition for a {C}lass of ``{P}ossibilistic'' {S}ecurity {P}roperties}, journal = {IEEE Transactions on Software Engineering}, year = {1996}, volume = {22}, number = {1}, pages = {53--67}, } @inproceedings{Mar98, author = {Martinelli, F.}, title = {Partial {M}odel {C}hecking and {T}heorem {P}roving for {E}nsuring {S}ecurity {P}roperties}, booktitle = {Proc. of the IEEE Computer Security Foundations Workshop (CSFW'98)}, year = {1998}, pages = {44--52}, publisher = {IEEE Computer Society Press}, } @inproceedings{FGM00, author = "Focardi, R. and Gorrieri, R. and Martinelli, F.", title = "Information Flow Analysis in a Discrete-Time Process Algebra", booktitle = {Proc. of the IEEE Computer Security Foundations Workshop (CSFW'00)}, year = {2000}, pages = {170--184}, publisher = {IEEE Computer Society Press}, } @inproceedings{GLM03, author = {Gorrieri, R. and Locatelli, E. and Martinelli, F.}, title = {A Simple Language for Real-Time Cryptographic Protocol Analysis}, booktitle = {Proc. of European Symposium on Programming (ESOP'03)}, year = {2003}, pages = {114--128}, editor = {P. Degano}, volume = {2618}, series = lncs, publisher = springer, } @inproceedings{Mil94, author = {Millen, J. K.}, title = {Unwinding {F}orward {C}orrectability}, booktitle = {Proc. of the IEEE Computer Security Foundations Workshop (CSFW'94)}, year = {1994}, pages = {2--10}, publisher = {IEEE Computer Society Press}, } @BOOK{Mil89, author = {R. Milner}, title = {Communication and {C}oncurrency}, publisher = {Prentice-Hall}, year = {1989}, } @ARTICLE{MM0, author = {M. M\"{u}ller-Olm}, title = {Derivation of {C}haracteristic {F}ormulae}, journal = {Electronic Notes in Theoretical Computer Science}, year = {1998}, volume = {18}, } @inproceedings{O'H90, author = {O'Halloran, C.}, title = {A {C}alculus of {I}nformation {F}low}, booktitle = {Proc. of the European Symposium on Research in Security and Privacy (ESoRiCS'90)}, year = {1990}, pages = {180--187}, publisher = {AFCET}, } @inproceedings{O'H92, author = {O'Halloran, C.}, title = {Refinement and {C}onfidentiality}, booktitle = {Proc. of the 5th Refinement Workshop}, year = {1992}, pages = {119--139}, } @inproceedings{Paulson97csfwa, author = {Paulson, L. C.}, title = {Proving {P}roperties of {S}ecurity {P}rotocols by {I}nduction}, booktitle = {Proc. of the IEEE Computer Security Foundations Workshop (CSFW'97)}, year = {1997}, pages = {70--83}, publisher = {IEEE Computer Society Press}, } @inproceedings{RWW94, author = {Roscoe, A. W. and Woodcock, J. C. P. and Wulf, L.}, title = {Non-{I}nterference through {D}eterminism}, booktitle = {Proc. of the European Symposium on Research in Computer Security (ESoRiCS'94)}, year = {1994}, series = lncs, publisher = springer, pages = {33--53}, volume = {875}, } @article{RWW96, author = {Roscoe, A. W. and Woodcock, J. C. P. and Wulf, L.}, title = {Non-{I}nterference through {D}eterminism}, journal = {Journal of Computer Security}, year = {1996}, volume = {4}, number = {1}, } @inproceedings{SS00, author = {Sabelfeld, A. and Sands, D.}, title = {{P}robabilistic {N}oninterference for {M}ulti-threaded {P}rograms}, booktitle = {Proc. of the IEEE Computer Security Foundations Workshop (CSFW'00)}, year = {2000}, pages = {200--215}, publisher = {IEEE Computer Society Press}, } @inproceedings{SS05, author = {Sabelfeld, A. and Sands, D.}, title = {Dimensions and {P}rinciples of {D}eclassification}, booktitle = {Proc. of the IEEE Computer Security Foundations Workshop (CSFW'05)}, year = {2005}, pages = {255--269}, publisher = {IEEE Computer Society Press}, } @inproceedings{MS91, author = {Montanari, U. and Sassone, V.}, title = {{CCS} {D}ynamic {B}isimulation is {P}rogressing}, booktitle = {Proc. of the Int. Symposium on Mathematical Foundations of Computer Science (MFCS'91)}, year = {1991}, pages = {346--356}, series = lncs, volume = {520}, publisher = springer, } @ARTICLE{Rya91, author = {Ryan, P. Y. A.}, title = {A {CSP} {F}ormulation of {N}on-{I}nterference and {U}nwinding}, journal = {Cipher}, year = {1991}, pages = {19--27}, } @ARTICLE{schnTSE, author = {S. Schneider}, title = {Verifying {A}uthentication {P}rotocols in {CSP}}, journal = {IEEE Transactions on Software Engineering}, year = {1998}, volume = {24}, number = {9}, } @ARTICLE{Sch00, author = {S. Schneider}, title = {May {T}esting, {N}on-{I}nterference, and {C}ompositionality}, journal = {Electronic Notes in Theoretical Computer Science}, year = {2000}, volume = {40}, } @inproceedings{SM00, author = {V. Shmatikov and Mitchell, J. C.}, title = {{A}nalysis of a {F}air {E}xchange {P}rotocol}, booktitle = {Proc. Symposium on Network and Distributed System Security (NDSS'00)}, year = {2000}, pages = {119--128}, publisher = {Internet Society}, } @inproceedings{SV98, author = {G. Smith and Volpano, D. M.}, title = {Secure {I}nformation {F}low in a {M}ulti-threaded {I}mperative {L}anguage}, booktitle = {Proc. of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'98)}, year = {1998}, pages = {355--364}, publisher = {ACM Press}, } @inproceedings{VS00, author = {Volpano, D. M. and Smith, G.}, title = {Verifying {S}ecrets and {R}elative {S}ecrecy}, booktitle = {Proc. of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'00)}, year = {2000}, pages = {268--276}, publisher = {ACM Press}, } @ARTICLE{SI94, author = {B. Steffen and A. Ing\`olfsd\`ottir}, title = {Characteristic {F}ormulae for {Processes} with {D}ivergence}, journal = infocom, year = {1994}, volume = {110}, number = {1}, pages = {149--163}, } @inproceedings{Sti96, author = {Stirling, C.}, title = {Modal and {T}emporal {L}ogics for {P}rocesses}, booktitle = {Logics for Concurrency: Structures versus Automata}, year = {1996}, editor = {E. Brinksma and R. Cleaveland and Larsen, K.~G. T. Margaria and B. Steffen}, volume = {1043}, pages = {149--237}, series = lncs, publisher = springer, } @inproceedings{Sut86, author = {Sutherland, D.}, title = {A {M}odel of {I}nformation}, booktitle = {Proc. of the 9th National Computer Security Conference}, year = {1986}, pages = {175--183}, } @ARTICLE{VS99, author = {Volpano, D. M. and Smith, G.}, title = {Probabilistic {N}oninterference in a {C}oncurrent {L}anguage}, journal = {Journal of Computer Security}, year = {1999}, volume = {7}, number = {2-3}, pages = {231 - 253}, } @inproceedings{VS97, author = "D. M. Volpano and G. Smith", title = "A {T}ype-{B}ased {A}pproach to {P}rogram {S}ecurity", booktitle = "{TAPSOFT}", pages = "607-621", year = "1997" } @inproceedings{ZL97, author = {Zakinthinos, A. and Lee, E. S.}, title = {A {G}eneral {T}heory of {S}ecurity {P}roperties}, booktitle = {Proc. of the IEEE Symposium on Security and Privacy (SSP'97)}, year = {1997}, pages = {74--102}, publisher = {IEEE Computer Society Press}, } @TECHREPORT{TR-pbndc, author = {R. Focardi and S. Rossi}, title = {Information {F}low {S}ecurity in {D}ynamic {C}ontexts}, institution = {Dipartimento di Informatica, Universit\`a Ca' Foscari di Venezia, Italy}, year = {2001}, type = {Technical Report}, number = {CS-2001-16}, } @unpublished{WITS02, author = {R. Focardi and S. Rossi}, title = {A {S}ecurity {P}roperty for {P}rocesses in {D}ynamic {C}ontexts (extended abstract)}, note = {In \emph{Proc. of Workshop on Issues in the Theory of Security (WITS'02)}.}, } @ARTICLE{Ko83, author = {D. Kozen}, title = {Results on the {P}ropositional $\mu$-calculus}, journal = tcs, year = {1983}, volume = {27}, pages = {333--354}, } @ARTICLE{Ta55, author = {A. Tarski}, title = {A {L}attice-{T}heoretical {F}ixpoint {T}heorem and its {A}pplication}, journal = {Pacific Journal of Mathematics}, year = {1955}, volume = {5}, pages = {285--309}, } @inproceedings{Ma95, author = {A. Mader}, title = {Modal $\mu$-calculus, {M}odel {C}hecking, and {G}auss elimination}, booktitle = {Proc. of Int. Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'95)}, year = {1995}, editor = {E. Brinksma and R. Cleaveland and Larsen, K.G. T. Margaria and B. Steffen}, volume = {1019}, pages = {72--88}, series = lncs, publisher = springer, } @inproceedings{NCSU, author = {R. Cleaveland and S. Sims}, title = {The {NCSU} {C}oncurrency {W}orkbench}, booktitle = {Proc. of Int. Conference on Computer Aided Verification (CAV'96)}, year = {1996}, editor = {R. Alur and T. Henzinger}, volume = {1102}, pages = {394--397}, series = lncs, publisher = springer, } @article{PT87, author = {Paige, R. and Tarjan, R. E.}, title = {Three {P}artition {R}efinement {A}lgorithms}, journal = {{SIAM} {J}ournal on {C}omputing}, year = 1987, volume = 16, number = 6, pages = {973--989}, } @InProceedings{XEVE, author = {A. Bouali}, title = {{XEVE}, an {ESTEREL} verification environment}, booktitle = {Proc. of Int. Conference on Computer Aided Verification (CAV'98)}, editor = {A. J. Hu and M. Y. Vardi}, volume = {1427}, OPTnumber = {}, series = lncs, pages = {500--504}, year = {1998}, OPTmonth = {}, OPTorganization = {}, publisher = springer} @InProceedings{BS92, author = {A. Bouali and R. de Simone}, title = {Symbolic {B}isimulation {M}inimization}, booktitle = {Proc. of Int. Conference on Computer Aided Verification (CAV'92)}, OPTcrossref = {}, OPTkey = {}, editor = {G. von Bochmann and D. K. Probst}, volume = {663}, OPTnumber = {}, series = lncs, pages = {96--108}, year = {1992}, OPTmonth = {}, OPTorganization = {}, publisher = springer} @InProceedings{LY, author = {D. Lee and M. Yannakakis}, title = {Online {M}inimization of {T}ransition {S}ystems}, booktitle = {Proc. of ACM Symposium on Theory of Computing (STOC'92)}, OPTcrossref = {}, OPTkey = {}, OPTeditor = {}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, pages = {264--274}, year = {1992}, OPTorganization = {}, publisher = {ACM Press}} @InProceedings{DPP01, author = "A. Dovier and C. Piazza and A. Policriti", title = "A {F}ast {B}isimulation {A}lgorithm", pages = "79--90", editor = "G. Berry and H. Comon and A. Finkel", booktitle = "Proc. of Int. Conference on Computer Aided Verification ({CAV}'01)", series = lncs, volume = "2102", publisher = springer, year = "2001", } @PHDTHESIS{Nu95, author = {E. Nuutila}, title = {Efficient {T}ransitive {C}losure {C}omputation in {L}arge {D}igraphs}, school = {Helsinki University of Technology}, year = {1995}, } @InProceedings{GK79, author = "A. Goralcikova and V. Koubek", title = "A reduct and closure algorithm for graphs", pages = "301--307", booktitle = "Proc. of Mathematical Foundations of Computer Science (MFCS'79)", series = lncs, volume = "74", publisher = springer, year = "1979", } @InProceedings{CW87, author = {D. Coppersmith and S. Winograd}, title = {Matrix multiplication via arithmetic progression}, pages = {1--6}, booktitle = {Proc. of the 19th Symposium on Theory of Computing}, year = {1987}, } @BOOK{CGP, author = {Clarke, E. M. and O. Grumberg and Peled, D. A.}, title = {Model {C}hecking}, publisher = mit, year = {1999}, } @BOOK{Roscoe, author = {Roscoe, A. W.}, title = {The {T}heory and {P}ractice of {C}oncurrency}, publisher = {Prentice Hall}, year = {1998}, series = {Series in Computer Science}, } @InProceedings{LBC94, author = "D. Long and A. Browne and E. Clarke and S. Jha and W. Marrero", title = "An improved {A}lgorithm for the {E}valuation of {F}ixpoint expressions", pages = "338--350", editor = "D. L. Dill", booktitle = "Proc. of Int. Conference on Computer Aided Verification ({CAV}'94)", series = lncs, volume = "818", publisher = springer, year = "1994", } @InProceedings{FV99, author = {K. Fisler and Vardi, M. Y.}, title = {Bisimulation and {M}odel {C}hecking}, booktitle = {Proc. of Correct Hardware Design and Verification Methods (CHARME'99)}, OPTcrossref = {}, OPTkey = {}, editor = {L. Pierre and T. Kropf}, volume = {1703}, OPTnumber = {}, series = lncs, pages = {338--341}, year = {1999}, OPTmonth = {}, OPTorganization = {}, publisher = springer} @ARTICLE{KS90, author = "Kannellakis, P. C. and Smolka, S. A.", title = "{CCS} {E}xpressions, {F}inite {S}tate {P}rocesses, and {T}hree {P}roblems of {E}quivalence", journal = "Information and Computation", year = "1990", volume = "86", number = "1", pages = "43--68", } @BOOK{cormen, author = {Cormen, T. H. and Leiserson, C. E. and Rivest, R. L.}, title = {Introduction to {A}lgorithms}, publisher = mit, year = {1990}, } @inproceedings{Vol00, author = {D. Volpano}, title = {Secure {I}ntroduction of {O}ne-{W}ay {F}unctions}, booktitle = {Proc. of the IEEE Computer Security Foundations Workshop (CSFW'00)}, year = {2000}, pages = {246--254}, publisher = {IEEE Computer Society Press}, } @inproceedings{csfw02, author = {R. Focardi and S. Rossi}, title = {Information {F}low {S}ecurity in {D}ynamic {C}ontexts}, booktitle = {Proc. of the IEEE Computer Security Foundations Workshop (CSFW'02)}, year = {2002}, pages = {307--319}, publisher = {IEEE Computer Society Press}, } @TECHREPORT{rapp:fcs02, author = {A. Bossi and R. Focardi and C. Piazza and S. Rossi}, title = {Compositionality and {S}ecure {C}ontexts for Bisimulation-based Information Flow Security}, institution = {Dipartimento di Informatica, Universit\`a Ca' Foscari di Venezia, Italy}, year = {2002}, type = {Technical Report}, number = {CS-2002-6}, } @PHDTHESIS{TesiRic, author = {R. Focardi}, title = {Analysis and {A}utomatic {D}etection of {I}nformation {F}lows in {S}ystems and {N}etworks}, school = {University of Bologna}, year = {1999}, type = {PhD Thesis, UBLCS-99-16}, } @article{SM03, author = "A. Sabelfeld and A. C. Myers", title = "Language-{B}ased {I}nformation-{F}low {S}ecurity", journal = "IEEE Journal on Selected Areas in Communication", year = 2003, volume = 21, number = 1, pages = "5--19", } @TECHREPORT{rapp:wits03, AUTHOR = "A. Bossi and D. Macedonio and C. Piazza and S. Rosssi", TITLE = "Secure {C}ontexts for {I}nformation {F}low {S}ecurity", INSTITUTION = "Dipartimento di Informatica, Universit\`a Ca' Foscari di Venezia, Italy", YEAR = "2002", type = "Technical Report", number = "CS-2002-18",} @InProceedings{VMCAI03, author = "A. Bossi and R. Focardi and C. Piazza and S. Rossi", title = "Bisimulation and {U}nwinding for {V}erifying {P}ossibilistic {S}ecurity {P}roperties", booktitle = "Proc. of Int. Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'03)", series = lncs, publisher = springer, year = "2003", editor = { Zuck, L. D. and Attie, P. C. and Cortesi, A. and Mukhopadhyay, S.}, volume = {2575}, pages = "223--237", } @TECHREPORT{Low99, author = {G. Lowe}, title = {Defining {I}nformation {F}low}, institution = {Department of Mathematics and Computer Science, University of Leicester}, year = {1999}, type = {Technical Report}, number = {1999/3}, } @ARTICLE{RS01, author = "Ryan, P.Y.A. and Schneider, S.", title = "Process {A}lgebra and {N}on-{I}nterference", journal = "Journal of Computer Security", year = "2001", volume = "9", number = "1/2", pages = "75--103", } booktitle = "{PCSFW}: Proceedings of The 12th Computer Security Foundations Workshop", publisher = "IEEE Computer Society Press", year = "1999", url = "citeseer.nj.nec.com/roscoe99what.html" } @ARTICLE{HR03, author = {M. Hennessy and J. Riely}, title = {Information {F}low vs. {R}esource {A}ccess in the {A}synchronous {P}i-calculus}, journal = {ACM Transactions on Programming Languages and Systems (TOPLAS)}, volume = {24}, number = {5}, year = {2002}, pages = {566--591}, publisher = {ACM Press}, } @article{ML00, author = {Myers, A. C. and Liskov, B.}, title = {Protecting {P}rivacy {U}sing the {D}ecentralized {L}abel {M}odel}, journal = {ACM Transactions on Software Engineering and Methodology (TOSEM)}, volume = {9}, number = {4}, year = {2000}, pages = {410--442}, publisher = {ACM Press}, } @article{JL00, author = {Joshi, R. and Leino, K. R. M.}, title = {A {S}emantic {A}pproach to {S}ecure {I}nformation {F}low}, journal = {Science of Computer Programming}, volume = {37}, number = {1--3}, year = {2000}, pages = {113--138}, publisher = {Elsevier}, } @InProceedings{BCMS02, author = {M. Bugliesi and S. Crafa and M. Merro and V. Sassone}, title = {Communication {I}nterference in {M}obile {B}oxed {A}mbients}, editor = {M. Agrawal and A. Seth}, booktitle = {Proc. of Int. Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'02)}, publisher = springer, series = lncs, volume = {2556}, year = {2002}, pages = {71--84}, } @InProceedings{BBC03, author = {Benzaken, V. and Burelle, M. and Castagna, G.}, title = {Information flow security for XML transformations}, booktitle = {Proc. of Asian Computing Science Conference (ASIAN'03)}, publisher = springer, series = lncs, year = {2003}, note = {To appear}, } @article{Abadi99, author = "Mart{\'\i}n Abadi", title = "Secrecy by Typing in Security Protocols", journal = "{Journal of the ACM}", volume = "46", number = "5", pages = "749--786", year = "1999", } @InProceedings{BC01, author = {G. Boudol and I. Castellani}, title = {Noninterference for {C}oncurrent {P}rograms}, editor = {F. Orejas and P. G. Spirakis and J. van Leeuwen}, booktitle = {Proc. of Int. Colloquium on on Automata, Languages and Programming (ICALP'01)}, publisher = springer, series = lncs, volume = {2076}, year = {2001}, pages = {382--395}, } @ARTICLE{cl-vmcai03, author = {A. Bossi and R. Focardi and C. Piazza and S. Rossi}, title = {Verifying {P}ersistent {S}ecurity {P}roperties}, journal = {Computer Languages, Systems and Structures}, year = {2004}, volume = {30}, number = {3-4}, pages = {231-258}, } @inproceedings{PPR04, author = {C. Piazza and E. Pivato and S. Rossi}, title = {CoPS - {C}hecker of {P}ersistent {S}ecurity}, booktitle = {Proc. of International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'04)}, year = {2004}, note = {To appear.}, series = lncs, publisher = springer, } @inproceedings{BP03, author = {Backes, M. and Pfitzmann, B.}, title = {Intransitive {N}on-{I}nterference for Cryptographic Purposes}, booktitle = {Proc. of the IEEE Symposium on Security and Privacy (SSP'03)}, year = {2003}, pages = {140--152}, publisher = {IEEE Computer Society Press}, } @inproceedings{Man01a, author = {Mantel, H.}, title = {{I}nformation {F}low {C}ontrol and {A}pplications - {B}ridging a {G}ap}, booktitle = {Proc. of the nternational Symposium of Formal Methods Europe (FME'01)}, year = {2001}, pages = {153--172}, series = lncs, publisher = springer, } @ARTICLE{entcs-mefisto, author = {A. Bossi and R. Focardi and D. Macedonio and C. Piazza and S. Rossi}, title = {{U}nwinding in {I}nformation {F}low {S}ecurity}, journal = {Electronic Notes in Theoretical Computer Science}, year = {2004}, volume = {}, number = {}, pages = {}, note = {To appear. Available at \texttt{http://www.dsiunive.it/} \texttt{$\sim$srossi/entcs04.ps}}, } @TECHREPORT{action-ref, AUTHOR = "A. Bossi and D. Macedonio and C. Piazza and S. Rosssi", TITLE = "Compositional {A}ction {R}efinement and {I}nformation {F}low {S}ecurity", INSTITUTION = "Dipartimento di Informatica, Universit\`a Ca' Foscari di Venezia, Italy", YEAR = "2003", type = "Technical Report", number = "CS-2003-13", } @INPROCEEDINGS{ZM01, AUTHOR = "Zdancewic, S. and Myers, A. C.", TITLE = "Robust {D}eclassification", BOOKTITLE = "Proc. of the IEEE Computer Security Foundations Workshop (CSFW'01)", pages = "15--23", YEAR = "2001", publisher = "IEEE Computer Society Press", } @Article{Wir71, author = "N. Wirth", title = "{Program Development by Stepwise Refinement}", journal = "Communications of the ACM", volume = "14", number = "4", pages = "221--227", year = "1971", } @ARTICLE{HY87, author = {J. T. Haigh and W. D. Young}, title = {Extending the noninterference version of MLS for SAT}, journal = {IEEE Transactions on Software Engineering}, year = {1987}, volume = {13}, number = {2}, pages = {141--150}, } @ARTICLE{SRSKAT00, author = "G. Schellhorn and W. Reif and A. Schairer and P. A. Karger and V. Austel and D. Toll", title = "Verified {F}ormal {S}ecurity {M}odels for {M}ultiapplicative {S}mart {C}ards", journal = {Journal of Computer Security}, year = {2002}, volume = {10}, number = {2}, pages = {339--367}, } @InProceedings{NEL89, author = {Nielsen, M. and Engberg, U. and Larsen, K. S.}, title = {Fully {A}bstract {M}odels for a {P}rocess {L}anguage with {R}efinement}, editor = {J. W. de Bakker and W. P. de Roever and G. Rozenberg}, booktitle = {Workshop on Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency}, publisher = springer, series = lncs, volume = {354}, year = {1989}, pages = {523--548}, } @TECHREPORT{GorrieriTR, author = {Gorrieri, R. and Rensink, A.}, title = {{A}ction {R}efinement}, institution = {University of Bologna (Italy)}, year = {1999}, type = {Technical Report}, number = {UBLCS-99-09}, } @Article{GGR96, Author="U. Goltz and R. Gorrieri and A. Rensink", Title="{Comparing {S}yntactic and {S}emantic {A}ction {R}efinement}", Journal="Information and Computation", Volume=125, Number=2, Year=1996, Pages="118--143", } @Article{DG95, Author="P. Degano and R. Gorrieri", Title="{A {C}ausal {O}perational {S}emantics of {A}ction {R}efinement}", Journal="Information and Computation", Volume=122, Number=1, Year=1995, Pages="97--119", } @Article{GG01, author = "R. J. van Glabbeek and U. Goltz", title = "{{R}efinement of {A}ctions and {E}quivalence {N}otions for {C}oncurrent {S}ystems}", journal = "Acta Informatica", volume = "37", number = "4/5", pages = "229--327", year = "2001", } @InProceedings{GG89, author = "R. J. van Glabbeek and U. Goltz", title = "{{E}quivalence {N}otions for {C}oncurrent {S}ystems and {R}efinement of {A}ctions}", editor = {A. Kreczmar and G. Mirkowska}, booktitle = {Proc. of Mathematical Foundations of Computer Science (MFCS'89)}, publisher = springer, series = lncs, volume = {379}, year = {1989}, pages = {237--248}, } @Article{BV94, author = "J. W. de Bakker and E. P. de Vink", title = "Bisimulation {S}emantics for {C}oncurrency with {A}tomicity and {A}ction {R}efinement", journal = "Fundamenta Informaticae", volume = "20", number = "1", pages = "3--34", year = "1994", } @Article{Bou89, author = "G. Boudol", title = "{Atomic Actions}", journal = "Bulletin of the EATCS", volume = "38", pages = "136--144", year = "1989", } @Article{GMM90, author = "R. Gorrieri and S. Marchetti and U. Montanari", title = "A$^2${CCS}: {A}tomic actions for {CCS}", journal = tcs, volume = "72", number = "2-3", pages = "203--223", year = "1990", } @Article{AH94, author = "L. Aceto and M. Hennessy", title = "{Adding Action Refinement to a Finite Process Algebra}", journal = "Information and Computation", volume = "115", number = "2", pages = "179--247", year = "1994", } @proceedings{BRR90, editor = {J. W. de Bakker and W. P. de Roever and G. Rozenberg}, title = {{Stepwise Refinement of Distributed Systems, Models, Formalisms, Correctness, REX Workshop, Mook, The Netherlands, May 29 - June 2, 1989, Proceedings}}, booktitle = {REX Workshop}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {430}, year = {1990}, } @inproceedings{GM04, author = {R. Giacobazzi and I. Mastroeni}, title = {Abstract {N}on-{I}nterference: {P}arameterizing {N}on-{I}nterference by {A}bstract {I}nterpretation}, booktitle = {Proc. of ACM Symposium on Principles of Programming Languages (POPL'04)}, year = {2004}, pages = {186--197}, publisher = {ACM Press}, } @inproceedings{Agat00, author = {J. Agat}, title = {Transforming out {T}iming {L}eaks}, booktitle = {Proc. of ACM Symposium on Principles of Programming Languages (POPL'00)}, year = {2000}, pages = {40--53}, publisher = {ACM Press}, } @BOOK{winskel, AUTHOR = {G. Winskel}, TITLE = {The formal semantics of programming languages}, PUBLISHER = {The MIT Press}, YEAR = 1993 } @InProceedings{Collins, author = {Collins, G. E.}, title = {Quantifier Elimination for Real Closed Fields by Cylindrical Algebraic Decomposition}, booktitle = {2nd Gl Conf. on Automata Theory and Formal Languages}, pages = {134--183}, year = {1975}, editor = {H. Barkhage}, volume = {33}, series = lncs, publisher = springer, } @Book{Tar, author = {A. Tarski}, title = {A Decision Method for Elementary Algebra and Geometry}, publisher = {CA: University of California Press}, year = {1951}, edition = {2nd}, } @article{SS01, author = "A. Sabelfeld and D. Sands", title = "A {P}er {M}odel of {S}ecure {I}nformation {F}low in {S}equential {P}rograms ", journal = "Higher-Order and Symbolic Computation", volume = "14", number = "1", pages = "59--91", year = "2001", } @InProceedings{AB04, author = {T. Amtoft and A. Banerjee}, title = {Information {F}low {A}nalysis in {L}ogical {F}orm}, booktitle = {Proceedings of the 11th Static Analysis Symposium (SAS'04)}, pages = {100--115}, year = {2004}, volume = {3148}, series = {LNCS}, publisher = {Springer-Verlag}, } @Article{mati, author = {Matiyasevich, Y. V.}, title = {Enumerable sets are Diophantine}, journal = {Soviet Mathematics Doklady}, year = {1970}, volume = {11}, number = {2}, pages = {354--358}, } @ARTICLE{BC-tcs02, author = {G. Boudol and I. Castellani}, title = {Noninterference for {C}oncurrent {P}rograms and {T}read {S}ystems}, journal = tcs, year = {2002}, volume = {281}, number = {1}, pages = {109--130}, } @inproceedings{BPN04, author = {G. Barthe and L. Prensa Nieto}, title = {Formally {V}erifying {I}nformation {F}low {T}ype {S}ystems for {C}oncurrent and {T}hread systems}, booktitle = {Proc. of the ACM workshop on Formal {M}ethods in {S}ecurity {E}ngineering (FMSE'04)}, year = {2004}, pages = {13--22}, publisher = {ACM Press}, } @InProceedings{SM-isss03, author = {A. Sabelfeld and A. C. Myers}, title = {A {M}odel for {D}elimited {I}nformation {R}elease}, booktitle = {Proceedings of the International Symposium on Software Security, Theories and Systems (ISSS 2003)}, pages = {174--191}, year = {2003}, volume = {3233}, series = {LNCS}, publisher = {Springer-Verlag}, } @inproceedings{DvO-Noninfluence04, author = {Oheimb, David von}, title = {Information flow control revisited: {Noninfluence = Noninterference + Nonleakage}}, booktitle = {Proc. of the 9th European Symposium on Research in Computer Security (ESORICS'04)}, publisher = {Springer}, series = {LNCS}, volume = {3193}, pages = {225--243}, year = 2004, } @inproceedings{LZ05, author = {P. Li and S. Zdancewic}, title = {Downgrading {P}olicies and {R}elaxed {N}oninterference}, booktitle = {Proc. of ACM Symposium on Principles of Programming Languages (POPL'05)}, year = {2005}, pages = {158--170}, publisher = {ACM Press}, } @inproceedings{LS89, author = {K. G. Larsen and A. Skou}, title = {Bisimulation through {P}robabilistic {T}esting}, booktitle = {Proc. of ACM Symposium on Principles of Programming Languages (POPL'89)}, year = {1989}, pages = {344--352}, publisher = {ACM Press}, } @inproceedings{Smi01, author = {G. Smith}, title = {A {N}ew {T}ype {S}ystem for {S}ecure {I}nformation {F}low}, booktitle = {Proc. of the IEEE Computer Security Foundations Workshop (CSFW'01)}, year = {2001}, pages = {115--125}, publisher = {IEEE Computer Society}, } @inproceedings{Sabelfeld:PSI03, author = "A. Sabelfeld", title = "Confidentiality for {M}ultithreaded {P}rograms via {B}isimulation", booktitle = "Proc. of Andrei Ershov 5th International Conference on Perspectives of System Informatics (PSI'03)", pages = "260--273", year = 2003, series = "LNCS", volume = 2890, publisher = "Springer-Verlag", } @inproceedings{Myers99, author = {A. C. Myers}, title = {{JFlow}: {P}ractical {M}ostly-{S}tatic {I}nformation {F}low {C}ontrol}, booktitle = {Proc. of ACM Symposium on Principles of Programming Languages (POPL'99)}, year = {1999}, pages = {228-241}, publisher = {ACM Press}, } @inproceedings{MSZ04, author = {A. C. Myers and A. Sabelfeld and S. Zdancewic}, title = {Enforcing {R}obust {D}eclassification}, booktitle = {Proc. of the 17th IEEE Computer Security Foundations Workshop (CSFW'04)}, year = {2004}, pages = {172--186}, publisher = {IEEE Computer Society}, } @inproceedings{LOPSTR04, author = {A. Bossi and C. Piazza and S. Rossi}, title = {Unwinding {C}onditions for {S}ecurity in {I}mperative {L}anguages}, booktitle = {Logic Based Program Synthesis and Transformation (LOPSTR'04)}, note = {volume 3573}, series = lncs, year = {2005}, pages = "85--100"", publisher = springer, } @TECHREPORT{rapporto_esorics05, AUTHOR = "A. Bossi and C. Piazza and S. Rosssi", TITLE = "Compositional {I}nformation {F}low {S}ecurity for {C}oncurrent {P}rograms", INSTITUTION = "Dipartimento di Informatica, Universit\`a Ca' Foscari di Venezia, Italy", YEAR = "2005", type = "Technical Report", number = "CS-2005-?",} @article{grigoriev, author = "D. Grigoriev", title = "{Complexity of Deciding Tarski Algebra}", journal = "Journal of Symbolic Computation", volume = "5", pages = "65--108", year = "1988" } @Article{renegar, author = { J. Renegar}, title = {{On the Computational Complexity and Geometry of the First-order Theory of the Reals, parts I-III}}, journal = { Journal of Symbolic Computation }, year = {1992}, volume = {13}, pages = {255--352} } @Article{hong, author = {Collins, G. E. and H. Hong}, title = {{Partial cylindrical algebraic decomposition for quantifier elimination}}, journal = { Journal of Symbolic Computation }, year = {1991}, volume = {12}, pages = {299--328} } @inproceedings{MSAsian04, author = "Mantel, H. and Sands, D.", title = "{C}ontrolled {D}eclassification based on {I}ntransitive {N}oninterference", booktitle = "Proceedings of the 2nd ASIAN Symposium on Programming Languages and Systems, (APLAS'04)", pages = "129--145", year = "2004", series = "LNCS", volume = "3302", publisher = "Springer-Verlag", } @BOOK{andrews, author = {Andrews, G. R.}, title = {{F}oundation of {M}ultithreaded, {P}arallel, and {D}istributed {P}rogramming}, publisher = {addison}, year = {2000}, } @INPROCEEDINGS{Dam06, author = {Mads Dam}, title = {Decidability and proof systems for language-based noninterference relations}, booktitle = {POPL '06: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages}, year = {2006}, isbn = {1-59593-027-2}, pages = {67--78}, location = {Charleston, South Carolina, USA}, doi = {http://doi.acm.org/10.1145/1111037.1111044}, publisher = {ACM Press}, address = {New York, NY, USA}, }