RULE 2005 Preliminary Version

Completeness and Counter-Example
Generations of a Basic Protocol Logic(Extended Abstract)
Koji Hasebe 1,2 and Mitsuhiro Okada 1,3
Department of Philosophy
Keio University
2-15-45, Mita, Minato-ku, Tokyo 108-8345, Japan

Abstract
We give an axiomatic system in ﬁrst-order predicate logic with equality for proving
security protocols correct. Our axioms and inference rules derive the basic inference
rules, which are explicitly or implicitly used in the literature of protocol logics,
hence we call our axiomatic system Basic Protocol Logic (or BPL, for short). We
give a formal semantics for BPL, and show the completeness theorem such that for
any given query (which represents a correctness property) the query is provable iﬀ
it is true for any model. Moreover, as a corollary of our completeness proof, thedecidability of provability in BPL holds for any given query. In our formal semantics
we consider a “trace” any kind of sequence of primitive actions, counter-models(which are generated from an unprovable query) cannot be immediately regarded
as realizable traces (i.e., attacked processes on the protocol in question). However,with the aid of Comon-Treinen’s algorithm for the intruder deduction problem, we
can determine whether there exists a realizable trace among formal counter-models,
if any, generated by the proof-search method (used in our completeness proof). We
also demonstrate that our method is useful for both proof construction and ﬂaw
analysis by using a simple example.
Key words: security protocol analysis, ﬁrst-order predicate logic,
agreement properties, proof-search method.

1

This work was partly supported by Grants-in-Aid for Scientiﬁc Research of MEXT, Centerof Excellence of MEXT on Humanity Sciences (Keio University) and Oogata-kenkyu-jyosei
grant (Keio University). The ﬁrst author was also supported by Fellowship for Japan Young
Scientists from Japan Society for the Promotion of Science.
2
Email: hasebe@abelard.flet.keio.ac.jp
3
Email: mitsu@abelard.flet.keio.ac.jp
This is a preliminary version. The ﬁnal version will be published inElectronic Notes in Theoretical Computer Science
URL: www.elsevier.nl/locate/entcs

Hasebe and Okada

1Introduction

For the formal analysis of security protocols, there are two typical approaches
among others: one emphasizing a syntactic method such as BAN-logic [2] andprotocol logics of [9,7,16] (cf. also [1] for a protocol composition logic project
overview), and the other emphasizing a semantic method such as the strand
space method [18] and MSR [4]. The former approach aims at proving a property which guarantees a protocol correct in terms of a certain logical inference
system, while the latter approach aims at detecting ﬂaws in a protocol (i.e.,
concrete attacks on a protocol) in terms of a kind of trace-model. In this paper
we take the former approach. That is, our main purpose in this paper is to
give a simple formulation of a core part of the protocol logics of [9,7,16] forproving protocols correct. We also aim at connecting this formal approach toa method for the ﬂaw detection. Especially, we concentrate on several typesof agreement properties in the sense of [20,14], and investigate how much one
can formulate a basic part of the protocol logics, which is enough to prove our
aimed properties, within the ﬁrst-order predicate logic. (Thus, in this paper
we do not go into the secrecy property about nonces or session keys. Such aproperty is also an important matter for security analysis because agreement
properties of some protocols depend on their secrecy properties.) Moreover,
we also give a complete formal semantics of BPL, and present how to apply
our framework for both proving correctness and detecting ﬂaws of security
protocols.
For that purpose, we ﬁrst give an axiomatic system in ﬁrst-order predicate
logic for proving the agreement properties. In this system, we formalize someproperties about nonces and cryptographic assumptions as non-logical axioms
in ﬁrst-order predicate logic with equality, and give a special form of formulas,called query form, which represents an agreement property restricted to thenumber of data items (i.e., nonces) in the protocol in question. Then the basic
inference rules, which are explicitly or implicitly used for proving agreement
properties in the protocol logics of [9,7,16], are derived rules of our system.
Hence our formulation is called Basic Protocol Logic (or BPL, for short).
Next, we give a formal semantics for BPL and show the completeness theorem such that for any given query, the query is provable in BPL iﬀ it is true
for any model. This theorem is proved by adjusting the usual proof-searchmethod for the ﬁrst-order predicate logic into our framework (cf. [17]). As a
direct corollary of the completeness theorem, our proof-search method of thecompleteness proof provides a counter-example generation if the given queryis unprovable. Moreover, as a corollary of our completeness proof, the decidability of provability in BPL also holds for any query. (In this paper, we only
sketch out the proofs of the completeness theorem and its corollaries. The
detailed proofs will appear in the full version of this paper.) In our formal
semantics we consider a “trace” any kind of sequence of primitive actions, thus
a counter-example (generated from an unprovable query) cannot be immedi2

Hasebe and Okada

ately regarded as a realizable trace (i.e., an attacked process on the protocol
in question). However, with the aid of Comon-Treinen’s algorithm for the
intruder deduction problem [6], we can determine whether there exists a realizable trace among formal counter-examples. Therefore, by the combinationof our completeness proof and the Comon-Treinen’s algorithm, for any given
query we can generate attacked processes on the protocol, if any, whenever we
set any upper-bound on the number of data items.
Since our proof construction procedure is directly a counter-example generation, this work would make a contribution to bridge the gap between thetwo diﬀerent directions of security protocol analysis, namely proving correctness and ﬁnding attacks. Finally, we also demonstrate by a simple example
that our method is useful for both proof constructions and ﬂaw detections.
Organization of this paper. In Section 2 we introduce an axiomatic system, called Basic Protocol Logic in ﬁrst-order predicate logic, and formalize
our aimed correctness properties as a special form of formulas, called queryform. In Section 3 we give a trace-based formal semantics and show thesoundness theorem for the query form. In Section 4 we show the completenesstheorem and the decidability of provability for the query form, and explain
how to construct proofs/attacked processes for a given query by means of theproof-search method and Comon-Treinen’s algorithm for the intruder deduction problem. Finally, in Section 5 we present the conclusions and outline
some further directions of this research.

2

Basic Protocol Logic

We ﬁrst ﬁx our language in ﬁrst-order predicate logic with equality, and givean axiomatic system, called Basic Protocol Logic. In this system, our aimed
correctness properties are described as a special form of formulas, called queryform.
2.1 Language
Sorts and terms. Our language is order-sorted, which consists of sorts
name, nonce and message. A, B, . . . , A1 , A2 , . . . (P, Q, . . . , P1 , P2 , . . ., resp.) areconstants (variables, resp.) of sort name (which represent principal name), andN, N ′ , . . . , N1 , N2 , . . . (n, n′ , . . . , n1 , n2 , . . ., resp.) are constants (variables,
resp.) of sort nonce. All terms of sorts name and nonce are terms of sortmessage. The symbols m, m′ , . . . , m1 , m2 , . . . are used to denote variables ofsort message. Compound terms of sort message are made by the functions〈m1 , . . . , mn 〉, {m}P and {m}P −1 , which represent n-tuple concatenation of
messages, encryption of public key and secret key for P , respectively. We also
use the meta-symbols s, s′ , . . . , t, t′ , . . . to denote any terms of sort message. 4
4In order to make our discussion simpler, in this paper we do not consider symmetric
cryptography nor protocols for sharing session keys, however our formalization can be easily

3

Hasebe and Okada

Formulas. We introduce ﬁve binary predicate symbols: P generates n,
P receives m, P sends m, m = m′ and m ⊆ m′ , which represent “P generates
a fresh value n as a nonce”, “P receives a message m”, “P sends a messagem”, and usual equality and subterm relation (i.e., “m is identical with m′ ”
and “m is a subterm of m′ ”), respectively. The ﬁrst three are called action
predicates, and the meta expression acts is used to denote one of the action
predicates: generates, receives and sends.
Atomic formulas are the following expressions: P1 acts 1 m1 ; P2 acts 2 m2 ; · · · ;Pk acts k mk (where k ≥ 1 and Pi (mi , resp.) may be the same as Pj (mj ,resp.) for any i ̸= j), m = m′ and m ⊆ m′ . The ﬁrst one is called trace
formula. This type of atomic formulas is used to represent a sequence ofprincipal’s actions: for example, the intuitive meaning of the atomic formula P sends m; Q receives m′ is “P sends a message m before Q receives
a message m′ ”. We also use the following symbols as meta expressions.
αP , β P , . . . , α1P , α2P , . . . (or simply, α, β, . . . , α1 , α2 , . . .) is used to denote a trace⃗ , for short) is used toformula of the form P acts m, and α1P1 ; · · · ; αkPk (or αdenote P1 acts 1 m1 ; · · · ; Pk acts k mk (where k indicates the length of α⃗ ). Especially, when every Pi is identical with P for 1 ≤ i ≤ k (i.e., a sequence ofactions performed by a single principal P ), we also use α⃗ P to denote such a
trace formula. For α⃗ (≡ α1 ; · · · ; αm ) and β⃗ (≡ β1 ; · · · ; βn ), we say β⃗ includes⃗ if αα⃗ (denoted by α
⃗ ⊆ β),⃗ and β⃗ satisﬁes the following condition: αi appearsin β⃗ for all i (1 ≤ i ≤ m), and for any αi ≡ βj and αk ≡ βl if i < k then j < lfor any 1 ≤ i, k ≤ m. (Roughly speaking, α⃗ ⊆ β⃗ means that all the action
predicates in α
⃗ appear in β⃗ with preserving the order of α
⃗ .)The formulas (denoted by ϕ, ψ, . . .) are made by the following grammar.
ϕ ::= α⃗ | m = m′ | m ⊆ m′ | ¬ϕ | ϕ ∧ ϕ | ϕ ∨ ϕ | ϕ → ϕ | ∀xϕ | ∃xϕ

We use the meta expression ϕ[m]⃗ to indicate the list of terms m⃗ occurringin ϕ. Substitutions are represented in terms of this notation.
Finally, we introduce the notion of (strict) order-preserving merge of trace⃗ which is deﬁned as follows.
formulas α⃗ and β,Deﬁnition 2.1 (Order-preserving merge) An order-preserving merge ofα⃗ (≡ α1 ; · · · ; αl ) and β⃗ (≡ β1 ; · · · ; βm ) is a trace formula ⃗δ (≡ δ1 ; · · · ; δn ) which
is made by the following rules. (As a special case, if α
⃗ and β⃗ is empty thenwe respectively consider l = 0 and n = 0.)(i) δ1 ≡ α1 or β1 .

(ii) For each i (1 ≤ i ≤ n), if α1 ; · · · ; αj ⊆ δ1 ; · · · ; δi and β1 ; · · · ; βk ⊆
δ1 ; · · · ; δi (for some 0 ≤ j ≤ l and 0 ≤ k ≤ m), then δi+1 ≡ αj+1 or
βk+1 .
(iii) If ⃗δ ≡ δ1 ; · · · ; δi ; δi+1 ; · · · ; δn is an order-preserving merge of α
⃗ and β⃗ with
δi ≡ δi+1 , then ⃗δ′ ≡ δ1 ; · · · ; δi−1 ; δi+1 ; · · · ; δn is also an order-preserving
extended so as to include such notions.

4Hasebe and Okada⃗
merge of α
⃗ and β.
We also introduce another type of order-preserving merge which is made onlyby the rules (i) and (ii), and call it strict order-preserving merge of α⃗ and⃗β. For example, both α1 ; α2 ; α2 ; α3 and α2 ; α1 ; α3 ; α2 and α1 ; α2 ; α3 are orderpreserving merges of α1 ; α2 and α2 ; α3 , while the last one is not a strict orderpreserving merge.
Description of roles
A protocol is a set of roles, and each role for a principal (say, P ) is described
as a trace formula of the form α⃗ P ≡ P acts 1 m1 ; · · · ; P acts k mk .
As an example, here we consider the Needham-Schroeder public key protocol [15], whose informal description is as follows.
1. P → Q: {n1 , P }Q

2. Q → P : {n1 , n2 }P
3. P → Q: {n2 }Q

Initiator’s and responder’s roles of the Needham-Schroeder public key protocol(denoted by InitN S and RespN S , respectively) are described as the following
formulas.
Example 2.2 (Roles of the Needham-Schroeder protocol)
InitN S [P, Q, n1 , n2 ] ≡P generates n1 ; P sends {n1 , P }Q ; P receives {n1 , n2 }P ; P sends {n2 }Q
RespN S [P, Q, n1 , n2 ] ≡Q receives {n1 , P }Q ; Q generates n2 ; Q sends {n1 , n2 }P ; Q receives {n2 }Q⃗ and ⃗n with
A run of a role α⃗ P is a formula obtained by substituting P , Q
some terms of the same sorts. For example, InitN S [A/P, B/Q, N1 /n1 , N2 /n2 ]and RespN S [A/P, B/Q, N1 /n1 , N2 /n2 ] are runs of InitN S and RespN S , respectively, and we call such a set of instances A, B, N1 , N2 data items. A strict
order-preserving merge of runs of a role α⃗ P is called multiple runs of α⃗P.
2.2 Basic Protocol Logic
We extend the usual ﬁrst-order predicate logic with equality by adding thefollowing axioms (I), (II) and (III). This axiomatic system is called Basic
Protocol Logic.
(I) Axioms of universal sentences over terms. We presume the following
axioms for = and ⊆. When a ﬁnite set of literals {t1 = t′1 , . . . , tn = t′n , s1 ⊆s′1 , . . . sj ⊆ s′j , u1 ̸= u′1 , . . . , uk ̸= u′k , v1 ̸⊆ v1′ , . . . , vl ̸⊆ vl′ } is unsatisﬁable in
the free term algebra of our language (where = and ⊆ are the identity terms′
and subterm relation in the free term algebra), then ∀m¬(t⃗
1 = t1 ∧ · · · ∧ tn =t′n ∧ s1 ⊆ s′1 ∧ · · · ∧ sj ⊆ s′j ∧ u1 ̸= u′1 ∧ · · · ∧ uk ̸= u′k ∧ v1 ̸⊆ v1′ ∧ · · · ∧ vl ̸⊆ vl′ )5Hasebe and Okada

is an axiom. Note that the satisfaction problem is decidable in the free term
algebra (cf. [19]), hence the set of axioms of type 1 is recursive.
(II) Rules for trace formulas. We introduce the following axioms (1) and(2) for trace formulas, where γ⃗i ’s in (2) are the list of order-preserving merges⃗of α⃗ and β.
(1) β⃗ → α⃗⃗(for α⃗ ⊆ β)(2) γ⃗1 ∨ · · · ∨ γ⃗n ↔ α⃗ ∧ β⃗(III) Axioms for relationship between properties. We introduce thefollowing set of formulas as non-logical axioms. These axioms represent someproperties about nonces and cryptographic assumptions.
(1) Ordering 1:∀P Qnm(P generates n ∧ Q sends/receives m ∧ n ⊆ m→ ¬(Q sends/receives m; P generates n))(2) Ordering 2:∀P Qmm′ (P sends/receives m ∧ {m′ }Q−1 ⊆ m→ ∃m′′ (Q sends m′′ ; P sends/receives m ∧ {m′ }Q−1 ⊆ m′′ ))(3) Nonce Veriﬁcation 1:∀P Qn1 m2 m5 m6 (P generates n1 ∧ P sends m2 ∧ n1 ⊆ m2 ∧ P receives m5∧ n1 ⊆ m6 ∧ {m6 }Q−1 ⊆ m5
∧ ∀m7 (P sends m7 ∧ n1 ⊆ m7 → m7 = m2 )→ ∃m3 m4 (P sends m2 ; Q receives m3 ; Q sends m4 ; P receives m5∧ n1 ⊆ m3 ∧ {m6 }Q−1 ⊆ m4 ))(4) Nonce veriﬁcation 2:∀P Qn1 m2 m5 m6 (P generates n1 ∧ P sends m2 ∧ n1 ⊆ m2 ∧ P receives m5∧ {m6 }Q ̸⊆ m5 ∧ n1 ⊆ m5 ∧ {m6 }Q ⊆ m2
∧ ∀m7 (P sends m7 ∧ n1 ⊆ m7 → m7 = m2 )∧ ∀m8 (n1 ⊆ m8 ∧ m8 ⊆ m2 → m8 ⊆ {m6 }Q )→ ∃m3 m4 (P sends m2 ; Q receives m3 ; Q sends m4 ; P receives m5∧ {m6 }Q ⊆ m3 ∧ n1 ⊆ m4 ))(5) Nonce veriﬁcation 3:∀P Qn1 m4 m5 m6 m9 (P generates n1 ∧ P sends m2 ∧ n1 ⊆ m2 ∧ P receives m5∧ {m6 }Q ̸⊆ m5 ∧ n1 ⊆ m5 ∧ {m6 }Q ⊆ m2
∧ ∀m7 (P sends m7 ∧ n1 ⊆ m7 → m7 = m2 )∧ ∀m8 (n1 ⊆ m8 ∧ m8 ⊆ m2 → m8 ⊆ {m6 }Q )∧ Q sends {m4 }P ∧ n1 ⊆ m4
∧ ∀m10 (Q sends m10 ∧ n1 ⊆ m10 → m10 = {m9 }P )→ {m9 }P = m5 )Here, the expression “sends/receives” denotes sends or receives, and these
are corresponding in each axiom. Ordering 1 and 2 represent ordering of6

Hasebe and Okada

actions related to nonces and encrypted messages, respectively. Nonce Veriﬁcation 1−3 largely depend on the idea of authentication tests-based strand
space method introduced by [10]: Nonce Veriﬁcation 1 is a formalization ofIncoming tests and Nonce Veriﬁcation 2 and 3 are formalizations of Outgoingtests.
2.3 Query form and correctness properties
Our aimed correctness properties are described in a special form of formulas,called query form. The query form includes a formalization of principal’s
honesty (denoted by Honest(⃗αP )), which is deﬁned as follows.
Deﬁnition 2.3 (Principal’s honesty)⃗ ⃗n])
Honest(⃗αP [P, Q,W
def⃗n⃗ ⃗n] ∧ Only(⃗⃗ ⃗n])≡ ∃Q⃗α⃗ P (i)[P, Q,
αP (i)[P, Q,
P⃗
i∈{j | mj ∈Sends(⃗
α [P,Q,⃗n])}∪{k}⃗ ⃗n] is a role of the form P acts1 m1 ; P acts2 m2 ; · · · ; P actsk mkHere, α⃗ P [P, Q,
where each actsi (1 ≤ i ≤ k) is one of sends, receives and generates, and⃗ ⃗n] denotes an initial segment of α⃗ ⃗n] ending with P acts i miα
⃗ P (i)[P, Q,⃗ P [P, Q,⃗ ⃗n] ≡ P acts1 m1 ; · · · P actsi mi . (As a special(for 0 ≤ i ≤ k), i.e., α⃗ P (i)[P, Q,
P
case, α⃗ (0) denotes ⊤.) Only(⃗αP (i)) denotes the following formula, whose⃗ ⃗n]”.
intuitive meaning is “P performs only α⃗ P (i)[P, Q,
Only(⃗αP (i)) ≡ ∀n1 (P generates n1 → n1 ∈ Generates(⃗αP (i)))∧∀m2 (P sends m2 → m2 ∈ Sends(⃗
αP (i)))∧∀m3 (P receives m3 → m3 ∈ Receives(⃗
αP (i))))
Here, Sends(⃗
αP (i)) denotes the set {mj | P sends mj ⊆ α⃗ P (i)}. (Receives(⃗
αP (i))
P
and Generates(⃗
α (i)) are similar.) Set theoretical notation, such as m ∈PSends(⃗
α (i)) (as well as m ∈ Receivess(⃗αP (i)) and m ∈ Generates(⃗αP (i)))
is an abbreviation of the disjunctive form: for example, if Sends(⃗
αP (i)) =′′P′{m1 , . . . , mj }, then m ∈ Sends(⃗
α (i)) denotes the formula (m = m1 ) ∨ (m =′′m2 ) ∨ · · · ∨ (m = mj ). (As a special case, if Sends(⃗
αP (i)) is empty thenPm ∈ Sends(⃗
α (i)) denotes ⊥.)Intuitively, each disjunct α⃗ P (i) ∧ Only(⃗αP (i)) in Honest(⃗
αP ) represents ahistorical record of P ’s actions at each step of his/her run: the sequence ofactions α⃗ P (i) ≡ P acts 1 m1 ; · · · ; P acts i mi represents the P ’s performance atthis step, and Only(⃗αP (i)) represents that P performs only α⃗ P (i). Especially,
as a special case, α⃗ P (0) ∧ Only(⃗αP (0)) represents that P performs no action.
⃗ ⃗n]) represents “P performs only a (possibly multiple)
Thus, Honest(⃗
αP [P, Q,
run of an initial segment of α
⃗ P which ends with a sending action or the last
⃗ and ⃗n, for each run”.
action of α
⃗ P , and uses the same data items Q
As an example, we present the honesty of initiator (say, A) of the NeedhamSchroeder protocol below.
7

Hasebe and Okada

Example 2.4 (Initiator’s honesty of the NS protocol)
Honest(InitN S [A/P, Q, n1 , n2 ]) ≡∀n3 (A generates n3 → ⊥)
∃Qn1 n2  ∧∀m4 (A sends m4 → ⊥) ∧∀m5 (A receives m5 → ⊥)
 A generates n1 ; A sends {n1 , A}Q ∧∀n3 (A generates n3 → n3 = n1 )∨ ∧∀m (A sends m → m = {n , A} ) 
4
4
4
1
Q 

∧∀m5 (A receives m5 → ⊥)
 A generates n1 ; A sends {n1 , A}Q ; A receives {n1 , n2 }A ; A sends {n2 }Q  ∧∀n3 (A generates n3 → n3 = n1 )∨ ∧∀m (A sends m → m = {n , A} ∨ m = {n } )
4
4
4
1
4
2 Q
Q


∧∀m5 (A receives m5 → m5 = {n1 , n2 }A )Note that our formalization of honesty is stronger than the usual sense.
That is, our deﬁnition of honesty is restricted to a single set of data items used
for the honest principal’s runs, whereas the usual sense of honesty means that
P may perform multiple runs whose data items may diﬀer from each other.
However, by regarding a strict order-preserving merge of a certain numberof the same role as a single role, we can represent the honesty with respect
to any ﬁnite number of the sets of data items which are used for all possible
runs by the honest principal. As an example, we present the case of initiator’s(say, A’s) honesty of the Needham-Schroeder protocol, such that A may use
a couple of sets of data items [Q, n1 , n2 ] and [Q′ , n′1 , n′2 ].
∀n3 (A generates n3 → ⊥)∃QQ′ n1 n2 n′1 n′2  ∧∀m4 (A sends m4 → ⊥) ∧∀m5 (A receives m5 → ⊥)A generates n1 ; A sends {n1 , A}Q ∧∀n3 (A generates n3 → n3 = n1 )∨ ∧∀m4 (A sends m4 → m4 = {n1 , A}Q ) ∧∀m5 (A receives m5 → ⊥)A generates n1 ; A sends {n1 , A}Q ; A receives {n1 , n2 }A ; A sends {n2 }Q ∧∀n3 (A generates n3 → n3 = n1 )∨ ∧∀m4 (A sends m4 → m4 = {n1 , A}Q ∨ m4 = {n2 }Q )∧∀m5 (A receives m5 → m5 = {n1 , n2 }A )A generates n1 ; A sends {n1 , A}Q ∧ A generates n′1 ; A sends {n′1 , A}′Q ∧∀n3 (A generates n3 → n3 = n1 ∨ n3 = n′1 )∨ ∧∀m4 (A sends m4 → m4 = {n1 , A}Q ∨ m4 = {n′1 , A}Q′ )∧∀m5 (A receives m5 → ⊥)8Hasebe and Okada
A generates n1 ; A sends {n1 , A}Q ; A receives {n1 , n2 }A ; A sends {n2 }Q ∧A generates n′1 ; A sends {n1 , A}Q′∨  ∧∀n3 (A generates n3 → n3 = n1 ∨ n3 = n′1 ) ∧∀m4 (A sends m4 → m4 = {n1 , A}Q ∨ m4 = {n2 }Q ∨ m4 = {n′1 , A}Q′ ) ∧∀m5 (A receives m5 → m5 = {n1 , n2 }A )A generates n1 ; A sends {n1 , A}Q ; A receives {n1 , n2 }A ; A sends {n2 }Q ∧A generates n′1 ; A sends {n′1 , A}Q′ ; A receives {n′1 , n′2 }A ; A sends {n2 }Q′ 


′

 ∧∀n3 (A generates n3 → n3 = n1 ∨ n3 = n1 )∨ ∧∀m4 (A sends m4
→ m4 = {n1 , A}Q ∨ m4 = {n2 }Q ∨ m4 = {n′1 , A}Q′ ∨ m4 = {n′2 }Q′ ) ∧∀m5 (A receives m5 → m5 = {n1 , n2 }A ∨ m5 = {n′1 , n′2 }A )First-order formalization of correctness properties
We introduce a general form of formulas, called query form, to represents
our aimed correctness properties. In order to make the discussion simpler,
we consider only the case of two party authentication protocols, however ourquery form can be easily extended so as to represent the correctness properties with respect to other types of protocols which include more than two
principals.
Deﬁnition 2.5 (Query form) Query form is a formula of the following form.
Honest(⃗αP ) ∧ β⃗ Q ∧ Only(β⃗ Q ) → ⃗γ
Our aimed correctness properties are described as a special case of thequery form. For example, the non-injective agreement of protocol Π = {⃗αP [P, Q, ⃗n],β⃗ Q [P, Q, ⃗n]} from responder’s (say, B’s) view can be described as the following
formula.
⃗ /⃗n]
Honest(⃗αP [A/P, Q, ⃗n]) ∧ β⃗ Q [A/P, B/Q, N⃗ /⃗n]) → α⃗ /⃗n]∧Only(β⃗ Q [A/P, B/Q, N⃗ P [A/P, B/Q, N
The matching conversations and the injective agreement can be obtained byreplacing the right hand side of implication with the strict order-preserving⃗ /⃗n] and β⃗ Q [A/P, B/Q, N⃗ /⃗n] deﬁned by the protocol
merge of α
⃗ P [A/P, B/Q, NPP⃗ /⃗n] ∧ Only(⃗⃗ /⃗n]), respectively.
Π, and with α⃗ [A/P, B/Q, N
α [A/P, B/Q, N
Actually, our formalization of the agreement properties is weaker than theusual sense, because our honesty assumption is stronger than the usual sense.
However, as we have explained in the deﬁnition of honesty (Deﬁnition 2.3),
our query form can be extended so that the honest principal may use a ﬁnite
number of sets of data items used for his/her runs.
A comparison between BPL and other protocol logics
In closing this chapter, we would like to point out some diﬀerences between
BPL and other protocol logics.
9

Hasebe and Okada

One of the main diﬀerences is the formalization of inferences on honesty.
In the protocol logics of [9,7,16], the notion of honesty is formalized as an
atomic formula and inferences on honesty are drawn by a special inference
rule. On the other hand, in BPL, the notion of honesty is formalized as a nonatomic formula and all inferences on honesty are drawn by logical inference
rules, and the inferences on honesty essentially used in [9,7,16] are derived
rules in BPL. More precisely, to prove protocols correct, the protocol logics of[9,7,16] implicitly or explicitly use the three types of inferences: we pick up
these inferences as Honesty rules presented in Appendix A.
As for the non-logical axioms, our proposed non-logical axioms (1)-(5) of(III) introduced in Section 2.2 do not essentially depend on our framework.
Especially, as we shall show in Section 4, our completeness and decidability
arguments are not aﬀected by the choice of non-logical axioms. Our choice of
non-logical axioms in this paper is one of the simplest formalism suﬃcient toprove our aimed correctness properties. Then the basic inference rules usedin the protocol logics are essentially derived rules of BPL. Here we emphasizethat BPL is formalized in ﬁrst-order predicate logic without any temporalmodal operators nor Floyd-Hoare style dynamic operator which are used in
the protocol logics of [9,7]: this is the reason why we call our system “basic”.

3

Formal Semantics and Soundness

In this section, we give a semantics of our system.
A trace model (or model) is M = (DP , DN , α⃗ , Φ) where DP is a set, calleda name domain, DN is a set called a nonce domain, DM is the free algebra domain (i.e., the set of ﬁrst-order terms) determined by DP and DN along withthe term construction rules using 〈 , 〉, K( , ) and K −1 ( , ), (where 〈 , 〉 is theordered pair function symbol, and K( , ) and K −1 ( , ) are the key-encryption
and decryption function symbols), and α⃗ is a trace. (Note that we often use
abbreviation, say {n1 , {n2 }A , n3 }B −1 for K −1 (B, 〈〈n1 , K(A, n2 )〉, n3 〉).) In thispaper we consider only three kinds of forms of actions: A sends m, A receives m
and A generates n, where A ∈ DP , m ∈ DM . A trace α⃗ is of the formof a ﬁnite sequence α1 ; · · · ; αn of (primitive) actions αi . Φ(A) ∈ DP for
a constant symbol A of the name sort, and Φ(N ) ∈ DN for a constantsymbol N of the nonce sort. We extend Φ to evaluation of variables suchthat Φ(P ) ∈ DP and Φ(n) ∈ DN , as usual. Φ(〈t1 , t2 〉) = 〈Φ(t1 ), Φ(t2 )〉,Φ(K(A, t)) = K(Φ(A), Φ(t)), Φ(K −1 (A, t)) = K −1 (Φ(A), Φ(t)). For any
action predicate α(A, m), Φ(α(A, m)) = α(Φ(A), Φ(m)). For a trace formula of the form α1 ; · · · ; αn , Φ(α1 ; · · · ; αn ) = Φ(α1 ); · · · ; Φ(αn ). For a modelM = (DP , DN , α⃗ , Φ), m1 ⊆ m2 is true in M iﬀ Φ(m1 ) is a subterm of Φ(m2 ),and m1 = m2 is true in M iﬀ Φ(m1 ) and Φ(m2 ) are identical terms (of the⃗ ⊆αsame sort). β⃗ is true in M iﬀ Φ(β)⃗ . All ﬁrst-order logical connectives areinterpreted in the standard way.
10

Hasebe and Okada

Theorem 3.1 (Soundness) For any closed formula of the query form
Honest(⃗αP ) ∧ β⃗ Q ∧ Only(β⃗ Q ) → ⃗γ ,if this formula is provable in BPL, then it is true for any model M = (DP , DN , α⃗ , Φ).
This theorem is proved by a standard induction on the length of the proof.

4

Completeness, Decidability and Their Application toCounter-Example Generations

In this section, we ﬁrst show the completeness theorem for the query form bymeans of the proof-search method. Moreover, as a corollary of our completeness proof, we also show the decidability of provability for any given query.
(Actually, in this preliminary report we only sketch out these proofs. The
detailed proofs will appear in the full version of this paper.) Next, as anapplication of these results, we show how to ﬁnd an attack on the protocol
in question. As the main result, with the aid of Comon-Treinen’s algorithm
for the intruder deduction problem [6], for any given query we can determine
whether there exists an attack on the protocol in question, whenever we set
any upper-bound on the number of data items. At the end of this section,
we also present a concrete example of our proof construction/counter-example
generation.
4.1 Completeness and decidability for the query form
Our completeness is stated as follows.
Theorem 4.1 (Completeness) If a closed formula of the query form
Honest(⃗αP ) ∧ β⃗ Q ∧ Only(β⃗ Q ) → ⃗γ

is true for any model M = (DP , DN , ⃗δ, Φ), then this formula is provable in
BPL.
To prove the completeness theorem, we use the proof-search method (whichis essentially the same as Beth’s tableau method). Especially, we follow themethod and several terminologies (such as stage, branch, and available terms)
described in Section 1.8 of Takeuti [17]. In order to ﬁx our query form to thesequent calculus-style proof-search method, we ﬁrst slightly modify our query
form as the following sequent, called a query sequent.
Honest(⃗αP ), β⃗ Q , Only(β⃗ Q ), Axioms(1)-(5) ⊢ ⃗γHere, Axioms(1)-(5) denotes the set of non-logical axioms (1)-(5) of (III)
introduced in Section 2.2. We put these formulas as assumptions of the query.
Now we review the proof-construction process and remark the point to beslightly modiﬁed in our setting.
11

Hasebe and Okada

Proof-construction process. For any query sequent S, we shall deﬁne theproof-construction tree for S (denoted by T (S)). T (S) is a (possibly inﬁnite)
tree which is constructed in rounds: the proof-construction process begins
with Round 0, where we write the query sequent S at the bottom of the tree,
and go to Round 1. Then each Round i (for i = 1, 2, . . .) consists of stages(k = 0, 1, 2, . . . , 14) deﬁned by cases:
Case I: Every topmost sequent, which is of the form Γ ⊢ ∆, satisﬁes oneof the following conditions (C1)−(C3), then the proof-construction process
terminates. We call such a sequent closed sequent.
(C1) Γ and ∆ include a formula in common.
(C2) t1 = t′1 , . . . , tn = t′n , s1 ⊆ s′1 , . . . sm ⊆ s′m ∈ Γ and u1 = u′1 , . . . , uk =u′k , v1 ⊆ v1′ , . . . , vl ⊆ vl′ ∈ ∆, and the literal {t1 = t′1 , . . . , tn = t′n , s1 ⊆s′1 , . . . sm ⊆ s′m , u1 ̸= u′1 , . . . , uk ̸= u′k , v1 ̸⊆ v1′ , . . . , vl ̸⊆ vl′ } is not satisﬁable in
the free term algebra of our language. This condition is essentially the sameas axiom (I) in Section 2.2.
(C3) Γ includes a trace formula α⃗ and ∆ includes a trace formula β⃗ withβ⃗ ⊆ α⃗ . This condition is essentially the same as axiom (1) of (II) in Section
2.2.
Case II: Not Case I. Then this stage is deﬁned according as k = 0, 1, 2, . . . , 13,
14, where the cases k = 0, 1, 2, . . . , 11 and 14 are the same as [17], i.e., k = 0
and 1 concern the symbol ¬, k = 2 and 3 concern ∧, k = 4 and 5 concern ∨,k = 6 and 7 concern →, k = 8 and 9 concern ∀, k = 10 and 11 concern ∃. In
addition to the above stages, we insert the following rules as k = 12 and 13.
••

k = 12 (equality rule): Let Γ[t] ⊢ ∆[t] be any topmost sequent of the tree
which has been deﬁned by stage k − 1. Then write down
Γ[t] ⊢ ∆[t], s = t and s = t, Γ[t], Γ[s/t] ⊢ ∆[t], ∆[s/t]
above Γ[t] ⊢ ∆[t] for all terms s and t, which are made by all available termsof sorts name and nonce with function symbols.
We introduce this stage instead of the inﬁnite scheme ∀x∀y(x = y ∧F (x) → F (y)) as a hypothesis in the query.

k = 13 (rule for trace formulas): Let Γ ⊢ ∆ be any topmost sequent of
the tree which has been deﬁned by stage k − 1, and α⃗ 1, . . . , α⃗ j be the trace
formulas appearing in Γ. Then write down all sequents of the form
⃗γi , Γ′ ⊢ ∆above Γ ⊢ ∆, where ⃗γi is an order-preserving merge of α
⃗ 1, . . . , α⃗ j , and Γ′ isΓ − {⃗
α1 , . . . , α⃗ j }.
This stage is the combination of the if-part of axiom (II) (2) in Section⃗ and the ∨-left reduction. Note that we do not
2.2 (i.e., ⃗γ1 ∨· · ·∨⃗γn → α⃗ ∧ β)
need to consider the only-if part of axiom (II) (2) (i.e., α⃗ ∧ β⃗ → ⃗γ1 ∨· · ·∨⃗γn ),because in our proof-construction process there is no sequent such that aformula of the form α⃗ ∧ β⃗ appears in the right hand side.

After applying the rule of Stage 14, if the topmost sequent is not closed, then12

Hasebe and Okada

we go to Round i + 1 and repeat the above procedure.
Proof sketch of the completeness theorem. From now we show ourcompleteness proof, which is proved by using the following lemma.
Main Lemma. If there exists a branch S0 , . . . , S3×14 in T (S0 ), where S3×14
is a sequent at the end of Round 3 and not closed, then there exists a countermodel M = (DP , DN , ⃗δ, Φ) for S0 .
Here we sketch out how to construct such a counter-model M from S3×14 .
Assume that θ⃗ is the trace formula appearing in the left hand side of
S3×14 . (Note that at the end of each round, the left hand side of the sequent
always includes only a single trace formula.) We ﬁx DP and DN by thefollowing steps: we ﬁrst take the set of all literals appearing in S3×14 andsolve the satisfaction problem of these literals, then decompose each literal
which consists of compound terms (e.g., {N1 , A}B = {n1 , P }Q is decomposed
as N1 = n1 , A = P and B = Q), then take DP and DN as representatives ofthese decomposed literals. We deﬁne the assignment Φ for terms by induction
on the length of terms as follows. As the base case, each constant and variableof sort name or nonce is interpreted by its representative (i.e., Φ(N ) = N ∗(∈ DN ), Φ(n) = n∗ (∈ DN ) where N ∗ and n∗ are the representatives of
equivalence classes of N and n, respectively, and the interpretation for termsof sort name is similar.) Each variable (say, m) of sort message which is neitherof sort name nor nonce is interpreted by the representative of the equivalenceclass of m. The induction step for terms and the deﬁnition of evaluation foreach formula are followed by the deﬁnition of Φ in Section 3. Finally, as ⃗δ, we⃗
take ⃗δ = Φ(θ).
From now we show that M is a counter-model of S0 . The essential idea toprove this fact is to use the following facts: (1) Every non-logical Π02 axiom
is satisﬁable in M ; (2) Axioms about trace formulas are satisﬁable in M ; (3)Axioms about = and ⊆ are satisﬁable in M . As for the fact (1), for any branch
in a proof-construction tree, if an eigenvariable (say, m) appears in the branch,such an eigenvariable always appears in a formula of the form A acts m. On theother hand, as the descendants of the honesty assumption, ¬A acts m ∨ m = t
always appears in the branch, where t is a term appearing at this stage. Thus,
if T is the set of terms in Round 3, for the eigenvariable m which appears above
Round 3, an equation m = t with some t ∈ T always appears in the left side,then the search domain does not increase above Round 3. As for the facts (2)and (3), these are immediately derived from the correspondence of the logicalaxioms (I) (introduced in Section 2.2) and the termination condition (C2),and the correspondence of the logical axiom (II) (introduced in Section 2.2)
and the termination condition (C3), respectively.
By this Main Lemma, proof of our completeness theorem goes as follows.
For any given query form, if each branch of the reduction tree up to Round13

Hasebe and Okada

3 terminates, then we can easily write a proof of this query. Then by thecontraposition, for any unprovable query there exists a branch which includes
a non-closed sequent (say, S3×14 ) at the end of Round 3. By Main Lemma,
we obtain a counter-model from the information of S3×14 . Then by the contraposition, the completeness theorem holds.
2This Main Lemma guarantees not only that our completeness holds, butalso that we only need to make a proof-construction tree up to Round 3 toﬁnd a counter-model. Therefore, if we introduce a suitable enumeration of all
instantiations for ∀-left, ∃-right and equality rules, the following decidability
is immediately derived from Main Lemma.
Corollary 4.2 (Decidability) For any given query form, the provability ofthe query in BPL is decidable.
Moreover, the following theorem holds.
Theorem 4.3 (Finite number of minimal counter-models) For any unprovable query form, the number of counter-models, which are obtained fromthe proof-construction tree of the query up to the end of Round 3, is ﬁnite.
4.2 Construction of attacked processes
By the proof-search method presented in the previous subsection, for any
given query we obtain a proof if the query holds. Otherwise we obtain countermodels for the query. However, the traces obtained from these counter-models
cannot be immediately considered as attacked processes because in our semantics we consider as a “trace” any sequence of primitive actions. In order to ﬁnd
an attacked process, we introduce the notion of realizable trace by means of
the Comon-Treinen’s algorithm for the intruder deduction problem such thatfor any given ﬁnite (or regular) set of messages T , and for any given messagem, whether it is possible for the intruder to retrieve m from T or not.
The deﬁnition of realizable trace is as follows.
Deﬁnition 4.4 (Realizable trace) Let ⃗δ be a sequence of actions, P1 receives m1 ,. . . , Pk receives mk be the list of all receiving actions in ⃗δ, and ⃗δ(i) be the initial segment of ⃗δ, which ends with Pi receives mi . ⃗δ is realizable if it satisﬁes
the following condition: for any Pi receives mi (1 ≤ i ≤ k), mi is provable(retrievable) from Sends(⃗δ(i − 1)) in Comon-Treinen’s system of [6].
Intuitively, a realizable trace is a sequence of actions, where each receiving
message can be generated by the Dolev-Yao intruder [8]. Clearly, from a
realizable trace, which is obtained from a counter-model of a query, we caneasily construct a concrete attacked process on the protocol in question by
inserting some suitable intruder’s actions.
Since the procedure to check the realizable trace is decidable (cf. [6]), thefollowing theorem is immediately derived.
14

Hasebe and Okada

Theorem 4.5 (Decidability of the attacked process detection) For any
given query, the problem whether there exists a counter-model M = (DP , DN , ⃗δ, Φ)such that ⃗δ is an realizable trace is decidable.
As we have explained in the deﬁnition of our query form, we can represent
the correctness properties for any number of sets of data items (used by thehonest principal). Thus, this decidability guarantees that we can determine
whether there exists an attacked trace whenever we set any upper-bound on
the number of data items used by the principals. This decidability corresponds
to the result of former works (cf. [4]).
A suitable tactics to ﬁnd an attack on the protocol in question is to increase
the search domain by extending the query form. This procedure is generally
inﬁnite if we set no limit to the search domain. However, this procedure is optimal since the same undecidability result also holds in some other framework(cf. [4]).
4.3 An example of attacked process detection
In this subsection, we show a simple example of how to ﬁnd an attacked processfrom counter-models obtained by a proof-search of unprovable query. Here we
consider the matching conversations for the Needham-Schroeder public key
protocol (from responder’s view), whose query sequent is as follows.
RespN S [A/P, B/Q, N1 /n1 , N2 /n2 ], Honest(InitN S [A, Q, n1 , n2 ]), Axioms,∀n3 (B generates n3 → n3 = N2 ), ∀m4 (B sends m4 → m4 = {N1 , N2 }A ),∀m5 (B receives m5 → m5 = {N1 , A}B ∨ m5 = {N2 }B )⊢ A generates N1 ; A sends {N1 , A}B ; B receives {N1 , A}B ; B generates N2 ;B sends {N1 , N2 }A ; A sends {N2 }B ; B receives {N2 }B
In the proof-construction tree of this query, there are 16 non-closed branches
at the end of Round 3, which are of the following form. (Here we use schematic
expressions: t1 is N1 or n1 , t2 is N2 or n2 .)••in the left hand side, a trace formula appears which is made by orderpreserving merges of the following trace formulas:· A generates t1 ; A sends {t1 , A}Q ; A receives {t1 , t2 }A ; A sends {t2 }Q· B receives {t1 , A}B ; B generates t2 ; B sends {t1 , t2 }A ; B receives {t2 }B· B sends {t1 , t2 }A ; A receives m1 ; A sends m2 ; B receives {t2 }BA ̸= B, A ̸= Q, B ̸= Q, N1 ̸= N2 , n1 ̸= n2 , N1 = n1 , N2 = n2 , m1 =
{t1 , t2 }A and m2 = {t2 }Q are satisﬁed by all equations in this sequent.

Among the counter-models obtained by these non-closed sequents, we canﬁnd a model M = (DP , DN , α⃗ , Φ) such that DP = {A, B, Q}, DN = {N1 , N2 },where A ̸= B, A ̸= Q, B ̸= Q, N1 ̸= N2 , α⃗ = A generates N1 ; A sends {N1 , A}Q ;B receives {N1 , A}B ; B generates N2 ; B sends {N1 , N2 }A ; A receives {N1 , N2 }A ;A sends {N2 }Q ; B receives {N2 }B . Moreover, the trace α⃗ is realizable: actually, we can construct an attacked process as follows.
15

Hasebe and Okada

A generates N1 ; A sends {N1 , A}Q ; Q receives {N1 , A}Q ; Q sends {N1 , A}B ;B receives {N1 , A}B ; B generates N2 ; B sends {N1 , N2 }A ; A receives {N1 , N2 }A
A sends {N2 }Q ; Q receives {N2 }Q ; Q sends {N2 }B ; B receives {N2 }B .
This is the scenario of the attack on the Needham-Schroeder protocol detected by Lowe [13].
Remark. It is known that the modiﬁcation of the second message (i.e., replacing {N1 , N2 }A with {N1 , N2 , B}A ) makes impossible the Lowe’s attack.
Actually, in our case, this modiﬁcation changes the A’s honesty as follows:∀m(A receives m → m = {n1 , n2 , Q}A ). Then, after the appearance of B sends{N1 , N2 , B}A ; A receives m1 ; A sends m2 ; B receives {N2 }B ∧ {N1 , N2 , B}A ⊆m1 ∧ N2 ⊆ m2 , the equation B = Q should appear in the left hand side. (Otherwise such branches should be closed by the termination condition (C2).)Therefore, the trace formula A generates N1 ; A sends {N1 , A}B ; A receives{N1 , N2 , B}A ; A sends {N2 }B should appear in the left hand side. Then, by
the termination condition (C3), such branches should be closed. Therefore, allbranches should be closed and then the agreement of this modiﬁed protocol isprovable.

5

Conclusions and Future WorkWe introduced an axiomatic system in ﬁrst-order predicate logic for proving
protocols correct, called Basic Protocol Logic, as a simple formulation of a basicpart of the protocol logics [9,7,16]. We also gave a simple trace-based semantics
which is complete for our query form in BPL. Moreover, as a corollary of ourcompleteness proof, we obtained the decidability of provability in BPL withrespect to our query. Then by combining our completeness proof and theComon-Treinen’s algorithm, for any given query we can generate concrete
attacks on the protocol in question, if any, whenever we set any upper boundon the number of data items used in the protocol.
There are several directions in which this work can be developed. First, weare interested in the extension in order to prove secrecy property about session
keys issued in a protocol. As we have mentioned in Section 1, by this extension we can treat correctness properties which are related to secrecy property,
such as in the case of Kerveros Version 5 (cf. [3]). We are also interested
in compositional approach to prove correctness of compound protocols (cf.
[9,7,16]). In our previous work [11,12], we proposed some inference systems toprove correctness properties of a composed protocol by reusing proofs about its
components. The main idea in [11,12] was to weaken the notion of honesty.
However, our decidability result does not hold by introducing such a weakhonesty. In this paper we omitted the compositionality, although we consider
such a problem to be one of our good target to develop our framework.
16

Hasebe and Okada

Acknowledgments
We thank Andre Scedrov and Iliano Cervesato for their helpful comments anddiscussions at early stages of this research.

References[1] www.stanford.edu/~danupam/logic-derivation.html[2] M. Burrows and M. Abadi and R. Needham. A Logic of Authentication.
Technical Report 39, Digital System Research Center, 1989.
[3] F. Butler, I. Cervesato, A.D. Jaggard and A. Scedrov. A Formal Analysis
of Some Properties of Kerberos 5 Using MSR. University of Pennsylvania
Department of Computer and Information Science Technical Report MS-CIS04-04, 59 pages, 2004.
[4] I. Cervesato, N.A. Durgin, P.D. Lincoln, J.C. Mitchell and A. Scedrov. Multiset
Rewriting and the Complexity of Bounded Security protocols. Journal ofComputer Security, vol.12, no.1, pp.677-722, 2004.
[5] J. Clark and J. Jacob. A Survey of Authentication Protocol Literature: Version
1.0 (web draft), 1997.
[6] Hubert Comon-Lundh and Ralf Treinen. Easy Intruder Deductions. In
Veriﬁcation: Theory and Practice, essays dedicated to Zohar Manna. LNCS
series 2772, Springer-Verlag, 2003.
[7] A. Datta and A. Derek and J. C. Mitchell and D. Pavlovic. A Derivation System
for Security Protocols and its Logical Formalization. Journal of Computer
Security (Special Issue of Selected Papers from CSFW-16), 52 pages, to appear,
2005.
[8] D. Dolev and A. Yao. On the Security of Public Key Protocols. IEEE
Transactions on Information Theory, vol.29, no.2, 1983.
[9] N. Durgin and J. C. Mitchell and D. Pavlovic. A Compositional Logic for
Proving Security Properties of Protocols. Journal of Computer Security, vol.11,
no.4, pp.677-721, 2003.
[10] J. D. Guttman and F. J. Thayer Fábrega. Authentication Tests. IEEE
Symposium on Security and Privacy, pp.96-109, 2002.
[11] K. Hasebe and M. Okada. Inferences on Honesty in Compositional Logic forProtocol Analysis. Proceedings of the International Symposium on Software
Security 2003, LNCS 3233, pp.65-86, 2004.
[12] K. Hasebe and M. Okada. Non-monotonic Properties for Proving Correctness
in a Framework of Compositional Logic. Proceedings of the workshop on
Foundations of Computer Security ’04, pp.97-113, 2004.

17

Hasebe and Okada[13] G. Lowe. Breaking and Fixing the Needham-Schroeder Public-key Protocol
Using FDR. Tools and Algorithms for the Construction and Analysis of Systems(TACAS), vol.1055, pp.147-166, 1996.
[14] G. Lowe. A Hierarchy of Authentication Speciﬁcations. Proceedings of the 10th
Computer Security Foundations Workshop, pp. 31-43, 1997.
[15] R. Needham and M. Schroeder. Using Encryption for Authentication in Large
Networks of Computers. Communications of the ACM, vol.21, no.12, pp.993999, 1978.
[16] C. Meadows and D. Pavlovic. Deriving, Attacking and Defending the GDOI
Protocol. Proceedings of 9th European Symposium on Research in Computer
Security. pp.53-72, 2004.
[17] G. Takeuti. Proof Theory (2nd edition). North-Holland. 1987.
[18] F. J. Thayer Fábrega, J. C. Herzog and J. D. Guttman. Strand Spaces: Why
is a Security Protocol Correct? Proceedings of the 1998 IEEE Symposium on
Security and Privacy, pp.160-171, 1998.
[19] K. N. Venkataraman. Decidability of the Purely Existential Fragment of the
Theory of Term Algebras. Journal of the ACM, vol.34 no.2, pp.492-510, 1987.
[20] T. Y. C. Woo and S. S. Lam. Verifying authentication protocols: Methodology
and example. Proceedings of the International Conference on Network Protocols,
1993.

A

Some Derived Rules on Honesty

In this appendix, we present some rules on honesty (called honesty rules),which are explicitly or implicitly used to prove security protocols correct in
the protocol logics of [9,7,16]. Although we omit the formal proofs, we caneasily prove that these rules are derived rules in BPL. We also show a simple
example of correctness proof (i.e., the non-injective agreement property of the
Needham-Schroeder-Lowe protocol from the responder’s view) in the system
where the notion of honesty (denoted by Honest(⃗αP )) is introduced as an
atomic formula and the honesty rules as axioms.
Honesty rules
The honesty rules with respect to P ’s role α⃗ P (≡ P acts1 m1 ; · · · ; P actsk mk )are the following formulas, and we admit the formulas obtained by replacing
each sends with receives or generates.
(Hon 1) ∀m(P sends m ∧ Honest(⃗
αP ) → m ∈ Sends(⃗
αP ))(Hon 2) ∀m(P sends m∧Honest(⃗
αP ) → P sends mi ∨m ∈ Sends(⃗
αP )−{mi })(Hon 3) P sends mi ∧ Honest(⃗
αP ) → P actsi−1 mi−1 ; P sends mi18

Hasebe and Okada

The following rules (1′ ) and (2′ ) are variants of (1) and (2), respectively.
(Hon 1′ ) ∀m′ (∃m(P sends m∧m′ ⊆ m)∧Honest(⃗
αP ) → m′ ⊆ m′′ ∈ Sends(⃗
αP ))(Hon 2′ ) ∀m′ (∃m(P sends m ∧ m′ ⊆ m) ∧ Honest(⃗
αP ) → P sends mi ∨ m′ ⊆m′′ ∈ Sends(⃗
αP ) − {mi })Here, the set theoretical notation such as m ∈ Sends(⃗
αP ) is the same abbreviation used in Deﬁnition 2.3 in Section 2.3. The abbreviation m′ ⊆ m′′ ∈Sends(⃗
αP ) denotes the formula m′ ⊆ m′′1 ∨ m′ ⊆ m′′2 ∨ · · · ∨ m′ ⊆ m′′j , whereSends(⃗
αP ) = {m′′1 , . . . , m′′j }.
Note that these rules (1), (2) and (3) correspond to the rules introducedin our previous works [11,12]: Substitution, Matching and Deriving anotheraction, respectively. See [11,12] for the intuitive meanings of these rules.
Proof of the non-injective agreement of the NS protocol from responder’s view
Init

Resp[A, B, N1 , N2 ] ⊢ Resp[A, B, N1 , N2 ](1)(1), NV2

Resp[A, B, N1 , N2 ]⊢ ∃m1 m2 (A rec m1 ; A sen m2 ∧ {N1 , N2 , B}A ⊆ m1 ∧ N2 ⊆ m2 )(2)

Resp[A, B, N1 , N2 ] ∧ Honest(Init[P, Q, n1 , n2 ])⊢ N1 = n1 ∧ N2 = n2 ∧ B = Q(3)

Resp[A, B, N1 , N2 ] ∧ Honest(Init[P, Q, n1 , n2 ])⊢ A sen {N2 }B ∨ N2 ⊆ {n1 , A}Q(4)

Resp[A, B, N1 , N2 ] ∧ Honest(Init[P, Q, n1 , n2 ])⊢ A sen {N2 }B(5)Resp[A, B, N1 , N2 ] ∧ Honest(Init[P, Q, n1 , n2 ])⊢ A gen n1 ; A sen {n1 , A}Q ; A rec {n1 , n2 , Q}A ; A sen {n2 }Q(6)

Resp[A, B, N1 , N2 ] ∧ Honest(Init[P, Q, n1 , n2 ])⊢ A gen N1 ; A sen {N1 , A}B ; A rec {N1 , N2 , B}A ; A sen {N2 }B(6)′(2), Hon 1 , Eq(2), Hon 2′(4), Eq(5), Hon 3(2), (6), Eq

19