Formal Security Analysis of Electronic Software Distribution Systems

  • Monika Maidl
  • David von Oheimb
  • Peter Hartmann
  • Richard Robinson
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5219)


Software distribution to target devices like factory controllers, medical instruments, vehicles or airplanes is increasingly performed electronically over insecure networks. Such software often implements vital functionality, and so the software distribution process can be highly critical, both from the safety and the security perspective. In this paper, we introduce a novel software distribution system architecture with a generic core component, such that the overall software transport from the supplier to the target device is an interaction of several instances of this core component communicating over insecure networks. The main advantage of this architecture is reduction of development and certification costs. The second contribution of this paper describes the validation and verification of the proposed system. We use a mix of formal methods, more precisely the AVISPA tool, and the Common Criteria (CC) methodology, to achieve high confidence in the security of the software distribution system at moderate costs.


Model Checker Security Protocol Security Property Target Device Security Objective 
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.
    Armando, A., von Oheimb, D., et al.: The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576. Springer, Heidelberg (2005)Google Scholar
  2. 2.
    AVISPA project homepage (2005),
  3. 3.
    Blanchet, B.: From Secrecy to Authenticity in Security Protocols. In: Hermenegildo, M., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 342–359. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  4. 4.
    Bodei, C., Buchholtz, M., Degano, P., Nielson, H.R., Nielson, F.: Static validation of security protocols. Journal of Computer Security 13(3), 347–390 (2005)Google Scholar
  5. 5.
  6. 6.
    Dolev, D., Yao, A.: On the Security of Public-Key Protocols. IEEE Transactions on Information Theory 29(2), 198–208 (1983)zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    Hartmann, P., Tappe, J., von Oheimb, D.: Asset Signer Verifier Protection Profile, Available upon request (2008)Google Scholar
  8. 8.
    Robinson, R., Li, M., Lintelman, S., Sampigethaya, K., Poovendran, R., von Oheimb, D., Bußer, J., Cuellar, J.: Electronic Distribution of Airplane Software and the Impact of Information Security on Airplane. In: Saglietti, F., Oster, N. (eds.) SAFECOMP 2007. LNCS, vol. 4680, pp. 28–39. Springer, Heidelberg (2007)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Monika Maidl
    • 1
  • David von Oheimb
    • 1
  • Peter Hartmann
    • 2
  • Richard Robinson
    • 3
  1. 1.Siemens Corporate TechnologyMünchenGermany
  2. 2.University of Appl. SciencesLandshutGermany
  3. 3.Boeing Phantom WorksSeattleUSA

Personalised recommendations