Computational Semantics for First-Order Logical Analysis of
Cryptographic Protocols
Gergei Bana, Koji Hasebe, and Mitsuhiro Okada
1

SQIG - Instituto de Telecomunicações andDepartment of Mathematics, IST, Technical University of Lisbon, Portugal
2
Graduate School of Systems and Information Engineering, University of Tsukuba, Japan3
Department of Philosophy, Keio University, Tokyo, Japangbana@math.ist.utl.pt hasebe@iit.tsukuba.ac.jp
mitsu@abelard.flet.keio.ac.jp

Abstract. This paper is concerned about relating formal and computational models of cryptography in case of active adversaries when formal security analysis is done with ﬁrst orderlogic As opposed to earlier treatments, we introduce a new, fully probabilistic method to assign computational semantics to the syntax. The idea is to make use of the usual mathematical treatment of stochastic processes, hence be able to treat arbitrary probability distributions,non-negligible probability of collision, causal dependence or independence, and so on. We
present this via considering a simple example of such a formal model, the Basic Protocol
Logic by K. Hasebe and M. Okada [20], but we think the technique is suitable for a wide
range of formal methods for protocol correctness proofs. We ﬁrst review our framework of
proof-system, BPL, for proving correctness of authentication protocols, and provide computational semantics. Then we give a full proof of the soundness theorem. We also comment on
the differences of our method and that of Computational PCL.
Keywords. cryptographic protocols, formal methods, ﬁrst order logic, computational semantics

1

Introduction

In the past few years, linking the formal and computational models of cryptography has becomeof central interest. Several different methods have emerged for both active and passive adversaries.
In this paper we consider the relationship of the two models when formal security analysis is donewith ﬁrst order logic. Protocol correctness is analyzed by deﬁning a syntax with adding some
additional axioms (expressing security properties etc.) to the usual axioms and inference rulesof ﬁrst order logic and then proving some security property directly, instead of eliminating thepossibility of successful (formal) adversaries. A logical proof then ensures that the property willbe true in any formal model (semantics) of the syntax. The link to the computational world thenis done by assigning a computational semantics (instead of formal) to the syntax, proving that theaxioms and inference rules hold there, and hence a property correct in the syntax must be truein the computational model. However, as it turns out, it is not unambiguous how to deﬁne thecomputational semantics, and when a property should be deemed “true” computationally.
Recently, Datta et al. in [13] gave a computational semantics to the syntax of their Protocol
Composition Logic of [16, 12] (cf. also [1] for a protocol composition logic project overview).
In their treatment, every action by the honest participants is recorded on each (non-deterministic)
execution trace, and bit strings emerging later are checked whether they were recorded earlier andto what action they corresponded (the only actions of the adversary that are recorded are send andreceive). This way, they ﬁrst deﬁne whether a formula is true on a particular trace (more exactly
this is only true for a formula not containing their predicate Indist), and they say the formula istrue in the model if it is true on an overwhelming number of traces. This method however, since it
focuses on coincidences on individual traces, discards a large amount of information carried by theprobabilistic structure of the protocol execution, and deﬁnes satisfaction and validity of formulas
ignoring that information. As the comparisons are done on each trace separately it is not possible
to track independence, correlations. But there are more serious problems too, as we will discusslater - such as, some of the syntactic axioms are deﬁned through the semantics. We do not claimthat it is impossible to ﬁx these issues in their framework, but we suggest a different viewpoint inwhich these issues can be easily eliminated.
Our approach puts more emphasis on probabilities. Instead of deﬁning what is true on eachtrace, we say - roughly speaking - that a property is true in the model if a “cross-section” oftraces provides the right probabilities for computational realizations of the property in question.
An underlying stochastic structure ensures that can detect if something depends on the past or doesnot. It is not coincidences on traces that we look for, but indistinguishable probability distributions.
We introduce our method on a rather simple syntax, namely, a somewhat modiﬁed version of
Basic Protocol Logic (or BPL, for short) by K. Hasebe and M. Okada [20] and leave extensions tomore complex situations such as the Protocol Composition Logic to future work. The reason forthis is partly to avoid distraction by an elaborate formal model from the main ideas, but also thata complete axiomatization of the syntax used by Datta et al. for their computational PCL has not
yet been published anywhere, important details of the formalization is not yet publicly available.
We would like to emphasize though that our point is not to give a computational semantics to BPL
but to provide a technique that works well in much more general situations as well.
BPL is a logical inference system to prove correctness of a protocol. Originally, it included
signatures as well, but for simplicity, we leave that out from this analysis. BPL was deﬁned togive a simple formulation of a core part of the protocol logics (PCL) of [16, 12, 11] for provingsome aimed properties in the sense of [25, 22] within the framework of ﬁrst order logic; all notions
and assumptions are strictly formulated by the ﬁrst order logical language explicitly. Contrary to
PCL, in BPL there are no explicit encrypt, decrypt, match actions, only nonce generation, send
and receive. The version which we utilized as a simple sample of formal rule-based model in thispaper does not accomodate some correctness proofs such as secrecy-properties although one could
extend BPL to support them. Besides the usual axioms and derivation rules of ﬁrst order logic,
further axioms set the behavior of equality and subterm relations of terms created via pairing andencryption, two nonce-veryﬁcation axioms incorporating the notion that only the person with thecorrect decryption key can read what is inside an encryption, and an axiom about the order of
events in traces. Although this system is very simple, given a protocol (as we will indicate in thecase of agreement in NSL), the nonce-veryﬁcation axioms forcing certain messages to be included
in others, and then the term axioms restricting what a certain pair of terms in a subterm relation
can possibly be, the required property can be veriﬁed.
We ﬁrst give the axiomatic system in ﬁrst-order predicate logic for proving the agreement
properties. A message is represented by a ﬁrst-order term that uses encryption and pairing symbols,
an atomic formula is a sequence of primitive actions (as send, receive and generate) of principals
on terms. We set some properties about nonces and cryptographic assumptions as non-logicalaxioms, and give a speciﬁc form of formulas, called query form, which has enough expressive
power to specify our intended authentication properties.
Although BPL is sound with respect to formal semantics as shown in [20] with the traditional(Tarskian) model-theoretic formal semantics based on the free term algebra domain, in order toensure soundness for computational semantics, some modiﬁcations of the original syntax of BPL
were necessary:
1. Instead of denoting encryptions as {m}A , which was used in the original version of thepurely symbolic model-based BPL inference system, we indicate the random seed of the encryption as {m}rA (as Datta et al. do). As it turned out, a consistent computational interpretation ismuch harder, if not impossible without the random seed in the syntax.
2. The original subterm and equiterm axioms were not all computationally sound so we justtake a certain subset, the elements of which we know that they are computationally sound. We are
not taking all the sound term axioms, as it is not known how to give a complete characterizationof them. 4
The original BPL also proved completeness for formal semantics with the original set of axioms, however, we do not consider completeness in this paper. It is an open question whether
anything about completeness can be said in the computational case.
We then deﬁne the computational semantics. This involves giving a stochastic structure that
results when the protocol is executed. Principals output bit strings (as opposed to terms) with certain probability distributions. The bit strings are then recorded in a trace as being generated, sentor received by some principal. This provides a probability distribution of traces. We show how toanswer whether a bit string corresponding to a term was sent around with high probability or not.
For example a formal term {M }rA was sent around in the computational model if a cross-sectionof all traces provides the correct probability distribution that corresponds to sending {M }rA . Or, anonce N was generated, if another cross- section provides the right probabilities, and that distribution must be independent of everything that happened earlier. This way we deﬁne when a certain
formula in the syntax is true in the computational semantics. We then analyze whether the axiomsof the syntax are true in the semantics, and if they are, then we conclude that a formula that can beproved in the syntax is also true in the semantics.
Related Work. Formal methods emerged from the seminal work of Dolev and Yao [15],whereas computational cryptography grew out of the work of Goldwasser and Micali [17]. The
ﬁrst to link the two methods were Abadi and Rogaway in [3] ”soundness” for passive adversaries
in case of so-called type-0 security. A number of other papers for passive adversaries followed,
proving ”completness” [23, 5], generalizing for weaker, more realistic encryptions schemes [5],considering purely probabilistic encryptions [19, 5], including limited models for active adversaries [21], addressing the issue of forbidding key-cycles [4], considering algebraic operations andstatic equivalence [8, 2]. Other approaches including active adversaries are considered by Backes
et al. and Canetti in their reactive simulatability [6] and universal composability [10] frameworks,
respectively. Non trace properties were investigated elsewhere too, however, not in the context ofﬁrst order logic. A brief account of this present work was given in [7].
Organization of this paper. In Section 2, we outline the syntax of Basic Protocol Logic. In
Section 3, we give a computational semantics to Basic Protocol Logic, and discuss soundness.
Finally, in Section 4, we conclude and present directions for future work.
4

The uses of subterm and equiterm relations, such as s ⊆ t and s = t, are essential for correctness
proofs of protocols in general, including BPL and PCL. Any symbolic term model, hence, should reﬂect
the symbolic term structures, and such a term model maybe called a ”standard” model with respect tosubterm and equiterm relations. BPL’s symbolic semantics takes such standard term model which alsosatisfy certain properties for nonce-veriﬁcations, which are listed as non-logical axioms in our BPL syntax.
Our result 2 above shows that only the truth of a certain useful subset of the subterm theory axioms ispreserved under computational interpretation. As we will show, the nonce-veriﬁcation axioms turn out tobe sound.

2

Basic Protocol Logic

In this section, we present the syntax of Basic Protocol Logic modiﬁed to be suitable for computational interpretation. For the original BPL, please consult [20].
2.1

Language

Sorts and terms. Our language is order-sorted, with sorts coin , name, nonce and message
such that terms of sorts name and nonce are terms of sort message. Let Cname be a ﬁnite setof constants of sort name (which represent principal names), and Cnonce a ﬁnite set of constantsof sort nonce. Let Ccoin be a ﬁnite set of constants of sort coin. The sort coin represent the
random input of encryptions. We require countably inﬁnite variables for each sort. We will use
A, B, . . . , A1 , A2 , . . . (Q, Q′ , . . . , Q1 , Q2 , . . ., resp.) to denote constants (variables, resp.) of sort
name, N, N ′ , . . . , N1 , N2 , . . . (n, n′ , . . . , n1 , n2 , . . ., resp.) denote constants (variables, resp.) of
sort nonce, r, r′ , . . . , r1 , r2 , . . . (s, s′ , . . . , s1 , s2 , . . ., resp.) denote constants of sort coin (variables of sort coin, resp.). The symbols m, m′ , . . . , m1 , m2 , . . . are used to denote variables of sortmessage and M, M ′ , . . . , M1 , M2 , . . . to denote constants of sort message (that is, either nameor nonce). Let P, P ′ , . . . , P1 , P2 , . . . denote any term of sort name, let ρ, ρ′ , . . . , ρ1 , ρ2 , . . . denoteanything of sort coin, and let ν, ν ′ , . . . denote any term of sort nonce. Compound terms of sortmessage are built from constants and variables, and are deﬁned by the grammar:
t ::= M | m | 〈t, t〉 | {t}ρP .
Where again, M ∈ Cname ∪ Cnonce , m is any variable of sort message, P is any constant or variableof sort name, and ρ is any constant or variable of sort coin. For example, 〈〈A1 , {〈n, A2 〉}rQ 〉, m〉
is a term. We will use the shorter {n, A2 }rQ instead of {〈n, A2 〉}rQ . We will use the meta-symbols
t, t′ , . . . , t1 , t2 , ... to denote terms.
Formulas. We introduce a number of predicate symbols: P generates ν,
P receives t, P sends t, t = t′ , t ⊆ t′ , t ⊆P t′ , t ⊆¬P t′ and |t1 ⊆ t2 ⊆ t3 | which represent“P generates a fresh value ν as a nonce”, “P receives a message of the form t”, “P sends a message of the form t”, “t is identical with t′ ”, “t is a subterm of t′ ”, “t is a subterm of t′ such thatt can be received from t′ decrypting only with the private key of P ”, “t is a subterm of t′ suchthat t can be received from t′ without decrypting with the private key of P ”, “t1 ⊆ t2 ⊆ t3 andthe only way t1 occurs in t3 is within t2 ”, 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. We also introduce the trace predicate P1 acts 1 t1 ; P2 acts 2 t2 ; · · · ; Pk acts k tk . A
trace predicate is used to represent a sequence of the principals’ actions such as “P sends a
message m, and after that, Q receives a message m′ ”. Atomic formulas are either of the form
P1 acts 1 t1 ; P2 acts 2 t2 ; · · · ; Pk acts k tk , or t = t′ , or t ⊆ t′ , or t ⊆P t′ , or t ⊆¬P t′ or|t1 ⊆ t2 ⊆ t3 |. The ﬁrst one we also call trace formula. We also use α1 ; · · · ; αk (or α in short) todenote P1 acts 1 t1 ; · · · ; Pk acts k tk (where k indicates the length of α). When every Pi is identical with P for 1 ≤ i ≤ k, then αP denotes such a trace formula. For α (≡ α1 ; · · · ; αm ) andβ (≡ β1 ; · · · ; βn ), we say β includes α (denoted by α ⊆ β), if there is a one-to-one, increasing
function j : {1, ..., m} → {1, ..., n} such that αi ≡ βj(i) . Formulas are deﬁned by
¯ ¯
¯
¯
¯
¯
¯
¯
¯
¯
¯
¯ ¯
¯
¯
¯
¯
¯
¯
¯
¯
¯
ϕ ::= α¯t1 = t2 ¯t1 ⊆ t2 ¯t1 ⊆P t2 ¯t1 ⊆¬P t2 ¯|t1 ⊆ t2 ⊆ t3 |¯¬ϕ¯ϕ∧ϕ¯ϕ∨ϕ¯ϕ → ϕ¯∀mϕ¯∃mϕwhere m is any variable. Those variables in a formula that are bound by the binding operators ∃and ∀ will be referred to as bound variables, those that are not will be referred to as free variables.

We use the meta expression ϕ[m] to indicate the list of all free variables m occurring in ϕ. We
will also use ϕ[M , m] to specify some constants M that occur in ϕ where m again is all freevariables in ϕ.
Finally, order-preserving merge of trace formulas α (≡ α1 ; · · · ; αl ) and β (≡ β1 ; · · · ; βm )is a trace formula δ (≡ δ1 ; · · · ; δn ) if there are one-to-one increasing functions j α : {1, ..., l} →{1, ..., n}, j β : {1, ..., m} → {1, ..., n} such that αi ≡ δj α (i) , βi ≡ δj β (i) , and the union of theranges of j α and j β cover {1, ..., n}. δ is called a strict order-preserving merge if, furthermore,
the ranges of j α and j β are disjoint.
Roles. Roles of principals are described by trace formulas of the form αA ≡ A acts 1 t1 ;· · · ; A acts k tk . Honest principals (those who generate keys, encryptions, nonces honestly, anddon’t share information with the adversary) are denoted by constants. Nonces and coins that theseparticipants generate are also denoted by constants. Protocols are a set of roles together with a listof values that the principals have to agree on.
Example 1. (Roles of the Needham-Schroeder-Lowe protocol)
We consider the Needham-Schroeder-Lowe public key protocol [24], whose informal description
is as follows.
1. A → B: {n1 , A}rB1
2. B → A: {n1 , n2 , B}rB1
3. A → B: {n2 }rB2
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.
InitA
N SL [Q2 , N1 , n2 , r1 , s2 , r3 ] ≡A generates N1 ; A sends {N1 , A}rQ12 ; A receives {N1 , n2 , Q2 }sA2 ; A sends {n2 }rQ32
RespB
N SL [Q1 , n1 , N2 , s1 , r2 , s3 ] ≡B receives {n1 , Q1 }sB1 ; B generates N2 ; B sends {n1 , N2 , B}rQ21 ; B receives {N2 }sB3
They further have to agree that Q1 = A, Q2 = B, n1 = N1 , n2 = N2 .
Remark 1. Notice that, for example, in the responder’s role, we wrote B receives {n1 , Q1 }sB1 instead of B receives {m, Q1 }sB1 , although n1 may come from the adversary. This is, because wewill assume in the semantics, that because of tagging, it is recognizable whether a string is anonce or not. But, the distribution of n1 , if coming from the adversary, may not follow the correct
distribution of nonces.
2.2

The Axioms of Basic Protocol Logic

We extend the usual ﬁrst-order predicate logic with equality by adding the following axioms (I),(II) and (III).
Remark 2. For the axioms below to be more understandable, we make a few remarks about thesemantics that we will deﬁne later. For each η, names will be interpreted as some constant bit
string names of the participating principals, such that the principals corresponding to constants
will generate nonces, keys and encrypt honestly. Other possible principles may be malicious, creating encryptions and nonces dishonestly. Nonces will have to have a certain ﬁxed length, theinterpretation of nonce constants will have to have the correct distribution and be independent ofwhat happened earlier. The interpretation of coins will have to have the correct form for the random feed into the encryption, and further, constants of sort coin will have to have the correctdistribution, and when used for encryption, such a constant coin will have to have a distributionthat is independent of the distribution of encrypted plaintext as well as independent of everythingthat happened earlier. The public keys of constants will also have to have the correct distributions
and be generated at the very beginning. The interpretation of encryptions and pairing are deﬁned
the intuitive way.
(I) Term axioms. Consider the set C¯ of all variables and constants of each of sort name, sort nonce
and sort coin. Let Ā be the free algebra constructed from C¯ via 〈·, ·〉 and {·}·· (with the appropriate
sorts in the indexes of the encryption terms) not including constants and variables of sort coin.
The elements of Ā are of sort message. Let ⊆Ā denote the natural subterm relation in Ā. Let
′
Ā ′
t ⊆Ā
t such that t can be received from t′ by decrypting encryptions by theP t mean that t ⊆Ā
key of P only. Let t ⊆¬P t′ mean that t ⊆Ā t′ such that t can be received from t′ by decrypting
encryptions that are not done with the key of P .
Let |t1 ⊆Ā t2 ⊆Ā t3 | mean that t1 ⊆Ā t2 ⊆Ā t3 and the only way t1 occurs in t3 is within
t2 . That is: |t1 ⊆Ā t2 ⊆Ā t3 | := t1 ⊆Ā t2 ⊆Ā t3 ∧ ∀t(t1 ⊆Ā t ⊆Ā t3 → t2 ⊆Ā t ∨ (t ⊆Ā
t2 ∧ ∀t4 (t2 ⊆Ā t4 → 〈t, t4 〉 ̸⊆Ā t3 ∧ 〈t4 , t〉 ̸⊆Ā t3 ))).
We postulate the following term axioms. Here, and also later by using ⊆(¬)P we mean two
sentences, one with and one without ¬. Let m be all variables occurring in the corresponding
terms. We require these for all A, B ∈ Cname :(a) If t = t′ is true in Ā, then ∀m(t = t′ ) is axiom. If t ⊆Ā t′ is true in Ā, then ∀m(t ⊆ t′ ) is axiom. If
′
Ā ′
Ā
′
t ⊆Ā
P t is true in Ā, then ∀m(t ⊆P t ) is axiom. If ∀mQ(Q ̸= P1 ∧ ... ∧ Q ̸= Pk → t ⊆¬Q t ) istrue in Ā for all (possibly equal) constant or variable substitutions to m and Q, then it is an axiom.
(b) ∀m(t1 = t2 → t2 = t1 ), ∀m(t1 = t2 ∧ t2 = t3 → t1 = t3 ), ∀m(t1 ⊆ t2 ∧ t2 ⊆ t3 → t1 ⊆ t3 ),(c) ∀mP (t1 ⊆(¬)P t2 → t1 ⊆ t2 ), ∀mP (t1 = t2 → t1 ⊆(¬)P t2 ), ∀mP (t1 ⊆(¬)P t2 ∧ t2 ⊆(¬)P t3 →t1 ⊆(¬)P t3 )′(d) ∀mQss′ ({t1 }sQ = {t2 }sQ → t1 = t2 ),(e) ∀m(〈t1 , t2 〉 = 〈t3 , t4 〉 → t1 = t3 ∧ t2 = t4 )(f) ∀mQs({t}sQ ̸= 〈t1 , t2 〉), ∀mQsn({t}sQ ̸= n), ∀mQQ′ s({t}sQ ̸= Q′ )(g) ∀mn(〈t1 , t2 〉 ≠ n), ∀mQ(〈t1 , t2 〉 ≠ Q)(h) ∀m(t ⊆ 〈t1 , t2 〉 → t ⊆ t1 ∨ t ⊆ t2 ∨ t = 〈t1 , t2 〉), ∀mQs(t1 ⊆ {t2 }sQ → t1 = {t2 }sQ ∨′∃mQ′ s′ ({t2 }sQ = {m}sQ′ ∧ t1 ⊆ m))(i) ∀mP (t ⊆P 〈t1 , t2 〉 → t ⊆P t1 ∨ t ⊆P t2 ∨ t = 〈t1 , t2 〉), ∀mQsP (t1 ⊆P {t2 }sQ → t1 =′{t2 }sQ ∨ ∃ms′ ({t2 }sQ = {m}sP ∧ t1 ⊆P m)), ∀msP (t1 ⊆P {t2 }sP → t1 = {t2 }sP ∨ t1 ⊆P t2 ))(j) ∀mP (t ⊆¬P 〈t1 , t2 〉 → t ⊆¬P t1 ∨ t ⊆¬P t2 ∨ t = 〈t1 , t2 〉), ∀mQsP (t1 ⊆¬P {t2 }sQ → t1 =′{t2 }sQ ∨ ∃mQ′ s′ (Q′ ̸= P ∧ {t2 }sQ = {m}sQ′ ∧ t1 ⊆ m))(k) ∀mn(m ⊆ n → m = n), ∀mQ(m ⊆ Q → m = Q)(l) ∀m|t1 ⊆ t2 ⊆ t3 | is an axiom if |t1 ⊆Ā t2 ⊆Ā t3 |[M /m] holds for all M vector of constans of appropriate sort.

(II) Rules for trace formulas. We postulate that β → α for α ⊆ β and γ1 ∨ · · · ∨ γn ↔ α ∧ β,
where γi ’s are the list of order-preserving merges of α and β. These axioms express the intuition
that if a trace “happens”, then a subtrace of it also happens, and two traces happen if and only if
one of their possible merges happen.
(III) Axioms for relationship between properties. We introduce the following set of formulas
as non-logical axioms. These axioms represent some properties about nonces and cryptographic
assumptions.
(1) Ordering:∀Q1 Q2 nm(n ⊆ m → ¬(Q2 sends/receives/generates m; Q1 generates n)).

(2) Nonce veriﬁcation 1: For each A, B constants of sort name, r constant of sort coin, we
postulate∀Qn1 m5 m6 (A generates n1 ; Q receives m5 ∧ n1 ⊆¬B m5∧ ∀m7 (A sends m7 ∧ n1 ⊆ m7 → |n1 ⊆ {m6 }rB ⊆ m7 |)→ ∃m2 m3 m4 (A sends m2 ; B receives m3 ; B sends m4 ; Q receives m5
n1 ⊆ m2 ∧ {m6 }rB ⊆B m3 ∧ n1 ⊆ m4 ))(3) Nonce veriﬁcation 2: For each A, B C of sort name (where A and C may coincide), r1 , r2constants of sort coin, we postulate we postulate∀n1 m5 m6 m8 (A generates n1 ; C receives m5 ∧ n1 ⊆¬B m5∧ ∀m7 (A sends m7 ∧ n1 ⊆ m7 → |n1 ⊆ {m6 }rB1 ⊆ m7 |)∧ ∀m4 (B sends m4 ∧ n1 ⊆ m4 → |n1 ⊆ {m8 }rC2 ⊆ m4 |)∧ ∀m10 (¬(C sends m10 ∧ n1 ⊆ m10 ) ∨ A = C)
→ {m8 }rC2 ⊆C m5

There are other possible axiomatizations, but the authors of [20] found this particularly useful(more exactly a somewhat less general version). The meaning of the Ordering axiom is clear.
Nonce verﬁcation 1 and 2 are based on the idea of the authentication-tests [18]. Nonce veriﬁcation
1 means that if A generated a nonce n1 that Q received in m5 , and A only sent n1 encrypted withthe public key of B always in a given form {m6 }rB , and Q received this nonce in some other form,
then the encrypted nonce had to go through B, and before that, it had to be actually sent out by
A. The reason that we require A and B to be names and not arbitrary variables is that we do notwant to require any principals in an arbitrary run to encrypt securely. Nonce veriﬁcation 2 meansthat with the premises of Nonce veriﬁcation 1, and if B sends n1 only inside {m8 }rC2 , and C neversends n1 unless C = A, then C had to receive {m8 }rC2 so that it is accessible to him.
2.3

Query form and correctness properties

We introduce a general form of formulas, called query form, to represent our aimed correctness
properties. In order to make the discussion simpler, we consider only the case of two party authentication protocols, however our query 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 1. (Query form) Query form is a formula of the following form: ∃mHonest(αA ) ∧β B ∧ Only(β B ) → γ
We present the precise deﬁnition of Only(αB ) and of Honest(αA ) in the Appendix. Only(αB )means that B performs only the actions of αB , and nothing else, whereas Honest(αA ) represents “A performs only a run of an initial segment of αA which ends with a sending actionor the last action of αA ”. For example, from responder’s (namely, B’s) view, the non-injective
agreement of the protocol Π = {αA [B/Q2 , N1 , n2 , r1 , s2 ], β B [A/Q1 , n1 , N2 , s1 , r2 ]} canbe described as the following formula: ∃n1 n2 s1 s2 Honest(αA )[Q2 , N1 , n2 , r1 , s2 ] ∧ (β B ∧Only(β B )[A/Q1 , n1 , N2 , s1 , r2 ]) → αA [B/Q2 , N1 , N2 /n2 , r1 , r2 /s2 ] ∧ n1 = N1
Example 2. (Agreement property in the responder’s view of the NSL protocol)
The initiator’s honesty of the NSL protocol is Honest(InitA
N SL )[Q1 , N1 , n2 , r1 , s2 , r3 ] ≡0
1
1
A generates N1 ; A sends {N1 , A}rQ11∀n3 ¬(A generates n3 )BC@@ ∧∀m4 ¬(A sends m4 ) A ∨ B ∧∀n3 (A generates n3 → n3 = N1 ) r1 C
@ ∧∀m4 (A sends m4 → m4 = {N1 , A}Q ) A
1∧∀m5 ¬(A receives m5 )∧∀m5 ¬(A receives m5 )
00

0

11
A generates N1 ; A sends {N1 , A}rQ11 ; A receives {N1 , n2 , Q1 }sA2 ; A sends {n2 }rQ31
B ∧∀n3 (A generates n3 → n3 = N1 )
CC
CC
∨B
AA
@ ∧∀m4 (A sends m4 → m4 = {N1 , A}rQ1 ∨ m4 = {n2 }rQ2 )1
1
s2∧∀m5 (A receives m5 → m5 = {N1 , n2 , Q1 }A )We refer to Remark 1 for an explanation why nonce variables are used for even those nonces thatare sent by the adversary.
The main steps of proving agreement from the responder’s view are the following:B∃n1 s1 s3 RespBN SL ∧ Only(RespN SL )[A/Q1 , n1 , N2 , s1 , r2 , s3 ]implies by the 1st nonce veriﬁcation axiom that∃m3 m4 (B sends {n1 , N2 , B}rA2 ; A receives m3 ; A sends m4 ; B receives {N2 }sB3 ∧∧{n1 , N2 , B}rA2 ⊆A m3 ∧ N2 ⊆ m4 )).
Then from this together with ∃Q1 n2 s2 Honest(InitA
N SL )[Q1 , N1 , n2 , r1 , s2 , r3 ] it follows that
{n1 , N2 , B}rA2 ⊆A {N1 , n2 , Q1 }sA2 .
From this, using the term axioms (f), (i) and (k), we get that {N1 , n2 , Q1 }sA2 = {n1 , N2 , B}rA2 ,and then from (d) and (e) that n1 = N1 , n2 = N2 , Q1 = B. Then with a similar argument{N1 , A}rB1 = {n1 , A}sB1 and {n2 }rB3 = {N2 }sB3 are also proven, from which ﬁnally the completed initiator’s role, InitA
N SL [B, N1 , N2 , r1 , r2 , r3 ] follows. That is, the initiator also ﬁnishedthe protocol and the values agree.

3Computational Semantics

3.1

Computational Asymmetric Encryption Schemes

The fundamental objects of the computational world are strings, strings = {0, 1}∗ , and familiesof probability distributions over strings. These families are indexed by a security parameter η ∈param := {1}∗ ≡ N (which can be roughly understood as key-length).
Deﬁnition 2 (Negligible Function). A function f : N → R is said to be negligible, if for anyc > 0, there is an nc ∈ N such that |f (η)| ≤ η −c whenever η ≥ nc .
Pairing is an injective pairing function [·, ·] : strings×strings → strings. We assume that changing a bit string in any of the argument to another bit string of the same length does not inﬂuence
the length of the output of the pairing. An encryption scheme is a triple of algorithms (K, E, D)
with key generation K, encryption E and decryption D. Let plaintexts, ciphertexts, publickey andsecretkey be nonempty subsets of strings. The set coins is some probability ﬁeld of (possibly
inﬁnite) bit-strings that stands for coin-tossing, i.e. feeds randomness into the Turing-machinesrealizing the algorithms.
Deﬁnition 3 (Encryption Scheme). A computational asymmetric encryption scheme is a tripleof algorithms E = (K, E, D) where:– K : param × coins → publickey × secretkey is a key-generation algorithm with param = {1}∗ ,– E : publickey × plaintexts × coins → ciphertexts ∪ {⊥} is an encryption algorithm, and– D : secretkey × strings → plaintexts ∪ {⊥} is such that for all (e, d) ∈ publickey × secretkey
and c ∈ coins
D(d, E(e, m, c)) = m for all m ∈ plaintexts and (e, d) output of the key generation.

All these algorithms are computable in polynomial time with respect to the length of their input.
In this paper, we assume that the encryption scheme satisﬁes adaptive chosen ciphertext security (CCA-2) deﬁned the following way:Deﬁnition 4 (Adaptive Chosen Ciphertext Security). A computational public-key encryption
scheme E = (K, E, D) provides indistinguishability under the adaptive chosen-ciphertext attack if
for all PPT adversaries A and for all sufﬁciently large security parameter η:| Pr[ (e, d) ←− K(1η ); b ←− {0, 1} ;m0 , m1 ←− AD1 (·) (1η , e);c ←− E(e, mb );g ←− AD2 (·) (1η , e, c) :b=g
] − 21 | ≤ neg (η)
The oracle D1 (x) returns D(d, x), and D2 (x) returns D(d, x) if x ̸= c and returns ⊥ otherwise.
The adversary is assumed to keep state between the two invocations. It is required that m0 and m1
be of the same length. The probability includes all instances of randomness: key generation, thechoices of the adversary, the choice of b, the encryption.
In the above deﬁnition, what the brackets of the probability contains, is a commonly used shorthand for the following game: First a public key-private key pair is generated on input 1η , as well
as a random bit b with probabilities 1/2 – 1/2. Then, the adversary is given the public key, and adecryption oracle, which it can invoke as many times as wished, and at the end it comes up with apair of bit strings m0 , m1 of the same length, which it hands to an encryption oracle. Out of these
two messages, the oracle encrypts the one determined by the initial choice of random bit b, andhands the ciphertext back to the adversary. The adversary can further invoke the decryption oracle(which decrypts everything except for the ciphertext computed by the encryption oracle). At theend, the adversary has to make a good guess for b. This guess is g, and the adversary wins if theprobability of making a good guess signiﬁcantly differs from 1/2.
It was shown in [9] that the above deﬁnition is equivalent with another that seems stricter atﬁrst, namely, when an n-tuple of encryption and decryption oracles are given, each with separate
encryption and decryption keys, but using the same bit b to choose from the submitted plaintexts.
The adversary is allowed to invoke the oracles in any order but it cannot submit a message thatwas received from an encryption oracle to the corresponding decryption oracle.
3.2

Filtrations and Stopping Times

In the following, we discuss the mathematical objects that we use to represent a computational
execution of a protocol. Our plan is to deﬁne a computational semantics, show that the syntactic
axioms hold if the encryption scheme is CCA-2 secure, and, as a result, if the query-form (oranything else) is provable in the syntax, it must be true in any computational model.
First, since probabilities and complexity are involved, we need a probability space for eachvalue of the security parameter. Since time plays an important role in the execution, what we needis the probability space for a stochastic process. For the presentation here, we limit ourselves toﬁnite probability spaces as explaining the notion of measurability and stochastic processes is much
simpler this way, but for anyone familiar with these notions in inﬁnite spaces it is near to trivial togeneralize the method to allowing inﬁnite steps (but polynomial expected runtime). So, here weassume that for each security parameter, there is a maximum number of execution steps nη . The
following notions that we introduce are standard in probability theory.

We will denote the ﬁnite probability space for an execution of a protocol with security parameter η by Ω η , subsets of which are called events. Let F η denote the set of all subsets of Ω η(including the empty set). A subset containing only one element is called an elementary event. The
set Ω η is meant to include all randomness of an execution of the protocol. A probability measurepη assigns a probability to each subset such that it is additive with respect to disjoint unions of sets
(so it is enough to assign a probability to each element of Ω η , then the probability of any subset
can be computed). When it is clear which probability space we are talking about, we will just use
the notation Pr.
In order to describe what randomness was carried out until step i ∈ {0, 1, ..., nη }, we assign
a subset Fiη ⊆ F η to each i, such that Fiη is closed under union and intersection, and includes ∅ηand Ω η , and Fiη ⊆ Fi+1
. We also assume that Fnηη = F η , that is, Ω does not include information
η
irrelevant to the protocol execution. The set {Fiη }ni=1 is called ﬁltration. Since everything is ﬁnite,Fiη is atomistic, that is, each element of it can be obtained as a union of disjoint, minimal (withrespect to inclusion) nonempty elements. The minimal nonempty elements are called atoms. We
introduce the notationηPr = {(Ω η , {Fiη }ni=0 , pη )}η∈param .
We included F0η to allow some initial randomness such as key generation. A discrete randomvariable on Ω η is a function on Ω η taking some discrete value. Since Fiη contains the events
determined until step i, a random variable g η depends only on the randomness until i exactly ifg η is constant on the atoms of Fiη ; this is the same as saying that for any possible value c, theset [g η = c] := {ω | g η (ω) = c} is an element of Fiη . In this case, we say that g η is measurablewith respect to Fiη . We will, however need a somewhat more complex dependence-notion. We willneed to consider random variables that are determined by the randomness until step i1 on certain
random paths, but until step i2 on other paths, and possibly something else on further paths. For
this, we have to ﬁrst consider a function J η : Ω η → {0, 1, ..., nη } that tells us which time step toconsider on each ω. This function should only depend on the past, so for each i ∈ {0, 1, ..., nη },we require that the set [J η = i] ∈ Fiη . Such a function is called stopping time. The events thathave occurred until the stopping time J η are contained in
FJη := {S | S ⊆ Ω η , and for all i = 0, 1, ..., nη , S ∩ [J η = i] ∈ Fiη }.
Then, a random variable f η depends only on the events until the stopping time J η iff for each cin its range, [f η = c] ∈ FJη . Furthermore, a random variable hη on Ω η is said to be independentof what happened until J η iff for any S ∈ FJη and a c possible value of hη , Pr([hη = c] ∩ S) =Pr([hη = c]) Pr(S). Finally, it is easy to see that for each random variable f η , there is a stopping
time Jfη such that f η is measurable with respect to FJηf , and Jfη is minimal in the sense that f η is
not measurable with respect to any other FJη if there is an ω such that J η (ω) < Jfη (ω).
Example 3. Let coins be tossed three times, one after the other. Then Ω = {(a, b, c) | a, b, c =0, 1}. Let (1, ·, ·) := {(1, b, c) | b, c = 0, 1}. (0, ·, ·), etc. are deﬁned analogously. At step i = 1,
the outcome of the ﬁrst coin-tossing becomes known. So, F1 = {∅, (0, ·, ·), (1, ·, ·), Ω}. At stepi = 2, the outcome of the second coin becomes known too, therefore F2 , besides ∅ and Ω, contains(0, 0, ·), (0, 1, ·), (1, 0, ·) and (1, 1, ·) as atoms, and all possible unions of these. F3 is all subsets. A
function g that is measurable with respect to F1 , is constant on (0, ·, ·) and on (1, ·, ·), that is, g only
depends on the outcome of the ﬁrst coin tossing, but not the rest. Similarly, an f measurable on
F2 , is constant on (0, 0, ·), on (0, 1, ·), on (1, 0, ·) and on (1, 1, ·). A stopping time is for example
the J that equals the position of the ﬁrst 1, or 3 if there is never 1: J( (a1 , a2 , a3 ) ) = i if ai =1 and ak = 0 for k < i, and J( (a1 , a2 , a3 ) ) = 3 if ak = 0 for all k = 1, 2, 3. The atoms of FJ
are (1, ·, ·), (0, 1, ·), {(0, 0, 1)} and {(0, 0, 0)}.

We will also have to assume that the stopping times are such that they are polynomially decidable,that is, in the execution of a PPT algorithm, the computation of value of a stopping time on an
execution trace should not destroy the polynomial bound. This is not really a restriction as incase of security properties, stopping times are just decided simply by the position of the protocol
execution, carrying out some decryptions, and matching values.
3.3

Stochastic Model for the Computational Execution of BPL

For each value of the security parameter, an execution of the protocol involves some principals. Each principal has a distinct name, a bit-string not longer than the upper bound nη . Eachprincipal generates an encryption-key, decryption-key pair at the initialization. Hence, if Pr =η{(Ω η , {Fiη }ni=0 , pη )}η∈param is the stochastic space of the execution of the protocol, let P η be a setηof (polynomially bounded number of) elements of the form (Aη , (eηA , dηA )) where Aη ∈ {0, 1}n ,ηηηand (eA , dA ) is a pair of probability distributions on Ω η measurable with respect to F0 such thatPr[ω : (eηA (ω), dηA (ω)) ̸∈ Range(K(η, ·))] is a negligible function of η. We assume that if A = B,then (eηA , dηA ) = (eηB , dηB ). The set {P η }η∈param describes all the principals, corrupted and uncorrupted, that take part in the execution at a given security parameter, along with their public andsecret keys. Let P = {P η }η∈param .
For nonces, we choose the following deﬁnition. Since CCA-2 security is length-revealing, wehave to assume that nonces are always of some ﬁxed length mη for each security parameter η. Weηassume mη is at most polynomial in η, and 1/2m is negligible. Let N be a set of elements ofη
the form {N η }η∈param where N η : Ω η → {0, 1}m ∪ {⊥} (taking the value ⊥ means N η has
no bit-string value on that particular execution). This set describes the nonces that were generated
during the execution of the protocol. The nonces generated by honest participants must have someﬁxed distribution (uniform for example) over set of bit strings with the given length and also haveto be independent of what happened earlier when they are being generated, but we will require thislater in the deﬁnition of interpretation of constants and at the deﬁnition of the satisfaction of theformula A generates N .
Let R be a set of elements of the form R = {Rη }η∈param where Rη : Ω η → coins ∪ {⊥}.
Messages: Let the set of messages be M elements of the form M = {M η }η∈param , whereηηM : Ω η → {0, 1}n ∪ {⊥}. For any two messages, M1 , M2 , we will denote that M1 ≈ M2 iffpη [ω : M1 (ω) ̸= M2 (ω)] is a negligible function of η. This way, ≈ is an equivalence notion on
the set of messages. Let DM := M/≈, let DN := N /≈ ⊂ DM , and let
DP := {A ∈ M : (Aη , (eηA , dηA )) ∈ P η for some (eηA , dηA )}/≈ ⊂ DM
We have to deﬁne what we mean by a computational pairing and encryption. For any X, X1 , X2 ∈DM , we write that X =C 〈X1 , X2 〉, if for some (hence for all) M1 = {M1η }η∈param ∈ X1 andM2 = {M2η }η∈param ∈ X2 , the ensemble of random variables {ω 7→ [M1η (ω), M2η (ω)]}η∈paramis an element of X. Further, if A ∈ P, and R ∈ R, then we will write that X =C {X1 }R
A if
for any (hence for all) M1 = {M1η }η∈param ∈ X1 , the ensemble of random variables {ω 7→E(eηA (ω), M1η (ω), R(ω))}η∈param is an element of X. If the value of any of the input distributionsis ⊥ then we take the output to be ⊥ as well. This way, we can consider an element of the freeterm algebra T (DM ) over DM as an element of DM . Let ⊆T (DM ) denote the subterm relation on
T (DM ). This generates a subterm relation ⊆C on DM by deﬁning X1 ⊆C X2 to hold iff there
is an element X ∈ T (DM ) such that X1 ⊆T (DM ) X and X2 =C X. Let for P ∈ DP , let theT (D )T (DM )
notions analogous to ⊆P (⊆¬P respectively) be denoted by ⊆P M and ⊆Cand ⊆CP (⊆¬P¬P
respectively).

For any set of subsets Dη ∈ F η , D = {Dη }η∈η with non-negligible pη (Dη ), we say thatfor P ∈ DP , X1 , X2 ∈ DM , X1 = X2 on D if there are M1 = {M1η }η∈param ∈ X1 andM2 = {M2η }η∈param ∈ X2 with M1η (ω) = M2η (ω) for all ω ∈ Dη . We say that X1 ⊆C X2
T (DM )
(or, X1 ⊆C
X (or,(¬)P X2 ) on D iff there is an element X ∈ T (DM ) such that X1 ⊆T (D)

X1 ⊆(¬)PM X) and X2 =C X on D.
Execution trace: The execution trace is deﬁned as Tr = {Trη }η∈param where Trη : ω 7→
ηTr (ω) with eitherTrη (ω) = P1η (ω) acts η1 (ω) sη1 (ω); ...; Pnηη (ω) (ω) acts ηnη (ω) (ω) sηnη (ω) (ω)
where for each η security parameter, ω ∈ Ω η , nη (ω) is a natural number less than nη , Piη (ω) ∈DP , acts ηi (ω) is one of generates, sends, receives and sηi (ω) ∈ {0, 1}∗ ; or Trη (ω) = ⊥with nη (ω) = 0 meaning that no generate, send or receive action happened. For each η, ω, andi ∈ {1, ..., nη }, let½ η
Pi (ω) acts ηi (ω) sηi (ω) if i ∈ {1, ..., nη (ω)}
Trηi (ω) =⊥ otherwise
We also require that for each i there is a stopping time Ji with Jj (ω) < Jj+1 (ω) for all ω and jsuch that Trηi is measurable with respect to FJηi for all i. Moreover, we require that any of Tr is
PPT computable from the earlier ones.
3.4

Computational Semantics

We now explain how to give computational semantics to the syntax, and what it means that aformula of the syntax is true in the semantics. For a given security parameter, an execution isplayed by a number of participants.
Assumptions. In a particular execution, we assume that the principals corresponding to namesin the syntax (that is, they correspond to elements in Cname ) are regular (non-corrupted). We assume
that these participants generate their keys and encrypt correctly (that is, the keys are properly distributed, and also r is properly randomized) with a CCA-2 encryption scheme, and never use theirprivate keys in any computation except for decryption. For other participants (possibly corrupted),
we do not assume this. (Encrypting correctly is essential to able to prove the nonce veriﬁcation
axioms.) We further assume that pairing of any two messages differs from any nonce and fromany principal name on sets of non-negligible probability (this can be achieved by tagging; in any
case, we will call this tagging condition), and that honestly generated nonces have some ﬁxed distribution over a set of bit strings with ﬁxed length such that their collision probability is negligiblein η. The network is completely controlled by an adversary. The sent and received bit strings arerecorded in a trace in the order they happen. Freshly generated bit-strings produced by the regularparticipants are also recorded. The combined algorithms of the participants and the adversary are
assumed to be probabilistic polynomial time. We also assume that at one time only one action
happens.
Such a situation, with the deﬁnitions of the previous section, produces a computational trace
structure associated with the execution of the form
M = (Π, E, [·, ·], N0 , Pr, P, Tr, ΦC , D),
where D = {Dη }η∈η , Dη ∈ F η a sequence of subsets where we focus our attention with pη (Dη )non-negligible; N0 = {N0η }η is the distribution of correctly generated nonces; ΦC is a one-toone function on Cname ∪ Cnonce ∪ Ccoin such that (i) ΦC (A) ∈ DP for any A ∈ Cname such that(eηΦC (A) , dηΦC (A) ) is measurable with respect to F0 and has the correct key distribution, and for
different constants are independent of each other; (ii) ΦC (N ) ∈ DN for any N ∈ Cnonce andfor different constants the interpretations are not equal on D, and we further require that overη{0, 1}m , ΦC (N )η has the distribution (up to negligible probability) ﬁxed for nonces (i.e. N0η , e.g.
uniform), and ΦC (N )η is independent of FJηΦ (N ) −1 for all η on the condition that [ΦC (N )η ̸= ⊥].
C(More precisely, there is an N ′ ∈ ΦC (N ) such that N ′η is independent of FJηN ′ −1 on the condition
that [N ′η ̸= ⊥]. For Jfη see the paragraph before Example 3); (iii) ΦC (r) ∈ R for any r ∈ Ccoin ,and for different constants the interpretations are not equal on D, and we further require thatover coins, Φ(r)η has the distribution ﬁxed for coins (e.g. uniform), and ΦC (r)η is independent of
FJηΦ (r) −1 for all η on the condition that [ΦC (r)η ̸= ⊥].
CAn extension of ΦC to evaluation of free variables is a function Φ that is the same on constants
as ΦC , and for variables Q, n, m, s of sort name, nonce, message, and coin respectively, Φ(Q) ∈DP , Φ(n) ∈ DN , Φ(m) ∈ DM , and Φ(s) ∈ R hold. Let Φ̄ be deﬁned to be the same as Φ on
constants and variables, and let’s extend the deﬁnition of Φ̄ to any term such that it takes values inΦ(r)T (DM ) by the rules (i) Φ̄(〈t1 , t2 〉) = 〈Φ̄(t1 ), Φ̄(t2 )〉 ; (ii) Φ̄({t}rP ) = {Φ̄(t)}Φ(P ) . Finally, for anyt term, let Φ(t) ∈ DM be deﬁned by Φ(t) =C Φ̄(t).
We say that an ensemble of random variables M = {M η }η∈param such that M η is deﬁned
on Dη is a realization of the term t through Φ on D, which we denote M ≪Φ,D t, if there isan M1 ∈ Φ(t) with M1η (ω) = M η (ω) ̸= ⊥ for all ω ∈ Dη ; and if also t = {t′ }rP , r being a
constant, then we further require that there is an M ′ ∈ Φ(t′ ) such that M ′ ≪Φ,D t′ and Φ(M ′ ) ismeasurable with respect to FJηr −1 .
In the following, we give the interpretation of BPL. Note, that the interpretation of conjunction,
disjunction, negation and conclusion are deﬁned in the most standard manner. We ﬁrst deﬁne whena formula ϕ is satisﬁed by Φ (remember, D = {Dη }η∈η with Dη ∈ F η from M):– For any terms t1 , t2 , ϕ ≡ t1 = t2 is satisﬁed by Φ, iff Φ(t1 ) = Φ(t2 ) on D, ϕ ≡ t1 ⊆ t2
is satisﬁed by Φ iff Φ(t1 ) ⊆C Φ(t2 ) on D, ϕ ≡ t1 ⊆(¬)P t2 is satisﬁed by Φ on D iff
Φ(t1 ) ⊆C(¬)Φ(P ) Φ(t2 ) on D.
– For any terms t1 , t2 , t3 , |t1 ⊆ t2 ⊆ t3 | is satisﬁed by Φ, iff there are X1 , X2 , X3 ∈ T (DM )such that Φ(t1 ) =C X1 , Φ(t2 ) =C X2 and Φ(t3 ) =C X3 on D, such that the bottom of theparsing tree of Xi agrees with the parsing tree of ti , and the interpretation of constants andvariables in ti is given on D by the sub-trees rooted in the corresponding positions in Xi , andfurther that also |X1 ⊆T (DM ) X2 ⊆T (DM ) X3 | holds where this is deﬁned the same way on
T (DM ) as we deﬁned it on Ā, that is, X1 occurs in X3 only within X2 .
– For any term u and acts = sends/receives, ϕ ≡ P acts u is satisﬁed by Φ iff there is apolynomially decidable stopping time J η such that apart from sets of negligible probability,
TrηJ η (ω) (ω) is of the form Aη acts M η (ω) for ω ∈ Dη where M := {M η }η∈param ≪Φ,D u
and A := {Aη }η∈param ≪Φ,D P . We also require that the interpretation of every constant andvariable in u be measurable with respect to FJη . We will denote this as TrJ ≪Φ,D P acts u.
– If acts = generates then the u above is a nonce ν, and so M := {M η }η∈param ≪Φ,D umeans there is an N ∈ Φ(ν) such that M η |Dη ≈ N η |Dη in this case, and we further requireηthat over {0, 1}m , N η has the distribution ﬁxed for nonces (i.e. N0η ), and N η is independent
η
of FJ−1 for all η on the condition that [N ̸= ⊥].
– ϕ ≡ β1 , ..., βn sequence of actions is satisﬁed by Φ if each of βk (k = 1, ..., n) is satisﬁed by
Φ, and if Jk is the stopping time belonging to βk , then we require that Jk < Jl on D wheneverk < l (that is, for each η ∈ param and ω ∈ Dη , Jkη (ω) < Jlη (ω).

– For any formulas ϕ, ϕ1 , ϕ2 , ¬ϕ is satisﬁed by Φ iff ϕ is not satisﬁed by Φ; ϕ1 ∨ ϕ2 is satisﬁedby Φ iff ϕ1 is satisﬁed by Φ or ϕ2 is satisﬁed by Φ; ϕ1 ∧ ϕ2 is satisﬁed by Φ iff ϕ1 is satisﬁedby Φ and ϕ2 is also satisﬁed by Φ. ϕ1 → ϕ2 is satisﬁed by Φ iff ¬ϕ1 ∨ ϕ2 is satisﬁed by Φ.
– If ϕ is a formula, m a variable, then ∀mϕ (or ∃mϕ, resp.) is satisﬁed by Φ iff ϕ is satisﬁed byeach (or some, resp.) Φ′ extension of ΦC when Φ′ only differs from Φ on m.
A formula ϕ is true in the structure M, iff ϕ is satisﬁed by every Φ extension of ΦC .
If in a structure, the Basic Protocol Logic axioms are true (in which case the structure is called
model), then by standard arguments of ﬁrst order logic, it follows that everything provable in thesyntax is true in the model. In particular, if the query form is provable in the syntax, then it mustbe true in any model. We now turn our attention to whether the axioms are satisﬁed by a structure.
Truth of the Term axioms.
(a) These axioms are true since if terms are equal in the free algebra Ā, then their interpretations
are also equal, no matter how Φ is extended to variables. Further, if t ⊆ t′ holds in the freealgebra, then the way we receive t′ from t by pairing and encryptions carries over to thecomputational world, no matter how Φ is evaluated on variables. Same is true for ⊆P . As for⊆¬Q , it is made sure that in the free algebra t can be received from t′ without encrypting withthe key of the substitution for Q as long as it is not equal the P ’s. Since the explicit inclusionin the free algebra carries over to the interpretation, the formula must be satisﬁed.
(b) These axioms hold as computational equality is also symmetric, reﬂexive and transitive. Further, subterm relation is also transitive for the interpretations.
(c) Almost the same as (b). Equality implies computation subterm relation by deﬁnition of computational subterm. Subterm reachable using only decryption with respect to the private keyof a speciﬁc principal (or other than a speciﬁc principal) is also clearly a general subterm.
′(d) If the interpretations of {t1 }sQ and {t2 }sQ are computationally equal up to negligible probability, then the interpretations of t1 and t2 must also be equal up to negligible probability
as the decryptions of both sides with the decryption key of Q give the interpretations of the′encrypted terms: Φ(t1 ) = D(dΦ(Q) , Φ({t1 }sQ )) and Φ(t2 ) = D(dΦ(Q) , Φ({t2 }sQ )) and theright-hand sides are equal up to negligible probability.
(e) Soundness of this axiom follows as we supposed that computational pairing is one-to-one.
(f) These follow from the tagging condition as tagging ensures that encryption is never confusedwith pairs, nonces, names.
(g) Follows from tagging.
(h) Soundness of the ﬁrst formula follows as if t ⊆ 〈t1 , t2 〉 is satisﬁed, then either the interpretations of the two sides are equal (up to negligible probability) and hence t = 〈t1 , t2 〉 is satisﬁed,or (by deﬁnition of satisfaction of t ⊆ 〈t1 , t2 〉) the interpretation of 〈t1 , t2 〉 can be received
from the interpretation of t via encryptions and pairing, of which the last has to be pairing
because the tags have to match; then by soundness of (e), it follows that the paired items mustin fact be interpretations of t1 and t2 , which implies that either of the interpretations of t1 orof t2 was received from the interpretation of t via pairing and encryptions, which means thateither t ⊆ t1 or t ⊆ t2 is satisﬁed, and that proofs the soundness of this formula. As for thesecond formula, if t1 ⊆ {t2 }sQ is satisﬁed, then either the interpretations of the two sides areequal, or the interpretation of {t2 }sQ can be received from the interpretation of t1 via encryptions and pairing, of which the last has to be encryption because the tags have to match, andso soundness follows.
(i) Proof for the ﬁrst and second formulas are the same as in (h), For the third, if the premise holds,
then the interpretation of {t2 }sP can be received from the interpretation of t1 with pairing withothers and encrypting only with the encryption key of P . Therefore there is some t and s′′
such that t1 ⊆P t ∧ {t}sP = {t2 }sP is satisﬁed. But then from (d) it follows that t = t2 and so
t1 ⊆P t2 .
(j) Similar to (h) and (i).
(k) Also follows from tagging.
(l) This follows trivially from the interpretation and that we assumed that the interpretations ofconstants are distinguishable. So if |t1 ⊆Ā t2 ⊆Ā t3 |[M /m] holds for all M vector of constans of appropriate sort, then with X1 = Φ̄(t1 ), X2 = Φ̄(t2 ) and X3 = Φ̄(t3 ), the relation|X1 ⊆T (DM ) X2 ⊆T (DM ) X3 | must also hold as the parsing tree of Φ̄(ti ) is the same as thatof ti , and further, for differing constants in ti the interpretations are assumed to differ, andalthough the interpretations of differing variables may coincide, the relation in T (DM ) must
hold as we assumed that |t1 ⊆Ā t2 ⊆Ā t3 |[M /m] holds for all M vector of constans ofappropriate sort (hence also replacement by identical constants).
Truth of the Ordering axiom. Suppose that there is an extension Φ and a domain D such thatthe formula Q2 sends m; Q1 generates n is satisﬁed on D with non-negligible probability as wellas the formula n ⊆ m. Then, there are stopping times J1η , J2η such that TrJ1 ≪Φ,D Q sends m,
and TrJ2 ≪Φ,D Q generates n, and J1 < J2 . Then, TrJ1 ≪Φ,D Q sends m implies that there
is M ≪Φ,D m such that M η is measurable with respect to FJη1 and since n ⊆ m is satisﬁed,some N ∈ Φ(n) can be obtained as a series of decryptions and breaking up pairs from M . Since
there is no new randomness used there, N η only depends on the randomness until J1 , so N η
is measurable with respect to FJη1 . But, TrJ2 ≪Φ,D Q generates n implies that Φ(n) has anelement N ′η measurable with respect to FJη2 and independent of FJη2 −1 on [N ′η ̸= ⊥], and hence
independent of FJη1 and of N η on [N ′η ̸= ⊥]. So, N and N ′ only differ up to negligible probability,
but N η and N ′η are independent for all η, which is possible only if Pr[N ′η ̸= ⊥] is negligible.
That means D has negligible probability, a contradiction.
Truth of the Nonce veriﬁcation axioms. In order to show that the axioms are satisﬁed, we use
the assumption that regular participants (the ones represented by constants) encrypt with a CCA-2
secure encryption scheme. For the ﬁrst nonce-veriﬁcation axiom, suppose there is a Φ and nonnegligible D such that the premise of the axioms are satisﬁed by Φ on D, but the conclusion is not.
Then, if the conclusion is not satisﬁed, that means that either A never sends the nonce out (whichclearly cannot happen with non-negligible probability as later Q receives it and the probability ofcollision of nonces is negligible), or {m6 }rB does not go through B between A sending it and Q
receiving it with non-negligible probability. The premise however says that n1 shows up in m5
later in another form, and it can be recovered from there up to negligible probability via a seriesof de-coupling and decryption such that the key of B does not have to be used. We have to showthat a PPT algorithm can be constructed that breaks CCA-2 security.
First observe, that the satisfaction of ∀m7 (A sends m7 ∧ n1 ⊆ m7 → |n1 ⊆ {m6 }rB ⊆ m7 |)means that B indeed sent n1 out only in the form of {m6 }rB . The reason is that if, according
to the satisfaction of this formula, there are X1 , X2 , X3 ∈ T (DM ) such that Φ(n1 ) =C X1 ,Φ({m6 }rB ) =C X2 and Φ(m7 ) =C X3 on D so that X1 occurs in X3 , but only within X2 ,then there cannot be any way to create X3 at the point when A sends it ﬁrst out other than fromΦ({m6 }rB ), because otherwise without the decryption of Φ({m6 }rB ) we could access n1 contradicting the CCA-2 security of Φ({m6 }rB ). Why is this encryption CCA-2? Because at the ﬁrst time
when n1 is sent out, r had to be created by A, and hence never revealed to anyone. The fact that
we assume in the interpretation of {m6 }rB that r has to be independent of what happened earlier
and that m6 has to be part of the earlier history, ensures that this term is not confused by any otherencryption that was sent out by A.

The algorithm that breaks CCA-2 security is simply the protocol execution itself with thefollowing modiﬁcations:
1. The encryption-key decryption-key pair of B is generated by the challenger in the CCA-2
game. The encryption key is accessible to the algorithm, that is, the protocol execution uses it
every time encryption with the public key of B is necessary.
2. Since the algorithm cannot use the decryption-key of B known only to the challenger, the decryption oracle (that the algorithm may access according to the deﬁnition of CCA-2 security)
does all decryptions that occur in the protocol execution using the private key dB , except forthe decryption of the interpretation of {m6 }rB .
3. The algorithm generates two samples of n1 when (indicated by the stopping time from thesatisfaction of the formula; notice, that we need to know in polynomial time where it is) the
protocol execution samples n1 .
4. From this on, run the protocol parallel with the two values of n1 . Hence, when (again, givenby the corresponding stopping time) the protocol execution is to produce m6 , compute two
samples of the realization of m6 using the two samples of n1 and using the same samples forthe other parts of m6 .
5. Submit to the encryption oracle of the CCA-2 game the pair of samples of m6 , and use thecipher that it outputs in both of the parallel processes whenever {m6 }rB occurs again (that is,if the protocol execution is deﬁned to use it).
6. If one of the parallel processes happens to crash as that process is running with the wrong
encryption, then output the value of b that corresponds the other process.
7. If the sample for {m6 }rB goes through B in either of the parallel processes, terminate, andoutput a random guess of b. If not, continue until the Q receives the sample for m5 (that is,until the value of the stopping time indicating the point of reception of m5 ).
8. Recover the sample for n1 via de-coupling and decryption. Since m5 contains m1 not encrypted by the key of B, it can be recovered. The bit string hence obtained is the one (out of
the two generated for n1 ) that was in the plaintext encrypted by the oracle, so the bit value bof the game can be determined.
9. If any one of 3., 4., or 6. does not happen on an execution trace then proceed to the end andoutput a random guess of b.
10. If the premise of the axiom is satisﬁed, then, of course n1 had to be sent out by A in somemessage m2 before Q received it, otherwise whoever Q received it from could only guess n1 ,but guessing it correctly has only negligible probability as we assumed.
11. If the premise of the axiom is satisﬁed but rest of the conclusion is not satisﬁed, that is,{m6 }rB does not go through B, but n1 turns up unencrypted by the key of B, then, since
this algorithm determines the value of b in all these cases, the algorithm has probability nonnegligibly different from 1/2 of winning the CCA-2 game to break {m6 }rB as D is nonnegligible.
In order to show the validity of the second nonce-veriﬁcation axiom, we have to use the modiﬁed version of CCA-2 (equivalent to the original) when there are two encryption - decryption pairsof oracles, each corresponding to independently generated encryption key - decryption key pairs.
The algorithm then is the following:
1. The encryption-key decryption-key pairs of B and C are generated by the challenger in the
CCA-2 game. The encryption keys are accessible to the algorithm.
2. The decryption oracles (that the algorithm may access according to the modiﬁed deﬁnition of
CCA-2 security) do all decryptions with the private keys dB and dC .
3. The algorithm generates two samples of n1 when the protocol execution samples n1 .

4. From this on, run the protocol parallel with the two values of n1 . Hence, when the protocol
execution is to produce {m6 }rB1 , compute two samples of the realization of m6 using the two
samples of n1 and using the same samples for the other parts of m6 .
5. Submit to the ﬁrst encryption oracle of the CCA-2 game the pairs of samples of m6 , and use
the cipher that it outputs in both of the parallel processes whenever {m6 }rB1 occurs again (thatis, if the protocol execution is deﬁned to use it).
6. Skip the step when B decrypts {m6 }rB1 .
7. When {m8 }rC2 is constructed, compute two samples of m8 just as in the case of m6 . Stop if thesamples have different length, otherwise submit the results to the second encryption oracle.
8. If one of the parallel processes happens to crash as that process is running with the wrong
encryption, then output the value of b that corresponds the other process.
9. Continue until C receives the sample for m5 .
10. Recover the sample for n1 via de-coupling and decryption. The bit string hence obtained isthe one that was in the plaintext encrypted by the oracles, so the bit value b of the game canbe determined.
11. If any one of 2., 3., 6., or 7. does not happen on an execution trace then proceed to the end andoutput a random guess of b. This is again PPT algorithm given that the protocol execution was
PPT, so it breaks CCA-2 security.
Soundness Since the axioms are true in the structure M, by a standard argument of ﬁrst orderlogic, the following theorem is true:
Theorem 1. With our assumptions on the execution of the protocol, if the associated computational trace structure is M = (Π, E, [·, ·], N0 , Pr, P, Tr, ΦC , D), then, if a formula (the query
form in particular) is provable in the syntax with ﬁrst-order predicate logic and axioms (I), (II),(III), then it is true in M.
Proof. We have showed that the term axioms and non-logical axioms of BPL are true in the model.
It is routine to check that all the logical axioms and logical inference rules of ﬁrst order logic arealso true in the model, because we followed the usual ﬁrst-order logical operations of composed
formulas in the interpretation. Hence the theorem holds.
3.5

Our semantics and Computational PCL

We would like to point out some aspects where problems arise in case of the treatment of Datta et
al. and how they are related to our treatment. We emphasize that we do not claim that these issues
are impossible to be ﬁxed in their framework, we only indicate what our answers are to them.
1. Their treatment is non-deterministic, that is, they rely on counting equiprobable traces. Unequal probabilities may be dealt with by counting a trace more then once (although a priori it
is not quite clear whether this will lead to problems), but their method certainly only applies to
executions when the number of possible computational traces for a given security parameter is ﬁnite. Since some formulations of probabilistic polynomial time processes are not limited to ﬁnitely
many traces (only the expected termination time must be polynomial), it is better not to exclude
inﬁnite number of traces. Our method works for inﬁnite number of traces and arbitrary probability
distributions. Removing the bound nη from the length of executions is not a difﬁcult step (change
the ﬁnite sequence of the ﬁltration to an inﬁnite one, and the deﬁnition of measurability to thestandard one for inﬁnite spaces) in our framework, only the presentation of the deﬁnition of measurability is more involved in this case, that is why we chose to stick to the bound. It is perhaps
worthwhile to note that although manipulations with expected polynomial time algorithms maylead out of their realm, the proof of the nonce-veriﬁcation axioms only involve minor modiﬁcations (no compositions of two expected PT algorithms) of the expected polynomial-time protocol
execution that should not lead out of the realm.
2. As Datta et al. derive the validity of a formula in the model from validity of the formula onindividual traces, they have to make sure that there are not too many accidental coincidences. This
results in a weaker set of syntactic axioms then what would otherwise be possible in our method.
For example, they postulate that ¬Send(X̂, t)[b]X ¬Send(X̂, t) is an axiom whenever for all σevaluation of variables by bit-strings, σ(b) ̸= σ(Send(X̂, t)). Let us now not be bothered by the
problem that they deﬁne a syntactic axiom using the semantics. Here, X̂ is a principle, t is a term,[b]X is an action b carried out by principal X̂ in thread X assuming also that nothing else is carriedout. In other words, it is an axiom that if X̂ did not send t before action b, then it did not send it
even after action b as long as no σ evaluates b and Send(X̂, t) the same way. However, if there iseven one coincidence in their evaluations, that prevents the axiom. We think this is an unnecessary restriction. As long as the probability distributions are different (up to negligibility) for any
computational interpretation of b and Send(X̂, t), we can include ¬Send(X̂, t)[b]X ¬Send(X̂, t)
in our axioms. We did not introduce modal formulas here in the syntax, and it is our work inprogress to extend our approach to PCL. As we keep track of the actual probability distributions
and correlations, it should be no problem to deﬁne the semantics of modal formulas so that theseaxioms hold as long as the interpretations (distributions, not bit-strings) of b and Send(X̂, t) are
different up to negligible probability.
3. A further problem, that even makes the soundness proofs of Datta et al. questionable is thefollowing: They deﬁne a formula (e.g. Send(X̂, t)) to be true in the model if it holds on all traces
except for some with negligible probability. They ignore the fact that the position of Send(X̂, t) on
the traces may vary badly from trace to trace, for example, may depend on the future of the trace.
A simple example of such a situation is when on two traces, which coincide up to step t0 , say,Send(X̂, t) is chosen on one trace for t1 < t0 , but on the other trace it is chosen somewhere else.
Since the two traces coincide at step t1 , if this time is picked on one trace, it must be picked on
the other trace too. Maybe it is possible to prove that if there is a bad choice of the positions thenthere is a good choice as well, but we see no indication of such concerns in the papers of Datta et
al. As we suggest to use the standard tool of ﬁltration, according to which random variables haveto be measurable, dependence on the future is taken care of by measurability.
4. Finally, ignoring probability distributions and correlations give rise to pathologies like thisone, putting further doubts at the correctness of their soundness proofs: Suppose that the encryption scheme is such that for any n1 , n2 bit-strings generated randomly as nonces, any public key
bit-string k2 and any random seed r2 for the encryption, there is another public key bit-string
k1 and a random seed r1 such that {n1 }rk11 = {n2 }rk22 . This does not contradict CCA-2 security. Suppose principal A generates randomly nonce n1 , and then principal B receives {n2 }rk22
from the adversary. In such a case, it will be true according to the semantics of Datta et al., that∃N ∃R∃K.New(A, N ) ∧ Receive(B, {N }RK ). This is however pathologic, and is a consequenceof ignoring the fact that k1 , if created by the adversary, cannot correlate with n1 , which was not
yet sent around. Furthermore, this seems to contradict their axiom (which though does not appear
in their computational PCL papers) saying that FirstSend(X, t, t′ ) ∧ a(Y, t′′ ) → Send(X, t′ ) <a(Y, t′′ ) where X ̸= Y and t subterm of t′′ (meaning in our case that the ﬁrst send action of A
sending N had to occur before B could do anything with N ) in Section 4.7 of[14]. This problem
persists even if such a coincidence cannot be efﬁciently computed. In our method, we required thatthe distribution of keys are measurable with respect to F0η , and generated nonces are independentof the past, so this anomaly cannot happen as N and K must have independent interpretations. The
reader may be worried that we don’t require that the generated R has to be dependent of N as R

is generated by the adversary or a corrupted participant. It is true that we could introduce anotherﬁltration that indicates the knowledge of the adversary up to a certain time, which may be needed
in a more complex syntax (for example if we allow corrupted participants to generate their keys
sometime in the middle), however, in BPL this is not necessary as this does not result in undesired
coincidences and the proofs work even without this tool.

4

Conclusions

We have given a computational semantics to Basic Protocol Logic that uses stochastic structures,and showed a soundness theorem. In order to show that the axioms of BPL were true in the semantics, we had to modify BPL as the original axioms were not all computationally sound. We
showed our method on BPL as it is simple enough for a ﬁrst, concise presentation. As the idea ofmaking use of the notions from the theory of stochastic processes in the deﬁnition of satisfactionof formulas does not require the special properties of BPL, we believe that it should not be difﬁcult
to adopt this method to a wide range of formal models such as PCL or strand space models.

References
1. Website of www.stanford.edu/˜danupam/logic-derivation.html.
2. M. Abadi, M. Baudet, and B. Warinschi. Guessing attacks and the computational soundness of static
equivalence. In Proceedings of FoSSaCS’06, Lecture Notes in Computer Science. Springer-Verlag,
March-April 2006.
3. M. Abadi and P. Rogaway. Reconciling two views of cryptography. Journal of Cryptology, 15(2):103–
127, January 2002.
4. P. Adão, G. Bana, J. Herzog, and A. Scedrov. Soundness of formal encryption in the presence of keycycles. In Proceedings of ESORICS’05, volume 3679 of LNCS, pages 374–396, Milan, Italy, September
12–14 2005. Springer.
5. P. Adão, G. Bana, and A. Scedrov. Computational and information-theoretic soundness and completenessof formal encryption. In Proceedings of CSFW’05, pages 170–184, Aix-en-Provence, France, June 20–22
2005. IEEE Computer Society Press.
6. M. Backes, B. Pﬁtzmann, and M. Waidner. A composable cryptographic library with nested operations.
In Proceedings of CCS’03, pages 220–230. ACM Press, 2003.
7. G. Bana, K. Hasebe, and M. Okada. Computational semantics for basic protocol logic - a stochastic
approach. In Proceedings of 12th Asian Computing Science Conference, volume 4846 of LNCS, pages
86–94, Doha, Qatar, November 2007. Springer.
8. M. Baudet, V. Cortier, and S. Kremer. Computationally sound implementations of equational theories
against passive adversaries. In Proceedings of ICALP’05, volume 3580 of Lecture Notes in Computer
Science, pages 652–663. Springer-Verlag, July 2005.
9. M. Bellare, A. Boldyreva, and S. Micali. Public-key encryption in a multi-user setting. In Proceedingsof EUROCRYPT’00, pages 258–274. Springer-Verlag, 2000.
10. Ran Canetti and Jonathan Herzog. Universally composable symbolic analysis of mutual authenticationand key exchange protocols. In Proceedings, Theory of Cryptography Conference (TCC), March 2006.
11. I. Cervesato, C. Meadows, and D. Pavlovic. An encapsulated authentication logic for reasoning about
key distribution protocols. In Proceedings of CSFW’05, pages 48–61, 2005.
12. A. Datta, A. Derek, J. C. Mitchell, and D. Pavlovic. A derivation system and compositional logic for
security protocols. Journal of Computer Security, 13:423–482, 2005.
13. A. Datta, A. Derek, J. C. Mitchell, V. Shmatikov, and M. Turuani. Probabilistic polynomial-time semantics for a protocol security logic. In Proceedings of ICALP’05, volume 3580 of LNCS, pages 16–29.
Springer, 2005.
14. Anupam Datta, Ante Derek, John C. Mitchell, and Arnab Roy. Protocol composition logic (pcl). Electron. Notes Theor. Comput. Sci., 172:311–358, 2007.

15. D. Dolev and A. C. Yao. On the security of public-key protocols. IEEE Transactions on Information
Theory, 29(2):198–208, March 1983. Preliminary version presented at FOCS’81.
16. N.A. Durgin, J.C. Mitchell, and D. Pavlovic. A compositional logic for proving security properties ofprotocols. Journal of Computer Security, 11:677–721, 2003.
17. S. Goldwasser and S. Micali. Probabilistic encryption. Journal of Computer and Systems Sciences,28(2):270–299, April 1984. Preliminary version presented at STOC’82.
18. J. D. Guttman and F. J. Thayer Fábrega. Authentication tests. In IEEE Symposium on Security andPrivacy, pages 96–109, 2002.
19. J. D. Guttman, F. J. Thayer, and L. D. Zuck. The faithfulness of abstract protocol analysis: Message
authentication. In Proceedings of CCS’01, pages 186–195. ACM Press, November 05–08 2001.
20. K. Hasebe and M. Okada. Completeness and counter-example generations of a basic protocol logic.
In Proceedings of RULE’05, volume 147(1), pages 73–92. Elsevier Science, 2005. Available also at
http://dx.doi.org/10.1016/j.entcs.2005.06.038.
21. P. Laud. Symmetric encryption in automatic analyses for conﬁdentiality against active adversaries. In
Proceedings of S&P’04, pages 71–85. IEEE Computer Society Press, May 9–12 2004.
22. G. Lowe. A hierarchy of authentication speciﬁcations. In PCSFW: Proceedings of The 10th Computer
Security Foundations Workshop. IEEE Computer Society Press, 1997.
23. D. Micciancio and B. Warinschi. Completeness theorems for the Abadi-Rogaway logic of encrypted
expressions. Journal of Computer Security, 12(1):99–130, 2004.
24. R. Needham and M. Schroeder. Using encryption for authentication in large networks of computers.
Communications of the ACM, 21(12):993–999, 1978.
25. T. Woo and S. Lam. Verifying authentication protocols: Methodology and example. In Proceedings ofthe International Conference on Network Protocols, 1993.

A

Deﬁnition of Only and Honest

Our aimed correctness properties are described in a special form of formulas, called query form.
Let αA [Q, N , n, r, s] be a role A acts1 t1 ; A acts2 t2 ; · · · ; A actsk tk where each actsi (1 ≤ i ≤k) is one of sends, receives and generates, ti is a term built from nonces in N = {N1 , ..., Ng }and n = {n1 , ..., nh } from coins in r = {r1 , ..., ri } and s = {s1 , ..., sj } and from names A
A
and Q = {Q1 , ..., Ql }. Let αA≤i denote an initial segment of α ending with A acts i ti (forAA
1 ≤ i ≤ k), i.e., α≤i ≡ A acts1 t1 ; · · · A actsi ti . Let α≤0 ≡ A = A.
The query form includes a formalization of principal’s honesty Honest(αA ), which is deﬁned
as follows, the intuitive meaning being that A follows the role αA and does nothing else, but it
may not complete it:
def W

Honest(αA ) ≡i∈{0}∪{j | acts j = sends }∪{k}A
αA≤i ∧ Only(α ≤i )Only(αA ) denotes the following formula, whose intuitive meaning is “A performs only αA ”.
Only(αA ) ≡ ∀n(A generates n → n ∈ Generates(αA )) ∧ ∀m1 (A sends m1 → m1 ∈ Sends(αA ))∧∀m2 (A receives m2 → m2 ∈ Receives(αA ))Here, Sends(αA ) denotes the set {tj | A sends tj ⊆ αA }, and (Receives(αA ), Generates(αA )are deﬁned similarly. Set theoretical notation as m ∈ Sends(αA ) (as well as m ∈ Receives(αA )and m ∈ Generates(αA )) is an abbreviation of a disjunctive form: for example, if Sends(αA ) ={t′1 , . . . , t′j }, then m ∈ Sends(αA ) denotes the formula (m = t′1 )∨(m = t′2 )∨· · ·∨(m = t′j ). (Asa special case, if Sends(αA ) is empty then m ∈ Sends(αA ) denotes A ̸= A, that is, impossible.)A
A
Intuitively, each disjunct αA≤i ∧ Only(α≤i ) in Honest(α ) represents a historical record ofA
P ’s actions at each step of his run: the sequence of actions α≤i represents A’s performance untilAA
this step, and Only(αA≤i ) represents that A performs only α≤i . Only(α≤0 ) means that nothing
was performed.