\begin{thebibliography}{10}

\bibitem{Abadi:99:IC}
M.~Abadi and A.~D. Gordon.
\newblock A calculus for cryptographic protocols: The spi calculus.
\newblock {\em Inf. and Comp.}, 148(1):1--70, 1999.

\bibitem{Alur:06:ICALP}
R.~Alur and S.~Zdancewic.
\newblock Preserving secrecy under refinement.
\newblock In {\em Proc. of ICALP}, number 4052 in {LNCS}, pages 107--118.
  Springer-Verlag, 2006.

\bibitem{Andres:10:TechRep}
M.~E. Andr\'es, C.~Palamidessi, P.~van Rossum, and A.~Sokolova.
\newblock Information hiding in probabilistic concurrent systems.
\newblock \url{www.cs.ru.nl/M.Andres/downloads/SAuN.pdf}.

\bibitem{Back:92:TCS}
R.~J.~R. Back and J.~von Wright.
\newblock Combining angels, demons and miracles in program specifications.
\newblock {\em TCS}, 100(2):365--383, 1992.

\bibitem{Bhargava:05:CONCUR}
M.~Bhargava and C.~Palamidessi.
\newblock Probabilistic anonymity.
\newblock In {\em Proc. of CONCUR}, volume 3653 of {\em LNCS}, pages 171--185.
  Springer, 2005.

\bibitem{Canetti:06:WODES}
R.~Canetti, L.~Cheung, D.~Kaynar, M.~Liskov, N.~Lynch, O.~Pereira, and
  R.~Segala.
\newblock Task-structured probabilistic i/o automata.
\newblock In {\em Proc. of WODES}, 2006.

\bibitem{Canetti:06:DISC}
R.~Canetti, L.~Cheung, D.~K. Kaynar, M.~Liskov, N.~A. Lynch, O.~Pereira, and
  R.~Segala.
\newblock Time-bounded task-{PIOA}s: {A} framework for analyzing security
  protocols.
\newblock In {\em Proc. of DISC}, volume 4167 of {\em LNCS}, pages 238--253.
  Springer, 2006.

\bibitem{Chatzikokolakis:09:FOSSACS}
K.~Chatzikokolakis, G.~Norman, and D.~Parker.
\newblock Bisimulation for demonic schedulers.
\newblock In {\em Proc. of FOSSACS}, volume 5504 of {\em LNCS}, pages 318--332.
  Springer, 2009.

\bibitem{Chatzikokolakis:07:CONCUR}
K.~Chatzikokolakis and C.~Palamidessi.
\newblock Making random choices invisible to the scheduler.
\newblock In {\em Proc. of CONCUR'07}, volume 4703 of {\em LNCS}, pages 42--58.
  Springer, 2007.

\bibitem{Chaum:88:JC}
D.~Chaum.
\newblock The dining cryptographers problem: Unconditional sender and recipient
  untraceability.
\newblock {\em Journal of Cryptology}, 1:65--75, 1988.

\bibitem{Clarkson:08:CSF}
M.~R. Clarkson and F.~B. Schneider.
\newblock Hyperproperties.
\newblock In {\em CSF}, pages 51--65. IEEE, 2008.

\bibitem{deAlfaro:01:CONCUR}
L.~de~Alfaro, T.~A. Henzinger, and R.~Jhala.
\newblock Compositional methods for probabilistic systems.
\newblock In {\em Proc. of CONCUR}, volume 2154 of {\em LNCS}. Springer, 2001.

\bibitem{Delaune:09:JCS}
S.~Delaune, S.~Kremer, and M.~Ryan.
\newblock Verifying privacy-type properties of electronic voting protocols.
\newblock {\em Journal of Computer Security}, 17(4):435--487, 2009.

\bibitem{Dubreil:09:TAC}
J.~Dubreil, P.~Darondeau, and H.~Marchand.
\newblock Supervisory control for opacity.
\newblock {\em IEEE Transactions on Automatic Control}, 55(5):1089 --1100,
  2010.

\bibitem{Giro:09:SBMF}
S.~Giro.
\newblock Undecidability results for distributed probabilistic systems.
\newblock In {\em Proc. of SBMF}, volume 5902 of {\em LNCS}, pages 220--235.
  Springer, 2009.

\bibitem{Giro:07:FORMATS}
S.~Giro and P.~R. D'Argenio.
\newblock Quantitative model checking revisited: Neither decidable nor
  approximable.
\newblock In {\em FORMATS}, volume 4763 of {\em {LNCS}}, pages 179--194.
  Springer, 2007.

\bibitem{Giro:09:CONCUR}
S.~Giro, P.~R. D'Argenio, and L.~M.~F. Fioriti.
\newblock Partial order reduction for probabilistic systems: {A} revision for
  distributed schedulers.
\newblock In {\em Proc. of CONCUR}, volume 5710 of {\em LNCS}, pages 338--353.
  Springer, 2009.

\bibitem{Jacob:89:SSP}
J.~Jacob.
\newblock On the derivation of secure components.
\newblock In {\em S\&P}, pages 242--247. IEEE, 1989.

\bibitem{Martin:2007:SCP}
C.~E. Martin, S.~A. Curtis, and I.~Rewitzky.
\newblock Modelling angelic and demonic nondeterminism with multirelations.
\newblock {\em Science of Computer Programming}, 65(2):140--158, 2007.

\bibitem{Milner:89:BOOK}
R.~Milner.
\newblock {\em Communication and Concurrency}.
\newblock Series in Comp. Sci. Prentice Hall, 1989.

\bibitem{Milner:99:BOOK}
R.~Milner.
\newblock {\em Communicating and mobile systems: the $\pi$-calculus}.
\newblock CUP, 1999.

\bibitem{Morgan:09:SCP}
C.~Morgan.
\newblock The shadow knows: Refinement and security in sequential programs.
\newblock {\em Science of Computer Programming}, 74(8):629--653, 2009.

\bibitem{Reiter:98:TISS}
M.~K. Reiter and A.~D. Rubin.
\newblock Crowds: anonymity for {Web} transactions.
\newblock {\em ACM Transactions on Information and System Security},
  1(1):66--92, 1998.

\bibitem{Schneider:96:ESORICS}
S.~Schneider and A.~Sidiropoulos.
\newblock {CSP} and anonymity.
\newblock In {\em Proc. of ESORICS}, volume 1146 of {\em LNCS}, pages 198--218.
  Springer, 1996.

\bibitem{Segala:95:PhD}
R.~Segala.
\newblock {\em Modeling and Verification of Randomized Distributed Real-Time
  Systems}.
\newblock PhD thesis, 1995.
\newblock Tech. Rep. MIT/LCS/TR-676.

\bibitem{Segala:95:NJC}
R.~Segala and N.~Lynch.
\newblock Probabilistic simulations for probabilistic processes.
\newblock {\em Nordic Journal of Computing}, 2(2):250--273, 1995.

\end{thebibliography}