Measuring the Speed of Information Leakage in Mobile Processes

  • Benjamin Aziz
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4019)


This paper presents a syntax-directed non-uniform static analysis of the stochastic π-calculus to safely approximate the amount of time required before name substitutions occur in a process. Name substitutions form the basis for defining security properties, like information leakage. The presence of the quantitative and qualitative information in the results of the analysis allows us to reason about the speed at which sensitive information is leaked in a computing environment with malicious mobile code. We demonstrate the applicability of the analysis through a simple example of firewall breaches.


Security Policy Information Leakage Process Algebra Abstract Domain Mobile Process 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    CERT: CERT\(^{\text{\copyright}}\) incident note in-2003-01. Technical report, Software Engineering Institute (2003)Google Scholar
  2. 2.
    Moore, D., Paxson, V., Savage, S., Shannon, C., Staniford, S., Weaver, N.: Inside the slammer worm. IEEE Security and Privacy 1(4), 33–39 (2003)CrossRefGoogle Scholar
  3. 3.
    Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes (parts I & II). Information and Computation 100(1), 1–77 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    Cardelli, L., Gordon, A.: Mobile ambients. In: Nivat, M. (ed.) ETAPS 1998 and FOSSACS 1998. LNCS, vol. 1378, pp. 140–155. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  5. 5.
    Hillston, J., Ribaudo, M.: Modelling mobility with pepa nets. In: Aykanat, C., Dayar, T., Körpeoğlu, İ. (eds.) ISCIS 2004. LNCS, vol. 3280, pp. 513–522. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  6. 6.
    Priami, C.: Stochastic π-calculus. The Computer Journal 38(7), 578–589 (1995)CrossRefGoogle Scholar
  7. 7.
    Priami, C.: Stochastic π-calculus with general distributions. In: Proceedings of the 4th International Workshop on Process Algebra and Performance Modelling, Torino, Italy, pp. 41–57. GLUT Press (1996)Google Scholar
  8. 8.
    Herescu, O.M., Palamidessi, C.: Probabilistic asynchronous pi-calculus. In: Tiuryn, J. (ed.) ETAPS 2000 and FOSSACS 2000. LNCS, vol. 1784, pp. 146–160. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  9. 9.
    Aziz, B.: A semiring-based quantitative analysis of mobile systems. In: Proceedings of the 3rd International Workshop on Software Verification and Validation, Manchester, UK. Electronic Notes in Theoretical Computer Science, Elsevier, Amsterdam (to appear, 2005)Google Scholar
  10. 10.
    Buchholz, P., Kemper, P.: Quantifying the dynamic behavior of process algebras. In: de Luca, L., Gilmore, S. (eds.) PROBMIV 2001, PAPM-PROBMIV 2001, and PAPM 2001. LNCS, vol. 2165, pp. 184–199. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  11. 11.
    Hirsch, D., Tuosto, E.: Shreq: Coordinating application level qos. In: Proceedings of the 3rd IEEE International Conference on Software Engineering and Formal Methods, Koblenz, Germany, IEEE Computer Society Press, Los Alamitos (to appear, 2005)Google Scholar
  12. 12.
    Rounds, W.C., Song, H.: The phi-calculus: A language for distributed control of reconfigurable embedded systems. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 435–449. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  13. 13.
    Aziz, B., Hamilton, G.: A privacy analysis for the π-calculus: The denotational approach. In: Proceedings of the 2nd Workshop on the Specification, Analysis and Validation for Emerging Technologies, Datalogiske Skrifter, Copenhagen, Denmark, Roskilde University, vol. 94 (2002)Google Scholar
  14. 14.
    Chothia, T.: Guessing attacks in the pi-calculus with computational justification (2005),
  15. 15.
    Pierro, A.D., Hankin, C., Wiklicky, H.: Measuring the confinement of probabilistic systems. Theoretical Computer Science 340(1), 3–56 (2005)zbMATHCrossRefMathSciNetGoogle Scholar
  16. 16.
    Milner, R.: A Calculus of Communication Systems. LNCS, vol. 92. Springer, Heidelberg (1980)Google Scholar
  17. 17.
    Pierro, A.D., Hankin, C., Wiklicky, H.: Approximate non-interference. In: Proceedings of the 15th IEEE Computer Security Foundations Workshop, Cape Breton, Nova Scotia, Canada, pp. 3–17. IEEE Press, Los Alamitos (2002)CrossRefGoogle Scholar
  18. 18.
    Pierro, A.D., Wiklicky, H.: An operational semantics for probabilistic concurrent constraint programming. In: Proceedings of the 1998 International Conference on Computer Languages, Chicago, USA, pp. 174–183. IEEE Computer Society, Los Alamitos (1998)Google Scholar
  19. 19.
    Gilmore, S., Hillston, J.: The pepa workbench: A tool to support a process algebra-based approach to performance modelling. In: Haring, G., Kotsis, G. (eds.) TOOLS 1994. LNCS, vol. 794, pp. 353–368. Springer, Heidelberg (1994)Google Scholar
  20. 20.
    Bernardo, M., Gorrieri, R.: Extended markovian process algebra. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 315–330. Springer, Heidelberg (1996)Google Scholar
  21. 21.
    Aziz, B., Hamilton, G.: A denotational semantics for the π-calculus. In: Proceedings of the 5th Irish Workshop in Formal Methods. Electronic Workshops in Computing, Dublin, Ireland, British Computing Society Publishing (2001)Google Scholar
  22. 22.
    Stark, I.: A fully abstract domain model for the π-calculus. In: Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, pp. 36–42. IEEE Computer Society, Los Alamitos (1996)CrossRefGoogle Scholar
  23. 23.
    Plotkin, G.: A powerdomain construction. SIAM Journal on Computing 5(3), 452–487 (1976)zbMATHCrossRefMathSciNetGoogle Scholar
  24. 24.
    Abramsky, S.: A domain equation for bisimulation. Information and Computation 92(2), 161–218 (1991)zbMATHCrossRefMathSciNetGoogle Scholar
  25. 25.
    Gillespie, D.T.: Exact stochastic simulation of coupled chemical reactions. Journal of Physical Chemistry 81(25), 2340–2361 (1977)CrossRefGoogle Scholar
  26. 26.
    Phillips, A., Cardelli, L.: A correct abstract machine for the stochastic pi-calculus. In: Proceedings of the 2nd Workshop on Concurrent Models in Molecular Biology, London, U.K. (2004)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • Benjamin Aziz
    • 1
  1. 1.Department of ComputingImperial College LondonLondonU.K.

Personalised recommendations