Advertisement

Journal of Medical Systems

, Volume 36, Issue 6, pp 3695–3711 | Cite as

Security Analysis of Standards-Driven Communication Protocols for Healthcare Scenarios

  • Massimiliano Masi
  • Rosario Pugliese
  • Francesco Tiezzi
Original Paper

Abstract

The importance of the Electronic Health Record (EHR), that stores all healthcare-related data belonging to a patient, has been recognised in recent years by governments, institutions and industry. Initiatives like the Integrating the Healthcare Enterprise (IHE) have been developed for the definition of standard methodologies for secure and interoperable EHR exchanges among clinics and hospitals. Using the requisites specified by these initiatives, many large scale projects have been set up for enabling healthcare professionals to handle patients’ EHRs. The success of applications developed in these contexts crucially depends on ensuring such security properties as confidentiality, authentication, and authorization. In this paper, we first propose a communication protocol, based on the IHE specifications, for authenticating healthcare professionals and assuring patients’ safety. By means of a formal analysis carried out by using the specification language COWS and the model checker CMC, we reveal a security flaw in the protocol thus demonstrating that to simply adopt the international standards does not guarantee the absence of such type of flaws. We then propose how to emend the IHE specifications and modify the protocol accordingly. Finally, we show how to tailor our protocol for application to more critical scenarios with no assumptions on the communication channels. To demonstrate feasibility and effectiveness of our protocols we have fully implemented them.

Keywords

Healthcare applications Electronic Health Records Medical records storage and retrieval Data security Authentication Model checking 

Notes

Conflict of Interest

The authors declare that they have no conflict of interest.

List of acronyms

AES

Advanced Encryption Standard

ARR

Audit Record Repository

ATNA

Audit Trail and Node Authentication

AVISPA

Automated Validation of Internet Security Protocols and Applications

CDA

Clinical Document Architecture

CMC

COWS model checker

COWS

Calculus for Orchestration of Web Services

EHR

Electronic Health Record

epSOS

European Patients Smart Open Services

HIPAA

Health Insurance Portability and Accountability Act

Hl7

Health Level Seven International

IHE

Integrating the Healthcare Enterprise

IP

Internet Protocol

LIFO

Last In First Out

OASIS

Organization for the Advancement of Structured Information Standards

RST

WS-Trust Request Security Token

RSTR

WS-Trust Request Security Token Response

SAML

Security Assertion Markup Language

SHA

Secure Hash Algorithm

SOAP

Simple Object Access Protocol

SOC

Service-Oriented Computing

SocL

Service-Oriented Computing Logic

STS

Security Token Service

TCP

Transmission Control Protocol

TLA+

Temporal Logic of Actions specification language

TLC

TLA+ model Checker

TLS

Transport Layer Security

UT

WS-Security Username Token

W3C

World Wide Web Consortium

WS-BPEL

Web Services Business Process Execution Language

XACML

eXtensible Access Control Markup Language

XCN

eXtended Composite ID Number and name for persons

XDM

Cross Enterprise Document Sharing using Portable Media

XDS

Cross Enterprise Document Sharing

XML

eXtensible Markup Language

References

  1. 1.
    Abadi, M., and Fournet, C., Mobile values, new names, and secure communication. In: POPL, pp. 104–115. ACM, 2001.Google Scholar
  2. 2.
    ARGE-ELGA, Die österreich elektronische gesundheitsakte. http://www.arge-elga.at, 2008.
  3. 3.
    Armando, A., et al., The AVISPA tool for the automated validation of internet security protocols and applications. In: CAV, LNCS, vol. 3576, pp. 281–285. Springer, 2005.Google Scholar
  4. 4.
    Armando, A., et al., Formal analysis of SAML 2.0 Web browser single sign-on: Breaking the SAML-based single sign-on for Google apps. In: FMSE, pp. 1–10. ACM, 2008.Google Scholar
  5. 5.
    Bhargavan, K., Corin, R., Fournet, C., and Gordon, A., Secure sessions for Web services. In: SWS, pp. 56–66. ACM, 2004.Google Scholar
  6. 6.
    Bhargavan, K., Fournet, C., Gordon, A., and Pucella, R., TulaFale: A security tool for Web services. In: FMCO, LNCS, vol. 3188, pp. 197–222. Springer, 2004.Google Scholar
  7. 7.
    Blanchet, B., CryptoVerif: Computationally sound mechanized prover for cryptographic protocols. In: Dagstuhl Seminar “Formal Protocol Verification Applied”, 2007.Google Scholar
  8. 8.
    Bradfield, J., and Stirling, C., Modal logics and mu-calculi: An introduction. Handbook of Process Algebra, pp. 293–330, 2001.Google Scholar
  9. 9.
    Broadfoot, P., and Lowe, G., On distributed security transactions that use secure transport protocols. In: CSFW, pp. 141–151. IEEE Computer Society, 2003.Google Scholar
  10. 10.
    Clarke, E.M., Grumberg, O., and Peled, D., Model Checking. MIT Press, 1999.Google Scholar
  11. 11.
    Dolev, D., and Yao, A., On the security of public key protocols. IEEE Trans. Inf. Theory 29(2):198–207, 1983.MathSciNetMATHCrossRefGoogle Scholar
  12. 12.
    EU Commission, M/403 EN: Standardisation mandate addressed to CEN, CENELEC and ETSI in the field of Information and Communication Technologies. Tech. rep., European Commission Enterprise And Industry Directorate-General (2007). http://ec.europa.eu/enterprise/standards_policy/mandates/database/index.cfm?fuseaction=search.detail&id=363#
  13. 13.
    eXtensible Access Control Markup Language TC v2.0 (XACML), Extensible access control markup language (XACML) version 2.0 (2005). http://docs.oasis-open.org/xacml/2.0/XACML-2.0-OS-NORMATIVE.zip
  14. 14.
    Fantechi, A., Gnesi, S., Lapadula, A., Mazzanti, F., Pugliese, R., and Tiezzi, F., A model checking approach for verifying COWS specifications. In: FASE, LNCS, vol. 4961, pp. 230–245. Springer, 2008.Google Scholar
  15. 15.
    Fidge, C., A Survey of Verification Techniques for Security Protocols. Tech. Rep. 01-22, Software Verification Research Centre, The University of Queensland (2001)Google Scholar
  16. 16.
    GIP DMP, Dossier Médical Personnel. http://www.d-m-p.org, 2009.
  17. 17.
    Groß, T., Security analysis of the SAML single sign-on browser/artifact profile. In: ACSAC, pp. 298–307. IEEE Computer Society, 2003.Google Scholar
  18. 18.
    Grumberg, O., and Veith, H. (eds.), 25 years of model checking—History, achievements, perspectives. In: LNCS, vol. 5000. Springer, 2008.Google Scholar
  19. 19.
    Hansen, S., Skriver, J., and Nielson, H., Using static analysis to validate the SAML single sign-on protocol. In: WITS, pp. 27–40. ACM, 2005.Google Scholar
  20. 20.
    Health Level Seven organization, Hl7 standards. http://www.hl7.org, 2009.
  21. 21.
    Johnson, J., Langworthy, D., Lamport, L., and Vogt, F., Formal specification of a Web services protocol. J. Log. Algebr. Program. 70(1):34–52, 2007.MathSciNetMATHCrossRefGoogle Scholar
  22. 22.
    Kleiner, E., and Roscoe, A., On the relationship between Web services security and traditional protocols. In: MFPS, ENTCS, vol. 155, pp. 583–603. Elsevier, 2006.Google Scholar
  23. 23.
    Lamport, L., Specifying systems, the TLA+ language and tools for hardware and software engineers. Addison-Wesley, 2002.Google Scholar
  24. 24.
    Lamport, L., and Yu, Y., TLC—The TLA+ Model Checker. http://research.microsoft.com/en-us/um/people/lamport/tla/tlc.html, 2003.
  25. 25.
    Pugliese, R., and Tiezzi, F., A calculus for orchestration of Web services. J. Applied Logic 10(1):2–31, 2012.MathSciNetCrossRefGoogle Scholar
  26. 26.
    Lapadula, A., Pugliese, R., and Tiezzi, F., Specifying and analysing SOC applications with COWS. In: Concurrency, Graphs and Models, LNCS, vol. 5065, pp. 701–720. Springer, 2008.Google Scholar
  27. 27.
    Lowe, G., A hierarchy of authentication specifications. In: CSFW, pp. 31–44. IEEE Computer Society, 1997.Google Scholar
  28. 28.
    Lowe, G., Casper: A compiler for the analysis of security protocols. J. Comp. Security 6(1–2):53–84, 1998.Google Scholar
  29. 29.
    Ma, L., and Tsai, J., Formal verification techniques for computer communication security protocols. SE&KE Handbook 1:23–46, 2001.Google Scholar
  30. 30.
    Neuman, B., and Ts’o, T., Kerberos: An authentication service for computer networks. IEEE Comm. Magazine 32(9):33–38, 1994.CrossRefGoogle Scholar
  31. 31.
    OASIS Security Services TC, Assertions and protocols for the OASIS security assertion markup language (SAML) v2.02. http://docs.oasis-open.org/security/saml/v2.0/saml-core-2.0-os.pdf, 2005.
  32. 32.
    OASIS Security Services TC, Profiles for the OASIS Security Assertion Markup Language (SAML) V2.0. http://docs.oasis-open.org/security/saml/v2.0/saml-profiles-2.0-os.pdf, 2005.
  33. 33.
    OASIS Security Services TC, SAML V2.0 Holder-of-Key Assertion Profile. http://docs.oasis-open.org/security/saml/Post2.0/sstc-saml2-holder-of-key-cd-01.pdf, 2009.
  34. 34.
    OASIS Web Services Security TC, Username token profile v1.1. http://www.oasis-open.org/committees/download.php/16782/wss-v1.1-spec-os-UsernameTokenProfile.pdf, 2006.
  35. 35.
    OASIS Web Services Security TC, WS-Trust 1.3. http://docs.oasis-open.org/ws-sx/ws-trust/200512/ws-trust-1.3-os.pdf, 2007.
  36. 36.
    OASIS WS-BPEL TC, Web Services Business Process Execution Language Version 2.0. http://docs.oasis-open.org/wsbpel/2.0/OS/wsbpel-v2.0-OS.html, 2007.
  37. 37.
    Roessler, T., Yiu, K., Solo, D., Hirsch, F., Reagle, J., and Eastlake, D., XML signature syntax and processing version 1.1. W3C working draft, W3C. http://www.w3.org/TR/2009/WD-xmldsig-core1-20090730/, 2009.
  38. 38.
    Rogers, T., Hadley, M., and Gudgin, M., Web services addressing 1.0—core. W3C recommendation, W3C. http://www.w3.org/TR/2006/REC-ws-addr-core-20060509, 2006.
  39. 39.
    Tech. rep., Security Analysis of Standards-Driven Communication Protocols for Healthcare Scenarios. http://dl.dropbox.com/u/1952111/xds-xdm-blind.pdf, 2011.
  40. 40.
    The Direct Project, Threat Models. http://wiki.directproject.org/Threat+Models, 2010.
  41. 41.
    The epSOS project, A European ehealth project. http://www.epsos.eu, 2010.
  42. 42.
    The IHE Initiative, IT Infrastructure Tecnical Framework. http://www.ihe.net, 2009.
  43. 43.
    The Nationwide Health Information Network (NHIN), An American eHealth Project. http://healthit.hhs.gov/portal/server.pt, 2009.
  44. 44.
    The South African Department of Health, EHR project in South Africa. http://southafrica.usembassy.gov/root/pdfs/pepfar-hmis-docs/ndoh-e-hr-for-south-africa.pdf, 2009.
  45. 45.
    US Congress, Health Insurance Portability and Accountability Act. Tech. rep., Department of Health. http://www.cms.gov/HIPAAGenInfo/, 1996.

Copyright information

© Springer Science+Business Media, LLC 2012

Authors and Affiliations

  • Massimiliano Masi
    • 1
    • 2
  • Rosario Pugliese
    • 2
  • Francesco Tiezzi
    • 3
  1. 1.Tiani “Spirit” GmbH, GuglgasseViennaAustria
  2. 2.Università degli Studi di Firenze, Viale MorgagniFirenzeItaly
  3. 3.IMT Advanced Studies Lucca, Piazza S. PonzianoLuccaItaly

Personalised recommendations