goals. We outline a novel approach for formally verifying zero-knowledge protocols building on Dynamic Epistemic Logic (DEL) as an abstract semantics for a low-level protocol specification language called SPEC. One of the main benefits is that our methodology abstracts the logical structure of the interactions from the mathematical subtleties related to cryptographic primitives. Furthermore, we leverage the DEL action structures to verify the knowledge dynamics generated by the protocol runs. We illustrate our methodology by applying it to a new protocol called BKP, and we prove that it meets the participants' ∗Corresponding author.
Zero Knowledge Proofs (ZKP) play a key role in security-critical applications, such as blockchain
technology [
The formal verification of the epistemic properties of ZKP is thus essential and challenging at the same time: the definition of a general framework for their design and verification is still an open problem. Very often, only a combination of methods provides robust mathematical proofs that security desiderata are met by specific ZKP. 1
In this paper, we suggest, by a working example, how epistemic logics can help in formally
verifying ZKP of a security protocol, challenging some known limitations (according to [
© 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
1See, e.g., [
CEUR
ceur-ws.org
We present an original protocol specification language (SPEC) designed to ofer a lucid
and exact framework for delineating protocol actions. We then use the semantics of dynamic
epistemic logic (DEL), based on action models [
More precisely, we prove that by applying to the epistemic model for the initial configuration of BKP the action model interpretations of (respectively) the honest prover and the honest verifier SPEC-formalisations, we obtain new epistemic models that validate, for each participant, the protocol security desiderata (namely, zero-knowledge, proof-of-knowledge, and no-repudiation, for the honest prover; proof-of-knowledge for the honest verifier) rendered as formulas in the language of epistemic logic.
The results on BKP show that our approach of modelling a low-level specification language, as our SPEC, via a semantics based on mathematical structures for dynamic epistemic reasoning allows us to faithfully represent the evolution of the protocol from the perspectives of both the participants (prover and verifier), and asses the main security features expected from the protocol by each of the interacting agents.
The paper is structured as follows: in Section 2 we present our broken key protocol (BKP) as a working example of zero-knowledge protocol; in Section 3 we introduce the syntax and operational semantics for the Simple Protocol Epistemic Calculus (SPEC), our protocol specification language; Section 4 recalls the basics of dynamic epistemic logic (DEL) which we apply to define an abstract interpretation for statements in SPEC (Definition 6); in Section 5 we show how to model the BKP evolution using that DEL-based abstract semantics and prove that, after a single run of the protocol, the prover’s and verifier’s goals are satisfied; in Section 6 we discuss related work.
In this section, we introduce the broken key protocol (BKP) that will also serve as a working example along the rest of the paper. The execution of a single session of BKP is depicted in
, who wants to inform that one between her keys is compromised without revealing which one. To achieve their goals, and run the following protocol steps:
check(enc( 1, ), enc( 2, )) enc( 1, ) enc( 2, ) h( )
:= fresh()
1. initiates the session by pinging (with a constant message ∗).
2. generates a fresh, random message , encrypts it with both 1 and 2 (enc( 1, ) and
enc( 2, ) , respectively), and computes the hash of (ℎ() ). Then, she sends the three
values enc( 1, ) , enc( 2, ) and ℎ() to .
3. controls the received values by checking that:
a. enc( 1, ) and enc( 2, ) are ciphertexts for the same message (e.g., through a secure
multiparty computation equality test [
We present the syntax and operational semantics of our protocol specification language, named Simple Protocol Epistemic Calculus (SPEC).
We start by providing the syntax of protocol statements inspired by the Simple Protocol
Specification language (SPS) of [
Definition 1.
A protocol statement is a term generated through the following grammar.
::= ∶= ∣⇾ ∶ ∣⇽ ∶ ∣ [] ∣ ; ′
Briefly, a statement can be an assignment ( ∶= ), a sending (⇾ ∶ ), a reception (⇽ ∶ ), a conditional ([] ) or a sequence (; ′). We use , , ⋯ to denote variables. Expressions , ′, ⋯ behave as usual and also include uninterpreted function symbols, e.g., enc(…), and constants, e.g., ∗ and ■ . The same holds for boolean guards , ′ in conditional statements. , are agent labels used in the communication mechanism detailed in Section 3.1 and Appendix B. Finally, we feel free to use parentheses for grouping terms and we introduce the following abbreviations. skip ≜ _ ∶= ∗2 fail ≜ [ ≠ ] skip3 ⇽ ∶ ≜ ⇽ ∶ ; [ ≠ ] fail ⇾ ∶ 1, … , ≜ ⇾ ∶ 1; …; ⇾ ∶ ⇽ ∶ 1, … , ≜ ⇽ ∶ 1; …; ⇽ ∶ Example 1. Consider the BKP protocol described in Section 2. The following statements implement the honest prover and verifier .
≜ ⇾ ∶ ∗; ⇽ ∶ , , ; [ comp(, )][ = h(trydec(, , ))]⇾ ∶ trydec(, , ) ≜ ⇽ ∶ ∗; ∶= fresh(); ⇾ ∶ enc( 1, ), enc( 2, ), h(); ⇽ ∶ ; [ = ] skip
The two statements rely on a few cryptographic functions: h, enc and fresh are quite traditional, and they represent hashing, encryption and generation of a fresh value, respectively; comp is used by the prover to check whether and encrypt the same message with diferent keys. trydec attempts to decrypt both and using key and returns the cleartext if at least one of the two operations is possible. 2Where _ is a reserved variable name that cannot appear in any other statement. 3For some variable .
In the rest of this paper, with no loss of generality, we also assume protocol statements to be well typed. Correct typing is guaranteed statically and dynamically through a utility function Type() that assigns the proper type to any expression . Types can be either base or function. For instance, we assume basic types to include Key and Msg (for keys and simple messages, respectively), while function types include Hash(Msg) and Enc(Key,Msg). Moreover, we assume that value binding, which occurs in both assignment and receipt statements, always ensures type correctness, e.g., in ∶= we have Type() = Type() . 3.1. Operational semantics In this section, we define the operational semantics of SPEC. We first introduce some preliminary definitions.
Definition 2. An agent state is a finite, partial mapping from variable names to values. We use to denote the empty state and [ /] for the state where is (re-)assigned to value . Consequently, the resolution of a variable in a state is defined as
∅ if is () = { if is ′[ /] where ∅ stands for the undefined value.
′() if is ′[ / ] We call the pair ⟨ , ⟩ an agent configuration .
For explaining the operational semantics rules, we assume that a support function for evaluating expressions and guards (see Definition 1) is defined. We use J K = to denote that, under state , expression evaluates to value . Similarly, J K = 1/0 indicates whether, under state , the guard is satisfied ( 1) or not (0).
The structural operational semantics of an agent configuration ⟨ , ⟩ is then defined by the rules of Figure 2.
⟨ , ⟩ ⟶ ⟨ ′, ″⟩ ⟨ , ; ′⟩ ⟶ ⟨ ′, ″; ′⟩ (Seq 1)
⟨ , ⟩ ⟶ ⟨ ′, ⋅⟩ ⟨ , ; ′⟩ ⟶ ⟨ ′, ′⟩ (Seq 2)
J K = 1 ⟨ , []⟩ ⟶ ⟨ , ⟩ (Cond 1)
J K = 0 ⟨ , []⟩ ⟶
A (Cond 2)
J K = ⟨ , ∶= ⟩ ⟶ ⟨ [ /], ⋅⟩ (Asgn)
J K = ⟨ , ⇾ ∶ ⟩ ⟶ ⟨ , ⋅⟩ ↑ , ⟨ , ⇽ ∶ ⟩ ⟶ ⟨ , ⋅⟩ ↓ , (Send) (Recv)
⟨ , ⟩ ⟶ ⟨ ′, ″⟩ ↑, ⟨ , ; ′⟩ ⟶ ⟨ ′, ″; ′⟩ ↑,
⟨ , ⟩ ⟶ ⟨ ′, ″⟩ ↓, ⟨ , ; ′⟩ ⟶ ⟨ ′, ″; ′⟩ ↓, (Send-P) (Recv-P)
Briefly, sequences are evaluated by reducing the first statement (Seq 1) until, eventually, it gets to a terminal configuration (denoted by ⋅), and then the second statement is executed (Seq 2). Conditional statements behave as the guarded statement when the guard is satisfied (Cond 1) or, otherwise, they lead to a faulty configuration A (Cond 2). An assignment updates the current state by binding the variable to the value obtained from the evaluation of (Asgn). Both sending to (Send) and receiving from (Recv) lead to special, blocking configurations labelled with ↑,
and ↓, , respectively. Moreover, according to rules (Send-P) and (Recv-P), blocking configurations propagate through the sequences of statements.
Protocol agents compose to form a choreography, i.e., the actual execution of a protocol where agents communicate over a network. We provide an SOS for protocol choreographies in Appendix B.
In this section, we address the task of formalizing through dynamic epistemic logic the epistemic properties of SPEC protocols.
Dynamic Epistemic Logic (DEL) is a branch of modal logic that deals with knowledge change
over time. Following [
Definition 3 (Action model).
Let Atm be a set of propositional atoms. Let ℒ denote the set of formulas built on top of Atm w.r.t. a given grammar. Let Ag be a finite set of agents. An action model is a quadruple ⟨ , ≈,
pre, post⟩, where • is a finite set of action labels { 1, ⋯ , };
4 indistinguishability of two actions for the agent ; is true in a state if can be executed on that state; • ≈ is a function associating to each agent ∈ Ag an accessibility relation ≈ ⊆ × modelling • the precondition function pre ∶ ⟶ ℒ
assigns to each action a formula ∈ ℒ such that • the postcondition function post ∶ ⟶
Subℒ assigns to each action ∈ a substitution from Atm to formulas in the language ℒ, i.e. a function behaving as the identity map except for a ifnite number of atoms; we write ↦
for the substitution that maps the atom to , leaving all the other propositional atoms unchanged; the identity substitution that leaves all the atoms unchanged is denoted by idsub.
Any action model operates on a relational structure that models a static epistemic situation; by performing an action, the structure of the original model changes, and consequently, the truth values of epistemic assertions do. Moreover, the postcondition function implements a notion of factual change, the fact that performing an action changes the truth value of propositional atoms (as well as epistemic statements) by modifying the basic facts of the world.
For static epistemic logic (EL), we need to extend a classical propositional language with an indexed modal operator as in the following ∈ ℒ EL ::= ⊤ ∣ ∣ ¬ ∣ ∧ ∣ The epistemic formula formalizes the fact that agent knows that holds.5 where belongs to a given set of propositional atoms and belongs to a given finite set of agents. 4From now on, we use (indexed) initial Greek letters , , , , , , ⋯
denote generic formulas of a formal language for (dynamic) epistemic logic.
5Classical connectives are defined as usual in terms of ¬ and ∧ (see e.g. [
to denote action labels, while terminal Greek letters
The relational semantics for ℒEL is standard, and we report its definition below.
Definition 4. An epistemic model ℳ is a triple ⟨ , { }, ev⟩ made of a non-empty set “of possible worlds”, a set of binary “accessibility” relations ⊆ × indexed over the given finite set of agents Ag,6 an evaluation function ev ∶ × Atm ⟶ {0, 1} associating to each ∈ and each ∈ Atm a truth-value ev(, ) ∈ {0, 1} .
The forcing relation ⊩ holding between a model ℳ ≜ ⟨ , { }, ⟩ , a world ∈ and a formula of ℒEL is inductively defined on the structure of as follows.
⊩ ℳ if ev (, ) = 1 ; ⊩ ℳ ⊤ for any , ℳ ; ⊩ ℳ ∧ if ⊩ ℳ and ⊩ ℳ ; ⊩ ℳ if for all ∈ , if , then ⊩ ℳ .
In words, when ⊩ ℳ , we say that is forced by in ℳ. When every world in ℳ forces a formula , we write ℳ ⊨ .
For dynamic epistemic settings, the syntax of ℒEL needs to be extended to ℒDEL by a dynamic modal operator [, ] , where is an action model, and is an action in : the formula formalises the fact that, after the action in is performed, (belonging to the extended language ℒDEL) holds.
To give a precise semantics to action performing, we need to formalize the update of a static relational model via an action model. The resulting structure is called model update. Definition 5 (Model update). Let ℳ ≜ ⟨ , { }, ev⟩ be an epistemic model and ≜ ⟨ , ≈, pre, post⟩ be an action model. The model for ℳ updated by is denoted by ∘ ℳ and consists of the triple ⟨ ′, ′, ev′⟩, where • ′ ≜ {⟨, ⟩ ∶ ⊩ ℳ pre()} ; • ′ ≜ ∈ Ag.{⟨⟨ 1, 1⟩, ⟨ 2, 2⟩⟩ ∶ & 1 ≈ 2} • ev′(⟨, ⟩, ) = 1 if ⊩ ℳ post()() .
This allows us to define the meaning of all DEL formulas: it sufices to extend Definition the following forcing clause: 4 by ⊩ ℳ [, ] if
⊩ ℳ pre() implies that ⟨, ⟩ ⊩ ∘ℳ , where ∘ ℳ
is the update model of ℳ with of Definition 5.
Example 2. Consider again the BKP protocol. Below, we give the security goals of the protocol in ℒEL.
⋅ Zero knowledge: ZK ≜ ¬ (has ( 1)) ∧ ¬ (has ( 2)) ⋅ Proof of knowledge: PoK ≜ (has ( 1) ∨ has ( 2)) ⋅ No repudiation: NR ≜ ( ( (has ( 1) ∨ has ( 2)))))
In words, ZK states that should not know whether owns 1 or 2, PoK states that must know that owns one between 1 and 2, and NR states that and reciprocally acknowledge that owns one of the two keys. 6We write to mean that is accessible to for . Further general conventions are collected in Appendix A. 4.1. Modeling BKP in DEL This section shows how to interpret SPEC-statements as action models. The actions are applied to epistemic models that formalize the system made of agent states and the knowledge of each agent, modeled through an accessibility relation.
accessible to agent . Nevertheless, the information encoded by is local to agent , as it contains ’s computational data, and information about any other agent is not part of . Instead, the accessibility relation models a more general (though potentially uncertain) information possessed by , which concerns the status of the whole system of interactive agents. To describe this proper form of knowledge (and uncertainty), agent states do not sufice since, by definition, the information encoded in each state is private. Thus, we start by fixing the set Atm of propositional atoms for BKP, defined as
∈ Atm ::= 1 = 2 ∣ has () ∣ const () where ∈ Ag = { , } , 1, 2 are expressions, and = denotes identity of values. Formulas for BKP are built according to the grammar for ℒDEL on top of this set of atoms.
denotes that can build expression . Trivially, has () subsumes const () ; that is encoded by the rule has () (has) stating that any local information of is per se constructible by .
const ()
Then, for every uninterpreted function f(…) appearing in SPEC expressions, we require proper inference rules to define their constructibility. For instance, the rules for the functions used in our working example are the following.
const (∗) (∗) const (fresh()) (fresh)
const () const (h()) (h) has () has () const (enc(, )) (enc) has (enc(, )) has () (trydec)1 has (enc(, )) has () (trydec)2 const (trydec(, enc(, ), )) const (trydec(, , enc(, )))
They state that agent can construct the constant ∗ and fresh() values. Moreover, if has a message , it can compute its hash h() and encrypt it with a key it also has. Finally, can decrypt a ciphertext enc(, ) when she has the proper key.7
For what concerns uninterpreted functions appearing in guards, we assume that an interpretation Lf(…)M of f(…) is defined in terms of a finite set of literals, i.e., positive or negative atoms, of our language. Intuitively, Lf(…)M = {ℓ1, … , ℓ } represents the fact that the litearals ℓ1, … , ℓ must be satisfied for f(…) to be true. For instance, we have that
Lcomp(enc( 1, 1), enc( 2, 2))M ≜ {const (enc( 1, 1)), const (enc( 2, 2)), 1 ≠ 2, 1 = 2}.
Next, we need to interpret our protocol statements in terms of action models. Definition 6. We define an interpreting function ⟨⟨⋅⟩⟩ from protocol statements (and agent ) to action models ⟨⟨⟩⟩ by induction on the structure of as follows.8 7It is worth noticing that these rules are not the only candidates. For instance, one may want to model encryption recursively, e.g., to deal with terms such as enc(, enc( ′, )) . However, nested encryption has no role in the BKP protocol, and thus we omit it. 8In these and the following graphics, we adopt some standard visual conventions, detailed in Appendix A.
The action model ⟨⟨ ∶= ⟩⟩ for the assignment ∶= by agent is given by ( ∶= ). ⟨ , ≈,
pre, post⟩ where • ≜ { 1, 2} other agents involved in the protocol are unaware of the event. (⇾ ∶ ). The action model ⟨⟨⇾ ∶ ⟩⟩ for agent sending to agent is given by ⟨ , ≈, pre, post⟩ where • ≜ {} • ≜ { ℎ ∶ const ( ℎ) & Type( ℎ) = Type()} • ≈ ≜ ∈
Ag. { • pre ≜ ℎ ∈ . const ( ℎ) • post ≜ ℎ ∈ . has ( ℎ) ↦ ⊤ {⟨ ℎ, ⟩ ∶ ℎ ∈ & ∈ } {⟨ ℎ, ℎ⟩ ∶ ℎ ∈ }
In words, sending an expression is a public action that can be performed whenever the sender is able to construct the value of that expression; after the event, that value is stored in the local information of the receiver. (⇽ ∶ ). The action model ⟨⟨⇽ ∶ ⟩⟩ for agent receiving values on variable from agent is • • • • • • • • • Ag
Ag i
Thus, we can informally interpret the receiving statement from the agent as an equivalence class of sending statements from the same agent. ([] ). The action model ⟨⟨[]⟩⟩ , for a guarded statement with ⟨⟨⟩⟩ = ⟨ , ≈ , pre , post ⟩, is given by ⟨ , ≈,
pre, post⟩ where ∪ {} , where does not occur in
Ag. ≈ ∪ {⟨, ⟩} ⟨⟨⟩⟩ ≈ ≜ ∈ pre ≜ ∈ . post ≜ ∈ .
{ ⋀L M ∧ pre ()
L ¬ ⋀ post () { A ↦ ⊤
M when ≠ otherwise when ≠ otherwise where the expression A ↦ ⊤ denotes the substitution mapping, for each ∈ Ag, has (■ ) to ⊤. 1–16 . ⋯ Graphically, we have ⋯ ′
′
In words, we model the fact that in SPEC guards are external: in [] whenever the guard evaluates to true by agent , we proceed with the action formalized by ; when the same guard evaluates to false, we have a public announcement of protocol failure. (; ′). The action model ⟨⟨; ′
⟩⟩ is given by ⟨ , ≈, action model ⟨⟨⟩⟩ = ⟨ , ≈ , pre , post ⟩ with the action model ⟨⟨ ′⟩⟩ = ⟨ ′, ≈ ′, pre ′, post ′⟩, pre, post⟩, obtained by the composition of the ′⟩ ∈ . post () ⋅ post ′( ′), where ⋅ is an abbreviation for .( ())
Finally, we model the agent states by an epistemic structure. Assuming that the given protocol involves agents, the whole system state corresponds to an epistemic model with possible worlds as -tuples of lists assigning values to variables (defined on the basis of the current for each ∈ Ag). The epistemic uncertainty of an individual agent regarding the actual state of the system is represented by an accessibility relation among such worlds. The evaluation function ev for worlds and propositional atoms is given by the information thus encoded in each -tuple and according to the semantics of const () defined in Section 4.1.
Graphically, to distinguish the local information of, say, agent from agent , we use colors: when agent assigns a value to a variable of hers, we write it inside the node’s area with a color conventionally assigned to ; similarly for . Epistemic possibility and uncertainty for agent are represented by (bi-)directed arrows, labeled by .9 The figures in the next section will make these graphical conventions more concrete.
We can finally prove that each agent implementation complies with the respective goal. First, we fix the epistemic scenario as described by the initial assumptions of the protocol: has two keys ( 1 and 2), and has at most one10 of them. We call this model ℐBKP and we depict it in Figure 3 (we assigned blue to and red to ).
of Example 1 for the honest prover in BKP. starts by sending ∗: this does not change the epistemic model, apart from adding ∗ to the local information of , which we skip for brevity.
Then, receives . Since the actual message sent by is unknown, must assume that any constructible (and type-compatible) message might be received. This results in an unfolding of 9As for the ≈ symbol of Definition 6, we omit the symbol to enhance picture readability. 10We neglect the case when knows both the keys since it is irrelevant for our scenario. three configurations are possible, i.e., has no key (left node), has 1 (middle node) or has 2 (right node). In terms of knowledge, can distinguish between these three states (self-loops), but cannot. the epistemic model where, in each world, ’s local information is extended with the possible message from : from ’s perspective, all the states obtained by extending the same initial state with ’s message are epistemically indistinguishable. Next, receives another message on variable . This event is analogous to the previous one and leads to a similar efect: cannot distinguish what message will send. The third receiving, stored in , behaves in the same way.
Because of our typing discipline, the resulting model is then made of 3 × 4 × 4 × 2 = 96 worlds.
The first guard [comp(, )]
allows us to select from the 96 nodes of the epistemic model those containing the local information of triggering the guard. The subsequent guard [ = h(trydec(, , ))]
further narrows down the possibilities. After calculating (based on Definitions 6 and 5) the appropriate accessibility relations for and , we obtain the final model ℱBKP, as depicted in Figure 4.
Notice that ’s epistemic uncertainty is narrowed by eliminating the worlds where ’s key variable is unassigned but unaltered for the remaining worlds: there are bi-directed -arrows connecting the worlds where has value 1 with worlds where has value 2. The bi-directed -arrows connect worlds in which does not need to diferentiate between scenarios where has swapped the order of sent ciphertexts. Likewise, these arrows eliminate distinctions between worlds where cryptographic functions have been applied to one message ( 1) versus 11Those epistemic possibilities are summarized in the three-part table given in Appendix C and omitted here for brevity.
another ( 2). By an easy inspection of ℱBKP, we see that each component of ’s goal (see
statement of Example 1 for the honest verifier in BKP. The first statement applied to consists of receiving ∗ from ; as before, we skip this event, which only adds ∗ to ’s local information. After generating a new message, assigns its value to a variable named . Given that value assignment is a private action, the resulting model is essentially a replica of ℐBKP. The nodes are -accessible from their counterparts in the model derived from ℐBKP by removing -loops and incorporating the value of into ’s local information. After that, sequentially sends three messages to : enc( 1, ) , enc( 2, ) , and h() . These actions consist of three public announcements. Since each of those values is constructible in any of its worlds, the ℐBKP structure of the previous model is preserved, though the values enc( 1, ) , enc( 2, ) and h() join ’s local information for any world.
At this point, receives a message from , whose value is assigned to . Since does not know the actual value she will receive, she must consider the epistemic possibility where sends and the one where sends another value 2. This situation unfolds the previous model, whose worlds difer for the local information available to ; still, ’s epistemic possibilities are preserved.
Finally, checks whether the value stored in is equal to the value of : if that is the case,
Again, one can check that ℱ BKF ⊨ PoK, i.e., the honest verifier achieves a PoK.
We outlined the application of dynamic epistemic logic (DEL) to verify zero-knowledge proofs (ZKP) formally. We consider it a first step towards a comprehensive verification framework of ZKP. The approach’s potential is demonstrated through a practical example, illustrating how DEL semantics can capture the perspectives of protocol participants on the protocol’s evolution.
Formal verification of security protocols is a vast research field, where several methodologies
co-exist. Model checking [
A DY-based implementation of zero-knowledge in the Tamarin prover is introduced in [
The paper [
In [
The seminal papers [
Diferently, [
In this appendix, we recap the principal conventions adopted in the paper to facilitate understanding and maintain consistency in our presentation.13 Mathematical notations. From the logical viewpoint, we will use diferent formal languages that interact at various levels. To distinguish these abstraction layers, we adopt some general conventions: operators of the epistemic language we use in our abstract semantics are denoted by standard symbols in logical practice;14 operators of the higher-order/set-theoretic language we use to define the relational semantics of the epistemic language are denoted by standard set-theoretic symbols extended by logical symbols that are kept distinct from those used in the epistemic language;15 operators of the meta-language, i.e. used to reason about the epistemic system (language or semantics), are preferably written in plain English.16
Whenever we formally define the basic syntax of a language, we recur to (an easier-to-read
version of) the Backus-Naur form convention [
Moreover, variants of the identity symbol = are omnipresent in the following pages: plain = between expressions of our protocol language denotes identity between values within the type of both the expressions; we reserve the symbol ∶= for value assignment to a variable of the protocol language; ≜ denotes definitional equality.
Functions are preferably defined by -abstraction: e.g., . +1 denotes the successor function. Nevertheless, we occasionally recur to the standard notation to enhance readability. Whenever needed, we also recur to standard conventions to denote the domain and target of a given function: e.g., ∶ Atm ⟶ ℒ expresses the fact that the function maps elements of Atm into elements of ℒ.17 Function definition by cases is expressed by the standard notation distinguishing values for each case considered. 13Further conventions, abbreviations, and notation overload are promptly and appropriately signaled in the main body of the paper as soon as they are introduced. 14E.g., conjunction is denoted by the symbol ‘∧’. 15E.g., the expression { ∈ × ℬ ∶ 1() & 2()} denotes the set of pairs of elements in and ℬ satisfying a given condition 1 and a given condition 2. 16However, we may write, e.g., ∈ Ag to express that the item with label denotes an agent of our protocol. 17Notice the diference between the long arrow symbol ⟶ used for functions, from the arrow symbol ⇾ we use for sending statements in our protocol language. Graphical conventions.
We use squares to denote actions in action models, reserving more rounded nodes for the worlds of static epistemic models. Whenever ≈ in the action model, we draw an arrow with label from the square labeled by to the square labeled by ; whenever ≈ and ≈ we draw a bi-directed arrow between and ; an arrow labeled by Ag denotes a collection of labeled arrow, namely one for each agent in our given set; when we remove the -labelled arrows from that collection, we obtain the collection represented by the (Ag − ) -labeled arrow. Similar conventions are applied to arrows between worlds rendered in Section 5.
In symbols, (, ) = label .
A protocol choreography in SPEC is defined as ‖ ⟨ , ⟩ where ∈ {1, … , } . is a function mapping each agent label appearing in each protocol agent to another agent in the choreography. denotes that agent will send to (and receive from) agent when using
For the sake of presentation, we use ⟨ 1, 1⟩ ‖ ⟨ 2, 2⟩ for ⟨ 1, 1⟩‖ ⟨ 2, 2⟩ where () and are the only labels appearing in 2 and 1 (respectively), and () (1, ) = 2 and (2, ) = 1 .
We can now introduce the operational semantics of protocol choreographies, given in Figure 6. Briefly, choreographies allow internal reduction of their protocol agents (Step) and synchronous ⟨ , ⟩ ⟶ ⟨ ′, ′⟩ communications between agents (Sync) when the agent labels mapping permits it.
We say that a choreography ‖ ⟨ , ⟩ is successful when ∀. = ⋅ and we call stuck a choreography that () is not successful and () does not allow further reductions (denoted by ⇝̸). Furthermore, we use ⇝⋆ for the transitive closure of ⇝ and, given two choreographies and ′, we say that ⇝ ⋆
′ is a run of if ′⇝̸.
Then, a successful run of is a run ⇝ ⋆ ′ such that ′ is successful. For instance, by defining the choreography ≜ ⟨[ actual cryptographic keys, we have
k1/], ⟩ ‖ ⟨[ k1/ 1][k2/ 2], ⟩, where k1 and k2 denote ⇝ ⋆ ⟨[ −1/][ enc( , )/][ enc( , )/ ][ h()/][/ ′], ⋅⟩ ‖ ⟨[ / 1][ / 2][/], ⋅⟩.
Here, we provide full details on the intermediate model omitted in Section 5 when modeling . We render the model through the three-part table in Figure 7 (denoting that the variable is either 1, 2, or unassigned ∅) where: • rows represent the possible values of (namely: enc( 1, 1), enc( 1, 2), enc( 2, 1), enc( 2, 2)); • columns represent the possible values of ((namely: enc( 1, 1), enc( 1, 2), enc( 2, 1), ⎡⎢⎢ enc( 1, 1) aha(1a)ah( 2) aha(1a)ah( 2) aha(1a)ah( 2) aha(1a)ah( a2a) ⎢⎢ enc( 1, 2) aha(1a)ah( a2a)aha(1a)ah( a2a)aha(1a)ah( a2a)aha(1a)ah( a2a) ∅ ⎢⎢⎢ enc( 2, 1) aha(1a)ah( a2a)aha(1a)ah( a2a)aha(1a)ah( a2a)aha(1a)ah( a2a) ⎢⎢ enc( 2, 2) aha(1a)ah( aa2aa)aha(1a)ah( aa2aa)aha(1a)ah( aa2aa)aha(1a)ah( a2a) ⎣ ⎡⎢⎢ enc( 1, 1) aha(1a)ah( 2) aha(1a)ah( 2) aha(1a)ah( 2) aha(1a)ah( a2a) ⎢⎢ enc( 2, 2) aha(1a)ah( aa2aa)aha(1a)ah( aa2aa)aha(1a)ah( aa2aa)aha(1a)ah( a2a) ⎣ enc( 2, 1) enc( 2, 2) ⎢⎢ enc( 2, 2) aha(1a)ah( aa2aa)aha(1a)ah( aa2aa)aha(1a)ah( aa2aa)aha(1a)ah( a2a) ⎣ Figure 7: Modelling the epistemic evolution of ℐBKP when sequentially receives from messages in , , and .
Then, the first guard [comp(, )]
allows us to select from the 96 nodes of the epistemic model those containing the local information of triggering the guard, represented by the blue further narrows down the cells in the table.18 The subsequent guard [ = h(trydec(, , ))] possibilities, enabling us to identify, among the blue cells, the sub-cells highlighted with red text that satisfy the guard and allow to send trydec(, , ) to . 18Recall from Section 4.1 that comp(⋅) is true when keys are diferent and the message is the same.