DNSsec in Isabelle - Replay Attack and Origin Authentication

Kammueller F., KIRSAL EVER Y., Cheng X.

IEEE International Conference on Systems, Man, and Cybernetics (SMC), Manchester, İngiltere, 13 - 16 Ekim 2013, ss.4772-4777, (Tam Metin Bildiri) identifier identifier

  • Yayın Türü: Bildiri / Tam Metin Bildiri
  • Doi Numarası: 10.1109/smc.2013.812
  • Basıldığı Şehir: Manchester
  • Basıldığı Ülke: İngiltere
  • Sayfa Sayıları: ss.4772-4777
  • Orta Doğu Teknik Üniversitesi Kuzey Kıbrıs Kampüsü Adresli: Hayır

Özet

In this paper, we present a formal model and analysis for the security extensions of the Domain Name System (DNSsec) in the interactive theorem prover Isabelle/HOL. Based on the inductive approach of security protocol analysis by Paulson in Isabelle/HOL, we show how the protocol can be modelled and important properties are proved. We prove that origin authentication works securely. In order to illustrate that the model is adequate, we show that previous domain name requests can be replayed - as in the classical DNS - by an attacker. These replays luckily can be uniquely identified in DNSsec due to the origin authentication mechanism that we establish to enhance security.