Compositional Verification of Secure Streamed Data: A Case Study with EMSS

  • Fabio Martinelli
  • Marinella Petrocchi
  • Anna Vaccarelli
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2841)


We consider an instance of the EMSS protocol proposed in [19], authenticating streamed data in the presence of packet loss. We formally prove the integrity property of the instance by applying a compositional proof rule that allows us to check a specification with an arbitrary number of parallel processes. We argue that our approach may be applied to a wider class of stream signature protocols.


Security Compositional Analysis and Verification Digital Streams Integrity 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Archer, M.: Proving Correctness of the Basic TESLA Multicast Stream Authentication Protocol with TAME. In: Proc. of WITS 2002 (2002)Google Scholar
  2. 2.
    Boreale, M., Gorla, D.: On Compositional Reasoning in the Spi-Calculus. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 67–81. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  3. 3.
    Broadfoot, P., Lowe, G.: Analysing a Stream Authentication Protocol using Model Checking. In: Gollmann, D., Karjoth, G., Waidner, M. (eds.) ESORICS 2002. LNCS, vol. 2502, pp. 146–161. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  4. 4.
    Focardi, R., Gorrieri, R., Martinelli, F.: Non Interference for the Analysis of Cryptographic Protocols. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol. 1853, pp. 354–372. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  5. 5.
    Focardi, R., Martinelli, F.: A uniform approach for the definition of security properties. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 794–813. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  6. 6.
    Gennaro, R., Rohatgi, P.: How to Sign Digital Streams. Information and Computation 165(1), 100–116 (2001)zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    Goguen, J.A., Meseguer, J.: Security Policies and Security Models. In: Proc. of IEEE S&P 1982, pp. 11–20 (1982)Google Scholar
  8. 8.
    Golle, P., Modadugu, N.: Authenticating Streamed Data in the Presence of Random Packet Loss. In: Proc. of NDSS 2001 (2001)Google Scholar
  9. 9.
    Gordon, A.D., Jeffrey, A.: Authenticity by Typing for Security Protocols. In: Proc. of IEEE CSFW 2001, pp. 126–144 (2001)Google Scholar
  10. 10.
    Gordon, A.D., Jeffrey, A.: Types and Effects for Asymmetric Cryptographic Protocols. In: Proc. of IEEE CSFW 2002, pp. 77–91 (2002)Google Scholar
  11. 11.
    Gorrieri, R., Locatelli, E., Martinelli, F.: A Simple Language for Real-time Cryptographic Protocol Analysis. In: Degano, P. (ed.) ESOP 2003. LNCS, vol. 2618, pp. 114–128. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  12. 12.
    Gorrieri, R., Martinelli, F., Petrocchi, M., Vaccarelli, A.: Compositional Verification of Integrity for Digital Stream Signature Protocols. In: Proc. of IEEE ACSD 2003, pp. 142–149 (2003)Google Scholar
  13. 13.
    Guttman, J., Thayer, F.J.: Protocol Independence through Disjoint Encryption. In: Proc. of IEEE CSFW 2000, pp. 24–34 (2000)Google Scholar
  14. 14.
    Martinelli, F.: Analysis of Security Protocols as Open Systems. Theoretical Computer Science 290(1), 1057–1106 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  15. 15.
    Martinelli, F., Petrocchi, M., Vaccarelli, A.: Analysing EMSS with Compositional Proof Rules for Non-Interference. In: Proc. of WITS 2003, pp. 52–61 (2003)Google Scholar
  16. 16.
    Pannetrat, A., Molva, R.: Efficient Multicast Packet Authentication. In: Proc. of NDSS 2003 (2003)Google Scholar
  17. 17.
    Park, J.M., Chong, E.K.P., Siegel, H.J.: Efficient Multicast Packet Authentication using Signature Amortization. In: Proc. of IEEE S&P 2002, pp. 227–240 (2002)Google Scholar
  18. 18.
    Perrig, A., Canetti, R., Song, D.X., Tygar, D.: Efficient and Secure Source Authentication for Multicast. In: Proc. of NDSS 2001, The Internet Society, San Diego (2001)Google Scholar
  19. 19.
    Perrig, A., Canetti, R., Tygar, J.D., Song, D.X.: Efficient Authentication and Signing of Multicast Streams over Lossy Channels. In: Proc. of IEEE S&P 2000, pp. 56–73 (2000)Google Scholar
  20. 20.
    Postel, J.: The User Datagram Protocol - RFC 768 (1980)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Fabio Martinelli
    • 1
  • Marinella Petrocchi
    • 1
  • Anna Vaccarelli
    • 1
  1. 1.Istituto di Informatica e TelematicaC.N.R., Area della Ricerca di PisaPisaItaly

Personalised recommendations