Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Formal Verification of the xDAuth Protocol
Department of Computer Sciences, Institute of Management Sciences, Peshawar.
Department of Computer Sciences, COMSATS Institute of Information Technology, Islamabad.
Department of Computer Sciences, COMSATS Institute of Information Technology, Islamabad.
Department of Computer Sciences, COMSATS Institute of Information Technology, Islamabad.
Show others and affiliations
2016 (English)In: IEEE Transactions on Information Forensics and Security, ISSN 1556-6013, E-ISSN 1556-6021, Vol. 11, no 9, p. 1956-1969Article in journal (Refereed) Published
Abstract [en]

Service Oriented Architecture (SOA) offers a flexible paradigm for information flow among collaborating organizations. As information moves out of an organization boundary, various security concerns may arise, such as confidentiality, integrity, and authenticity that needs to be addressed. Moreover, verifying the correctness of the communication protocol is also an important factor. This paper focuses on the formal verification of the xDAuth protocol, which is one of the prominent protocols for identity management in cross domain scenarios. We have modeled the information flow of xDAuth protocol using High Level Petri Nets (HLPN) to understand protocol information flow in a distributed environment. We analyze the rules of information flow using Z language while Z3 SMT solver is used for verification of the model. Our formal analysis and verification results reveal the fact that the protocol fulfills its intended purpose and provides the security for the defined protocol specific properties, e.g. secure secret key authentication, Chinese wall security policy and secrecy specific properties, e.g. confidentiality, integrity, authenticity.

Place, publisher, year, edition, pages
2016. Vol. 11, no 9, p. 1956-1969
National Category
Media and Communication Technology
Research subject
Mobile and Pervasive Computing
Identifiers
URN: urn:nbn:se:ltu:diva-15379DOI: 10.1109/TIFS.2016.2561909Scopus ID: 2-s2.0-84978975669Local ID: ee2c8aa4-cf41-4453-b735-f73bafee1a96OAI: oai:DiVA.org:ltu-15379DiVA, id: diva2:988353
Note
Validerad; 2016; Nivå 2; 20160622 (andbra)Available from: 2016-09-29 Created: 2016-09-29 Last updated: 2018-07-10Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records BETA

Vasilakos, Athanasios

Search in DiVA

By author/editor
Vasilakos, Athanasios
By organisation
Computer Science
In the same journal
IEEE Transactions on Information Forensics and Security
Media and Communication Technology

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 364 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf