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:Ý nghĩa:
Alice gửi tới
Bob một gói tin chứa thông điệp
X 1 {\displaystyle X_{1}} được mật mã hóa bằng khóa chung
KAB.Một ví dụ khácÝ 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.