https://doi.org/10.31449/inf.v43i2.1617 Informatica 43 (2019) 161–175 161
On the Properties of Epistemic and Temporal Epistemic Logics of
Authentication
Sharar Ahmadi and Mehran S. Fallah
Department of Computer Engineering and Information Technology
Amirkabir University of Technology (Tehran Polytechnic), Hafez Ave., Tehran, Iran
E-mail: sharar.ahmadi@aut.ac.ir, msfallah@aut.ac.ir
Massoud Pourmahdian
Department of Mathematics and Computer Science
AmirKabir University of Technology (Tehran Polytechnic), Hafez Ave., Tehran, Iran
E-mail: pourmahd@ipm.ir
Overview paper
Keywords: epistemic logic, temporal epistemic logic, formal veriﬁcation, authentication protocol
Received: May 2, 2017
The authentication properties of a security protocol are speciﬁed based on the knowledge gained by the
principals that exchange messages with respect to the steps of that protocol. As there are many successful
attacks on authentication protocols, different formal systems, in particular epistemic and temporal epis-
temic logics, have been developed for analyzing such protocols. However, such logics may fail to detect
some attacks. To promote the speciﬁcation and veriﬁcation power of these logics, researchers may try to
construct them in such a way that they preserve some properties such as soundness, completeness, being
omniscience-free, or expressiveness. The aim of this paper is to provide an overview of the epistemic and
temporal epistemic logics which are applied in the analysis of authentication protocols to ﬁnd out how far
these logical properties may affect analyzing such protocols.
Povzetek: V preglednem prispevku je prestavljena epistemska in ˇ casovna epistemska logika overitvenega
postopka z namenom izboljšave delovanja.
1 Introduction
The principals communicating in a network need to be as-
sured that they are sending/receiving messages to/from the
intended principals as otherwise an attacker may imperson-
ate an authorized principal and gain access to conﬁdential
information. To prevent this, the principals use authenti-
cation protocols, which are built on cryptography, for ex-
changing messages [13]. Since there are many successful
attacks on authentication protocols [47, 60, 49, 35, 37, 33],
different formal sytems have been developed for analyzing
such protocols. Many of these systems are logical and are
known as logics of authentication [14, 8, 7, 36, 38].
The ﬁrst formal system designated for the speciﬁcation
and veriﬁcation of authentication protocols is an epistemic
logic - called BAN [14]. Although BAN can safely ver-
ify some protocols, it does not verify some other ones
successfully, e.g., it proved that the Needham-Schroeder
Public Key protocol (NSPK for short) was secure but
later it was shown that NSPK was vulnerable to man-
in-the-middle attack [46]. To promote the veriﬁcation
power of BAN, some extensions of it have been developed
[27, 3, 60, 62, 61, 17, 4]. Moreover, researchers have devel-
oped some other logics of authentication that are not BAN-
like, but are inherited from standard logics. Many of these
logics are epistemic and temporal epistemic ones that can
model different runs of a protocol or can be applied to in-
vestigate the knowledge acquired by principals at different
instants in protocol runs [16, 45, 50, 52, 8, 53]. For ex-
ample, a principal may ﬁnd out who originated a received
message at speciﬁc step of a protocol run and may agree
with the sender on the received information.
There are also dynamic epistemic logics that are useful
for modeling knowledge protocols, which model higher-
order information and uncertainties in terms of agents’
knowledge about each other. However, since these logics
are inconvenient in a cryptographic setting for generating
equivalence relations among messages, we do not consider
them in this paper [21].
Although the proposed epistemic and temporal epistemic
logics have signiﬁcantly improved the analysis of authen-
tication protocols, every now and then a problem is found
and we need to improve the logics to solve that problem.
For example, an attack may be detected by an omniscience-
free logic while it is ignored by another logic that is not
omniscience-free. Similarly, an authentication protocol can
be speciﬁed by a temporal epistemic logic while it can-
not be speciﬁed by a logic whose modalities are only epis-
162 Informatica 43 (2019) 161–175 S. Ahmadi et al.
temic ones. Such issues encourage researchers to ﬁnd out
if logics of authentication should preserve speciﬁc logical
properties. The properties that are usually discussed in this
context are soundness, completeness, expressiveness, and
being omniscience-free. Moreover, since a powerful at-
tacker is traditionally modeled as the well-known Dolev-
Yao message deduction system [24], it is valuable to see
if these logics can model such a system. In this way, if
a logic of authentication proves a security goal about an
authentication protocol, one can trust that the result is in-
deed valid in the presence of a powerful attacker who can
eavesdrop all communications, drop, manipulate and re-
play messages, and perform cryptographic operations using
his known keys and messages.
The aim of this paper is not to compare epistemic log-
ics of authentication to alternative security protocol analy-
sis, such as applied pi calculus and other process calculi,
strands, multiset and other forms of rewriting. The aim of
this paper is to provide an overview of the epistemic and
temporal epistemic logics of authentication to ﬁnd out how
far some of their logical properties such as soundness, com-
pleteness, being omniscience-free, and expressiveness may
affect analyzing authentication protocols. To do so, we dis-
cuss not only the conditions under which these logics sup-
port the Dolev-Yao message deduction, but also the logical
properties that encourage us to trust the derived judgements
about the authentication protocols.
The rest of the paper is as follows: In Section 2, we pro-
vide an overview of the notions of cryptography, Kripke
semantics, and epistemic logics of authentication. In Sec-
tion 3, we compare epistemic and temporal epistemic log-
ics of authentication and show how far some of their logical
properties may affect them in analyzing authentication pro-
tocols. Section 4 concludes the paper.
2 Basic notions
Authentication protocols are rules built on cryptographic
primitives that help principals authenticate each other while
communicating in a hostile environment [13]. An authen-
tication goal can be expressed in terms of a knowledge no-
tion, e.g., the sender authentication can be read as “the re-
ceiver knows the sender of a received message”. Consider
the NSPK protocol shown in Figure 1. Every principal in
this protocol has a public key and a private key such that
the public key of any principalA is known to everyone but
onlyA has the corresponding private key.
In this protocol, principalA generates a noncen
a
, pairs
n
a
with its name A, encrypts n
a
:A with principal B’s
public-keypk(B) so that onlyB can decrypt it by his pri-
vate key, and sendsfn
a
:Ag
pk(B)
to B. By receiving this
message, B decrypts it and sends n
a
back along with his
noncen
b
in an encrypted message so that onlyA can de-
crypt it. Then, A sends n
b
back to B. The goal of the
NSPK protocol is that both A and B can be assured that
they are talking to each other and not to an attacker. BAN
logic proved that the NSPK protocol was safe [14], whereas
Lowe showed that it was vulnerable to the man-in-the-
middle attack [46]. Although such a result seems confus-
ing, it is suggested by the well-known fact that the NSPK
protocol is safe assuming that no compliant initiator will
ever select a non-compliant responder for a session. Need-
ham and Schroeder assumed this fact about the principals.
However, it was certainly no longer a reasonable assump-
tion when cryptographic protocols were beginning to be
used on the open internet and Lowe outlined the man-in-
the-middle attack.
The man-in-the-middle attack, shown in Figure. 1, con-
sists of two interleaved sessions of the NSPK protocol. Af-
terA initiates a protocol run withI, the intruderI extracts
the message, impersonatesA, and sendsn
a
toB. WhenB
replies,I forwards this message toA and misusesA to ob-
tainn
b
. Then,I sendsn
b
back toB. Thus,B is deceived to
believe that he is talking toA while he is in fact communi-
cating withI. This attack shows that the result of analyzing
the NSPK protocol using BAN logic is questionable. Since
the original BAN did not have formal semantics, ﬁnding
such a semantics that could model the above attack became
an important topic of research.
As said earlier, the formal analysis of an authentication
protocol using epistemic logics depends on the knowledge
gained by the principals executing that protocol. There are
two main ways to formalize such knowledge. Assume the
statement: “B has sentm”, where the underlying semantics
of a logic of authentication interprets this statement as fol-
lows: “B is engaging in an event of a protocol sending mes-
sagem”. If we formalize this statement with a logical for-
mula  ,A knows  means: “A knows thatB has sentm".
This is called propositional knowledge which is implicit
and does not care about the details of computation [58].
There is also algorithmic knowledge formalizing the exact
models of principals’ knowledge such that if a principal
has some bit strings, he can apply cryptographic operators
to compute more strings using some predeﬁned algorithms
[30]. In this paper, we consider both of these knowledge
formalizations, but ﬁrst we need to explain some primitive
notions.
Assume that  is a set of principals exchanging messages
by executing an authentication protocol. We may use a log-
ical languageL to specify not only the steps of such a pro-
tocol, but also the intended authentication properties that
we want to prove about that protocol. To do so, we need to
formalize exchanged messages as message terms inL be-
cause protocols are a type of messages passing multi-agent
systems [26]. A message may be a plain termc or a com-
pound one constructed by encryption or pairing such that
fmg
k
is the encryption of messagem with the keyk and
m:m
0
is the pairing of messagesm andm
0
. There is a need
for a derivation system to derive new messages from known
ones using cryptographic functions. In this paper, we use
the well-known Dolev-Yao message deduction system [24]
as follows:m:m
0
is a message if and only if bothm andm
0
are messages. Iffmg
k
andk are messages, then so ism.
On the Properties of Epistemic. . . Informatica 43 (2019) 161–175 163
Figure 1: NSPK protocol and the man-in-the-middle attack
Finally, ifm andk are messages, then so isfmg
k
. Given a
set of message terms  and a ﬁnite set of Dolev-Yao mes-
sage deduction rules  , we say thatm is derivable from  if eitherm2   orm is derivable from  by applying the
rules in   . Assuming a set of message terms   , there are
two interpretations for knowledge.
The ﬁrst interpretation says that a principal i knows a
formula  if he is aware of  and  is true in all the worlds
he considers possible. In this case, a set of formulas, de-
noted byA
i
(w), is associated to every possible world w
such thati is aware of every formula inA
i
(w) [31]. The
intuition behind such an interpretation is that a principal
needs to be aware of a formula before he can know it. For
instance, a principali may be aware of an encrypted mes-
sagefmg
k
that he receives without being aware of message
m. In this way,i may know that he receivesfmg
k
if this
message holds in all the worlds that are possible to him
while he may not know that he receivesm. In the context
of verifying security protocols,A
i
(w) is implemented as
an algorithm that says "YES" for the formulas that agenti
is aware of in his local state inw. In this way, we say thati
knows  explicitly using algorithmic knowledge [45].
The second interpretation says that a principali knows a
formula  implicitly, shown by an epistemic formulaK
i
  ,
if i knows that   is true. The setF ofL-formulas then,
comprises not only atomic formulas about sending or re-
ceiving messages, but also compound formulas built induc-
tively as follows: For every ; 2F,i2   , andm2   ,
we have  ^ ,:  ,K
i
  , andA
i
  are inF.
The authentication protocols and goals formalized by
formulas inF need to be interpreted in a proper formal
semantics. Since an authentication protocol can be seen
as a multi-agent system and it is known that an interpreted
system
1
(IS for short) is a standard semantics for a multi-
1
Assume that  =fi
1
;:::;in;eg is a set of principals such that “e”
denotes a speciﬁc principal called the environment. For eachi2  , there
is a ﬁnite set L
i
of local states, a ﬁnite set a
i
of local actions, and a
local protocolp
i
: L
i
! 2
a
i
. The transition relationt
i
: L
i
  a
1
  :::  an ! L
i
is then deﬁned to return the next local state ofi after
all the principals perform their actions at the local state. Consider a set
of global states G   L
1
  :::Ln  Le , a set of joint actions a =
a
1
  :::  an  ae , a joint protocolp :
  p
1
;:::;pn;pe), and a global
transition relationt = (t
1
;:::;tn;te), which operates on global states
by composing all local and environmental transition relations. AnIS is
then a tuple
  G;I
0
;t;f 
i
g
i2A
;    , whereG is the set of all global states
accessible from any initial global state inI
0
via the transition relationt.
For eachi2   , there is an accessibility relation  i
  G  G such that
agent system, authentication protocols can be modeled by
interpreted systems too. This can build a foundation for
constructing Kripke semantics for epistemic logics of au-
thentication as follows [26].
A Kripke model of an epistemic logic of authentication
can reﬂect an authentication protocol. Such a model has a
set of possible worlds that can be deﬁned asW =R  N,
whereR is the set of all runs of that protocol andN is the
set of natural numbers. Thus, a pairhr;ni - called a point
- represents a runr at a time instantt. Such a point can be
associated to a set of formulas that hold (are true) in that
point. A Kripke model is then a tuple of the formM =
  W;f 
i
g
i2A
;    whereW is the set of all possible points
of the protocol. Moreover, the accessibility relation  i
can
be interpreted in different ways.
In one interpretation, for everyw
1
;w
2
2 W ,w
1
  i
w
2
holds if and only if the local states of a principali are the
same in w
1
and w
2
. For example, the local states of B
at the end of both runs of the NSPK protocol shown in
Figure. 1 are the same because B sends and receives the
same messages by completing the execution of these two
runs. In another interpretation, for every w
1
;w
2
2 W ,
w
1
  i
w
2
holds if and only if the local states of a princi-
pali are indistinguishable inw
1
andw
2
. For example, as-
sume that there is a protocol P such thatw
1
=hr
1
;t
1
i and
w
2
=hr
2
;t
2
i are two possible worlds of a Kripke model
that reﬂects P. PrincipalsA andB participate in two runs
of P, denoted byr
1
andr
2
, and formulasAsendsfmg
K
andAsendsfm
0
g
k
0 hold inw
1
andw
2
, respectively. As-
sume thatB does not know the proper decryption keys to
decrypt these messages, so he cannot distinguish formu-
lasAsendsfmg
K
andAsendsfm
0
g
k
0 because he sees
fmg
k
andfm
0
g
k
0 as two random messages. In this way,
he considers both of the formulas the same. If all of the
other formulas that hold inw
1
andw
2
are equal,B cannot
distinguish between w
1
and w
2
even iffmg
k
6=fm
0
g
k
0,
i.e., we have: w
1
  B
w
2
2
. In this model, K
i
  is true
atw2 W if  is true at everyw
0
2 W that is accessible
fromw inA’s view. Moreover,A
i
  is true inw2W if  can be computed by an awareness algorithmA
i
inw. Such
g  i
g
0
if and only ifl
i
(g) =l
i
(g
0
), wherel
i
:G!L
i
(g) returnsi’s
local state in the global stateg, and  :G  Atom!ftrue;falseg is
an interpretation function [26].
2
There are also some other interpretations for the accessibility relation.
We refer the interested reader to Ref. [17, 8].
164 Informatica 43 (2019) 161–175 S. Ahmadi et al.
an algorithm is deﬁned speciﬁcally for every protocol and
for computing intended formulas [30]. The truth of other
non-atomic formulas is deﬁned in a standard way and the
atomic formulas are interpreted by the interpretation func-
tion  [15].
Assume thatM =
  W;f 
i
g
i2A
;    is a Kripke model
that models a protocol P, andAuthR is an authentication
requirement formalized by a logical formula   . We say
that  is satisﬁable with respect toM when there is aw2
W such that   is true in w, i.e., AuthR holds in a run
of P that is associated to w. We say that   is valid with
respect toM if  is true in everyw2W i.e.AuthR holds
in all runs of P. We discuss authentication and formalizing
authentication in more detail below.
2.1 Formalizing authentication
Most of the security protocols have been designated for at-
taining authentication i.e. one principal should be assured
of the identity of another principal. A protocol designer
may assign different roles such as initiator, responder, or
server to principals. Authentication protocols can be clas-
siﬁed into two categories with respect to these roles: the
protocols that try to authenticate a responder B to an initia-
tor A, and the protocols that try to authenticate an initiator
A to a responder B.
The notion of authentication does not have a clear con-
sensus deﬁnition in the academic literature. However, the
most clear and hierarchical deﬁnition for authentication has
been devised by Lowe. In this deﬁnition, authentication
requirements depend on the use to which the security pro-
tocol is put. These requirements can then be classiﬁed as
aliveness, weak agreement, non-injective agreement, and
agreement [46]. A protocol guarantees to a principal A
“aliveness” of another principalB if the following condi-
tion holds: whenever the initiatorA completes a run of the
protocol, apparently with the responderB, thenB has pre-
viously been running the protocol. Aliveness can be ex-
tended to “weak agreement” ifB has previously been run-
ning the protocol with A. “Weak agreement" can be ex-
tended to non-injective agreement on a set of data items
(whereV is a set of free variables of the protocol) ifB has
previously been running the protocol withA,B was acting
as responder in his run, and the two principals agreed on
the values of all the variables inV . Weak agreement can
be extended to “agreement" if each such a run ofA corre-
sponds to a unique run ofB [46].
There are many attacks that occur due to parallel runs of
a protocol [47]. The deﬁnition of weak agreement for au-
thentication guarantees a one to one relationship between
the runs of two principals as follows: a protocol authen-
ticates a responder to an initiator, whenever a principalA
startsj runs of the protocol as an initiator andl runs as a
responder all in parallel; and completesk  j runs of the
protocol acting as initiator apparently with a responderB,
thenB has recently been runningk runs acting as respon-
der in parallel, apparently with A. Moreover, A protocol
authenticates an initiator to a responder, whenever a princi-
palB startsj runs of the protocol as a responder andl runs
as an initiator, all in parallel; and completesk  j runs of
the protocol acting as responder, apparently with initiator
A, thenA has recently been runningk runs acting as ini-
tiator in parallel, apparently withB [59]. In the following
example, we explain the deﬁnition of agreement in more
detail.
Example 2.1. Consider the following challenge-response
protocol that aims to authenticate an initiator A to a
responder B, and to authenticate a responder B to an
initiatorA. In this protocol,k
ab
is a shared key betweenA
andB. Moreover,n
a
andn
b
are two nonces generated by
A andB, respectively.
A!B :n
a
B!A :fn
a
g
k
ab
:n
b
A!B :fn
b
g
k
ab
There is the following reﬂection attack on the protocol
that consists of two sessions of the protocol executed in
parallel. In this attack,B has the responder role andI(A)
denotes an intruder who impersonatesA:
1:I(A)!B :n
a
2:B!I(A) :fn
a
g
k
ab
:n
b
1
0
:I(A)!B :n
b
2
0
:B!I(A) :fn
b
g
k
ab
:n
0
b
3:I(A)!B :fn
b
g
k
ab
B starts two runs of the protocol as a responder to A,
but it completes only one run (lines: 1, 2, and 3) withI(A)
whileA does not participate in these runs. So, the protocol
fails to aim the agreement requirement.
In the next example, we show how we can formalize an
authentication requirement.
Example 2.2. Consider the NSPK protocol, shown in Fig-
ure 1. We want to formalize the non-injective agreement
authentication requirement. To do so, we use epistemic
modalities as follows:
K
B
K
A
msgn
a
:n
b
This formula can be read as follows: “B knows thatA
knows the messagen
a
:n
b
". If this formula can be proven
for the NSPK protocol, then we say that the protocol guar-
antees “non-injective agreement” toB, wherefn
a
:n
b
g ap-
pears as the set of data items that the two principals agree
on their value. Since B encrypts n
b
with A’s public-key
and sendsfn
a
:n
b
g
pk(A)
toA, wheneverB receives a mes-
sage containing n
b
, he concludes that A has previously
been running the protocol with B because A is the only
principal who hasA’s private key to decryptfn
a
:n
b
g
pk(A)
in order to extract n
b
. The man-in-the-middle attack de-
ceives B to believe that he is talking to A while he is in
fact talking to I, who is an intruder. All BAN-like logics
On the Properties of Epistemic. . . Informatica 43 (2019) 161–175 165
proved the above formula for the NSPK protocol, whereas
an omniscience-free epistemic BAN-like logic, that is re-
ferred to WS5 throughout this paper, could identify this in-
sider attack [17]. In fact, being omniscience-free enabled
WS5 to model the Dolev-Yao message deduction properly.
We will explain this logic in detail at next sections.
3 Logical properties
In this section, we investigate how far some properties of
epistemic and temporal epistemic logics of authentication
may affect the analysis of authentication protocols. The
properties that we investigate are soundness, completeness,
being omniscience-free, and expressiveness.
3.1 Soundness and completeness
Beside syntax and semantics, every logic may have a proof
systemX consisting of some axioms and rules where the
axioms are valid with respect to the logic’s semantics and
the rules preserve validity i.e. if the premise of a rule is
valid, the result of it is also valid. LetX be a proof system
of a logic of authentication that is based on the Dolev-Yao
deduction system. Moreover, let the following statement be
an authentication property: “principals i and j know that
they are talking to each other”, wherei andj are engaging
only in one session and both peers has received certain mes-
sages as common knowledge to authenticate each other. In
this case, proving  inX means thati andj know that they
are indeed talking to each other even in an environment
where there are attackers who can derive messages due to
the Dolev-Yao deduction system.
The proof systemX may have some interesting proper-
ties, two of which are soundness and completeness:X is
sound if every derivable formula  inX is also valid.X is
complete if every valid formula  is provable inX . This is
also called “weak completeness” by some researchers [15].
Logical analysis of security protocols relies on formal mod-
els of cryptography where cryptographic operations and se-
curity properties are deﬁned as formal expressions. Such
models ignore the details of encryption and focus on an
abstract high-level speciﬁcation and analysis of a system
[1, 14, 24, 28].
Proving the soundness and completeness of a logic of au-
thentication gives a strong intuition that the formal seman-
tics of that logic is deﬁned properly and it is working as
expected. So, the logic can be applied safely in analyzing
authentication protocols. For formal veriﬁcation of a secu-
rity protocol, there is a need for a formal model to reﬂect
that protocol appropriately i.e. there is a need for a sound
formal model for that protocol. Using a logical model, the
veriﬁcation is then dependent on the following parameters:
ﬁrst, the protocol must be described in the language of the
logic. This description will be a part of a trust theory which
consists of correct and acceptable propositions used in de-
ducing security requirements. Even with a bad description
of a protocol and its initial assumptions, the logic should
consider all possible runs of that protocol.
To discuss the second parameter for deﬁning a sound for-
mal model, we ﬁrst provide an overview of the Dolev-Yao
indistinguishability relation. The intuitive idea for deﬁn-
ing this relation is the fact that two messages are indis-
tinguishable if any test - based on a limited set of opera-
tions on messages - gives the same result about the conﬁg-
uration of those messages. The Dolev-Yao indistinguisha-
bility relation can be related to cryptographic computing
models. In this case, a formal model is said to be com-
putationally sound. This is expressed for static equiva-
lence, which is a general form of indistinguishability, ex-
plicitly: two local states are static equivalents if they sat-
isfy the same equivalence tests. For a given theory of
equation, static equivalence is based on a computable ef-
ﬁcient set of operations such as symmetric and asymmet-
ric encryption and decryption. For example, consider the
simplest equivalence theory satisfying an equation of the
formdec(enc(m;pk);pr) = m, wherepk,pr, andm are
a public key, a private key, and a message, respectively.
Moreover, enc is an asymmetric encryption operator that
encrypts m with pk and dec is an asymmetric decryption
operator that decrypts an encrypted message withpr [2].
There is also another parameter for deﬁning a sound for-
mal model. Assume that there is a speciﬁcation of an au-
thentication protocolP and some initial assumptions using
a logic of authenticationL. We need to show whatever is
deduced inL aboutP should be consistent with what the
principals involved in executions ofP actually infer. As-
sume that   is a ﬁnite set of logical formulas including the
speciﬁcation of P and its initial assumptions. Moreover,
assume that the desired security goal is formalized by a
formula  that can be proven by applying the formuals in   and the axioms and rules ofL’s proof system. IfL is log-
ically sound andM is its model that satisﬁes the formulas
in   ,M also satisﬁes   . If we show thatM considers
all possible runs of P , including those that attackers may
participate in, the model reﬂectsP properly.
As said earlier, the other theorem that is usually inves-
tigated for every logic is completeness. All valid formu-
las of a complete logic are also provable in its proof sys-
tem. This motivates researchers to provide provers for the
analysis of security protocols [22, 52, 51, 29]. If such a
logic is also sound, the derived statements are more trusted
since completeness shows that the formal semantics work
as expected. Completeness may be a result of another prop-
erty. As an example, the completeness of BAN-like logics
has been an open problem for many years because some
of them do not have any formal semantics and some other
ones have inaccurate formal semantics. So, the logics could
not model some possible runs executed by a Dolev-Yao at-
tacker. However, it has been shown that the completeness
of BAN-like logics can be proven by presenting a formal
semantics that avoids logical omniscience [18]. We will
discuss logical omniscience in more details later.
There is also another line of research that proves com-
166 Informatica 43 (2019) 161–175 S. Ahmadi et al.
pleteness for monadic fragments of a ﬁrst-order temporal
epistemic logic with respect to their corresponding classes
of quantiﬁed interpreted systems. Such systems may have
the following typical properties: synchronicity, perfect re-
call, no learning, and unique initial state. In contrast to
most of the logics of authentication, such a logic has some
axioms and rules that explore the relationship between its
time and knowledge modalities [5, 6].
3.2 Logical omniscience
The semantics of a logic of authentication can be deﬁned
based on the standard Kripke structure. Such a semantics
may lead to the logical omniscience problem where princi-
pals know all logical truths i.e. they know all consequences
of what they know [31]. In fact, the problem bypasses the
limitations placed on the knowledge of a principal who re-
ceives an encrypted message but does not have the right
key to decrypt that message. Assume thatL is an epistemic
logic of authentication, which has a formal semantics built
on the standard Kripke structure, and   is a set of logical
formulas inL. Moreover, assume that a formula  can be
derived from   inL’s proof system and an agenti knows
all of the formulas in   . Then, the formal semantics ofL
leads to the logical omniscience wherei knows  . This fact
is an immediate result of the interpretation of the knowl-
edge modality ofL with respect to the underlying standard
Kripke semantics. In this way, a formulaK
i
  is true in a
state (possible world)w if and only if  is true in every state
that is indistinguishable (accessible) fromw ini’s view.
For example, assume that the following formula is true
in all possible runs of a protocol,
isentmsgfmg
k
!submsg(m)
wheresubmsg(m) is read asm is a sub-message i.e. m is
a sub-message offmg
k
. Using the standard Kripke seman-
tics and for every principalj, the following formula is also
true in all runs of that protocol:
K
j
isentmsgfmg
k
!K
j
submsg(m)
Now, assume that the anonymity ofi fails and the formula
K
j
isentmsgfmg
k
is valid. Therefore,K
j
submsg(m)
can be deduced by applying modus ponens. But in fact,
this judgment is true only if j knows the symmetric key
k to decryptfmg
k
. Thus, logical omniscience should be
avoided in order to restrict principals’ knowledge to what
they can compute from their known facts, messages, and
keys.
There are different approaches for solving the logical
omniscience problem in the analysis of security protocols.
In Ref. [19], the problem is solved by presenting a gen-
eralized Kripke semantics based on a permutation-based
IS. Such a semantics results in a weakened necessitation
rule for a logic faithful to BAN. Hence the logic becomes
an omniscience-free weakened S5. Such a logic formal-
izes an implicit form of knowledge that results in abstract
high-level reasoning of security protocols [17]. The logical
omniscience problem can also be avoided by exact mod-
els of knowledge that a principal acquires during protocol
runs. For example, such models are applied by a logic -
called TDL [45]. So, a part of the logic that links epistemic
modalities to awareness algorithms becomes omniscience-
free. In this way, a principal knows a fact if he is aware of
that fact. The idea of using awareness algorithms in formal
security was originated in Ref. [30]. We will talk about the
logics that use such algorithms at the end of this section.
3.3 Expressiveness
Epistemic logics of authentication usually have three dif-
ferent operators besides the standard ones of propositional
logics. These operators are temporal, epistemic, and aware-
ness. Hybrid systems may also have some other operators
such as type operators or algebraic operators, but we do not
consider hybrid systems in this paper and refer the inter-
ested reader to Ref. [39]. Temporal modalities formalize
precedence of actions, time intervals, etc., such as “next”
and “in a time interval [t
1
;t
2
]". Epistemic modalities for-
malize the knowledge of principals. Awareness operators
show the algorithms that principals use to become aware of
facts. The expressiveness of epistemic logics of authentica-
tion relies on their logical order and modalities. Moreover,
if a logic has temporal operators, its expressiveness also re-
lies on the method that the epistemic core is augmented by
temporal modalities.
There are three approaches for adding temporal modali-
ties to an epistemic core of a logic of authentication. The
ﬁrst approach, which makes the resulting temporal epis-
temic logic very expressive, is the fusion approach where
epistemic and temporal modalities may appear in each
other’s scope without any restrictions. Moreover, the re-
sulting logic may have axioms and rules that explore inter-
actions between time and knowledge [5, 8, 23, 4]. This
approach has been used in developing logics applied in
analyzing a wide range of security protocols. Two ex-
amples of these protocols are classical authentication pro-
tocols such as NSPK and stream authentication protocols
such as TESLA [57], which is used for sending streams of
messages: videos, audios, etc.
The second approach is to use ﬁbring technique where
temporal and epistemic modalities may appear in each
other’s scope without any restrictions. But, the time and
knowledge dimensions of a ﬁbred logic are orthogonal. So,
such a logic has no axioms and rules to explore the rela-
tionship between time and knowledge. Fibring technique
does not model the knowledge which is obtained as a con-
sequence of a particular event. Thus, a ﬁbred logic is less
intuitive for modeling security protocols and less expres-
sive in comparison with other logics built on the fusion ap-
proach. However, theorems such as soundness and com-
pleteness may be easily proven for a ﬁbred logic if its con-
stituent logics are sound and complete. Moreover, a prover
can be easily constructed for a ﬁbred logic if its constituent
logics have provers. Such a logic has been developed for
On the Properties of Epistemic. . . Informatica 43 (2019) 161–175 167
the analysis of the TESLA protocol [56].
Finally, the last approach for adding temporal modalities
to an epistemic core of a logic of authentication is using the
temporalization technique. This technique operates in a hi-
erarchical way such that the temporal modalities can never
appear in the scope of epistemic modalities i.e. the result-
ing logic does not have any formula of the formK
i
    ,
which can be read as follows: agent i knows that at the
next step  holds. This approach has been used for verify-
ing different protocols such as TESLA and WMF [53, 52].
In Figure 2, we compare some important epistemic and
temporal epistemic logics of authentication against the
above properties where every row of the ﬁgure is dedicated
to a speciﬁc logic. The 1
st
column of each row shows
the logic name. The 2
nd
column shows if the logic or-
der is “propositional” or “ﬁrst-order”, denoted by “PR” and
“FO”, respectively. The 3
rd
column shows the type of op-
erators used in the logic where “E”, “A”, and “T” denote
“epistemic”, “awareness”, and “temporal”, in order. The
4
th
column shows if the logic has a proof system, model
checker, tableau:::. The 5–7
th
columns show if the logic
is sound, complete, or omniscience-free, respectively. If a
logic is sound, complete, or omniscience-free, we show this
by a “X” symbol. If any of these properties does not hold,
we show this by a “  ” symbol. If a logic does not have a
proof system, it has no soundness and completeness theo-
rems. In this case, we use a “  ” symbol. Finally in the last
column, “EXP ” denotes that the explicit part of the logic
is omniscience-free. Some of the security protocols ana-
lyzed by these logics are shown in Figure 3. The attacker
models of these logics are also summarized in Figure 4.
In what follows, we explain the above logical properties in
more detail.
3.4 Inside the logics
In 1989 BAN logic was proposed as the ﬁrst formal sys-
tem for the speciﬁcation and veriﬁcation of authentication
protocols [14]. This is a simple intuitive propositional epis-
temic logic named after its developers Burrows, Abadi, and
Needham. The syntax of BAN consists of inference rules
about principals’ beliefs and their actions. This syntax en-
ables BAN not only to specify the steps of an authentica-
tion protocol and its security goals, but also to derive the
intended goals about that protocol. The ﬁrst step of ap-
plying BAN is to idealize a protocol into an abstraction. In
the second step, one should translate the initial assumptions
and the security goals into BAN language, relate each ide-
alized step of the protocol to a BAN formula, and then use
BAN inference rules to derive intended goals.
The soundness and completeness theorems cannot be
proven for BAN because it has no formal semantics. This
logic has only epistemic modalities and it is not expressive
enough to specify or verify highly time-dependent proto-
cols such as stream authentication protocols [29]. This,
along with BAN’s propositional order, results in its low
speciﬁcation power. BAN has no formal attacker model
but the capabilities of attackers are somehow embedded in
its proof system.
For example, BAN has a rule - called the message-
meaning rule - which has two premises. Assume that
P and Q are two agents, m is a message, k is a key,
andfmg
k
denotes that m is encrypted with k. The ﬁrst
premise of this rule says that P believes thatk is a shared
key between P and Q. This is formalized as follows:
P BelievesP$
k
Q. The second premise says that some-
one has sent a message which containsfmg
k
toP . This is
shown as follows: P seesfmg
k
. The conclusion of this
rule is thatP believes that at some timeQ sent a message
which containsm. This is formalized by the following for-
mula: P Believes Q saidfmg
k
. As k is a shared key
betweenP andQ, only these two agents can usek to en-
cryptm and no other agent can createfmg
k
. Thus, when
P receivesfmg
k
it concludes that at some timeQ has sent
a message which containsfmg
k
. In this way, even if an
attacker has sent a message containingfmg
k
toP ,P be-
lieves that this message has not been originated byQ [14].
As an example of formalizing authentication in BAN, we
say that authentication is complete for the NSPK protocol
if there are noncesn
a
andn
b
, generated byA andB, re-
spectively, such that the following statements hold:
ABelievesA$
na:n
b
B
BBelievesA$
na:n
b
B.
The above formalizations can be classiﬁed as non-
injective agreement. However, other weaker formalizations
can be presented too.
As said earlier, BAN has some problems while verify-
ing authentication protocols. Many extensions of this logic
have been developed to resolve its problems. One of these
extensions is GNY developed in 1990 for verifying a wider
range of authentication protocols. GNY emphasizes sepa-
rating the content and meaning of messages while it follows
the same method as BAN for formalizing authentication.
This logic is named after its developers Gong, Needham,
and Yahalom. Although GNY can be applied in verifying
a sample voting protocol successfully, the logic still suf-
fers the same problems as its predecessor. Neither BAN
nor GNY preserves the properties discussed in Subsections
3.1, 3.2, and 3.3. Thus, their derivations are not trustwor-
thy. Moreover, these logics cannot analyze highly time-
dependent protocols such as the TESLA protocol.
The ﬁrst attempt for developing a formal semantics for
BAN was in 1991 when Abadi and Tuttle improved the syn-
tax and inference rules of BAN and also presented a formal
semantics - called AT - for BAN [3]. This semantics is
based on the standard Kripke structure constructed from
interpreted systems. In this model, a principal i knows a
formula  if we have: “i knows  ” is true at a pointhr;ki
if it is true in every pointhr
0
;k
0
i that is indistinguishable
fromhr;ki ini’s view. This extension of BAN - called AT
logic - is sound with respect to the AT semantics. Thus,
the proofs in this logic are more trustworthy. However, the
completeness of AT remained an open problem for years
168 Informatica 43 (2019) 161–175 S. Ahmadi et al.
Figure 2: Some Logics Applied in Analyzing Authentication Protocols
Figure 3: Some Protocols Analyzed by The Logics in Figure 2
due to the logical omniscience problem, which was an im-
mediate consequence of its standard Kripke semantics [19].
Because of the logical omniscience problem, the logic by-
passes the principals’ restricted knowledge. Thus, AT is
not enough for modeling different runs of a protocol. This
logic follows BAN’s method for formalizing security prop-
erties. However, it can also formalize such properties at
speciﬁc points of protocol runs. For example, we may want
to verify whether a formula such asP $
k
Q is true at a
speciﬁc pointhr;ti of a protocol run or not.
The correctness of a security protocol highly depends
on the evolving knowledge of principals communicating
through the protocol steps while time is passing. In 1993,
Syverson added temporal operators to BAN for the ﬁrst
time. We call this logic TBAN throughout this paper [60].
TBAN could verify a key distribution protocol that the pre-
vious BAN-like logics could not because they lacked tem-
poral modalities and ignored a casual consistency attack on
the protocol. TBAN is sound with respect to the AT seman-
tics. Moreover, it is able to formalize temporal modalities
and statements. Thus, the speciﬁcation power of TBAN is
more than its predecessors. This logic was a starting point
in using both temporal and epistemic modalities for ana-
lyzing authentication protocols and later many other logics
followed this approach [53, 4, 23, 22, 52, 56, 8]. For exam-
ple, we can formalize authentication for NSPK as follows
where the symbol2 is read as “always":
2ABelievesA$
na:n
b
B
2BBelievesA$
na:n
b
B.
Although TBAN is more expressive than its prede-
cessors, it cannot analyze such protocols as M-TESLA,
Mix, and Dual Signature protocols [4, 17] since it is not
omniscience-free.
Contemporary to TBAN, van Oorschot followed another
line of research and extended BAN to facilitate the veriﬁ-
cation of key agreement protocols [62]. The extended logic
was named VO. Although BAN, GNY , and VO have proof
On the Properties of Epistemic. . . Informatica 43 (2019) 161–175 169
Figure 4: The Attacker Model of The Logics in Figure 2
systems, we cannot analyze their soundness or complete-
ness because they lack formal semantics. All of these BAN
extensions were uniﬁed into a sound logic - called SVO
[61] - whose axioms and rules were simpliﬁed. The com-
pleteness of BAN was ﬁnally proven in 2007 when a proper
proof system and formal semantics were provided for this
logic. GNY , AT, VO, and SVO have no formal attacker
model, but the capabilities of the attacker are somehow em-
bedded in the proof system. So, the attacker model of these
logics is similar to that of BAN.
In 2005, it was shown that the AT semantics could not
identify some possible attacks because of the logical om-
niscience problem. To solve this problem, Cohen and
Dam provided a generalized Kripke semantics for BAN
such that BAN’s soundness, completeness, and decidabil-
ity were proven [19, 18]. Using this semantics, BAN can
be embedded into an S5 logic where some speciﬁc message
permutations are deﬁned over messages. In this way, a for-
mulaK
i
  is true in a possible worldw if for every possible
worldw
0
of the model which is indistinguishable fromw in
i’s view and with respect to a message permutation  ,  (  )
is true inw
0
. The formula  (  ) is the one in which every
messagem is replaced by  (m) [19].
Such a generalized Kripke semantics results in a weak
necessitation rule for BAN. In this way, the application of
a weak necessitation rule along with axiom K does not lead
to logical omniscience in the derivations. So, the under-
lying semantics restricts the knowledge gained by an at-
tacker. We call this logic Weakened S5 - WS5 for short -
throughout the paper. WS5 can be extended by ﬁrst-order
quantiﬁers. The resulting logic is a sound and complete
ﬁrst-order logic [20], denoted by FOWS5 in this paper. It
is shown that these logics can safely specify and verify the
Mix protocol since they are omniscience-free. However,
they do not have temporal modalities to analyze such pro-
tocols as stream authentication.
WS5 can also be extended by temporal modalities. The
resulting logic is called TWS5. This logic successfully
veriﬁes a modiﬁed TESLA protocol - called M-TESLA -
which cannot be analyzed by the previous temporal epis-
temic logics that are not omniscience-free [4]. However,
these logics make use of message permutation functions,
170 Informatica 43 (2019) 161–175 S. Ahmadi et al.
which cause exponential run time [39]. Although WS5 and
its extensions are sound, complete, and omniscience-free,
the expressiveness of WS5 is less than its extensions since
it is propositional and does not have temporal modalities.
WS5, FWS5, and TWS5 use different symbols to for-
malize security properties. While WS5 can use epistemic
modalities, FWS5 and TWS5 can make use of quantiﬁers
and temporal modalities along with epistemic modalities,
respectively. As an example, assume that we want to for-
malize a message sending axiom in TESLA which says that
if the senderS sends a messageM to the receiverR, then
R may receive this message in time interval [u, v] [4]. This
can be done as follows wherenext
u
denotesu clock ticks
later:
S sends M ! (  u
R receives M) _ ::: _
(  v
RreceivesM).
It is proven that the underlying generalized Kripke se-
mantics of WS5 restricts knowledge gained by an attacker
because the message permutation functions make the logic
omniscience-free. In fact, it is shown that the Dolev-Yao
deduction system reﬂects the semantics of WS5 implicitly
because such a semantics considers all of the possible runs
of a protocol in the formal model by applying the permuta-
tion functions on messages even those runs executed by a
Dolev-Yao attacker [17, 4].
There are also many standard logics that were not origi-
nally developed for analyzing authentication protocols, but
they are well adapted to this purpose. One of these log-
ics is L
KX
n
proposed by Halpern and Pucella in 2003 [30].
This logic uses two kinds of knowledge: implicit knowl-
edge which is similar to that of BAN-like logics and ex-
plicit knowledge which links to some knowledge algo-
rithms. The attacker model is deﬁned based on the explicit
knowledge in L
KX
n
. In fact, L
KX
n
deﬁnes attackers as the
Dolev-Yao deduction system explicitly using a Dolev-Yao
knowledge algorithm. We refer the interested reader to Ref.
[30] to review the full algorithm.
Explicit knowledge prevents logical omniscience. Thus,
attackers infer the statements that they can compute. It
has been proven that algorithmic knowledge can model
the Dolev-Yao deduction system. This model is a useful
abstraction because it does not consider the cryptosystem
used in the protocol and it can easily capture probability
for guessing appropriate keys. L
KX
n
does not have a proof
system. Thus, it does not have soundness and completeness
theorems. However, a proof system may also be developed
for it. This logic is ﬂexible and modular. Moreover, it can
be extended with probabilities to guess keys [25, 32] ac-
cording to Lowe’s model for guessing attacks [49]. L
KX
n
cannot verify highly time-dependent protocols because it
has no temporal modalities. This logic also uses implicit
knowledge to model principals’ beliefs about what is hap-
pening during a protocol run.
Lomuscio and Wozan followed the same approach to de-
velop a temporal epistemic logic called TDL for the speciﬁ-
cation and veriﬁcation of TESLA [45]. The logic not only
has traditional knowledge modalities but also has aware-
ness operators to represent explicit knowledge. Thus, a part
of TDL that links to explicit knowledge is omniscience-
free. The logic deﬁnes attackers as the Dolev-Yao deduc-
tion system explicitly. This is formalized through a deriva-
tion relation that shows how an attacker can extract a mes-
sage from a set of received messages and keys using admis-
sible operations. As an example, there is a derivation rule
as follows: if an agent i derives m:m
0
using the Dolev-
Yao knowledge algorithm, denoted by an awareness oper-
atorA
DY
i
,i can also derivem using this algorithm. TDL
has a computationally-grounded semantics. Moreover, it is
intuitive, sound, complete, and decidable. TDL has a high
speciﬁcation power because it is a ﬁrst-order modal logic
that has three types of modalities: epistemic, awareness,
and temporal.
In 2004, Dixon, Fernandez Gago, Fisher, and van der
Hoek introduced a ﬁrst-order temporal logic of knowledge
- called KL
n
- for the speciﬁcation and veriﬁcation of au-
thentication protocols and veriﬁed NSPK as a case study
[23]. This logic is useful for reasoning about the evolving
knowledge of a principal over time. Especially, this is im-
portant if we want to be sure that a principal obtains certain
knowledge at a time instant. KL
n
is a fusion of a linear time
temporal logic and a multi modal epistemic logic S5. Thus,
the logic is powerful enough to specify agents’ capabili-
ties explicitly by logical formulas. As an example of using
quantiﬁers and modalities of KL
n
for formalizing security
requirements, consider the NSPK protocol as shown in Fig-
ure 1. Assuming that the predicatevalue  nonce(N;V )
of the logic indicates that the value of nonce N is V , we
want to show that every other principal, other thanA and
B, who are running the protocol can never know the value
ofA’s nonce. This is formalized as follows:
8V 2:K
C
value  nonce(N
a
;V )
where2 andK
C
are two modalities of KL
n
that are inter-
preted as “always" and “agent C knows", respectively.
To prove a security goal  from protocol speciﬁcation ,
where both  and are formulas in KL
n
, we must prove
 !   . To do so, a resolution method is applied which
is in fact a refutation system showing that ^:  is not
satisﬁable. A prototype theorem prover has been developed
for a single modal version of temporal logics of knowledge
but the developers insisted on a need to develop a more
powerful prover to deal with the multi-modal case in order
to prove theorems automatically [23].
Contemporary to KL
n
, Liu, Ozols, and Orgun devel-
oped the TML+ logic for analyzing authentication proto-
cols [41]. The logic uses the temporalization technique to
combine an epistemic logic - called TML - with a simple
linear-time temporal logic - called SLTL. This technique
allows adding SLTL to TML in a hierarchical way such
that the temporal operators can never appear in the scope of
epistemic ones. TML+ can be applied for the veriﬁcation of
time-dependent properties of security protocols. To do so,
a trust theory for a protocol that is to be veriﬁed is provided.
The theory consists of TML+ axioms and rules along with
On the Properties of Epistemic. . . Informatica 43 (2019) 161–175 171
a speciﬁcation of the protocol and initial assumptions in
the form of TML+ formulas. Then, the theory is applied to
drive security goals. TML+ is sound and complete, yet it
is not omniscience-free. However, the logic assumes that
an attacker cannot decrypt an encrypted message if he does
not have the right key for decryption.
In 2007, a tableau system was developed for TML+
[51]. This was used for verifying both static and dy-
namic aspects of some protocols such as WMF, Needham-
Schroeder symmetric key, and Kerbros. The developers
proved the soundness and completeness of the labelled
tableau calculus based on the soundness and complete-
ness results of the constituent logics of TML+. Then, they
sketched a resolution-type proof procedure and proposed a
model checking algorithm for TML+ [51].
In 2006, Orgun, Ji, Chuchang, and Governatori con-
structed the FL logic for analyzing stream authentication
protocols from TML and SLTL using the ﬁbring technique
[56]. In this way, FL is sound and complete with respect to
its ﬁbered model because its constituent logics are proven
to be sound and complete [40, 34]. The original idea of
the ﬁbring technique is based on the assumption that both
constituent logics are endowed with point-based semantics
so that a model of the ﬁbred logic is a point-based seman-
tics and every point of the ﬁbred model is closely related
to a point in a model of each constituent logic. Thus, a
model of a ﬁbred logic can be related to several models in
each of the constituent logics. As a consequence, a ﬁbred
logic preserves the theorems proven for its original logics
[42]. The FL ﬁbred model is such that the formulas of FL
may contain any number of temporal and belief operators
without any restrictions. Any formula whose main opera-
tor is a temporal modality, is interpreted by referring to the
SLTL semantics and any formula whose main operator is
a belief modality, is interpreted by referring to the Kripke
semantics of TML.
The ﬁbring technique also allows developing proof pro-
cedures from the constituent logics since the time and
knowledge dimensions of FL are orthogonal[29]. In 2008,
a modal tableau was developed for FL[29] by adapting
KEM, a modal tableau system, showing how combinations
of multi-modal logics can provide an effective tool for ver-
ifying the TESLA protocol. It has been proven that the
adapted KEM is sound and complete for SLTL and TML.
As a result of the ﬁbring technique, these theorems have
also been proven for FL. KEM can be used to automatically
check for formal properties of security protocols [29].
The logic FL is more expressive than a temporalised be-
lief logic such as TML+ [52] because temporal and belief
modalities may appear in each other’s domains. This logic
is ﬂexible because of its modular nature and it has a high
speciﬁcation power since it is a ﬁrst-order logic making use
of temporal and knowledge modalities. However, it is not
omniscience-free because of the standard Kripke seman-
tics of its belief aspect. In 2012, Ma et al. constructed
a temporalized belief logic - called TBL [53] - that was
less expressive than FL because of using the temporaliza-
tion technique. However, it was appllied in verifying the
TESLA protocol successfully. TBL is sound and complete,
yet it is not omniscience-free. This logic follows FL to de-
ﬁne the attacker’s capabilities where they are deﬁned simi-
lar to the Dolev-Yao model. However, neither of these two
logics prove if they can model such attackers.
In 2009, Boureanu, Cohen, and Lomuscio presented an
effective fully automatic approach for analyzing security
protocols in the presence of the Dolev-Yao attackers. This
approach makes use of a temporal epistemic logic, called
CTLK [8]. The ﬁrst step is to specify a security proto-
col in CAPSL [54], which is a high-level speciﬁcation lan-
guage formally describing protocols. Then, the speciﬁca-
tions of the security protocol and security goals in CAPSL
are translated by an automatic compiler into an ISPL (In-
terpreted Systems Programming Language), which is a set
of CTLK speciﬁcations to be checked. The result of this
translation is a ﬁle that a MCMAS model checker
3
takes as
input and checks whether or not the security goals are sat-
isﬁed by the protocol. In most cases, this gives a counter-
model if they are not satisﬁed by the protocol. The main
contribution is a compiler from protocol descriptions given
in CAPSL into ISPL, the input language for MCMAS. The
translation is optimised to limit the state explosion and
beneﬁt from MCMAS’s various optimisations. To do so,
the authors developed PD2IS (Protocol Descriptions to In-
terpreted Systems), an automatic compiler from CAPSL
protocol descriptions to ISPL programs. This veriﬁcation
method assumes a bounded number of concurrent protocol
sessions instantiated to run concurrently [8].
This CTLK approach makes use of the consistent mes-
sage permutations introduced in Ref. [19] through a smart
translation of security goals into CTLK formulas in order
to prevent bad effects of the logical omniscience. However,
CTLK is not omniscience-free. The approach models the
Dolev-Yao attacker explicitly as an environment which has
the capabilities of honest principals, can eavesdrop all com-
munications, compose and replay messages into any proto-
col session, and perform cryptographic operators using his
known keys. The attacker also has an identity and pub-
lic and private keys that may be used to communicate with
other principals and record their send actions. To avoid the
state-explosion problem while model checking, MCMAS
employs a ﬁxed limited number of interleaved sessions.
Moreover, it is assumed that the veriﬁcation process does
not support all types of nesting while encrypting messages
and the messages are of ﬁnite-length. These assumptions
are applied because an attack to a protocol may be usually
found in a small run of the protocol consisting of only a
few sessions [48].
No proof system has been presented for the CTLK logic
yet. So, this logic does not have any proven soundness and
completeness theorems [8]. However, one can develop a
proof system with respect to the underlying semantics of
CTLK and check if the logic is sound and complete accord-
3
This is a BDD-based model checker for multi-agent systems support-
ing temporal-epistemic speciﬁcations [43]
172 Informatica 43 (2019) 161–175 S. Ahmadi et al.
ing to that proof system. CTLK is powerful and ﬂexible
enough to be extended. As a variant of this logic, CTLS5
n
has been developed to model-check detectability of attacks
in multi-agent systems that are automatically generated for
security protocols [9]. As another extension of CTLK,
CTLKR has been developed for the analysis of an e-voting
protocol - called Foo - with a passive attacker model who
can link the receipt-providing principal and its vote [10].
Finally, ICTLK [12] has been developed for analyzing an
unbounded number of concurrent protocol sessions. These
extensions of CTLK use the same tools for verifying secu-
rity protocols automatically. Contemporary to CTLK, Luo
et al. provided a temporal epistemic logic - called ECKLn
- that was applied in verifying the NSPK protocol using
model checking techniques similarly. To do so, the authors
implemented and automatically veriﬁed security protocols
in a model checker for multiagent systems [9].
4 Conclusions
One of the main approaches for formal analysis of authen-
tication protocols is using epistemic or temporal epistemic
logics. The semantics of such logics should be able to
model the protocol runs, including those executed by at-
tackers. Then, theorem provers or model checkers are built
on these logics to analyze the protocols against intended
properties. Comparing the logics in Figure 2, it seems that
WS5 and its extensions are the best choices for protocol
analysis since they are sound, complete, and omniscience-
free. However, Figures 3 and 4 show that CTLK and its
extensions are very powerful in security protocol analysis,
make use of automatic compilers and model checkers, and
prevent bad effects of logical omniscience while modeling
the Dolev-Yao message deduction.
It has been shown that it is an undecidable problem to
ﬁnd whether a security protocol is indeed secure or not
[55]. Thus, it is practical to use trusted security protocols
analyzed by different formal methods to provide fast solu-
tions for existing problems of real life systems. At the same
time, it is practical to move toward the best formal system
for verifying authentication protocols. A good measure for
ﬁnding such a formal system for security protocol analysis
is to prove that it can model the Dolev-Yao message deduc-
tion. In this line, we investigated the epistemic and tempo-
ral epistemic logics and showed how far their properties
such as soundness, completeness, being omniscience-free,
and expressiveness may affect the analysis of authentica-
tion protocols. Some of these logics have no proof sys-
tem, thus they have no soundness or completeness theo-
rems. However, they may apply model checkers for analy-
sis and use awareness algorithms for preventing the logical
omniscience problem while modeling the Dolev-Yao mes-
sage deduction explicitly [30, 45, 8]. Preventing the logi-
cal omniscience or avoiding its bad effects restricts a prin-
cipal’s knowledge to what he can compute or derive with
his known keys and messages. Some other epistemic log-
ics have proof systems, are omniscience-free, and model
the attacker capabilities implicitly [19, 20, 4]. If such log-
ics are logically sound, their derived judgments are more
trustworthy. If they are complete, they may make use of
automatic provers.
Comparing Figures 2 and 4, the epistemic logics
modeling the Dolev-Yao message deduction are either
omniscience-free or prevent the bad effects of omniscience.
In fact, provers are usually built on logics that preserve
properties such as soundness, completeness, and being
omniscience-free so that one can trust their output. At the
same time, model checkers deal with the state explosion
problem by imposing some assumptions so that they can
verify security protocols within an acceptable time. How-
ever, such assumptions may not stop us from using model
checkers since they cover a wide range of security proto-
cols and use existing tools. Finally, the expressiveness of
such logics makes them powerful enough to both formal-
ize attacker’s capabilities by logical formulas and analyze
different classes of authentication protocols. Speciﬁcally, if
the logic has both temporal and epistemic modalities, it can
analyze highly time-dependent protocols such as stream
authentication protocols.
Although it has been shown that logics using algorith-
mic knowledge can model the Dolev-Yao message deduc-
tive explicitly [30], to the best of our knowledge it has not
been proven if a temporal epistemic logic of authentication
can model such an attacker implicitly using permutation-
based generalized Kripke semantics. This can be a topic for
further research. As seen in this paper, all of the logics that
model the attacker capabilities implicitly are omniscience-
free. Thus, this can be a starting point for this topic of re-
search. Finally, it would be beneﬁcial if such an overview
extends to the use of epistemic and temporal epistemic log-
ics in analyzing other security/privacy properties.
References
[1] M. Abadi and A.D. Gordon (1999) A calculus for
cryptographic protocols: The spi calculus, Infor-
mation and computation, Elsevier, 148(1): 1–70.
https://doi.org/10.1006/inco.1998.
2740
[2] M. Abadi and P. Rogaway (2002) Reconciling two
views of cryptography (the computational sound-
ness of formal encryption), Journal of cryptol-
ogy, Springer, 15(2): 103–127. http://dx.doi.
org/10.1007/s00145-007-0203-0
[3] M. Abadi and M.R. Tuttle (1991), A semantics for
a logic of authentication, Proceedings of the tenth
annual ACM symposium on Principles of distributed
computing, ACM, 201–216. https://doi.org/
10.1145/112600.112618
[4] S. Ahmadi and M.S. Fallah (2018) An Omniscience-
Free Temporal Logic of Knowledge for Verify-
On the Properties of Epistemic. . . Informatica 43 (2019) 161–175 173
ing Authentication Protocols, Bulletin of the Ira-
nian Mathematical Society, Springer, 44(5): 1–23.
https://doi.org/10.1007/s41980-018-0087-9
[5] F. Belardinelli and A. Lomuscio (2010) Interactions
between time and knowledge in a ﬁrst-order logic for
multi-agent systems, Proceedings of the Twelfth In-
ternational Conference on the Principles of Knowl-
edge Representation and Reasoning, AAAI Press,
38–48.
[6] F. Belardinelli and A. Lomuscio (2012) Interactions
between time and knowledge in a ﬁrst-order logic for
multi-agent systems: completeness results, Journal of
Artiﬁcial Intelligence Research, AI Access Founda-
tion, 1–45. https://doi.org/10.1613/jair.3547
[7] B. Blanchet, B. Smyth, and V . Cheval (2015) ProVerif
1.90: Automatic Cryptographic Protocol Veriﬁer,
User Manual and Tutorial.
[8] , I. Boureanu, M. Cohen, and A. Lomuscio (2009)
Automatic veriﬁcation of temporal-epistemic proper-
ties of cryptographic protocols, Journal of Applied
Non-Classical Logics, Taylor & Francis, 19(4): 463–
487. https://doi.org/10.3166/jancl.19.463-487
[9] I. Boureanu, M. Cohen, and A. Lomuscio (2010)
Model checking detectability of attacks in multiagent
systems, Proceedings of the 9th International Confer-
ence on Autonomous Agents and Multiagent Systems,
International Foundation for Autonomous Agents and
Multiagent Systems, 1: 691–698.
[10] I. Boureanu, A.V . Jones, and A. Lomuscio (2012)
Automatic veriﬁcation of epistemic speciﬁcations un-
der convergent equational theories, Proceedings of
the 11th International Conference on Autonomous
Agents and Multiagent Systems-Volume 2, Interna-
tional Foundation for Autonomous Agents and Mul-
tiagent Systems, 1141–1148.
[11] I. Boureanu, P. Kouvaros, and A. Lomuscio (2016)
MCMAS-S- An experimental model checker or
the veriﬁcation of security properties in unbounded
multi-agent systems. https://vas.doc.ic.
ac.uk/software/mcmas-extensions/
[12] I. Boureanu, P. Kouvaros, and A. Lomuscio (2016)
Verifying Security Properties in Unbounded Multia-
gent Systems, Proceedings of the 2016 International
Conference on Autonomous Agents & Multiagent
Systems, International Foundation for Autonomous
Agents and Multiagent Systems,1209–1217.
[13] C. Boyd and A. Mathuria (2013)Protocols for authen-
tication and key establishment, Springer Science &
Business Media, 2013. https://doi.org/10.
1007/978-3-662-09527-0
[14] M. Burrows, M. Abadi, and R.M. Needham (1989) A
logic of authentication, Proceedings of the Royal So-
ciety of London A: Mathematical, Physical and En-
gineering Sciences, The Royal Society, 426(1871):
233–271.
[15] C.C. Chang and H.J. Keisler (1990) Model theory,
North Holland, 73.
[16] L. Chao, L. Hui, and M. Jianfeng (2009) Analy-
sis the Properties of TLS Based on Temporal Logic
of Knowledge, Proceedings of the 5th International
Conference on Information Assurance and Security,
IEEE, 2: 19–22.https://doi.org/10.1109/
ias.2009.49
[17] M. Cohen (2007) Logics of Knowledge and Cryptog-
raphy: Completeness and Expressiveness, PhD The-
sis, KTH, Stockholm, Sweden.
[18] M. Cohen and M. Dam (2005) A completeness result
for BAN logic, Prococeedings of Methods for Modal-
ities, 4.
[19] M. Cohen and M. Dam (2005) Logical omniscience in
the semantics of BAN logic, Proceedings of the Foun-
dations of Computer Security, 121–132.
[20] M. Cohen and M. Dam (2007) A complete axiom-
atization of knowledge and cryptography, Proceed-
ings of the 22nd Annual IEEE Symposium on Logic
in Computer Science, IEEE, 77–88.
[21] F. Dechesne and Y . Wang (2010) To know or not to
know: epistemic approaches to security protocol ver-
iﬁcation, Synthese, Springer, 177(1): 51–76.https:
//doi.org/10.1007/s11229-010-9765-8
[22] C. Dixon, M.C. Fernández Gago, M. Fisher, and
W. van der Hoek (2007) Temporal logics of knowl-
edge and their applications in security, Electronic
Notes in Theoretical Computer Science, Elsevier,
186: 27–42. https://doi.org/10.1016/j.
entcs.2006.11.043
[23] C. Dixon, M.C.F. Gago, M. Fisher, and W. Van Der
Hoek (2004) Using temporal logics of knowledge in
the formal veriﬁcation of security protocols, Proceed-
ings of the 11th International Symposium on Tempo-
ral Representation and Reasoning, IEEE,148–151.
[24] D. Dolev and A. Yao (1983) On the security of public
key protocols, Proceedings of the IEEE Transactions
on Information Theory, IEEE, 29(2):198–208.
[25] R. Fagin and J.Y . Halpern (1994) Reason-
ing about knowledge and probability, Jour-
nal of the ACM, ACM, 41(2):340–367.
https://doi.org/10.1145/273865.274429
174 Informatica 43 (2019) 161–175 S. Ahmadi et al.
[26] R. Fagin, Y . Moses, J.Y . Halpern, and M.Y . Vardi
(2003) Reasoning about knowledge, The MIT Press.
https://doi.org/10.7551/mitpress/
5803.001.0001
[27] L. Gong, R. Needham, and R. Yahalom (1990)
Reasoning about belief in cryptographic proto-
cols, Proceedings of the IEEE Computer Society
Symposium on Research in Security and Privacy,
IEEE, 234–248. https://doi.org/10.1109/
risp.1990.63854
[28] A.D. Gordon and A. Jeffrey (2003) Authenticity by
typing for security protocols, Journal of computer se-
curity, IOS Press, 11(4): 451–519.https://doi.
org/10.3233/jcs-2003-11402
[29] G. Governatori, A.M. Orgun, and C. Liu (2008)
Modal tableaux for verifying stream authentication
protocols, Journal of Autonomous Agents and Multi
Agent Systems. https://doi.org/10.1007/
s10458-007-9027-4
[30] J.Y . Halpern and R. Pucella (2003) Modeling
adversaries in a logic for security protocol
analysis, Formal Aspects of Security, Springer,
115–132. https://doi.org/10.1007/
978-3-540-40981-6_11
[31] J.Y . Halpern and R. Pucella (2011) Dealing with
logical omniscience: Expressiveness and pragmatics,
Artiﬁcial intelligence, Elsevier, 175(1): 220–235.
https://doi.org/10.1016/j.artint.
2010.04.009
[32] J.Y . Halpern and M.R. Tuttle (1993) Knowl-
edge, probability, and adversaries, Journal of the
ACM, ACM,40(4):917–960. https://doi.org/
10.1145/153724.153770
[33] J. Heather, G. Lowe, and S. Schneider (2003)
How to prevent type ﬂaw attacks on security pro-
tocols, Journal of Computer Security, IOS Press,
11(2): 217–244. https://doi.org/10.3233/
jcs-2003-11204
[34] G.E. Hughes and M.J. Cresswell (2012) A new intro-
duction to modal logic, Routledge.https://doi.
org/10.4324/9780203028100
[35] G. Jakubowska, P. Dembinski, W. Penczek, and M.
Szreter (2009) Simulation of Security Protocols based
on Scenarios of Attacks, Fundamenta Informaticae,
93(1): 185-203.
[36] A. Jurcut, T. Coffey, and R. Dojen (2013) Establish-
ing and ﬁxing security protocols weaknesses using
a logic-based veriﬁcation tool, Journal of Communi-
cation, 8(11): 795–806.https://doi.org/10.
12720/jcm.8.11.795-805
[37] A.D. Jurcut, T. Coffey, and R. Dojen (2014) De-
sign guidelines for security protocols to prevent re-
play & parallel session attacks, computers & secu-
rity, Elsevier, 45: 255–273. https://doi.org/
10.1016/j.cose.2014.05.010
[38] F. Kammuller and C.W. Probst (2015) Mod-
eling and veriﬁcation of insider threats using
logical analysis, IEEE Systems Journal, IEEE,
11(2): 534–545. https://doi.org/10.1109/
jsyst.2015.2453215
[39] S. Kramer (2007) Logical concepts in cryptography,
PhD Thesis, École Polytechnique Fédérale de Lau-
sanne.
[40] C. Liu and M. Orgun (1996) Dealing with multi-
ple granularity of time in temporal logic program-
ming, Journal of Symbolic Computation, Elsevier,
22(5): 699–720. https://doi.org/10.1006/
jsco.1996.0072
[41] C. Liu, M.A. Ozols, and M. Orgun (2004) A tem-
poralised belief logic for specifying the dynamics of
trust for multi-agent systems Advances in Computer
Science-ASIAN 2004. Higher-Level Decision Mak-
ing, Springer, 142–156. https://doi.org/10.
1007/978-3-540-30502-6_10
[42] C. Liu, M. Ozols, and M. Orgun (2005) A ﬁbred be-
lief logic for multi-agent systems, AI 2015: Advances
in Artiﬁcial Intelligence, Springer, 29–38. https:
//doi.org/10.1007/11589990_6
[43] A. Lomuscio, H. Qu, and F. Raimondi (2009)
MCMAS: A model checker for the veriﬁcation
of multi-agent systems, Computer Aided Veriﬁca-
tion, Springer, 682–688.https://doi.org/10.
1007/978-3-642-02658-4_55
[44] A. Lomuscio, H. Qu, and F. Raimondi (2015) MC-
MAS: an open-source model checker for the veri-
ﬁcation of multi-agent systems International Jour-
nal on Software Tools for Technology Transfer,
Springer, 19(1): 9–30. https://doi.org/10.
1007/s10009-015-0378-x
[45] A. Lomuscio and B. Wo´ zna (2006) A complete and
decidable security-specialised logic and its applica-
tion to the TESLA protocol, Proceedings of the 5th
international joint conference on Autonomous agents
and multiagent systems, ACM, 145–152. https:
//doi.org/10.1145/1160633.1160658
[46] G. Lowe (1995) An attack on the Needham-
Schroeder public-key authentication protocol,
Information processing letters, Elsevier, 56(3):
131–133. https://doi.org/10.1016/
0020-0190(95)00144-2
On the Properties of Epistemic. . . Informatica 43 (2019) 161–175 175
[47] G. Lowe (1997) A family of attacks upon authentica-
tion protocols, epartment of Mathematics and Com-
puter Science, University of Leicester.
[48] G. Lowe (1998) Casper: A Compiler for the Anal-
ysis of Security Protocols, Journal of Computer Se-
curity, IOS Press, 6(1-2): 53–84. https://doi.
org/10.3233/jcs-1998-61-204
[49] G. Lowe (2004) Analysing protocols subject to guess-
ing attacks, Journal of Computer Security, IOS Press,
12(1): 83–97. https://doi.org/10.3233/
jcs-2004-12104
[50] X. Luo, Y . Chen, M. Gu, and L. Wu (2009)
Model Checking Needham-Schroeder Security Pro-
tocol Based on Temporal Logic of Knowledge, Pro-
ceedings of the NSWCTC’09. International Confer-
ence on Networks Security, Wireless Communications
and Trusted Computing, IEEE, 2: 551–554.https:
//doi.org/10.1109/nswctc.2009.384
[51] J. Ma, M.A. Orgun, and K. Adi (2011) An
analytic tableau calculus for a temporalised be-
lief logic, Journal of Applied Logic, Elsevier,
9(4): 289–304. https://doi.org/10.1016/
j.jal.2011.08.003
[52] J. Ma, M.A. Orgun, and A. Sattar (2009) Analysis of
authentication protocols in agent-based systems us-
ing labeled tableaux IEEE Transactions on Systems,
Man, and Cybernetics, Part B: Cybernetics, IEEE,
39(4): 889–900. https://doi.org/10.1109/
tsmcb.2009.2019263
[53] J. Ma and K. Schewe (2012) A Temporalised
Belief Logic for Reasoning about Authentication
Protocols, Proceedings of the IEEE 11th Inter-
national Conference on Trust, Security and Pri-
vacy in Computing and Communications (Trust-
Com), IEEE, 1721–1728. https://doi.org/
10.1109/trustcom.2012.59
[54] J.K. Millen (1996) CAPSL: Common Authentication
Protocol Speciﬁcation Language, Proceedings of the
1996 workshop on New security Paradigms (NSPW),
ACM, 96: 132. https://doi.org/10.1145/
304851.304879
[55] J. Mitchell, A. Scedrov, N. Durgin, and P. Lincoln
(1999) Undecidability of bounded security protocols,
Proceedings of the Workshop on Formal Methods and
Security Protocols.
[56] M.A. Orgun, J. Ma, C. Liu, and G. Governatori
(2006) Analysing stream authentication protocols in
autonomous agent-based systems2nd IEEE Interna-
tional Symposium on, Proceedings of the 2nd IEEE
International Symposium on Dependable, Autonomic
and Secure Computing, IEEE, 325–332.https://
doi.org/10.1109/dasc.2006.19
[57] A. Perrig, R. Canetti, J.D. Tygar, and D. Song
(2000) Efﬁcient authentication and signing of mul-
ticast streams over lossy channels, Proceedings
of the IEEE Symposium on Security and Pri-
vacy, IEEE, 56–73. https://doi.org/10.
1109/secpri.2000.848446
[58] R. Ramanujam and S.P. Suresh (2005) Deciding
knowledge properties of security protocols, Proceed-
ings of the 10th conference on theoretical aspects
of rationality and knowledge, National University of
Singapore, 219–235.
[59] R. Ramezanian (2015) Process Algebraic Model-
ing of Authentication Protocols for Analysis of Par-
allel Multi-Session Executions, The ISC Interna-
tional Journal of Information Security, Iranian So-
ciety of Cryptology, 1(1): 55-67. https://doi.
org/10.22042/isecure.2015.1.1.6
[60] P.F. Syverson (1993) Adding time to a logic of
authentication, Proceedings of the 1st ACM con-
ference on Computer and communications security,
ACM, 97–101. https://doi.org/10.1145/
168588.168600
[61] P.F. Syverson and P.C. Van Oorschot (1994) On uni-
fying some cryptographic protocol logics, Proceed-
ings of the IEEE Computer Society Symposium on
Research in Security and Privacy, IEEE, 14–28.
https://doi.org/10.21236/ada465512
[62] P. van Oorschot (1993) Extending cryptographic log-
ics of belief to key agreement protocols, Proceed-
ings of the 1st ACM Conference on Computer and
Communications Security, ACM, 232–243.https:
//doi.org/10.1145/168588.168617
176 Informatica 43 (2019) 161–175 S. Ahmadi et al.