Cryptographic Model and Formal Design for Distributed Network System
- 주제(키워드) security
- 발행기관 고려대학교 대학원
- 지도교수 최진영
- 발행년도 2009
- 제출일 2008-12-29
- 학위수여년월 2009. 2
- 학위명 박사
- 학과 컴퓨터학과 전산학전공
- 원문페이지 110 p
- 실제URI http://www.dcollection.net/handler/korea/000000006688
- 본문언어 영어
- 제출원본 000045532849
초록/요약
Mobile and distributed network system based environments are defined as environments where users can receive network services for anytime and anywhere access through any device, with the tag connected via a wired and wireless network, to information appliances, including the PC. More precisely, the ubiquitous networking environment has provided solutions ranging from a single commerce to the creation of an online technical service to its full extent in human society. However there is still little confidence among users concerning the security of their data for sending and receiving at invisible network. To diminish these doubt, cryptographic protocols are used to establish secure communication over insecure open networks and distributed systems. These protocols use cryptographic techniques to achieve goals such as confidentiality, authentication of principals and services, message integrity, non-repudiation, order and timeliness of the messages, and distribution of cryptographic keys. Formal methods play a very critical role in examining whether a cryptographic protocol is ambiguous, incorrect, inconsistent or incomplete. The application of formal techniques to the modeling and design of cryptographic protocols should help to improve their reliability and so enhance the choices of these new technologies. Cryptographic protocols are, in fact, excellent candidates for rigorous analysis techniques: they are critical components of distributed security architecture, very easy to express, however, extremely difficult to evaluate by hand. Recently, there have been some approaches for the security of ubiquitous computing focusing on the four topic. Firstly, RFID (Radio Frequency Identification) has been researched regarding privacy and authentication issues, including killing tags at the checkout, renaming the identifier of the tag, physical tag password, hash encryption, random access hash and hash based ID variation. Secondly, researchers have extensively studied the key exchange protocol, the efficient verifier-based key agreement protocol for three parties which does not require server's public key, and the key exchange protocol in the three-party setting for the application into ubiquitous computing. Thirdly, a secure and efficient user authentication schemes using smart card that is modified to enhance the security of the series of the Peyravian-Zunic scheme have been researched. Fourthly, the main payment phase of the E-commerce protocols and its key exchange is focused on. However, among these researches, a few proposed scheme has still susceptible to security attacks. Accordingly, the current thesis demonstrates the vulnerabilities regarding their attacks by using formal and informal description. In addition to analyzing these scheme, there are countermeasures against each of vulnerability.
more목차
1 Introduction
2 RFID based Cryptographic Model
2.1 Related Work with Security Problem in RFID
2.1.1 Kill Tag
2.1.2 Renaming Approach
2.1.3 Tag Password
2.1.4 The Hash Lock Scheme
2.1.5 The Randomized Hash Lock Scheme
2.1.6 The Hash based ID Variation Scheme
2.2 Modeling RFID Cryptographic Protocols in CSP
2.2.1 The Message Datatype
2.2.2 Modeling the Intruder and Putting the Network Together
2.2.3 Specifying Protocol Requirements
2.2.4 The Model Checking Application using Casper and FDR
2.3 Case Study : Analysis and Design of the Hash based RFID Authentication protocols with CSP and FDR
2.3.1 Hash Unlocking Protocol
2.3.2 The Randomized Hash Unlocking Protocol
2.3.3 The Hash based ID Variation Protocol
2.3.4 Preventing the Attacks and Design of Hash based RFID Authentication for RFID System
2.4 Modeling RFID Cryptographic Protocol in GNY Logic
2.5 Case Study : Analysis and Design of Challenge Response based Protocol with GNY
3 Password based Key Exchange Cryptographic Model
3.1 Related Work with Password based Key Exchange Scheme
3.2 A Variation of the BR1995 Model and BPR2000 Model for the STPKE Protocol
3.2.1 Participants
3.2.2 Adversary
3.2.3 Security Definition
3.3 Case Study : Analysis and Design of the STPKE Protocol with BPR
3.3.1 Review of the STPKE protocol
3.3.2 Undetectable On-line Password Guessing Attacks of STPKE
3.3.3 Preventing the Attacks and Design of the STPKE
4 Smart Card based Cryptographic Model
4.1 RelatedWork with Smart Card based Password Authentication System
4.2 Review of the Kwon et al.'s Scheme
4.2.1 Registration Phase
4.2.2 Session Key Agreement Phase
4.2.3 Authentication Phases
4.2.4 Cryptanalysis and Countermeasure of Kwon et al.'s Scheme
4.3 Review of the Chen and Lee's Scheme
4.3.1 Registration Phase
4.3.2 Authentication Phase
4.3.3 Cryptanalysis and Countermeasure of Chen and Lee's Scheme
5 E-Commerce based Cryptographic Model
5.1 Related Work with E-Commerce Security
5.2 Analysis of the Mu-Varadharajan BCY Protocol
5.2.1 Protocol Goals
5.2.2 The Result of Verification
5.3 Proposed Modification to BCY Protocols
5.3.1 Modeling the Revised Mu-Varadharajan using Casper
5.3.2 The Result of Verification
6 Discussion and Conclusions
7 Appendix
