Luận Văn Thạc Sĩ: Kiểm Tra Tính Bảo Mật Của Việc Xác Thực Người Dùng Trên Web

Luận văn thạc sĩ nghiên cứu máy tính kiểm tra tính bảo mật của việc xác thực người dùng trên web, khảo sát thực trạng, phân tích nguyên nhân, đề xuất giải pháp cải thiện thực tiễn.

• Tác giả: Lý Đoàn Duy Khánh
• Người hướng dẫn: PGS. Quản Thành Thơ
• Trường học: Đại học Bách Khoa
• Chuyên ngành: Khoa Học Máy Tính
• Đề tài: Kiểm Tra Tính Bảo Mật Của Việc Xác Thực Người Dùng Trên Web
• Loại tài liệu: luận văn thạc sĩ
• Năm xuất bản: 2015
• Địa điểm: Thành phố Hồ Chí Minh

Mục lục chi tiết

• LỜI CẢM ƠN
• TÓM TẮT LUẬN VĂN
• ABSTRACT
• LỜI CAM ĐOAN
• 1. CHƯƠNG 1: GIỚI THIỆU
• 1.1. Động cơ
• 1.2. Mục tiêu
• 1.3. Giới hạn
• 1.4. Ý nghĩa đề tài
• 1.5. Cấu trúc của luận văn
• 2. CHƯƠNG 2: TỔNG QUAN VÀ KHẢO SÁT CÁC CÔNG TRÌNH LIÊN QUAN
• 2.1. Đặc điểm giao thức và kiểm tra
• 2.2. Khai thác giao thức
• 2.2.1. Phương pháp khai thác giao thức David Lie
• 2.2.2. Mô hình biểu tượng Mihhail Aizatulin
• 2.3. Phân tích bảo mật của giao thức SSO
• 2.3.1. Phân tích bảo mật giao thức SSO thực tế
• 2.3.2. Phân tích bảo mật giao thức OAuth 2.0 bằng API của nó
• 2.3.3. Mô hình tấn công web của T. Sun
• 2.4. Hướng tiếp cận đề tài
• 3. CHƯƠNG 3: LÝ THUYẾT NỀN TẢNG
• 3.1. Hệ Thống Chuyển Trạng Thái (Transition System - TS)
• 3.2. Đường thực thi
• 3.3. Hệ Thống Chuyển Trạng Thái Có Đánh Nhãn
• 3.4. Luận Lý Tuyến Tính Theo Thời Gian (LTL)
• 4. CHƯƠNG 4: MÔ HÌNH ĐƯỢC ĐỀ XUẤT
• 4.1. Mô Hình Giao Thức
• 4.2. Hành vi của thành viên trong hệ thống
• 4.2.1. Hành vi nhận gói tin
• 4.2.2. Hành vi gửi gói tin
• 4.2.3. Hành vi tạo gói tin
• 4.2.4. Tóm tắt hành vi của thành viên giao thức
• 4.3. Hành vi của kẻ gian (intruder)
• 4.3.1. Hành vi làm giả gói tin
• 4.3.2. Hành vi nghe lén gói tin (overhear)
• 4.3.3. Hành vi chặn gói tin (intercept)
• 4.3.4. Tóm tắt hành vi của kẻ gian
• 4.4. Tập luật suy luận của các đối tượng trong giao thức
• 4.4.1. Giải mã (decryption) bằng khóa K
• 4.5. Kiểm tra thuộc tính của giao thức
• 4.5.1. Kiểm tra tính bảo mật
• 4.5.2. Kiểm tra thuộc tính xác thực
• 5. CHƯƠNG 5: HIỆN THỰC VÀ KẾT QUẢ THỰC NGHIỆM
• 5.1. Giao thức đăng nhập của hdvietnam
• 5.1.1. Mô hình giao thức
• 5.1.2. Mô hình của Client và Server
• 5.1.3. Mô hình của Intruder
• 5.2. Kết Quả Thí Nghiệm
• 6. CHƯƠNG 6: TỔNG KẾT VÀ HƯỚNG PHÁT TRIỂN
• 6.1. Tổng kết
• 6.2. Hướng phát triển
• TÀI LIỆU THAM KHẢO

Tóm tắt

I. Giới thiệu

Trong bối cảnh công nghệ thông tin phát triển mạnh mẽ, việc kiểm tra tính bảo mật xác thực người dùng trên web trở thành một vấn đề cấp thiết. Luận văn này nhằm nghiên cứu và đề xuất một lý thuyết mô hình hóa để kiểm tra tính an toàn của giao thức xác thực người dùng. Mục tiêu chính là phát triển một phương pháp có thể áp dụng cho nhiều loại giao thức khác nhau, từ đó nâng cao khả năng bảo mật cho các ứng dụng web. Theo đó, việc sử dụng các công cụ hỗ trợ kiểm tra mô hình sẽ giúp phát hiện các lỗ hổng bảo mật tiềm ẩn, từ đó đưa ra các giải pháp khắc phục hiệu quả.

1.1. Động cơ nghiên cứu

Sự phát triển nhanh chóng của các ứng dụng web đã tạo ra nhiều cơ hội nhưng cũng đồng thời mang đến nhiều thách thức về bảo mật. Việc kiểm tra tính bảo mật xác thực người dùng trên web không chỉ giúp bảo vệ thông tin cá nhân mà còn đảm bảo sự tin cậy của các dịch vụ trực tuyến. Nghiên cứu này sẽ cung cấp một cái nhìn tổng quan về các phương pháp hiện có và đề xuất một mô hình mới nhằm cải thiện khả năng phát hiện lỗ hổng bảo mật trong các giao thức xác thực.

II. Đặc điểm giao thức và kiểm tra

Nghiên cứu về giao thức bảo mật đã được thực hiện từ lâu với nhiều mô hình và công cụ khác nhau. Các mô hình như WL model, BAN logic, và Spi-calculus đã được phát triển để mô hình hóa các thuộc tính bảo mật. Công cụ kiểm tra như Athena, ProVerif, và AVISPA đã được sử dụng để xác minh tính đúng đắn của các giao thức bảo mật. Việc áp dụng các mô hình này giúp xác định các thuộc tính như tính phù hợp và tính bảo mật của giao thức, từ đó phát hiện các lỗ hổng có thể bị khai thác.

2.1. Khai thác giao thức

Phương pháp khai thác giao thức từ mã nguồn đã được đề xuất bởi nhóm nghiên cứu David Lie và các cộng sự. Họ đã phát triển một mô hình tự động hóa để khai thác giao thức và kiểm tra bằng công cụ Murphi. Mô hình này cho phép xác định các trạng thái vi phạm và phát hiện các lỗi bảo mật trong giao thức. Việc áp dụng phương pháp này không chỉ giúp tiết kiệm thời gian mà còn nâng cao độ chính xác trong việc phát hiện lỗ hổng bảo mật.

III. Lý thuyết nền tảng

Lý thuyết nền tảng cho việc kiểm tra tính bảo mật xác thực người dùng trên web bao gồm các hệ thống chuyển trạng thái và các phương pháp kiểm tra thuộc tính. Hệ thống chuyển trạng thái cho phép mô hình hóa hành vi của các thành viên trong giao thức, từ đó xác định các hành vi bất thường có thể dẫn đến lỗ hổng bảo mật. Các phương pháp như LTL (Luận lý tuyến tính theo thời gian) cũng được áp dụng để kiểm tra các thuộc tính bảo mật của giao thức, giúp phát hiện các vấn đề tiềm ẩn trong quá trình xác thực.

3.1. Hệ thống chuyển trạng thái

Hệ thống chuyển trạng thái (TS) là một công cụ quan trọng trong việc mô hình hóa các giao thức bảo mật. Nó cho phép phân tích các trạng thái khác nhau của hệ thống và hành vi của các đối tượng trong giao thức. Việc áp dụng TS giúp xác định các điểm yếu trong giao thức và đưa ra các giải pháp khắc phục hiệu quả. Hệ thống này cũng hỗ trợ việc kiểm tra các thuộc tính bảo mật như tính xác thực và tính toàn vẹn của thông điệp.

IV. Mô hình được đề xuất

Mô hình được đề xuất trong luận văn này nhằm mục đích cải thiện khả năng phát hiện lỗ hổng bảo mật trong các giao thức xác thực người dùng. Mô hình này sẽ sử dụng ngôn ngữ mô hình hóa để biểu diễn các giao thức và áp dụng các công cụ kiểm tra để xác minh tính an toàn. Việc mô hình hóa này không chỉ giúp phát hiện các lỗ hổng mà còn cung cấp một cái nhìn tổng quan về cách thức hoạt động của giao thức, từ đó đưa ra các giải pháp bảo mật hiệu quả.

4.1. Hành vi của thành viên trong hệ thống

Hành vi của các thành viên trong hệ thống được mô hình hóa để xác định các hành động hợp lệ và bất hợp lệ. Việc phân tích hành vi này giúp phát hiện các hành vi đáng ngờ có thể dẫn đến lỗ hổng bảo mật. Mô hình hóa hành vi cũng cho phép xác định các kịch bản tấn công tiềm năng, từ đó nâng cao khả năng bảo vệ cho hệ thống.

V. Kết quả thí nghiệm

Kết quả thí nghiệm cho thấy mô hình được đề xuất có khả năng phát hiện các lỗ hổng bảo mật trong các giao thức xác thực người dùng. Các thử nghiệm đã được thực hiện trên nhiều giao thức khác nhau, cho thấy tính hiệu quả của mô hình trong việc phát hiện các điểm yếu. Kết quả này không chỉ khẳng định giá trị của nghiên cứu mà còn mở ra hướng đi mới cho việc phát triển các phương pháp kiểm tra bảo mật trong tương lai.

5.1. Hướng phát triển

Hướng phát triển trong tương lai sẽ tập trung vào việc cải thiện mô hình hóa và mở rộng ứng dụng của nó trong các lĩnh vực khác nhau. Việc áp dụng mô hình này vào các giao thức mới và phức tạp hơn sẽ giúp nâng cao khả năng bảo mật cho các ứng dụng web. Đồng thời, nghiên cứu cũng sẽ tìm kiếm các phương pháp mới để tối ưu hóa quá trình kiểm tra và phát hiện lỗ hổng bảo mật.

Trích đoạn nội dung tài liệu

ĐẠI HỌC QUỐC GIA TP. HỒ CHÍ MINH TRƯỜNG ĐẠI HỌC BÁCH KHOA ________________________ LÝ ĐOÀN DUY KHÁNH KIỂM TRA TÍNH BẢO MẬT CỦA VIỆC XÁC THỰC NGƯỜI DÙNG TRÊN WEB CHUYÊN NGÀNH: KHOA HỌC MÁY TÍNH MÃ SỐ CHUYÊN NGÀNH: 60.01 LUẬN VĂN THẠC SĨ THÀNH PHỐ HỒ CHÍ MINH – tháng 7 năm 2015 CÔNG TRÌNH ĐƯỢC HOÀN THÀNH TẠI TRƯỜNG ĐẠI HỌC BÁCH KHOA –ĐHQG -HCM Cán bộ hướng dẫn khoa học : PGS.TS Quản Thành Thơ Cán bộ chấm nhận xét 1 : TS. Bùi Hoài Thắng Cán bộ chấm nhận xét 2 : TS. Nguyễn Thanh Hiên Luận văn thạc sĩ được bảo vệ tại Trường Đại học Bách Khoa, ĐHQG Tp.

HCM ngày 10 tháng 07 năm 2015 Thành phần Hội đồng đánh giá luận văn thạc sĩ gồm: 1. Dương Tuấn Anh 2. Nguyễn Đức Thái 3. Bùi Hoài Thắng 4.

Nguyễn Thanh Hiên 5. Võ Thị Ngọc Châu Xác nhận của Chủ tịch Hội đồng đánh giá LV và Trưởng Khoa quản lý chuyên ngành sau khi luận văn đã được sửa chữa (nếu có). CHỦ TỊCH HỘI ĐỒNG TRƯỞNG KHOA ĐẠI HỌC QUỐC GIA TP.HCM CỘNG HÒA XÃ HỘI CHỦ NGHĨA VIỆT NAM TRƯỜNG ĐẠI HỌC BÁCH KHOA Độc lập - Tự do - Hạnh phúc NHIỆM VỤ LUẬN VĂN THẠC SĨ Họ tên học viên: Lý Đoàn Duy Khánh MSHV: 13070238 Ngày, tháng, năm sinh: 09/08/1990 Nơi sinh: Tây Ninh Ngành: Khoa Học Máy Tính Mã số: 60. TÊN ĐỀ TÀI: Kiểm Tra Tính Bảo Mật Của Việc Xác Thực Người Dùng Trên Web II.

NHIỆM VỤ VÀ NỘI DUNG: Nghiên cứu, đề xuất và hiện thực một lý thuyết áp dụng mô hình để kiểm tra tính bảo mật, an toàn của giao thức xác thực người dùng trên web. Đồng thời, áp dụng lý thuyết đó lên một trường hợp cụ thể. NGÀY GIAO NHIỆM VỤ : 18/08/2014 IV. NGÀY HOÀN THÀNH NHIỆM VỤ: 08/05/2015 V.

CÁN BỘ HƯỚNG DẪN : PGS. QUẢN THÀNH THƠ Tp. CÁN BỘ HƯỚNG DẪN TRƯỞNG KHOA KH & KTMT (Họ tên và chữ ký) (Họ tên và chữ ký) PGS. QUẢN THÀNH THƠ NỘI DUNG CHỈNH SỬA  Sửa lỗi chính tả và font chữ, dấu câu.

 Viết lại tóm tắt bằng tiếng Việt và tiếng Anh.  Dịch lại cách từ tiếng Anh thành tiếng Việt Lời Cám Ơn Tôi xin gửi lời cảm ơn chân thành và sâu sắc nhất đến PGS. Quản Thành Thơ, thầy đã tận tình hướng dẫn tôi trong suốt quá trình thực hiện đề cương và luận văn cao học, tạo mọi điều kiện để tôi có thể hoàn thành tốt luận văn này. Tôi xin gửi lời biết ơn chân thành đến các Thầy Cô trong khoa Khoa Học & Kỹ Thuật Máy Tính trường Đại Học Bách Khoa TPHCM.

Các Thầy Cô đã rất tận tình chỉ dạy, trang bị cho tôi những kiến thức quý báu trong suốt thời gian tôi học cao học tại trường. Tôi xin gửi lời cảm ơn gia đình, bạn bè và anh chị nơi tôi học tập đã động viên và tạo mọi điều kiện thuận lợi giúp tôi hoàn thành luận văn. Mặc dù đã cố gắng hết sức có thể để hoàn thành tốt nhất luận văn trong phạm vi và khả năng cho phép nhưng chắc chắn luận văn sẽ không tránh khỏi những thiếu sót, kính mong nhận được sự chỉ bảo tận tình của quý Thầy Cô và các bạn. Lý Đoàn Duy Khánh TÓM TẮT LUẬN VĂN Hiện nay, ứng dụng mạng ngày càng phát triển.

Ứng dụng mạng đã đi vào cuộc sống hầu hết các mặt trong cuộc sống. Vì vậy, người ta ngày càng chú ý hơn tới kiểm tra tính an toàn của giao thức mà ứng dụng mạng sử dụng. Để kiểm tra tính an toàn của giao thức xác thực người dùng trên web, có nhiều cách và một trong những cách đó là mô hình hóa chúng và sử dụng các công cụ hỗ trợ kiểm tra trên mô hình đó. LTS là một ngôn ngữ biểu để biểu diễn mô hình được ứng dụng rộng rãi trong các lĩnh vực nghiên cứu.

Mục tiêu đề tài luận văn là nghiên cứu một lý thuyết mới có thể áp dụng biểu diễn được giao thức xác thực người dùng bằng LTS. Sau đó, kiểm tra tính an toàn trên mô hình đó. Từ đó, đưa ra cho chuyên gia một ví dụ mẫu về đường đi mà chúng có khả năng bị tấn công của giao thức xác thực người dùng trên web. ABSTRACT Nowaday, network applications are more and more growing.

They take an important role in human activities. Therefore, people are getting more and more concern about the sercurity of protocol. In order to be able to verify protocol, there are many ways and one of them is we convert it into a model and use supported tools to verify model. LTS is a well- known langluge which had been applied widely in researching.

This thesis aims to research a new theory which we can apply modelling authentication protocol by LTS. Then, we can verify the sercurity of LTS model. Final, we can suggest some counter-example which intruler can acttack in authencation protocol, for experts. LỜI CAM ĐOAN Tôi xin cam đoan rằng, ngoại trừ các kết quả tham khảo từ các công trình khác như đã ghi rõ trọng luận văn, các công việc được trình bày trong luận văn này là do chính tôi thực hiện và chưa có phần nội dung nào của luận văn này được nộp để lấy một bằng cấp ở trường này hoặc trường khác.

Lý Đoàn Duy Khánh MỤC LỤC 1 GIỚI THIỆU .5 Cấu trúc của luận văn.1 Đặc điểm giao thức và kiểm tra .2 Khai thác giao thức. 5 Phương pháp khai thác giao thức David Lie. 6 Mô hình biểu tượng Mihhail Aizatulin .3 Phân tích bảo mật của giao thức SSO. 9 Phân tích bảo mật giao thức SSO thực tế.

10 Phân tích bảo mật giao thức OAuth 2.0 bằng API của nó. 10 Mô hình tấn công web của T.1 Hướng tiếp cận đề tài. 11 3 LÝ THUYẾT NỀN TẢNG .1 Hệ Thống Chuyển Trạng Thái (Transition System - TS) .2 Đường thực thi .3 Hệ Thống Chuyển Trạng Thái Có Đánh Nhãn .4 Luận Lý Tuyến Tính Theo Thời Gian (LTL). 21 4 MÔ HÌNH ĐƯỢC ĐỀ XUẤT .1 Mô Hình Giao Thức .2 Hành vi của thành viên trong hệ thống .1 Hành vi nhận gói tin .2 Hành vi gửi gói tin .3 Hành vi tạo gói tin .4 Tóm tắt hành vi của thành viên giao thức .3 Hành vi của kẻ gian ( intruder).1 Hành vi làm giả gói tin .2 Hành vi nghe lén gói tin (overhear) .3 Hành vi chặn gói tin (intercept) .4 Tóm tắt hành vi của kẻ gian .4 Tập luật suy luận của các đối tượng trong giao thức .2 Giải mã (decryption) bằng khóa K.5 Kiểm tra thuộc tính của giao thức.1 Kiểm tra tính bảo mật.2 Kiểm tra thuộc tính xác thực .1 Giao thức đăng nhập của hdvietnam.1 Mô hình giao thức .2 Mô hình của Client và Server .2 Mô hình của Intruder .3 Kết Quả Thí Nghiệm.2 Hướng phát triển.

40 7 TÀI LIỆU THAM KHẢO. 42 iii MỤC LỤC HÌNH Hình 1.1 Kết nối xác thực của các user và client .2 Quy trình kiểm tra lỗ hổng bảo mật .1 Sơ đồ mô hình của phương pháp David Lie .2 Lược đồ của phương pháp kiểm tra lỗi giao thức code C.1 Mô hình máy bán card điện thoại .2 Mô hình LTS đèn điện.3 Hai mô hình LTS hệ thống tắt mở đèn.4 Mô hình kết hợp song song của hai hệ thống đèn.5 Mô hình LTS kết hợp tuần tự của hai hệ thống đèn.3 Ngữ nghĩa LTL .1 Mô hình LTS của client .2 Mô hình LTS của server .3 Mô hình LTS 𝑐𝑙𝑖𝑒𝑛𝑡 || 𝑠𝑒𝑟𝑣𝑒𝑟 .1 Mô hình của giao thức xác thực hdvietnam .2 Mô hình xác thực của kẻ gian. 33 iv MỤC LỤC BẢNG Bảng 4.1 Bảng ý nghĩa của biểu thức ý nghĩa .2 Hành vi của các thành viên trong giao thức .3 Hành vi của kẻ gian.1 Bảng kiểm tra mạng có bị deallock không .2 Bảng kiểm tra tính an toàn bảo mật tin nhắn của client .3 Bảng kiểm tra tính an toàn bảo mật của gói tin xác thực người dùng .4 Bảng kiểm tra tính an toàn của password người dùng .1 Động cơ Hiện nay, ứng dụng web ngày càng phát triển không ngừng. Trong nhiều lĩnh vực như lĩnh vực kinh tế, lĩnh vực giáo dục đều có sự đóng góp đáng kể của ứng dụng web.

Tuy nhiên, ứng dụng web có rất nhiều lỗi bảo mật và việc kiểm tra lỗi các lỗi rất khó khăn.1 Kết nối xác thực của các user và client Ví dụ 1.1: Giao thức xác thực người giữa sever và người dùng. Để kiểm tra khả năng, tấn công của giao thức phải kiếm tra rất phức tạp tại nhiều vị trí. Trên giao thức có khả năng bị tấn công vào vị trí thứ nhất, thì người lập trình phải tìm hiểu vị trí thứ nhất xem khả năng tấn công. Trên giao thức, lỗ hổng thứ hai có khả năng kẻ gian (intruder) tấn công thì người lập trình phải tìm hiểu, cách tấn công thử và tìm cách phòng thủ.

Tuy nhiên, 1 rất khó xác định được những khả năng và vị trí mà kẻ gian tấn công. Như hình minh họa, kẻ gian có thể có mặt bất kỳ ở đâu, chưa kể server cũng có lúc là trở thành kẻ gian. Do đó, việc kiểm tra các lỗ hổng giao thức rất quan trọng. Người dùng chỉ cần đặt tả lỗ hổng hay điểm yếu của giao thức, hệ thống sẽ kiểm tra xem các lỗ hổng, điểm yếu mà người dùng mô tả, đặt ra.

Tuy nhiên, ứng dụng web được viết bằng nhiều loại ngôn ngữ khác nhau hay sử dụng các framework khác nhau. Do đó, ta có thể có hai giải pháp: Thứ nhất, hệ thống này có thể xây dựng ứng dụng cho ngôn ngữ hay framework tương ứng. Như vậy, nếu ứng dụng sử dụng framework A thì phải sử dụng hệ thống ứng với framework A. Giải pháp này là một giải pháp thật sự tốn nhiều chi phí, sức lực và thời gian quá nhiều.

Có thể xem giải pháp này không khả thi về mặt chi phí. Thứ hai, hệ thống sẽ mô hình hóa lại giao thức theo một ngôn ngữ mô hình. Ngôn ngữ mô hình là một ngôn ngữ dạng mô hình mà ta quy định. Từ đó, người dùng đặt tả lỗi trên ngôn ngữ mô hình vào một công cụ kiểm tra mô hình [6,7].

Công cụ kiểm tra mô hình sẽ kiểm tra các lỗi. Sau khi kiểm tra, công cụ kiểm tra mô hình sẽ cho kết quả cách khả năng tấn công dự trên ví dụ mẫu (counter example). Dựa vào kết quả, người dùng sẽ kiểm tra lại và sửa chữa các lỗ hổng đó. Đây là giải pháp hiệu quả và khả thi hơn.2 Quy trình kiểm tra lỗ hổng bảo mật 1.2 Mục tiêu Mục tiêu đề tài này là nghiên cứu và đưa ra một lý thuyết mô hình hóa giao thức xác thực người dùng để chạy một số ví dụ thực tế.

Đề tài còn đưa ra phương thức để kiểm chứng lỗ hổng bảo mật trên giao thức.