Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Formal security analysis of near field communication using model checking
KTH, Skolan för elektro- och systemteknik (EES), Kommunikationsnät.
2016 (Engelska)Ingår i: Computers & security (Print), ISSN 0167-4048, E-ISSN 1872-6208, Vol. 60, 1-14 s.Artikel i tidskrift (Refereegranskat) Published
Resurstyp
Text
Abstract [en]

Near field communication (NFC) is a short-range wireless communication technology envisioned to support a large gamut of smart-device applications, such as payment and ticketing. Although two NFC devices need to be in close proximity to communicate (up to 10 cm), adversaries can use a fast and transparent communication channel to relay data and, thus, force an NFC link between two distant victims. Since relay attacks can bypass the NFC requirement for short-range communication cheaply and easily, it is important to evaluate the security of NFC applications. In this work, we present a general framework that exploits formal analysis and especially model checking as a means of verifying the resiliency of NFC protocol against relay attacks. Toward this goal, we built a continuous-time Markov chain (CTMC) model using the PRISM model checker. Firstly, we took into account NFC protocol parameters and, then, we enhanced our model with networking parameters, which include both mobile environment and security-aware characteristics. Combining NFC specifications with an adversary's characteristics, we produced the relay attack model, which is used for extracting our security analysis results. Through these results, we can explain how a relay attack could be prevented and discuss potential countermeasures.

Ort, förlag, år, upplaga, sidor
Elsevier, 2016. Vol. 60, 1-14 s.
Nyckelord [en]
Near field communication, Probabilistic model checking, Relay attack, Security analysis, Wireless communication, Continuous time systems, Markov processes, Model checking, Network protocols, Network security, Security systems, Wireless telecommunication systems, Continuous time Markov chain, Short-range communication, Short-range wireless communications, The near field communication (NFC), Wireless communications
Nationell ämneskategori
Telekommunikation Kommunikationssystem
Identifikatorer
URN: urn:nbn:se:kth:diva-186922DOI: 10.1016/j.cose.2016.03.002ISI: 000378438600001Scopus ID: 2-s2.0-84962408491OAI: oai:DiVA.org:kth-186922DiVA: diva2:928770
Anmärkning

QC 20160516

Tillgänglig från: 2016-05-16 Skapad: 2016-05-16 Senast uppdaterad: 2016-07-15Bibliografiskt granskad

Open Access i DiVA

Fulltext saknas

Övriga länkar

Förlagets fulltextScopus

Sök vidare i DiVA

Av författaren/redaktören
Alexiou, Nikolaos
Av organisationen
Kommunikationsnät
I samma tidskrift
Computers & security (Print)
TelekommunikationKommunikationssystem

Sök vidare utanför DiVA

GoogleGoogle Scholar

Altmetricpoäng

Totalt: 171 träffar
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf