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:
Để 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)
Ý 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:
Ở đâ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.
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" 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:
"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:
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;
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à:
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:
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"&lt;-&gt;"S") và S" sees {"t", key("K""ab", "A"&lt;-&gt;"B")}"K""as" nên "S" kết luận rằng "A" thực tế đã gửi {"t", key("K""ab", "A"&lt;-&gt;"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:
Do S" believes fresh("t") và S" believes "A" said {"t", key("K""ab", "A"&lt;-&gt;"B")}, nên
"S" tin rằng "A" thực sự tin ("believes") vào key("K""ab", "A"&lt;-&gt;"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":
Do gói tin 2 được mật mã hóa với "K""bs" và ""'B"
believes key("K""bs", "B"&lt;-&gt;"S") nên B tin rằng "S"
said {"t", "A", "A" believes key("K""ab", "A"&lt;-&gt;"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"&lt;-&gt;"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"&lt;-&gt;"B")). Vì B tin vào S nên B believes ("A" believes key("K""ab", "A"&lt;-&gt;"B")). Vì thế, B" believes key("K""ab", "A"&lt;-&gt;"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"&lt;-&gt;"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"&lt;-&gt;"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).