Lôgic BAN

Lôgic BAN (tiếng Anh: BAN logic, viết tắt của Burrows-Abadi-Needham logic) là một tập hợp các quy tắc để định nghĩa và phân tích các giao thức truyền thông. Cụ thể hơn, lôgic BAN được dùng để kiểm tra các giao thức có đảm bảo an toàn trước những kẻ tấn công hay không. Trong lôgic BAN, người ta giả định các giao dịch được thực hiện trên một môi trường không an toàn và kẻ tấn công luôn có khả năng đọc được các gói tin trên đường truyền. Điều này được phát triển thành một nguyên tắc trong an ninh hệ thống: "Không được tin vào mạng truyền dẫn".

Tên của lôgic BAN được đặt theo tên của 3 nhà khoa học đã tạo ra nó: Michael Burrows, Martín Abadi, và Roger Needham.

Một quy trình sử dụng lôgic BAN tiêu biểu bao gồm 3 bước:^[1]

1. Kiểm tra nguồn gốc các gói tin
2. Kiểm tra tính chất mới của các gói tin (chống lại việc phát lại gói tin cũ)
3. Kiểm tra độ tin cậy của nguồn gốc

Để phân tích các giao thức, lôgic BAN sử dụng các định đề và định nghĩa. Trước khi đưa vào phân tích, các giao thức cần được biểu diễn theo hệ thống ký hiệu giao thức mật mã (cách biểu diễn này thường có trong các bài nghiên cứu).

Kiểu ngôn ngữ và các lựa chọn khác

Lôgic BAN và các lôgic cùng lớp là các ngôn ngữ xác định. Điều này có nghĩa tồn tại thuật toán với đầu vào là các giả thuyết BAN và các yêu cầu của giao thức được xét và đầu ra là các kết luận liệu giao thức đó có đạt được các yêu cầu đã nêu hay không. Các thuật toán được sử dụng là các biến thể của thuật toán magic set nêu tại (Monniaux, 1999).

Lôgic BAN là tiền đề cho rất nhiều dạng lôgic tương tự, chẳng hạn như lôgic GNY. Một số trong những phát triển này nhằm khắc phục những điểm yếu tồn tại trong lôgic BAN như sự thiếu sót các giải thích rõ ràng về ngữ nghĩa trong những điều kiện cụ thể.

Các quy tắc cơ bản

Sau đây là định nghĩa và ý nghĩa của các quy tắc cơ bản (trong đó, P và Q là 2 thực thể cần liên lạc với nhau, X là một văn bản/gói tin còn K là khóa)

• P believes X: P coi X là đúng và có thể xác nhận X trong các gói tin khác.
• P has jurisdiction over X: Sự tin tưởng của P đối với X là có cơ sở.
• P said X: Tại một thời điểm trong quá khứ, P đã gửi (và tin) X, mặc dầu hiện tại P có thể không còn tin vào X.
• P sees X: P đã nhận được X, có thể đọc và gửi lại X.
• {X}_K: X được mật mã hóa với khóa K.
• fresh(X): X vừa mới được tạo ra và gửi đi.
• key(K, P<->Q): P và Q có chung khóa K để trao đổi thông tin mật.

Ý nghĩa của các định nghĩa trên có thể được diễn giải thông qua một số định đề sau:

• Nếu P believes key(K, P<->Q), và P sees {X}_K, thì P believes (Q said X)
• Nếu P believes (Q said X) và P believes fresh(X), thì P believes (Q believes X).

Ở đây, P phải tin tưởng rằng gói tin X là mới được tạo ra (fresh). Ngược lại, X có thể là một gói tin cũ được một kẻ tấn công nào đó thu và phát lại.

• Nếu P believes (Q has jurisdiction over X) và P believes (Q believes X), thì P believes X
• Có một số phương pháp để xử lý việc kết hợp (ghép) các gói tin. Chẳng hạn, nếu P believes that Q said <X, Y>, bản tin ghép X và Y, thì P cũng cho rằng Q said X và Q said Y.

Với phương pháp biểu diễn nêu trên, các giả định đằng sau các giao thức xác thực có thể được chuẩn hóa. Sử dụng các định đề, ta có thể chứng minh một thực thể nào đó tin tưởng rằng họ có thể thực hiện giao dịch an toàn với một vài khóa nhất định. Nếu chứng minh cho kết quả ngược lại (không đảm bảo an toàn), thì kết quả thường chỉ ra cách thức mà kẻ tấn công có thể thực hiện.

Phân tích giao thức Wide Mouth Frog với lôgic BAN

Sau đây là ứng dụng lôgic BAN vào phân tích giao thức giao thức Wide Mouth Frog, một giao thức đơn giản cho phép 2 thực thể, A và B, thiết lập một kênh truyền thông an toàn với sự tham gia của một máy chủ xác thực và các đồng hồ được đồng bộ hóa.

A và B đều có chung khóa (đối xứng) với máy chủ S: K_as và K_bs. Vì thế, ta có thể giả định:

A believes key(K_as, A<->S)

S believes key(K_as, A<->S)

B believes key(K_bs, B<->S)

S believes key(K_bs, B<->S)

A muốn thiết lập một giao dịch với B. A tạo ra một khóa phiên K_ab dùng để mật mã hóa các gói tin trao đổi với B. A tin rằng khóa này là an toàn vì khóa do chính mình tạo nên:

A believes key(K_ab, A<->B)

B sẽ chấp nhận khóa nếu như anh ta tin rằng khóa thực sự là do A gửi đến:

B believes (A has jurisdiction over key(K, A<->B))

Ngoài ra, B cũng tin S sẽ chuyển những thông tin từ A một cách chính xác;

B believes (S has jurisdiction over (A believes key(K, A<->B)))

Do đó, nếu B cho rằng S tin rằng A muốn dùng một khóa nhất định để trao đổi thông tin với B thì B sẽ tin S và khóa được gửi đến.

Mục tiêu của giao thức là:

B believes key(K_ab, A<->B)

Quá trình thực hiện giao thức như sau:

Đầu tiên, A xác định thời gian hiện tại t, và gửi gói tin:

1. A->S: {t, key(K_ab, A<->B)}_Kas

Gói tin bao gồm thời gian hiện tại cùng với khóa phiên do A chọn, tất cả được mật mã hóa với khóa chung giữa A và S - K_as.

Do S believes that key(K_as, A<->S) và S sees {t, key(K_ab, A<->B)}_Kas nên S kết luận rằng A thực tế đã gửi {t, key(K_ab, A<->B)}. Có nghĩa là S tin rằng gói tin này không phải do một kẻ tấn công nào đó tạo ra.

Vì tất cả đồng hồ được đồng bộ hóa, ta có thể giả định:

S believes fresh(t)

Do S believes fresh(t) và S believes A said {t, key(K_ab, A<->B)}, nên S tin rằng A thực sự tin (believes) vào key(K_ab, A<->B). (Cụ thể hơn, S tin rằng gói tin đã không bị một kẻ tấn công nào đó gửi lại.)

Sau đó S chuyển khóa phiên tới B:

2. S->B: {t, A, A believes key(K_ab, A<->B)}_Kbs

Do gói tin 2 được mật mã hóa với K_bs và B believes key(K_bs, B<->S) nên B tin rằng S said {t, A, A believes key(K_ab, A<->B)}. Do các đồng hồ được đồng bộ hóa nên B believes fresh(t) và fresh(A believes key(K_ab, A<->B)). Do B tin rằng gói tin của S gửi đến là mới nên B cũng tin rằng S believes (A believes key(K_ab, A<->B)). Vì B tin vào S nên B believes (A believes key(K_ab, A<->B)). Vì thế, B believes key(K_ab, A<->B). Lúc này B có thể liên lạc trực tiếp với A sử dụng khóa phiên K_ab.

Bây giờ ta giả sử các đồng hồ không được đồng bộ. Trong trường hợp này S nhận gói tin thứ nhất từ A: {t, key(K_ab, A<->B)} nhưng không thể kết luận gói tin này có mới hay không. S chỉ biết được rằng A đã từng tạo ra gói tin trên trong quá khứ (vì gói tin được mật mã hóa bằng khóa bí mật của A) nhưng không thể xác định được hiện tại A có còn muốn sử dụng khóa phiên K_ab nữa hay không. Vì vậy, một kẻ tấn công có thể lợi dụng điểm yếu này: kẻ tấn công có thể lấy được một khóa phiên cũ (việc này tốn nhiều thời gian) và gửi lại gói tin {t, key(K_ab, A<->B)}. Khi đó, S có thể không phát hiện được đây là gói tin gửi lại (do đồng hồ không đồng bộ) và chuyển tới B một khóa phiên cũ đã bị lộ.

Bài nghiên cứu gốc Logic of Authentication (xem liên kết ở phần sau) có bao gồm ví dụ trên cùng một số những dẫn chứng khác như phân tích giao thức Kerberos và 2 phiên bản của giao thức bắt tay Andrew RPC (trong đó có 1 giao thức có lỗi).

Tham khảo

1. “UT Austin CS course material on BAN logic (PDF)” (PDF). Bản gốc (PDF) lưu trữ ngày 26 tháng 1 năm 2020. Truy cập ngày 3 tháng 8 năm 2006.

• David Monniaux, Decision Procedures for the Analysis of Cryptographic Protocols by Logics of Belief, in Proceedings of The 12th Computer Security Foundations Workshop, 1999. (Online).

Liên kết ngoài

• A Logic of Authentication Lưu trữ 2003-12-22 tại Wayback Machine, bài nghiên cứu cơ sở của Burrows, Abadi, và Needham.
• Nguồn: The Burrows-Abadi-Needham logic Lưu trữ 2005-09-02 tại Wayback Machine
• BAN logic in context, from UT Austin CS (PDF) Lưu trữ 2020-01-26 tại Wayback Machine