Ký hiệu giao thức mật mã

Hệ thống ký hiệu giao thức mật mã là tập hợp những cách thức biểu diễn các gói tin trao đổi giữa các bên tham gia giao dịch theo một giao thức mật mã nhất định trong môi trường mạng máy tính. Cách thức biểu diễn này cho phép suy luận các đặc tính của giao thức và cung cấp một mô hình chuẩn tắc (formal model) để có thể áp dụng lôgic BAN.

Hệ thống ký hiệu bao gồm tập hợp một số thực thể tham giao vào quá trình truyền thông (thường được gọi là Alice and Bob, Charlie...) Họ có thể truy cập tới một máy chủ S, có chung khóa K, thời điểm T, và có thể tạo ra các số ngẫu nhiên (nonce) N dùng cho mục đích xác thực.

Một ví dụ đơn giản:

$A\rightarrow B:\{X_{1}\}_{K_{AB}}$

Ý nghĩa: Alice gửi tới Bob một gói tin chứa thông điệp $X_{1}$ được mật mã hóa bằng khóa chung K_AB.

Một ví dụ khác

$B\rightarrow A:\{N_{B}\}_{PK(A)}$

Ý nghĩa: Bob gửi tới Alice một số ngẫu nhiên N, mật mã hóa bằng khóa công khai của Alice.

Khóa với hai chỉ số dưới dùng để biểu diễn khóa đối xứng dùng giữa hai thực thể. Khóa với một chỉ số biểu diễn khóa công khai. Khóa bí mật được biểu diễn bằng cách nghịch đảo của khóa công khai.

Hệ thống ký hiệu như trên chỉ thể hiện cách hoạt động của giao thức chứ không phải là ý nghĩa. Chẳng hạn, theo hệ thống này thì mật mã hóa khóa công khai và chữ ký số được biểu diễn giống nhau.

Hệ thống này cũng có thể được dùng cho các giao thức phức tạp hơn, chẳng hạn như giao thức Kerberos.