Formal verification of PAP and EAP-MD5 protocols in wireless networks: FDR model checking

Il Gon Kim, Jin Young Choi

Research output: Chapter in Book/Report/Conference proceedingConference contribution

17 Citations (Scopus)

Abstract

IEEE 802.1x and authentication server based security protocols are mainly used for enhancing security of wireless networks. In this paper, we specify PAP and EAP-MD5 based security protocols formally with Casper and CSP, and then verify their security properties such as secrecy and authentication using FDR. We also show that they are vulnerable to the man-in-the-middle attack. Finally we discuss their security weakness and potential countermeasures related to PAP and EAP-MD5 protocols.

Original languageEnglish
Title of host publicationProceedings - International Conference on Advanced Information Networking and Application (AINA)
EditorsL. Barolli
Pages264-269
Number of pages6
Volume2
Publication statusPublished - 2004 Jul 7
EventProceedings - 18th International Conference on Advanced Information Networking and Applications, AINA 2004 - Fukuoka, Japan
Duration: 2004 Mar 292004 Mar 31

Other

OtherProceedings - 18th International Conference on Advanced Information Networking and Applications, AINA 2004
CountryJapan
CityFukuoka
Period04/3/2904/3/31

Fingerprint

Model checking
Wireless networks
Network protocols
Authentication
Servers
Formal verification

ASJC Scopus subject areas

  • Engineering(all)

Cite this

Kim, I. G., & Choi, J. Y. (2004). Formal verification of PAP and EAP-MD5 protocols in wireless networks: FDR model checking. In L. Barolli (Ed.), Proceedings - International Conference on Advanced Information Networking and Application (AINA) (Vol. 2, pp. 264-269)

Formal verification of PAP and EAP-MD5 protocols in wireless networks : FDR model checking. / Kim, Il Gon; Choi, Jin Young.

Proceedings - International Conference on Advanced Information Networking and Application (AINA). ed. / L. Barolli. Vol. 2 2004. p. 264-269.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Kim, IG & Choi, JY 2004, Formal verification of PAP and EAP-MD5 protocols in wireless networks: FDR model checking. in L Barolli (ed.), Proceedings - International Conference on Advanced Information Networking and Application (AINA). vol. 2, pp. 264-269, Proceedings - 18th International Conference on Advanced Information Networking and Applications, AINA 2004, Fukuoka, Japan, 04/3/29.
Kim IG, Choi JY. Formal verification of PAP and EAP-MD5 protocols in wireless networks: FDR model checking. In Barolli L, editor, Proceedings - International Conference on Advanced Information Networking and Application (AINA). Vol. 2. 2004. p. 264-269
Kim, Il Gon ; Choi, Jin Young. / Formal verification of PAP and EAP-MD5 protocols in wireless networks : FDR model checking. Proceedings - International Conference on Advanced Information Networking and Application (AINA). editor / L. Barolli. Vol. 2 2004. pp. 264-269
@inproceedings{b03ed2da6ee44d3f9d397ebc4f5f927a,
title = "Formal verification of PAP and EAP-MD5 protocols in wireless networks: FDR model checking",
abstract = "IEEE 802.1x and authentication server based security protocols are mainly used for enhancing security of wireless networks. In this paper, we specify PAP and EAP-MD5 based security protocols formally with Casper and CSP, and then verify their security properties such as secrecy and authentication using FDR. We also show that they are vulnerable to the man-in-the-middle attack. Finally we discuss their security weakness and potential countermeasures related to PAP and EAP-MD5 protocols.",
author = "Kim, {Il Gon} and Choi, {Jin Young}",
year = "2004",
month = "7",
day = "7",
language = "English",
isbn = "0769520510",
volume = "2",
pages = "264--269",
editor = "L. Barolli",
booktitle = "Proceedings - International Conference on Advanced Information Networking and Application (AINA)",

}

TY - GEN

T1 - Formal verification of PAP and EAP-MD5 protocols in wireless networks

T2 - FDR model checking

AU - Kim, Il Gon

AU - Choi, Jin Young

PY - 2004/7/7

Y1 - 2004/7/7

N2 - IEEE 802.1x and authentication server based security protocols are mainly used for enhancing security of wireless networks. In this paper, we specify PAP and EAP-MD5 based security protocols formally with Casper and CSP, and then verify their security properties such as secrecy and authentication using FDR. We also show that they are vulnerable to the man-in-the-middle attack. Finally we discuss their security weakness and potential countermeasures related to PAP and EAP-MD5 protocols.

AB - IEEE 802.1x and authentication server based security protocols are mainly used for enhancing security of wireless networks. In this paper, we specify PAP and EAP-MD5 based security protocols formally with Casper and CSP, and then verify their security properties such as secrecy and authentication using FDR. We also show that they are vulnerable to the man-in-the-middle attack. Finally we discuss their security weakness and potential countermeasures related to PAP and EAP-MD5 protocols.

UR - http://www.scopus.com/inward/record.url?scp=3042686296&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=3042686296&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:3042686296

SN - 0769520510

VL - 2

SP - 264

EP - 269

BT - Proceedings - International Conference on Advanced Information Networking and Application (AINA)

A2 - Barolli, L.

ER -