Analysis of security protocols with certificate over open networks: Electronic payment system

Hyun Seok Kim; Il Gon Kim; Jin Young Choi

doi:10.1109/ICDCSW.2005.41

Analysis of security protocols with certificate over open networks: Electronic payment system

Hyun Seok Kim, Il Gon Kim, Jin Young Choi

School of Cybersecurity

Research output: Contribution to conference › Paper › peer-review

2 Citations (Scopus)

Abstract

Electronic Commerce and Internet in wireless networks are profoundly changing the way of payment, but there is still little confidence among users concerning the security of their data. The application of formal techniques to the modelling and design of electronic commerce protocols should help to improve their reliability and so enhance the choices of these new technologies. In this paper, we show how the Casper, a special-purpose formal methods tool designed for the verification of the security protocols, was used in the analysis of the BCY(Beller, Chang, Yacobi), the Carlsen BCY and the Mu-Varadharajan BCY protocols. We describe the results of our analysis, which uncovered several vulnerabilities in the specification that would have made possible attacks such as man-in-the-middle attack and replay attack. Finally, we propose a new protocol resistant to these attacks and formally verify its correctness.

Original language	English
DOIs	https://doi.org/10.1109/ICDCSW.2005.41
Publication status	Published - 2005
Event	25th IEEE International Conference on Distributed Computing Systems Workshops, ICDCS 2005 - Columbus, OH, United States Duration: 2005 Jun 6 → 2005 Jun 10

Conference

Conference	25th IEEE International Conference on Distributed Computing Systems Workshops, ICDCS 2005
Country/Territory	United States
City	Columbus, OH
Period	05/6/6 → 05/6/10

Bibliographical note

Publisher Copyright:
© 2005 IEEE.

ASJC Scopus subject areas

Software
Hardware and Architecture
Computer Networks and Communications

Access to Document

10.1109/ICDCSW.2005.41

Cite this

@conference{327ef39202574c649dbd4dfff412bad6,

title = "Analysis of security protocols with certificate over open networks: Electronic payment system",

abstract = "Electronic Commerce and Internet in wireless networks are profoundly changing the way of payment, but there is still little confidence among users concerning the security of their data. The application of formal techniques to the modelling and design of electronic commerce protocols should help to improve their reliability and so enhance the choices of these new technologies. In this paper, we show how the Casper, a special-purpose formal methods tool designed for the verification of the security protocols, was used in the analysis of the BCY(Beller, Chang, Yacobi), the Carlsen BCY and the Mu-Varadharajan BCY protocols. We describe the results of our analysis, which uncovered several vulnerabilities in the specification that would have made possible attacks such as man-in-the-middle attack and replay attack. Finally, we propose a new protocol resistant to these attacks and formally verify its correctness.",

author = "Kim, {Hyun Seok} and Kim, {Il Gon} and Choi, {Jin Young}",

note = "Publisher Copyright: {\textcopyright} 2005 IEEE.; 25th IEEE International Conference on Distributed Computing Systems Workshops, ICDCS 2005 ; Conference date: 06-06-2005 Through 10-06-2005",

year = "2005",

doi = "10.1109/ICDCSW.2005.41",

language = "English",

}

TY - CONF

T1 - Analysis of security protocols with certificate over open networks

T2 - 25th IEEE International Conference on Distributed Computing Systems Workshops, ICDCS 2005

AU - Kim, Hyun Seok

AU - Kim, Il Gon

AU - Choi, Jin Young

PY - 2005

Y1 - 2005

N2 - Electronic Commerce and Internet in wireless networks are profoundly changing the way of payment, but there is still little confidence among users concerning the security of their data. The application of formal techniques to the modelling and design of electronic commerce protocols should help to improve their reliability and so enhance the choices of these new technologies. In this paper, we show how the Casper, a special-purpose formal methods tool designed for the verification of the security protocols, was used in the analysis of the BCY(Beller, Chang, Yacobi), the Carlsen BCY and the Mu-Varadharajan BCY protocols. We describe the results of our analysis, which uncovered several vulnerabilities in the specification that would have made possible attacks such as man-in-the-middle attack and replay attack. Finally, we propose a new protocol resistant to these attacks and formally verify its correctness.

AB - Electronic Commerce and Internet in wireless networks are profoundly changing the way of payment, but there is still little confidence among users concerning the security of their data. The application of formal techniques to the modelling and design of electronic commerce protocols should help to improve their reliability and so enhance the choices of these new technologies. In this paper, we show how the Casper, a special-purpose formal methods tool designed for the verification of the security protocols, was used in the analysis of the BCY(Beller, Chang, Yacobi), the Carlsen BCY and the Mu-Varadharajan BCY protocols. We describe the results of our analysis, which uncovered several vulnerabilities in the specification that would have made possible attacks such as man-in-the-middle attack and replay attack. Finally, we propose a new protocol resistant to these attacks and formally verify its correctness.

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

U2 - 10.1109/ICDCSW.2005.41

DO - 10.1109/ICDCSW.2005.41

M3 - Paper

AN - SCOPUS:77949838865

Y2 - 6 June 2005 through 10 June 2005

ER -

Analysis of security protocols with certificate over open networks: Electronic payment system

Abstract

Conference

Bibliographical note

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this