Table 2:
BAN Logic Rules.
Name
Description
Message-Meaning Rule
P
≡
P
↔
X
Q
,
P
⊲
X
K
P
≡
Q
∼
X
Nonce-Verification Rule
P
≡
#
(
X
)
,
P
≡
Q
∼
X
P
≡
Q
≡
X
Jurisdiction Rule
P
≡
Q
⇒
X
,
P
≡
Q
≡
X
P
≡
X
Belief Conjuncatenation Rule
P
≡
X
,
P
≡
Y
P
≡
(
X
,
Y
)
Freshness Conjuncatenation Rule
P
≡
f
r
e
s
h
(
X
)
P
≡
f
r
e
s
h
(
X
,
Y
)