BAN Logic Rules.

Table 2: BAN Logic Rules.

Name	Description
Message-Meaning Rule	$\frac{P\| \equiv P \overset{X}{\leftrightarrow} Q, P ⊲ {\{X\}}_{K}}{P\| \equiv Q\| \sim X}$
Nonce-Verification Rule	$\frac{P\| \equiv # (X), P\| \equiv Q\| \sim X}{P\| \equiv Q\| \equiv X}$
Jurisdiction Rule	$\frac{P\| \equiv Q \Rightarrow X, P\| \equiv Q\| \equiv X}{P\| \equiv X}$
Belief Conjuncatenation Rule	$\frac{P\| \equiv X, P\| \equiv Y}{P\| \equiv (X, Y)}$
Freshness Conjuncatenation Rule	$\frac{P\| \equiv f r e s h (X)}{P\| \equiv f r e s h (X, Y)}$