Tài liệu Nghiên cứu các phương pháp hình thức ứng dụng kiểm chứng giao thức an toàn

LỜI CẢM ƠN Sau một thời gian tìm hiểu đề tài “Nghiên cứu các phương pháp hình thức ứng dụng kiểm chứng giao thức an toàn”, em đã hoàn thành tiến độ dự kiến. Để đạt được kết quả này, em đã nỗ lực thực hiện và đồng thời em đã nhận được rất nhiều sự quan tâm, giúp đỡ của quý thầy cô, gia đình và bạn bè . Em xin chân thành cảm ơn giáo viên hướng dẫn: ThS. Nguyễn Hồng Tân – Bộ Môn Công nghệ phần mềm – Trường Đại Học Công Nghệ Thông Tin Và Truyền Thông Thái Nguyên đã tận tình giúp đỡ em hoàn thành đề tài một cách tốt nhất. Em xin chân thành cảm ơn quý thầy cô và ban lãnh đạo trường Đại Học Công Nghệ Thông Tin Và Truyền Thông Thái Nguyên đã nhiệt tình giảng dạy và truyền đạt kiến thức quý báu và bổ ích trong suốt quá trình em học tập tại trường. Em xin chân thành cảm ơn quý thầy cô thuộc Bộ Môn Công nghệ phần mềm – Trường Đại Học Công Nghệ Thông Tin Và Truyền Thông Thái Nguyên đã trang bị cho em những kiến thức chuyên ngành rất hữu ích để em hoàn thành đề tài và phục vụ cho công việc của em sau này. Trong quá trình thực hiện đề tài chắc chắn còn những thiếu sót, em rất mong nhận được sự đóng góp ý kiến từ thầy cô và các bạn. Em xin chân thành cảm ơn! Sinh viên Thiệu Thị Thắm 1 LỜI CAM ĐOAN Đề tài của em được thực hiện trên cơ sở những kiến thức đã tích lũy được trong quá trình học tập và làm việc, sự giúp đỡ tận tình của quý thầy cô, gia đình, bạn bè, cùng với một số tài liệu quý báu mà em sưu tầm được cũng như kho tàng Internet vô tận. Em xin cam đoan không sao chép từ bất cứ một đồ án tốt nghiệp nào. Nếu sai em xin hoàn toàn chịu trách nhiệm trước mọi kỷ luật của nhà trường đề ra. Sinh viên Thiệu Thị Thắm 2 MỤC LỤC LỜI CẢM ƠN .....................................................................................................1 LỜI CAM ĐOAN................................................................................................2 MỤC LỤC ..........................................................................................................3 LỜI NÓI ĐẦU ....................................................................................................5 TÓM TẮT NỘI DUNG.......................................................................................6 CHƯƠNG I. CƠ SỞ LÝ THUYẾT .....................................................................7 1.1. Giới thiệu chung .......................................................................................7 1.2. Giao thức bảo mật an toàn.........................................................................8 1.2.1. Định nghĩa giao thức bảo mật an toàn...............................................8 1.2.2. Các lỗ hổng trong bảo mật và phương thức tấn công mạng...............9 1.2.3. Một số giao thức bảo mật phổ biến .................................................11 1.3. Tổng quan về phương pháp hình thức .....................................................18 1.3.1. Phân loại ........................................................................................19 1.3.2. Sử dụng ..........................................................................................20 1.3.3. Các phương pháp hình thức và hệ thống kí hiệu .............................22 1.3.4. π-Calculus ......................................................................................23 1.3.5. Ưu điểm và nhược điểm .................................................................29 1.4. Công cụ Proverif.....................................................................................30 1.4.1. Đặc điểm của Proverif ....................................................................31 1.4.2. Cài đặt công cụ:..............................................................................32 1.4.3. Mô hình tổng quát ..........................................................................33 1.4.4. Thực thi..........................................................................................33 1.4.5. Ví dụ Hello World..........................................................................41 CHƯƠNG II. TIẾP CẬN VÀ PHÂN TÍCH BÀI TOÁN EXAM.......................44 2.1. Lí do chọn bài toán và phát biểu về bài toán ...........................................44 2.1.1. Giới thiệu bài toán............................................................................44 2.1.2. Đặc tả bài toán bằng ngôn ngữ tự nhiên ...........................................46 2.2. Xác thực và bảo mật trong Exams...........................................................48 2.2.1. Mô hình hóa Exam protocol trong việc áp dụng π-Calculus ............48 3 2.2.2. Thuộc tính xác thực và bảo mật........................................................51 2.3. Kiểm chứng trong Exams .......................................................................55 2.3.1. Kiểm chứng thuộc tính cá nhân. .......................................................55 2.3.2. Kiểm chứng thuộc tính phổ dụng (Universal Verifiability Properties)57 CHƯƠNG III. THỰC NGHIỆM KIỂM CHỨNG TRÊN ..................................58 CÔNG CỤ PROVERIF .....................................................................................58 3.1. Thực hiện mô hình hóa các quy trình ......................................................58 3.2. Thực thi trên proverif..............................................................................60 3.2.1. Kiểm chứng thuộc tính cá nhân........................................................60 3.2.2. Kiểm chứng thuộc tính phổ dụng .....................................................64 KẾT LUẬN.......................................................................................................68 TÀI LIỆU THAM KHẢO .................................................................................69 4 LỜI NÓI ĐẦU Vấn đề bảo đảm thông tin trong quá trình trao đổi thông tin luôn là vấn đề được quân tâm. Trong thực tế, khi hai người bất kỳ muốn trao đổi dữ liệu với nhau, họ phải xác định người kia là ai, sau đó thống nhất với nhau là phải dùng phương pháp mã hóa nào, khóa là gì,… Để làm được điều đó họ phải tiến hành thông qua giao thức bảo mật. Giao thức bảo mật là những chương trình nhằm đảm bảo thông tin liên lạc qua mạng lưới truyền tin dựa vào các kỹ thuật mã hóa. Tuy nhiên việc thiết kế và phát triển các giao thức bảo mật này rất dễ bị mắc lỗi. Điều này được chứng minh qua giao thức rất nổi tiếng Needham-Schroeder public-key đã được Lowe tìm thấy một lỗ hổng sau khi giao thức đã được công bố 17 năm. Một dẫn chứng khác gần đây là phát hiện một lỗ hổng logic trong các tính năng của giao thức TLS khi nó đã được sử dụng rộng rãi kể từ sau 13 năm phiên bản đầu tiên của giao thức được công bố dưới phiên bản SSL 3.0. Lỗi bảo mật có thể có hậu quả nghiêm trọng, dẫn đến việc mất thông tin hoặc mất lòng tin của người dùng trong hệ thống. Hơn nữa, các lỗi bảo mật không thể phát hiện bằng cách kiểm tra các phần mềm chức năng bởi vì chúng chỉ xuất hiện khi có mặt kẻ tấn công. Do đó việc sử dụng các phương pháp hình thức để mô hình hóa và thực hiện kiểm chứng chúng trên các công cụ tự động là rất hữu ích để có được sự bảo đảm thực tế rằng các giao thức bảo mật là chính xác. Điều này là lí do khiến lĩnh vực kiểm chứng giao thức bảo mật được nghiên cứu và phát triển mạnh ở trên thế giới tuy nhiên ở Việt Nam thì còn hạn chế và điều đó là lí do khiến em chọn đề tài “Nghiên cứu các phương pháp hình thức ứng dụng kiểm chứng giao thức an toàn” làm đề tài đồ án tốt nghiệp. 5 TÓM TẮT NỘI DUNG Bản báo cáo được chia thành 3 chương với nội dung như sau:  Chương 1. Cơ sở lý thuyết Trình bày tổng quan về phương pháp hình thức, giao thức bảo mật an toàn và giới thiệu về công cụ kiểm chứng giao thức Proverif.  Chương 2. Tiếp cận và phân tích bài toán Exam Phát biểu, phân tích yêu cầu bài toán và các thuộc tính của Exam, mô hình hóa hình thức cho các thuộc tính xác thực và thuộc tính bảo mật của Exam.  Chương 3. Thực nghiệm kiểm chứng trên công cụ Proverif Thực thi, phân tích và đánh giá kết quả sau khi thực hiện kiểm chứng thuộc tính của bài toán Exam trên công cụ Proverif. 6 CHƯƠNG I. CƠ SỞ LÝ THUYẾT 1.1. Giới thiệu chung Nguy cơ mất an toàn thông tin do nhiều nguyên nhân, đối tượng tấn công đa dạng… Thiệt hại từ những vụ tấn công mạng là rất lớn, đặc biệt là những thông tin thuộc lĩnh vực kinh tế, an ninh, quốc phòng… Theo số liệu thống kê về hiện trạng bảo mật mới nhất công bố của Symantec, Việt Nam đứng thứ 11 trên toàn cầu về các hoạt động đe dọa tấn công mạng. Những xu hướng đe dọa bảo mật ngày càng gia tăng nổi bật hiện nay mà các tổ chức tại Việt Nam cần quan tâm là: tấn công có chủ đích cao cấp, các mối đe dọa trên thiết bị di động, những vụ tấn công độc hại và mất cắp dữ liệu. Thực tế, nguy cơ mất an ninh anh toàn mạng máy tính còn có thể phát sinh ngay từ bên trong. Hệ thống máy tính luôn bị đe dọa bởi các nguy cơ mất an toàn. Một trong những công việc để bảo vệ hệ thống là làm sao giúp hệ thống tránh khỏi các nguy cơ đó. Các nguy cơ và hiểm họa bao gồm: - Hiểm họa vô tình: Khi người dùng khởi động lại hệ thống ở chế độ đặc quyền, họ có thể tùy ý chỉnh sửa hệ thống. Nhưng sau khi hoàn thành công việc họ không chuyển hệ thống sang chế độ thông thường, vô tình để kẻ xấu lợi dụng. - Hiểm họa cố ý: Cố tình truy nhập hệ thống trái phép. - Hiểm họa thụ động: Là hiểm họa nhưng chưa hoặc không tác động trực tiếp lên hệ thống, như nghe trộm các gói tin trên đường truyền. - Hiểm họa chủ động: Là việc sửa đổi thông tin, thay đổi tình trạng hoặc hoạt động của hệ thống Nguyên nhân xuất phát - Từ phía người sử dụng: Xâm nhập bất hợp pháp, ăn cắp tài sản có giá trị. Trong đó quan trọng nhất là những người dùng nội bộ. - Kiến trúc hệ thống thông tin: Tổ chức hệ thống kỹ thuật không có cấu trúc hoặc không đủ mạnh để bảo vệ thông tin. - Chính sách bảo mật an toàn thông tin: Không chấp hành các chuẩn an toàn, không xác định rõ các quyền trong vận hành hệ thống. 7 1.2. Giao thức bảo mật an toàn 1.2.1. Định nghĩa giao thức bảo mật an toàn Giao thức là tập hợp những quy tắc, quy ước truyền thông để thiết lập giao tiếp đúng ngữ nghĩa giữa các chủ thể tham gia. Giao thức bảo mật là những chương trình ngắn nhằm thực hiện các chức năng liên quan đến đảm bảo thông tin liên lạc qua một mạng lưới truyền tin như Internet được an toàn dựa trên các kỹ thuật mã hóa. Những cơ chế mã hóa chính thường được sử dụng như là: Cơ chế mã hóa khóa đối xứng ( Symmetric Key Cryptography), mã hóa khóa bất đối xứng (Asymmetric Key Cryptography) để đảm bảo thỏa mãn các thuộc tính của một giao thức bảo mật thông thường như: - Trao đổi khóa phiên bí mật để mã hóa dữ liệu. - Xác định rõ các bên tham gia, định danh hai cá thể trao đổi dữ liệu, chống phát lại thông điệp. - Truyền dữ liệu an toàn: + Đảm bảo tính bảo mật (Confidentiality): Ngăn chặn được vấn đề xem trộm thông điệp. + Đảm tính chứng thực (Authentication): Nhằm đảm bảo cho bên nhận rằng thông tin không bị thay đổi trong quá trình truyền tin. Như vậy tính chứng thực ngăn chặn các hình thức tấn công sửa thông điệp, mạo danh, và phát lại thông điệp. + Đảm tính không từ chối (Non_repudiation): Là cơ chế để xác định rằng trách nhiệm của các bên tham gia. Cơ chế để bảo đảm tính chứng thực và tính không từ chối của bên tham gia người ta cũng thiết lập một cơ chế như vậy, cơ chế này được gọi là chữ ký điện tử. + Đảm bảo tính rõ ràng (Message Freshness) Giao thức bảo mật được sử dụng phổ biến như sử dụng trong thương mại điện tử: có giao thức TLS (Transport Layer Security) được sử dụng cho https:// URLs. Sử dụng trong các giao dịch ngân hàng, mạng lưới điện thoại di động và hệ thống WiFi..v..v.. 8 1.2.2. Các lỗ hổng trong bảo mật và phương thức tấn công mạng. Các lỗ hổng là những điểm yếu trên hệ thống mà dựa vào đó đối tượng tấn công có thể xâm nhập trái phép vào hệ thống. Các loại lỗ hổng trong bảo mật: + Lỗ hổng loại C: Cho phép thực hiện hình thức tấn công theo kiểu DoS (Denial of Services – Từ chối dịch vụ) làm ảnh hưởng tới chất lượng dịch vụ, ngưng trệ, gián đoạn hệ thống, nhưng không phá hỏng dữ liễu hoặc đoạt được quyền truy cập hệ thống. + Lỗ hổng loại B: Lỗ hổng cho phép người sử dụng có thêm các quyền trên hệ thống mà không cần kiểm tra tính hợp lệ dẫn đến lộ, lọt thông tin. + Lỗ hổng loại A: Cho phép người ngoài hệ thống có thể truy cập bất hợp pháp vào hệ thống, có thể phá hủy toàn bộ hệ thống. Các hình thức tấn công mạng phổ biến. - Tấn công trực tiếp: Sử dụng một máy tính để tấn công một máy tính khác với mục đích dò tìm mật mã, tên tài khoản tương ứng,.. Kẻ tấn công có thể sử dụng một số chương trình giải mã để giải mã các file chứa password trên hệ thống máy tính của nạn nhân. Do đó, những mật khẩu ngắn và đơn giản thường rất dễ bị phát hiện. - Kỹ thuật đánh lừa (Social Engineering): Đây là thủ thuật được nhiều hacker sử dụng cho các cuộc tấn công thâm nhập vào hệ thống mạng và máy tính bởi tính đơn giản mà hiệu quả của nó. Kỹ thuật này thường được sử dụng để lấy cắp mật khẩu, thông tin, tấn công vào và phá hủy hệ thống. Ví dụ, kỹ thuật đánh lừa Fake Email Login. - Kỹ thuật tấn công vào vùng ẩn: Những phần bị dấu đi trong các website thường chứa những thông tin về phiên làm việc của các client. Các phiên làm việc này thường được ghi lại ở máy khách chứ không tổ chức cơ sở dữ liệu trên máy chủ. Vì vậy, người tấn công có thể sử dụng chiêu thức View Source của trình duyệt để đọc phần đầu đi này và từ đó có thể tìm ra các sơ hở của trang Web mà họ muốn tấn công. Từ đó, có thể tấn công vào hệ thống máy chủ. 9 - Tấn công vào các lỗ hổng bảo mật: Hiện, nay các lỗ hổng bảo mật được phát hiện càng nhiều trong các hệ điều hành, các web server hay các phần mềm khác, ... Các hãng sản xuất cũng luôn cập nhật các bản vá lỗ hổng và đưa ra các phiên bản mới sau khi đã vá lại các lỗ hổng của các phiên bản trước. Do đó, người sử dụng phải luôn cập nhật thông tin và nâng cấp phiên bản cũ mà mình đang sử dụng để tránh các hacker lợi dụng điều này tấn công vào hệ thống. - Khai thác tình trạng tràn bộ đệm: Tràn bộ đệm là một tình trạng xảy ra khi dữ liệu được gửi quá nhiều so với khả năng xử lý của hệ thống hay CPU. Nếu hacker khai thác tình trạng tràn bộ đệm này thì họ có thể làm cho hệ thống bị tê liệt hoặc làm cho hệ thống mất khả năng kiểm soát. - Nghe trộm: Các hệ thống trao đổi thông tin qua mạng đôi khi không được bảo mật tốt và lợi dụng điều này, hacker có thể truy cập vào data paths để nghe trộm hoặc đọc trộm luồng dữ liệu truyền qua. - Kỹ thuật giả mạo địa chỉ: Thông thường, các mạng máy tính nối với Internet đều được bảo vệ bằng tường lửa. Tường lửa có thể hiểu là cổng duy nhất mà người đi vào nhà hay đi ra cũng phải qua đó và sẽ bị “điểm mặt”. Tường lửa hạn chế rất nhiều khả năng tấn công từ bên ngoài và gia tăng sự tin tưởng lẫn nhau trong việc sử dụng tài nguyên chia sẻ trong mạng nội bộ. - Kỹ thuật chèn mã lệnh:Một kỹ thuật tấn công căn bản và được sử dụng cho một số kỹ thuật tấn công khác là chèn mã lệnh vào trang web từ một máy khách bất kỳ của người tấn công. - Tấn công dùng Cookies:Cookie là những phần tử dữ liệu nhỏ có cấu trúc được chia sẻ giữa website và trình duyệt của người dùng. Cookies được lưu trữ dưới những file dữ liệu nhỏ dạng text (size dưới 4KB). Chúng được các site tạo ra để lưu trữ, truy tìm, nhận biết các thông tin về người dùng đã ghé thăm site và những vùng mà họ đi qua trong site. Những thông tin này có thể bao gồm tên, định danh người dùng, mật khẩu, sở thích, thói quen. Do đó việc ngăn chặn và hạn chế các lỗ hổng, kiểm chứng các giao thức là điều cần thiết và đáng được quan tâm. Kiểm chứng giao thức bảo mật là việc kiểm tra các chương trình nhằm đảm bảo thông tin liên lạc qua một mạng lưới 10 truyền tin như Internet được an toàn dựa trên các kỹ thuật mã hóa. Lỗi bảo mật có hậu quả nghiêm trọng, dẫn đến mất tiền hoặc mất lòng tin của người sử dụng hệ thống. Hơn nữa, các lỗi bảo mật không thể được phát hiện bằng cách kiểm tra các phần mềm chức năng bởi vì lỗi chỉ xuất hiện khi có sự hiện diện của kẻ thù nguy hiểm. Để chứng minh giao thức bảo mật là chính xác, một trong những nhu cầu đầu tiên là mô hình hóa chúng bằng toán học. Hai mô hình của giao thức được xem xét là: Mô hình xác minh tính toán (Computational veri cation model): Dựa trên việc mô phỏng, chứng minh bằng tay các thuộc tính bảo mật. Việc chứng minh được thực hiện bởi các logic rời rạc, các phần tử. Các thông điệp là các chuỗi bít, chúng coi những hàm mã hóa là ánh xạ từ chuỗi bít-chuỗi bit, phức tạp hơn, hiện đại hơn và có tính xác suất, tính bảo mật chỉ được bảo toàn nếu xác suất các hàm mã hóa bị phá vỡ là vô cùng nhỏ. Trong mô hình này, chiều dài của khóa được xác định bởi tên giá trị là tham số bảo mật, và thời gian chạy của các đối thủ được coi là các hàm đa thức trong tham số bảo mật. Mô hình thứ hai là mô hình xác minh biểu trưng:( Symbolic veri cation model): Dựa trên phương pháp hình thức truy tìm các cuộc tấn công bằng dấu vết của giao thức, mô hình này coi những hàm mã hóa dữ liệu cơ bản là hộp đen, kẻ tấn công không thể giải mã các mật mã cơ sở. Mô hình này giới hạn các đối thủ tấn công để thực hiện tính toán và nó giả định các mật mã là hoàn hảo. Có thể kết hợp với các kĩ thuật khác để chứng minh tính đúng đắn. 1.2.3. Một số giao thức bảo mật phổ biến Mỗi một loại giao thức lại có những đặc tính, đặc điểm khác nhau nhằm bảo đảm các thuộc tính bảo mật và những đặc trưng riêng của từng lĩnh vực. Một số giao thức bảo mật cụ thể như là: Kao Chow Authentication Protocol ( giao thức chứng thực Kao Chow); the 3-D Secure Protocol ( Giao thức bảo mật 3D), Needham Schroeder Public Key Protocol ( Giao thức khóa công khai Needham Schroeder), Andrew Secure RPC Protocol ( Giao thức bảo mật RPC). Challenge Handshake Authentication Protocol ( Giao thức xác minh bắt tay chứng thực ). Diffie- Hellman Key Exchange Protocol ( Giao thức trao đổi khóa 11 Diffie_hellman) là những giao thức đã được sử dụng phổ biến và được quan tâm chú trọng. a. Kao Chow Authentication Protocol Là giao thức chứng thực lẫn nhau và phân phối khóa với mục đích là nhấn mạnh việc chứng thực đảm bảo tính đúng đắn của thông điệp - Đặc tả giao thức: + Kas , Kbs : là các khóa đối xứng tương ứng của các giá trị A và S, B và S. A và B là bên giao tiếp với nhau, phát sinh thêm một bên đáng tin cậy S. + Na, Nb: là số duy nhất cho việc chứng thực lẫn nhau và để kiểm chứng tính chứng thực của khóa đối xứng Kab + Thông điệp 3,4 được xác thực lặp đi lặp lại. Sau khi thông điệp 1,2 đã được hoàn thành thì 3,4 có thể phát lại dịch vụ nhiều lần bởi B trước khi bắt đầu giao tiếp bí mật với A và được mã hóa với khóa phiên Kab. Giao thức này được thiết kế để ngăn chặn các cuộc tấn công mới mẻ trên một phần xác thực lặp đi lặp lại của các giao thức Neumann Stubblebine. Thực ra, số duy nhất Na trong thuật toán mã hóa của thông điệp 2 ngăn chặn việc chia sẻ khóa bị xâm nhập sau mỗi lần chạy và sử dụng lại giao thức. Giao thức phải đảm bảo giứ bí mật của Kab: Trong mỗi phiên giá trị của Kab chỉ được biết bởi bên tham gia A,B và S. Khi A yêu cầu, B nhận khóa Kab trong thông điệp 3 và yêu cầu 2. Khóa này phải được ban hành trong cùng một phiên bởi máy chủ S với A bắt đầu giao tiếp bằng thông điệp 1. Giao thức cũng phải đảm bảo chứng thực lẫn nhau giữa A và B. b. Needham Schroeder Public Key Protocol Dựa trên mã hóa khóa công khai. Giao thức này được thiết kế để cung cấp chứng thực lẫn nhau giữa hai bên giao tiếp trên mạng. Nó được giả định rằng hai 12 bên biết được khóa công khai của nhau. Như vậy, việc mã hóa các dữ liệu có thể sử dụng khóa công khai của từng bên. -Đặc tả giao thức Giả sử A, B sử dụng một máy chủ (S) đáng tin cậy để phân phối khóa công khai theo yêu cầu. + KPA và KSA: Khóa công khai và khóa ẩn khi thực hiện mã hóa A ( S: khóa bí mật "secret key") + KPB và KSB: Khóa công khai và khóa bí mật khi thực hiện mã hóa B + KPS và KSS: Khóa công khai và khóa bí mật khi thực hiện mã hóa S ( có những thuộc tính mà Kss được sử dụng để mã hóa và giải mã KPS Giao thức được chạy như sau: A yêu cầu khóa công khai của B từ S S phản hổi với khóa công khai KPB cùng với danh tính của B có chữ ký của máy chủ với mục đích xác thực. A chọn ngẫu nhiên một một số NA và gửi nó cho B. B bây giờ biết A muốn giao tiếp, vì vậy B yêu cầu các khóa công khai của A. Máy chủ phản hồi B chọn một số ngẫu nhiên NB và gửi nó cho A cùng với NA để chứng minh khả năng giải mã với KSB. A xác nhận NB từ B để chứng minh khả năng giải mã với KSA 13 Tại thời điểm kết thúc của giao thức. A và B sẽ biết danh tính của nhau và biết cả NA,NB là những số duy nhất không được tiết lộ cho kẻ nghe lén thông tin. Tuy nhiên giao thức này dễ bị tổn thương từ một kẻ tấn công trung gian. Nếu một kẻ mạo danh có thể thuyết phục A để bắt đầu một phiên làm việc với A, nó có thể chuyển tiếp các thông điệp đến B và thuyết phục B giao tiếp với A. Bỏ qua các thông tin đến và đi từ S cái mà không thay đổi, các cuộc tấn công chạy như sau: A gửi NA đến I cài mà đã giải mã các thông tin với KSI I sẽ chuyển thông điệp tới B và trả vờ như là A đang giao tiếp B gửi NB I chuyển tiếp đến A A giải mã NB và xác nhận nó cho I người mà lấy cắp thông tin. I mã hóa lại NB và thuyết phục B rằng đã giải mã nó. Khi kết thúc cuộc tấn công, B đã sai lầm tin rằng mình đã giao tiếp với A và NA,NB chỉ biết bởi A và B. Cuộc tấn công được mô tả đầu tiên bởi Gavin Lowe trong năm 1995. Và cũng đã sửa chữa và đưa ra một phiên bản khác có tên Needham Schroeder Lowe Protocol. Việc sửa chữa được sửa đổi ở thông điệp thứ 6 bao gồm danh tính của người trả lời: Được thay thế bằng 14 c. Andrew Secure RPC Protocol Giao thức này nhằm phân phối khóa phiên làm việc mới giữa các bên tham gia A và B. Khi khóa phiên k được chia sẻ thì nó phải đảm bảo tính bí mật. - Đặc tả giao thức A, B : principal Kab, K'ab : symkey Na, Nb, N'b : nonce succ : nonce -> nonce 1. A->B: A, {Na}Kab 2. B->A: {succNa, Nb}Kab 3. A->B: {succNb}Kab 4. B ->A: {K'ab, N'b}Kab Giao thức này thiết lập việc chia sẻ một khóa đối xứng mới là K’ab. N’b là số duy nhất gửi đi trong thông điệp 4 sẽ được dùng trong các phiên tiếp theo. Giả định ban đầu khóa đối xứng Kab chỉ được biết bởi A và B . Giao thức phải bảo đảm giữ bí mật khóa K'ab mới được chia sẻ: Trong mỗi phiên, giá trị của K'ab chỉ được biết bởi người tham gia đóng vai trò Avà B. Giao thức phải bảo đảm tính xác thực của khóa K’ab. Trong mỗi phiên, khi tiếp nhận thông điệp 4 thì A phải đảm bảo rằng các khóa K'ab trong thông điệp đã được tạo ra bởi A trong cùng một phiên. d. Challenge Handshake Authentication Protocol Giao thức này dùng để chứng thực người dùng hoặc các máy chủ nhà mạng nhằm mục đích chứng thực các thực thể của các bên tham gia. Nó được sử dụng định kì để xác minh các danh tính ngang hàng sử dụng cách thức bắt tay 3 bước ( 3-way Handshake). Điều này được hình thành dựa việc thiết lập các liên kết ban đầu (LCP) và có thể được lặp lại bất cứ lúc nào. Giao thức này là một chương trình xác thực được sử dụng bởi giao thức Point To Point (PPP) máy chủ để xác nhận danh tính của khách hàng từ xa. Nó đòi hỏi cả client và sever phải biết các bí mật bản rõ mặc dù nó chưa được gửi qua môi trường mạng. Giao thức này cung cấp bảo mật tốt hơn sơ với Password Authentication Protocol (PAP) 15 - Chu kỳ làm việc 1. Sau khi hoàn thành giai đoạn thiết lập liên kết ban đầu. Việc chứng thực sẽ gửi một thông điệp thách thức (challenge) đến với những đối tượng ngang hàng. 2. Các đối tượng ngang hàng này sẽ phản hồi với một giá trị được tính toán bằng cách sử dụng một hàm băm một chiều trên các thách thức và bí mật được phối hợp. 3. Thực hiện chứng thực việc kiểm tra các đáp ứng chống lại tính toán riêng về các giá trị băm mong muốn. Nếu các giá trị phù hợp thì việc chứng thực được thừa nhận. Ngược lại nó sẽ châm dứt kết nối. 4. Tại những khoảng thời gian ngẫu nhiên, việc chứng thực sẽ gửi một thách thức mới cho các đối tượng ngang hàng và thực hiện việc lặp đi lặp lại các bước từ 1 đến 3. Ưu điểm: - Cung cấp giải pháp bảo vệ chống lại việc tấn công quay lại bởi các đối tượng ngang hàng thông qua việc từng bước thay đổi định danh và biến thách thức giá trị. Việc sử dụng các thách thức lặp đi lặp lại là nhằm hạn chế thời gian tiếp xúc với bất kỳ cuộc tấn công đơn nào. Thực hiện chứng thực ở trong kiểm soát tần số và thời gian của những thách thức. e. Diffie- Hellman Key Exchange Protocol Là một phương pháp cho hai người sử dụng máy tính tạo ra một khóa riêng chia sẻ với nhau để có thể trao đổi thông tin trên một kênh không an toàn. Khóa này có thể được sử dụng sau đó để mã hóa các thông báo tiếp theo bằng cách sử dụng một thuật toán mã hóa khóa đối xứng. - Đặc tả giao thức: Ta có hai bên giao tiếp là A và B. Đầu tiên họ đưa ra 2 số nguyên tố p và g. Trong đó p là số lớn ( thường ít nhất là 512 bit) và g là một phần gốc của nguyên tố p. Trong thực tế cũng có thể thay thế p bằng (p-1) / 2 cũng là số nguyên tố. Các con số g và p không cần phải được giữ bí mật từ những người dùng khác. 16 Đầu tiên A chọn một số ngẫu nhiên lớn a như một khóa riêng của mình và B cũng chọn một số lớn b làm khóa riêng của mình . Sau đó A thực hiện tính A= g ^ a (mod p) cái mà gửi cho B. Và B thực hiện tính B = g ^ b (mod p) cái mà nhận được từ A.Tiếp theo cả A và B tính toán khóa chia sẻ của họ K = g ^ (ab) (mod p). A thực hiện tính khóa K=B^a (mod p)=(g^b)^a (mod p). B thực hiện tính khóa K=A^b (mod p)=(g^a)^b (mod p). A và B có thể sử dụng khóa K để chia sẻ thông tin vơi nhau mà không cần lo lắng về người dùng khác biết được thông tin này. Để cho một kẻ nghe lén (Eve) có khả năng làm được điều đó thì đầu tiên họ cần có được K=g^(ab) (mod p) chỉ biết g, p, A = g ^ a (mod p) và B = g ^ b (mod p). Điều này có thể được thực hiện bằng cách tính toán a từ A = g ^ a (mod p) và b từ B = g ^ b (mod p). Đây là bài toán logarit rời rạc cái mà khả thi để tính toán cho số p lớn. Tính toán logarit rời rạc của một số lớn p cũng phải mất một khoảng thời gian như việc phân tích kết quả của hai số nguyên tố cùng kích thước với p cái mà dựa trên sự an toàn của hệ mật mã RSA. Như vậy giao thức này có độ an toàn gần tương đồng với RSA. f. The 3-D Secure Protocol Là giao thức dựa trên XML được dùng như một lớp bảo mật bổ sung cho các giao dịch thẻ tín dụng và ghi nợ trực tuyến. Ban đầu nó được phát triển bởi Hệ thống Arcot, Inc và lần đầu tiên được triển khai bởi Visa với ý định cải thiện sự an toàn của các tài khoản thanh toán trên Internet được cung cấp cho khách hàng theo tên xác minh bởi Visa. Mỗi bên phát hành có thể sử dụng bất kỳ loại phương pháp chứng thực nào. Phương pháp phổ biến nhất là phương pháp dựa trên mật khẩu. Như vậy , để thanh toán online thì ta sử dụng một mật khẩu bí mật gắn vào thẻ. Cách xác minh bởi giao thức của Visa là đề nghị trang xác minh của ngân hàng nạp vào một khung (frame) nội tuyến. Bằng cách này, hệ thống của ngân hàng có thể được tổ chức để chịu trách nhiệm cho hầu hết các lỗ hổng bảo mật. Các dịch vụ dựa trên giao thức cũng đã được thông qua bởi MasterCard như: MasterCard SecureCode và bởi JCB International như: J/Secure. American 17 Express đã thêm 3-D Secure vào 11/8/2010 như: American Express SafeKey trong các môi trường được chọn lọc và tiếp tục triển khai và bổ sung thêm một số môi trường nữa. Nhiều những nghiên cứu và phân tích các giao thức đã cho thấy nó có nhiều vấn đề bảo mật ảnh hưởng đến người dùng bao gồm tất cả các trường hợp có thể lừa đảo và sự thay đổi về trách nhiệm trong các trường hợp thanh toán gian lận. 1.3. Tổng quan về phương pháp hình thức Phương pháp hình thức là việc áp dụng các kỹ thuật toán học cho việc đặc tả và phân tích các thuộc tính và các hành vi của các đối tượng, phát triển và kiểm định các hệ thống phần mềm và phần cứng. Nó được phân biệt từ các đặc tả yêu cầu hệ thống bằng cách nhấn mạnh tính đúng đắn và chứng minh nó. Cách tiếp cận này đặc biệt quan trọng đối với các hệ thống cần có tính toàn vẹn cao, chẳng hạn hệ thống điều khiển lò phản ứng hạt nhân hay điều khiển tên lửa và các hệ thống mà an toàn, bảo mật giữ vai trò quan trọng, để góp phần đảm bảo rằng quá trình phát triển hệ thống sẽ không có lỗi. Các phương pháp hình thức đặc biệt hiệu quả tại giai đoạn đầu của quá trình phát triển (tại các mức yêu cầu và đặc tả hệ thống), nhưng cũng có thể được sử dụng cho một quá trình phát triển hoàn chỉnh của một hệ thống. Nó chỉ ra tính chính xác (correctness) của toàn bộ hệ thống (tính chính xác luôn luôn đi kèm thuộc tính cụ thể). Để thay thế cho kiểm thử (Các phương pháp hình thức chạy trên mã nguồn, hay có thể trên byte code). Lịch sử của phương pháp hình thức: - Những năm 80, kiểm định phần mềm được xem như “chết”. + Ít tự động, người lập trình phải nỗ lực “bằng chân tay” quá nhiều. + Chỉ có một số ít chương trình ví dụ có thể chạy được. - Những năm 90, kiểm tra mô hình (model checker) thành công. + Kiểm tra một cách đầy đủ và tự động hoàn toàn các mô hình (với một tập các trạng thái hữu hạn). + Kiểm định phần cứng và các giao thức giao tiếp. - Từ cuối những năm 90, mối quan tâm về kiểm định phần mềm tăng lên. 18 + Chứng minh/kiểm tra mô hình những phần quan trọng của phần mềm. - Những ứng dụng mới như proof-carrying-code (PCC). + Đặt các bằng chứng (proof) cùng với mã máy (machine code) và chứng minh rằng mã máy đó thỏa mãn một số thuộc tính về bảo mật/an toàn. - Xem xét những vấn đề mới: bảo mật. Phương pháp hình thức là chủ để “hot” trong nghiên cứu cũng như trong công nghiệp. 1.3.1. Phân loại Các phương pháp hình thức có thể được sử dụng tại nhiều mức: - Mức 0: Đặc tả hình thức có thể được thực hiện và rồi một chương trình được phát triển từ đặc tả này một cách không hình thức. Trong nhiều trường hợp, cách này có thể là lựa chọn hiệu quả nhất về mặt chi phí. - Mức 1: Sử dụng phát triển và kiểm định hình thức để tạo một chương trình theo một quy trình hình thức hơn. Ví dụ, có thể thực hiện các chứng minh về các tính chất hoặc quá trình tinh chỉnh (refinement) từ đặc tả hình thức tới một chương trình. Đây có thể là lựa chọn phù hợp nhất đối với các hệ thống yêu cầu tính toàn vẹn cao với các tiêu chí về an toàn và an ninh. - Mức 2: Sử dụng các bộ chứng minh định lý (theorem prover) để thực hiện các chứng minh hình thức hoàn toàn và được kiểm chứng bằng máy móc. Việc này có thể đòi hỏi chi phí rất cao và chỉ đáng lựa chọn trong thực tiễn nếu phí tồn cho các lỗi sai là cực kỳ cao (ví dụ, trong các phần quan trọng của thiết kế bộ vi xử lý). Cùng với việc phân loại ngữ nghĩa hình thức của ngôn ngữ lập trình, các phương pháp hình thức có thể được phân loại tương đối như sau: - Ngữ nghĩa ký hiệu (Denotational semantics): Trong đó ý nghĩa của một hệ thống được biểu diễn bằng lý thuyết toán học về miền xác định. Ưu điểm của những phương pháp này phụ thuộc vào bản chất được hiểu rõ của các miền xác định để từ đó đem lại ý nghĩa cho hệ thống. Nhược điểm của nó là không phải hệ thống nào cũng có thể được nhìn một cách tự nhiên hoặc trực quan dưới dạng một hàm số. 19 - Ngữ nghĩa hoạt động (Operational semantics): Trong đó, ý nghĩa của một hệ thống được biểu diễn bằng một chuỗi các hành động của một mô hình tính toán (các giả thiết) đơn giản hơn. Ưu điểm của phương pháp này là tính đơn giản của các mô hình tạo nên sự trong sáng của việc biểu diễn. Nhược điểm là phương pháp này đã trì hoãn các vấn đề của ngữ nghĩa (ai định nghĩa ngữ nghĩa của các mô hình đơn giản hơn?) - Ngữ nghĩa tiên đề (Axiomatic semantics): Trong đó, ý nghĩa của hệ thống được biểu diễn theo các tiền điều kiện (precondition) và hậu điều kiện (postcondition), đây lần lượt là các điều kiện phải được thỏa mãn tại các thời điểm trước và sau khi hệ thống thực hiện một nhiệm vụ. Ưu điểm phương pháp này là nó có mối quan hệ với lôgic kinh điển. Nhược điểm của nó là những ngữ nghĩa thuộc dạng này không thực sự mô tả xem hệ thống làm cái gì (chỉ là cái gì đúng trước đó và sau đó). 1.3.2. Sử dụng Các phương pháp hình thức có thể được áp dụng tại nhiều điểm khác nhau trong cả quá trình phát triển phần mềm. Tuy có thể nói đến một quá trình phát triển bất kỳ, nhưng để thuận tiện, ta sẽ dùng các thuật ngữ và quy trình của mô hình thác nước. a. Đặc tả: Các phương pháp hình thức có thể được sử dụng để mô tả về hệ thống cần phát triển, tại bất kỳ mức độ chi tiết mà ta muốn. Mô tả hình thức này có thể được sử dụng để hướng dẫn các hoạt động phát triển tiếp theo, ngoài ra nó có thể được sử dụng để kiểm định xem các yêu cầu cho hệ thống đang được phát triển đã được đặc tả một cách đầy đủ và chính xác hay chưa. Nhu cầu về các hệ thống đặc tả hình thức đã được nói đến từ nhiều năm. Trong Báo cáo ALGOL 60, John Backus đã trình bày một hệ thống ký hiệu hình thức để mô tả cú pháp ngôn ngữ lập trình (sau này đặt tên là Backus normal form hay Backus Naur Form (BNF) dạng chuẩn tắc Backus). 20