Notation used in BAN Logic.

Table 1: Notation used in BAN Logic.

Notations	Description
$P\| \equiv X$	P believes X.
$P ⊲ X$	P sees X.
$P\| \sim X$	P once said X.
$P \Rightarrow X$	P has jurisdiction over X.
$# (X)$	The formula X is fresh.
$P \overset{K}{\leftrightarrow} Q$	P and Q may communicate with each other using the shared key K, which is a good key.
$P \overset{X}{\leftrightarrow} Q$	The secret formula X is only known to P and Q.
${\{X\}}_{K}$	The formula X is encrypted with key K.
${〈X〉}_{Y}$	The formula X is combined with secret Y.