BRICS

Basic Research in Computer Science

The Full Abstraction of the UC Framework

Jesús Fernando Almansa BRICS Report Series RS-04-15 ISSN 0909-0878 August 2004 BRICS RS-04-15 J. F. Almansa: The Full Abstraction of the UC Framework Copyright \begin{matrix}c \\ ◯ \end{matrix} 2004, Jesús Fernando Almansa.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/04/15/

The Full Abstraction of the UC Framework

Jesús F. Almansa

                   jfa@brics.dk

BRICS^{∗}, Department of Computer Science University of Aarhus IT-parken, Aabogade 34 DK-8200 Aarhus N, Denmark

Abstract

We prove that security in the Universal Composability framework (UC) is equivalent to security in the probabilistic polynomial time calculus ppc. Security is defined under active and adaptive adversaries with synchronous and authenticated communication. In detail, we define an encoding from machines in UC to processes in ppc and show it is fully abstract with respect to UC-security and ppc-security, i.e., we show a protocol is UC-secure iff its encoding is ppc-secure. However, we restrict security in ppc to be quantified not over all possible contexts, but over those induced by UC-environments under encoding. This result is not overly-simplifying security in ppc, since the threat and communication models we assume are meaningful in both practice and theory.

∗Basic Research in Computer Science (www.brics.dk), funded by the Danish National Research Foundation

Contents

1 Introduction 1

2 UC framework 3 2.1 Interactive Setting . . . . . . . . . . . . . . . . . . . . . . . . . 3 2.2 Security Definition . . . . . . . . . . . . . . . . . . . . . . . . . 4

2.2.1 The Hybrid Model . . . . . . . . . . . . . . . . . . . . . 4 2.2.2 The Ideal Process . . . . . . . . . . . . . . . . . . . . . 5

3 Probabilistic calculus ppc 6

4 Encoding and Main Result 10 4.1 Encoding Environments . . . . . . . . . . . . . . . . . . . . . . 13 4.2 Main Result . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15

5 Appendix: 19 5.1 ∅-hybrid Model and Ideal Process . . . . . . . . . . . . . . . . 19 5.2 Encoding of Interactive Rules . . . . . . . . . . . . . . . . . . . 19 5.3 Proof Proposition1 . . . . . . . . . . . . . . . . . . . . . . . . . 19 5.4 Proof Lemma 1 . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 5.5 Proof Lemma 2 . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 5.6 ppc-Composition Theorem . . . . . . . . . . . . . . . . . . . . . 20

1 Introduction

For as long as at least two decades there has been a gap in the analysis of security protocols as approached by different research communities with distinct methods: notably process calculi and (probabilistic) machine-based.

Calculi appeal especially because they are susceptible to automated proofconstruction or at least automated proof-validation. However, they have traditionally fallen short of modeling realistic adversarial behaviours, thus disabling them as frameworks for reasoning about general security.

In contrast, probabilistic machine-based methods have traditionally better captured realistic adversarial threats. However, proofs are by nature handmade, thus error-prone when applied to challenging scenarios like large distributed systems.

Because security-reasoning is subject to specifying an (realistic as it can be) adversarial model, given the above said, it seems natural to look for bridging the gap in the direction from calculi to the machine-based field, aiming at soundness and completeness results. Nonetheless, several attempts in this line have focused on specific security concerns, mainly secure message transmission, and/or on restricted adversarial models, mainly passive adversaries.

In this document we take the other direction for bridging the gap and show the existence of a fully-abstract encoding of a machine-based framework into a process-calculus framework, under active and adaptive adversaries, with authenticated and synchronous communication.

We emphasize these are frameworks for reasoning about any protocolsecurity concerns. The term fully-abstract refers to the soundness and completeness of the notion of security in the calculus with respect to that in the machine-based framework. The adversarial model is active and adaptive, meaning respectively that a corrupt party can arbitrarily deviate from the protocol and corruptions can occur at any point of the computation.

The machine-based framework is that introduced by Canetti in [Can01], where secure protocols enjoy general concurrent composition or, as it is called there, Universal Composability (UC). All computing entities are modeled as probabilistic polynomial time (PPT) Interactive Turing Machines (ITM’s), which are basically PPT multi-tape Turing machines, that can exchange data by sharing some of their tapes. It adopts the simulatability paradigm to define security, where a protocol-run is compared to a simulated-run that has access to an ideal functionality (another ITM) defining the input/output behaviour of the protocol. The security definition states a protocol realizes the ideal functionality if no adversarial environment can tell apart interactions with the protocol and those with the simulation that uses the ideal functionality.

The calculus is the probabilistic polynomial-time process calculus ppc by Mateus, Mitchell and Scedrov in [MMS03], preceded by [LMMS99] and [LMMS98], where a compositional property is derived. It adopts the simulatability paradigm to define security, where a real-process is compared to an ideal-process that simulates its data-exchange behaviour. The security definition states that real and ideal process are equivalent if no context can tell apart data-exchange with the real process and that with the ideal process.

In [Can01] it had already been stated how that framework could serve as a computationally-sound basis for automated analysis with formal methods. With the advent of [MMS03] it was left open the question whether there was a correspondence between their PPT process calculus and the UC framework. We therefore answer this question in affirmative and moreover prove that a protocol is UC secure if and only if its encoding is ppc secure, subject to the adversarial model mentioned above.

We observe that to that end we restrict security in ppc to contexts induced by UC environments under encoding, instead of quantifying over any context. But we argue that this is a natural restriction to make due to our basic assumptions on the adversarial and computation models.

An Intuition The interactive setting of the UC framework can be thought of as a laboratory we use to carry out our experiments under controlled and unbiased conditions. In particular, it relies on an interleaving mode of concurrency. Similarly, linking tapes do not model communication channels of real protocols.

This is an importan clarificatory observation since it is this interactive setting what we encode in the ppc calculus. As an effect, we separate from the traditional notion of attacks over channels on process calculi, in order to introduce that of corruption of parties.

We believe this is a major step towards automation of security proofs in the UC framework. Having translated the framework once and for all, protocol design reduces to providing the code of parties, and security analysis reduces to study patterns of observable traces with the existent tools for process calculi.

Related Work Many research efforts stemmed from the process calculus approach. Among the most relevant is the project in [MMS98, LMMS98, LMMS99, MMS03], where PPT processes are considered. This is the source of the calculus we base our result on.

A parallel and independent work to ours is that in [DKM^{+}04, DKMR04, DKMR05], where they prove the equivalence of several simulatability-based security definitions in any process calculus satisfying certain axioms. Their result concentrates on three essential aspects of the simulatability paradigm when aiming at composition-preserving properties: The logical structure of security definitions (or the order of quantifiers), the scheduling or timing assumptions of adversaries and the adversarial attributes of distinguishers (or separation between adversaries and distinguishers). Although they relate their results to machine-based models in terms of expressivity they do not formally provide an evidence^{1}.

Their work and ours are thus complementary in that we treat explicitely the three above mentioned aspects, while crossing from a PPT machine-based model to a process-calculus approach, thus closing a gap up to now existing in literature.

Finally, the work by Backes, Pfitzmann and Waidner [PW00, BPW04], stands out as an alternative model for simulatability-based security analysis. By formalizing the notion of a reactive system using input/output automata, they have also achieved general concurrent composition properties while at the same time already provided tools for automated reasoning.

Organization The rest of this document is organized as follows. Section 2 begins with a general discussion about ITM’s and proceeds by describing the UC framework and its security definition. Section 3 describes the process calculus ppc and its security definition. Section 4 introduces an encoding from UC machines into ppc processes and ends by stating our main result and providing its proof.

Acknowledgments The author would like to thank Marco Carbone, Ivan Damgård, Karl Krukow, Peter D. Mosses, and Mogens Nielsen for numerous discussions and invaluable suggestions and insights. Likewise, I express my gratitude to Frank Valencia and Daniele Varacca for their comments on early versions or this document.

2 UC framework

2.1 Interactive Setting

Following [Can01], we adapt the notion of ITM from [GMR89, Gol01] to the multiparty case. An ITM E is a PPT multi-tape Turing Machine that interacts by sharing some of its tapes. We use !_{tape_{E,E′}} v to indicate the action of writing v on the (write-only) tape named tape_{E,E′}. Similarly, we use ?_{tape_{E′′,E}} v to indicate the action of reading v from the (read-only) tape named tape_{E′′,E}.

We say E_{1}, E_{2} are linked by (linking) tapes tape_{E_{1},E_{2}} and tape_{E_{2},E_{1}}, if whenever E_{1} executes !_{tape_{E_{1},E_{2}}} v then E_{2} will execute ?_{tape_{E_{1},E_{2}}} v, and vice-versa with the other tape. A machine’s signature is the set of its linking tapes.

The execution-mode is interleaving, i.e., only one machine is activated at a time. This is modeled by a tape activate shared by all machines and containing the identity of the currently running machine. A machine that is not activated is said to be waiting.

1To the best of the author’s knowledge, this is still the case when [DKMR04] made transit to [DKMR05].

The behaviour of an ITM E is defined by its associated interactive function (v′, ς′) ← E(v⃗, ς). It takes (v⃗, ς) as argument, formed by the vector of received values found at the moment of its activation, and its current state. It computes (v′, ς′), consisting of the values to be sent at the end of its activation, and its next state. The initial state contains only the system’s security parameter, the machine’s random tape and possibly some auxiliary input.

We define E(v⃗, ς) as a (finite) set of interactive rules of form

\frac{?_{rtape_{1},...,rtape_{R}} v_{1}, …, v_{R}}{(v′,ς′)←E(v⃗,ς) !_{wtape_{1},...,wtape_{W}} v′_{1},...,v′_{W}} ,

according to the values v⃗ can take. Such a rule is read: Upon activation, if E has received values v⃗ = v_{1}, …, v_{R}, with v_{i} on rtape_{i}, i = 1, …, R, and has current state ς, then compute E(v⃗, ς), to result in values v′ = v′_{1}, …, v′_{W} and new state ς′, write v′_{j} on wtape_{j} sequentially, and pick machine E_{j}, j = 1, …, W, to be activated next.

Thus, to describe an ITM E is sufficient to provide its signature and its set of interactive rules.

We define an n-party interactive protocol as consisting of n ITM’s P_{1}, …, P_{n} having distinct id’s, that are not linked among them. Such protocol is geared towards holding an ongoing interaction with an environment, which is explicitely modeled by an ITM Z that is linked to each party. With this definition we are to embed communication between each two parties through interactions with the environment. This setting shows particularly useful when providing adversarial attributes to the environment.

2.2 Security Definition

Security is defined by comparing a protocol execution with an ideal process that specifies its input/output (I/O) interaction with the environment. We declare security if no environment can distinguish interactions with the real protocol from those with the ideal process.

2.2.1 The Hybrid Model

We adopt the activation model of [DN03, Nie04], which is a specialization of the UC framework to synchronous networks. For space reasons we consider only the ∅-hybrid model or real-life model, but we observe that our result holds straightforwardly in the more general case.

The model consists of an n-party interactive protocol π, where P_{i} is the identity of the i-th machine running in π. The environment Z provides inputs to and receives outputs from the parties. Furthermore, it models point-to-point open but authenticated channels between each pair of parties and is assumed to provide (partially) synchronous communication.

This entity also models the adversary and so it schedules the order of activation of parties, and breaks into parties actively and adaptively. We emphasize that although Z reads the messages exchanged between parties, it is not allowed to inject, delete or modify any message.

Definition 1 The signature Σ(E) of E ∈ {Z, P_{i}}, i = 1, …, n, in the ∅-hybrid model is defined as follows, where -r-,-w- stand for read-only and write-only:

Σ(Z) =^{def} { -r-outByP_{i},  -w-inToP_{i},
-r-msgByP_{i},  -w-msgToP_{i},
-r-corrByP_{i},  -w-corrToP_{i} }
Σ(P_{i}) =^{def} { -r-inToP_{i},  -w-outByP_{i},
-r-msgToP_{i},  -w-msgByP_{i},
-r-corrToP_{i},  -w-corrByP_{i} }

The environment is activated first and the execution proceeds by rounds, where Z runs commands (beg rnd) and (end rnd), to begin and end a round, respectively. It can also run commands (corrupt) and (guess), to corrupt some party and to decide its observation of the execution and halt, respectively. The output of the ∅-hybrid execution is a bit b output by Z. The interactive rules appear in Fig 2 in Appendix, where it is formally defined how Z runs commands, how parties respond to them, and what linking tapes are used.

Notation 2 We denote HYB_{π,Z}^{∅}(k, z, 𝔯⃗), the bit output by Z on security parameter k, auxiliary input z to Z and random input 𝔯⃗ = 𝔯_{Z}, 𝔯_{1}, …, 𝔯_{n}. This gives rise to a random variable HYB_{π,Z}^{∅}(k, z), when 𝔯⃗ is uniformly chosen. We denote HYB_{π,Z}^{∅} the ensemble {HYB_{π,Z}^{∅}(k, z)}_{k∈ℕ,z∈{0,1}^{∗}}.

2.2.2 The Ideal Process

As mentioned in the begining of this section, security is defined with respect to an ideal functionality, ITM F, that specifies the I/O behaviour of the protocol. It also specifies information allowed to be leaked from the protocol.

We can think of F as all P_{i}’s comprised in one single machine. In fact, there are no parties in the ideal process. A special ITM T called interface is introduced to respond on behalf of parties to commands by Z.

We say π is secure if there exists an interface T capable of simulating a run of π maintaining its I/O behaviour having access to F. However, we note the interface works by being given solely the corrupt parties’ inputs as well as all leaked information from F. This captures both secrecy and correctness of the protocol.

The signature of Z is the same as in the ∅-hybrid model, but we include it in the next definition for the sake of completeness.

Definition 3 The signature Σ(E) of E ∈ {Z, F, T } in the ideal process is defined as follows, where -r-,-w- stand for read-only and write-only, and i = 1, …, n:

Σ(Z) =^{def} { -r-outByP_{i},  -w-inToP_{i},
-r-msgByP_{i},  -w-msgToP_{i},
-r-corrByP_{i},  -w-corrToP_{i} }
Σ(T ) =^{def} { -r-msgToP_{i},  -w-msgByP_{i},
-r-corrToP_{i},  -w-corrByP_{i},
-r-leaked,  -w-probe }
Σ(F) =^{def} { -r-inToP_{i},  -w-outByP_{i},
-r-probe,  -w-leaked }

The output of the ideal process is a bit b output by Z. Fig. 3 in Appendix formally describes the simulation.

Notation 4 We denote IDEAL_{F,T ,Z}(k, z, 𝔯⃗), the bit output by Z on security parameter k, auxiliary input z to Z and random input 𝔯⃗ = 𝔯_{Z}, 𝔯_{T} , 𝔯_{F}. This gives rise to a random variable IDEAL_{F,T ,Z}(k, z) when 𝔯⃗ is uniformly chosen. We denote IDEAL_{F,T ,Z} the ensemble {IDEAL_{F,T ,Z}(k, z)}_{k∈ℕ,z∈{0,1}^{∗}}.

In our next definition, ≈^{c} stands for computational indistinguishability.

Definition 5 (UC Security) A protocol π t-securely realizes a functionality F (in the ∅-hybrid model) if there exists an interface T such that for all environments Z corrupting at most t parties it holds that IDEAL_{F,T ,Z} ≈^{c} HYB_{π,Z}^{∅}.

We finish this section by stating two properties about the interactive pattern of machines in the UC framework.

Proposition 1 In both the ∅-hybrid model and the ideal process it holds that:

i) No execution leads to a deadlock.

ii) For each machine other than Z, there is one and only one interactive rule to be applied upon activation. For Z this is also the case except for the corruption rule and the guessing rule which can always be applied.

3 Probabilistic calculus ppc

We provide an overview of the probabilistic polynomial-time calculus ppc. The reader is referred to [MMS03] for full details.

The calculus is given a security parameter k and sets Var, Chan of variables and channels. Its set Term of terms represents all PPT functions on k, PPT (k), and only these. Moreover, if t_{f} ∈ Term corresponds to f ∈ PPT (k), then the probability that t_{f}(x) evaluates to some a is defined as the probability that the associated machine M_{f} computing f converges to a on input x,

i.e., P (t_{f}(x) → a) =^{def} P (a ← M_{f}(x, k)).

In addition, there is a bandwidth map w : Chan → q, where q is the set of all ℕ-valued polynomials in one variable. This map bounds the length of data sent through channels and guarantees that computations are polynomial time.

We use the synchronous version of ppc with input choice. Its expressions are of the following kind: Inaction 0, private channel ν_{c}.Q, output ⟨t⟩_{c}.Q, input (x)_{c}.Q, matching [t_{1} = t_{2}].Q, parallel Q_{1}|Q_{2}, input-choice ⟨t_{1}⟩_{c_{1}}.Q_{1}+⟨t_{2}⟩_{c_{2}}.Q_{2}, and replication !_{q}Q, where q is a polynomial in |k|, and the expression is expanded to polynomially in |k| many copies of Q. An expression Q where the security parameter takes a fix natural number m is called a process and denoted Q_{m}.

A free variable is one not in the scope of any (·)_{c}. A process is closed if it has no free variables.

It is customary to assume that private channels are named apart from other called public. Typically, private channels are used for modeling internal data exchange in a single machine, hence it is considered an unobservable behaviour. In contrast, data exchange through public channels models the observable behaviour. We will come back to this later.

The meaning of a process Q is a Markov chain over multisets of subprocesses of Q without parallel operator. Recall a Markov chain can be modelled as a state machine, where transiting from one state to another is assigned a probability and where the fan-out probabilities for each state sum up to one. Thus, the intuition for the Markov chain of a process is that states are stages of reduction and transitions are probabilistic choices between reductions.

The only two sources of probabilities in ppc are evaluation of terms and selection among simultaneous process reductions. The first case was already mentioned above. For the second case, a policy of reduction has to be fixed, so that the next process to be reduced can be selected probabilistically.

Given a process Q, a Markov chain S(Q) where a policy of reduction has been fixed is called a scheduler. The initial multiset (state) is obtained from Q by expanding all replications and next removing all parallel operators. Private channel operators are also removed by renaming private channels with fresh channels, from a set distinct to Chan, that conserve the bandwidth. In the sequel, unless the contrary is indicated, we will assume all replication and private operators have been removed.

The elegible processes for reduction are terms, matchings (mismatchings) and communications, in this order. It is defined that only communications over public channels are observable. They are pairs ⟨c, v⟩ of public channels and values. Any other reductions are silent actions and are modeled by τ. Private communications thus are silent. The set Ob includes both τ and all observable communications.

By establishing that τ actions have higher priority of reduction than public communication, it is ensured that an adversary will not distinguish two processes by sampling their internal (unobservable) behaviour.

Finally, in order to determine which observations take place in a process (out of the set Ob of all possible observations), a modulated Markov process K(Q) = (S(Q), O(Q)) is given, where S(Q) is a fix scheduler and O(Q) is the stochastic process of observations of Q over Ob. Roughly, K(Q) is like S(Q), but assigns probability zero to any other observation in Ob not ocurring in S(Q). Details on this are out of the scope of this document and can be found in [MMS03].

Given K(Q), the probability of observing some o ∈ Ob at any point of the reduction trace is written P (Tr(Q)_{k}^{S} = o). It is an infinite series indexed i = 1, 2, …, where series-term i is the probability that o is output for the first time at the i-th reduction step. Notice random variable Tr is parameterized with the security parameter k and scheduler S. We abbreviate Tr(Q) the random ensemble {Tr(Q)_{k}^{S}}_{k∈ℕ,S}.

For the next definition recall contexts are processes with holes.

Definition 6 A closed process Q_{1} is observationally equivalent to another Q_{2}, written Q_{1} ≃ Q_{2}, iff for all schedulers and for all contexts C[ ] it holds that

Tr(C[Q_{1}]) ≈^{c} Tr(C[Q_{2}]).

The definition of protocol security follows by relating a protocol with an ideal specification and showing they are observationally equivalent, with respect to classes A, B of contexts modeling real-process and ideal-process adversaries, respectively.

Definition 7 ([MMS03]) A closed process Q emulates an ideal specification closed process I with respect to sets of contexts A and B, written Q ≡_{A,B} I, iff for all A[ ] ∈ A there exists B[ ] ∈ B such that A[Q] ≃ B[I].

We note definition 7, seems to demand the class B of ideal-specification adversaries is defined independently from the class A of real-process adversaries. In fact, it does not really make sense to reason about an a priori class of ideal-process adversaries. While it is true that the specification I of a cryptographic task is provided with respect to and adversarial model, this model is but a generic description of threats (to later prove the attacks can be thwarted) that the calculus should be able to express but independently on whether they mean ideal-process attacks or real-process attacks.

For instance, an adaptive adversary is one that can make a corruption at any point of the reduction (execution). The term “at any moment” is what defines adaptiveness and should be expressed by the calculus, but it does not depend on whether the reduction is in an ideal or a real process. Clearly, “to make a corruption” is something to be defined too.

Only once the threat model is set, the notion of security is captured by taking any real-process adversarial strategy (constrained to the threat model) and proving there is some ideal-process adversarial strategy (constrained to the same threat model) but deemed unsuccessful in the ideal-process reduction, hence showing that a real-process is as secure as the ideal-process specification it emulates. As we will see later, a technical contribution of our work shows that different threat models can be expressed in the calculus, since they can already be expressed as (adversarial) machine behaviours that can be translated via encoding.

Under the above considerations, it would just suffice to drop A, B in definition 7: Definition 7’ (Revised) Fix a threat model. A closed process Q emulates an ideal specification closed process I, written Q ≡ I, iff for all A[ ] bound to the threat model there exists B[ ] bound to the same threat model such that A[Q] ≃ B[I].

One has to be careful with the meaning of quantifying over all contexts C[ ] in definition 7’. There, adversaries are separate entities from distinguishers, and so the process-interaction a context C[ ] sustains is limited to (public dataexchange) providing inputs and receiving outputs but without the capability of corrupting.

We are precisely now in a position similar to that in [Can01]^{2} where it could be argued there is not loss of generality in allowing distinguishers model adversaries too, since they both are contexts. Let us present the alternative security definition before resuming our discussion.

Definition 8 Fix a threat model. A closed process Q emulates an ideal specification closed process I iff there exists a context D[ ] bound to the threat model such that Q ≃ D[I], where observational equivalence is defined with respect to all contexts whose corrupting capabilities are bound to the threat model.

Contexts C[ ] in the definition above could be thought of as having the form C′[A′[ ]] where A′[ ] models its corrupting capabilities (bound to the underlying threat model) and C′[ ] models its reactive feature (of providing inputs and receiving outputs).

Notice well here that definitions 7’ and 8 are essentially swapping the order of quantifiers, from ∀A[ ] ∃B[ ] to ∃D[ ] ∀A′[ ], respectively^{3}. It follows the natural question of under which conditions the two definitions are the same.

2See Definition 4 in [Can01], where environments play also the role of adversaries.

One direction is obvious^{4}. The implication from definition 7’ to definition 8 is not immediate. At its core lies what black-box simulatability is, which is the most-known form of simulatability so far in the literature.

For concreteness, we mention two ways to get around this implication: We could in the first place prove our result of full abstraction of UC in ppc, with respect to both definition 7’ and 8 separately, and then use the fact that in the UC framework the corresponding two definitions are equivalent. But deriving the equivalence of the two definitions of security in ppc is not our goal. We aim at showing there is a correspondence between security in the UC framework and security in a non-machine-based framework as ppc.

An alternative is to directly use the result in [DKM^{+}04, DKMR04], where it is proved definitions 7’ and 8 are equivalent for any process calculus whose notion of process-equivalence satisfies certain axioms, and apply it in particular to ppc.

In the remaining of this document we will make use of definition 8. Our choice is motivated by the belief this definition is technically simpler and intuitively well justified, although arguably less pedagogical.

Finally, it is worth noticing the compositional-security guarantee of ppc in terms of definition 8 also holds (See section 5.6 in Appendix).

4 Encoding and Main Result

We define an encoding that translates the ITM’s of UC into processes in ppc. Since we are interested in transporting the interactive setting of UC, for an encoding to be “reasonable” we require it to preserve: machine signatures, interleaving mode, activation orders, and probability distributions over linking tapes.

Intuitively, a machine’s encoding consists of a choice of (the encoding of) its interactive rules wrapped up by a bigger process reminiscent of the machine’s shell.

A salient disctinction, however, is that while the premise of a rule is a predicate for a machine, the same premise is actually a prefix of inputs on channels for the machine’s encoding. This poses a challenge when encoding, in the case there are two intersecting rules, i.e., there is a tape in the premises of two rules from where they expect different values.

One solution is to group intersecting rules into a single one by prefixing with the common input channel (tape) and then branching according to the values they expect.

3To see why, develop in both definitions the meaning of observational equivalence and use the fact that C[ ] = C′[A′[ ]] in definition 8.

4Simply take B[ ] = A[D[ ]].

We observe the only difference between encodings of intersecting and nonintersecting rules is their input prefixes. But this does not affect the interactive pattern of the machine under encoding.

For simplicity, our definition of encoding does not consider intersecting rules, and we postpone encoding non-intersecting rules to section 5.2 in Appendix.

Definition 9 Let n ∈ ℕ and k ∈ ℕ be a security parameter. Let E ∈ {P_{i}, F}, i = 1, …, n, having l pairs of linking tapes^{5}, and m non-intersecting interactive rules of form

?_{rtape_{s_{1},...,s_{R_{i}}}} v_{s_{1}}, …, v_{s_{R_{i}}}

(v′_{t}, ς′) ← E(v⃗_{s}, ς) ∀_{t1,...,t_{W_{i}}}!_{wtape_{t.}} v′_{t.} !_{activate} E_{a} waiting

,

where s_{1}, …, s_{R_{i}}, t_{1}, …, t_{W_{i}} ∈ {1, …, l}, and a ∈ {t_{1}, …, t_{W_{i}}}. The encoding ⟦E⟧ is defined as:

⟦E(k)⟧ = !_{q(k)}( )_{unblock_{E}} .( )_{activate}. ( ⟨ ⟩_{isToDeliver}
| (b)_{deliverySet}. (
[b = empty]. (⟨ ⟩_{getState_{E}} | Rules)
| [b = notempty].⟨ ⟩_{deliver}))
|!_{q(k)}Store_{E}

with Rules = (ς)_{currentState_{E}} . (Rule_{1} + ⋯ + Rule_{m}), and

Rule_{i} = (v_{s_{1}})_{rtape_{s_{1}}} . · · · .(v_{s_{R_{i}}})_{rtape_{s_{R_{i}}}} .
(⟨proj_{1}(E)(v⃗_{s}, ς)⟩_{wtape_{t_{1}}} | ⋯ |⟨proj_{W_{i}}(E)(v⃗_{s}, ς)⟩_{wtape_{t_{W_{i}}}} |
⟨proj_{W_{i}+1}(E)(v⃗_{s}., ς)⟩_{updateStore_{E}} .⟨ ⟩_{unblock_{E}} .⟨E_{a}⟩_{activate})

where proj_{j}(E) is the j-th projection of E, j = 1, 2, …, W_{i}. Subprocess Store_{E} encodes E’s state. Channels ( )_{rtape_{s.}}, ⟨ ⟩_{wtape_{t.}} are public and encode E’s linking tapes; channel ( )_{activate} is private to the system and encodes its activation tape. All other channels are private to E but accessible to subprocess Store_{E}.

We define the encoding of n ITM’s E_{1}, …, E_{n}, as ⟦E_{1}, …, E_{n}⟧ =^{def} ⟦E_{1}⟧| … |⟦E_{n}⟧.

Since PPT (k) and Term are in one-to-one correspondence, we use the same expression for denoting functions proj_{j}(E) and its terms.

Even though a key element of our encoding is a heavy use of updatable storage cells in order to model machines’ states, the definition of Store_{E} is left out from this document. Encoding states does not require more than what is known in the literature for encoding data structures. On the other hand, this is a laborious effort that does not add clarity to our discourse. Nevertheless, we can informally specify what Store_{E} does and we observe its tasks are exclusively performed through private channels.

5For an n-party protocol, l_{P_{i}} = 3 and l_{F} = n + 1.

Several remarks justifying E’s encoding are in place: First, the replication operator ensures the encoding is polynomial-time in the same security parameter k. Also, the reduction of terms proj_{j}(E) on arguments (v_{s_{1}}, …, v_{s_{W_{i}}} , ς) has the same distribution as E’s computation on those arguments^{6}. Finally, E’s linking tapes with the environment are the only public channels, on which data-exchange is to be observed.

We recall a feature of ppc is that private data-exchange has higher priority than the public one. This is exploited to enforce some computations in sequence without altering the probability distributions of public events.

Process E = ⟦E⟧ computes by activations turns, where there is one copy of its replicator per activation. Observe all copies of E are blocked. Each activation turn finishes with two actions: First, it releases a new copy of itself through private channel ⟨ ⟩_{unblock_{E}} and second, it activates another process E_{a} through public activation channel ⟨E_{a}⟩_{activate}. This guarantees that only one copy of a process is available per activation.

When E is activated, it first asks through ⟨ ⟩_{isToDeliver} whether there is any data to deliver. Subprocess Store_{E} answers through ( )_{deliverySet}, based on a set containing the identities of processes for which there is data to deliver. If this set is not empty, then Store_{E} chooses a new process and activates it through its activation channel, and also releases a new copy of E. If the delivery-set is empty, Store_{E} is then asked to send E’s current state and next one of the encoded interactive rules will be used.

Process Rules receives first E’s state and then, in virtue of Proposition 1, reduces through the only rule whose input prefix is valid. Let Rule_{i} be this rule. It then computes the function E(v_{s_{1}}, …, v_{s_{R_{i}}} , ς), by using the projection functions proj_{j}, j = 1, …, W_{i}, in order to write each of the resulting values (v′_{t_{1}}, …, v′_{t_{W_{i}}}) in the corresponding public channels for processes E_{t.}, as well as writing its next state ς′ to Store_{E}.

Notice that writing ⟨v_{t.}⟩_{wtape_{t.}} does not activate processes E_{t.}. First, Store_{E} constructs the delivery set with the identities of processes E_{j} to be activated in sequence, one at a time. Only then a new copy of E is released, exhausting the current one, and the activation is handed over to E_{a}.

Furthermore, at the end of an activation there are not dangling subprocesses of the current activated copy, since all possible simultaneous alternatives are exhausted either by matchings or input choices.

6Consider e.g. the PPT machine that on input (v⃗, ς) computes (v′, ς′) like E, but then discharges say ς′.

⟦Z(k, z)⟧ =  !_{q(k)}( )_{unblock_{Z}} .( )_{activate}. (
⟨ ⟩_{corrupt}|( )_{corruptdone}. (
⟨ ⟩_{guess}|( )_{noguess}. (
⟨ ⟩_{isToDeliver}|(b)_{deliverySet}. (

[b = empty]. (⟨ ⟩_{getState_{Z}} | Rules)

| [b = notempty].⟨ ⟩_{deliver}))))
| !_{q(k)}Store_{Z}
| !_{q(k)}Corrupt
| !_{q(k)}Guess

with Rules = (ς)_{currentState_{Z}} . (( )_{beg rnd}.Rule BgnRnd + ( )_{end rnd}.Rule EndRnd)

Figure 1: Definition of Process Environment

4.1 Encoding Environments

Crucially, we can also encode both interfaces and environments, hence adversarial behaviours. Here we examine only the case of environments, but observe that the other case uses similar ideas.

The translation is somewhat different to that in definition 9, since an environment can corrupt a party at any moment or decide its guess on the execution and halt. Concretely, by the definition of an environment ITM in Fig. 2, its encoding has rules Rule BegRnd, Rule EndRnd, modeling Z’s behaviour when receiving messages or outputs from parties, respectively. In contrast, both the corruption case and the guessing case are not just rules, but replicated subprocesses Corrupt and Guess, which are at the same level of Z’s state. Figure 1 formally defines an environment.

We describe only Rule BegRnd, but observe that Rule EndRnd is similar. This rule is valid when a new round of computation is to begin and this happens when all honest parties have sent their previous-round outputs: Rule BegRnd = ⟨P_{1}⟩_{inHonest}|(a)_{isHonest} ([a = no].0 |

[a = yes].(v_{1})_{msbByP_{1}}.⟨v_{1}⟩_{fwdmsgByP_{1}}.

(⟨P_{2}⟩_{inHonest} … (⟦(·) ← Z⟧) …))

We have written ⟦(·) ← Z⟧ to abbreviate Z’s actions in that point of the rule. It consists in sending in parallel the new-round messages and inputs for each honest party through corresponding channels ⟨ ⟩_{msgToP_{i}} and ⟨ ⟩_{inToP_{i}}, by using the projections functions of Z.

This rule simply reads party P_{i}’s channel as long as this party is honest, and if so, forwards the value through a private channel to its inner-most process ⟦(·) ← Z⟧.

When process Corrupt is called, it reduces just like defined in Fig. 2, by modifying Z’s state. Given the current state, this process may corrupt up to t parties, one at a time. It selects a party P_{j} to corrupt and activates P_{j}’s store, Store_{P_{j}}, through public channel ⟨ ⟩_{corrToP_{j}}. It then receives P_{j}’s state back through public channel ( )_{corrByP_{j}}, and updates Z’s store, Store_{Z}, which also updates sets C := C ∪ {j}, H := H \ {j} of corrupt and honest parties, respectively. From this moment on, party P_{j} will not be activated any more, since in ⟦(·) ← Z⟧ above, new-round messages and inputs are computed and sent only to honest parties.

Encoding environments gives rise to a prominent set of processes in ppc:

Definition 10 Let n ∈ ℕ. We let Z_{UC}(n, k, z) be the image under encoding of the set of all UC environments modeling threshold, active and adaptive adversaries with synchronous and authenticated communication, that interact in n-party protocols with variable security parameter k ∈ ℕ and variable auxiliary input z ∈ {0, 1}^{∗}. i.e., Z_{UC}(n, k, z) =^{def} {⟦Z(k, z)⟧ : Z ∈ UC}.

We intend to use these processes as distinguishers in ppc. In order to do so, we restrict observational equivalence to the class of contexts of form Z|[ ], where Z ∈ Z_{UC}(n, k, z). More precisely,

Definition 11 A closed process Q_{1} is UC-observationally equivalent to another Q_{2}, written Q_{1} ≃_{UC} Q_{2}, iff for all schedulers and for all Z ∈ Z_{UC}(n, k, z) it holds that T r(Z|[Q_{1}]) ≈^{c} T r(Z|[Q_{2}]).

Consequently, we redefine the notion of secure processes:

Definition 12 A process Q UC-emulates an ideal specification process I, written Q ≡_{UC} I, if there exists a context D[ ] such that Q ≃_{UC} D[I].

An important observation is that if Q_{1}, Q_{2} are processes whose public dataexchange is exclusively with UC contexts^{7}, then the quantification over schedulers is virtually useless for the overall distribution, or in other words, distinguishing two processes is independent on any external scheduler. This is so because UC contexts (probabilistically) decide which process to send data to (activate) next, and choose one at a time. Hence, the only kind of simultaneous data-exchange are private, but these are silent actions, and therefore should not affect indistinguishability of processes. This reasoning is a direct consequence of the following:

Lemma 1 Let n ∈ ℕ. Let Q be a closed process whose public channels are contained among the public channels of Z_{UC}(n, ·, ·). Then, for any scheduler the transition probability on any public data-exchange is equal to one.

A second implication of interacting with UC contexts is that the probability distribution of values transmitted through public channels is preserved up to a factor dependable exclusively on the probability distribution for private dataexchange.

7This is precisely the case of the encodings of machines P_{i}, F, and T .

Lemma 2 Let n ∈ ℕ. Let Z, E be linked, and let E compute v′ ← E(v, ς), on value v and current state ς, and send v′ to Z through tape_{E,Z}. Then, p_{v′} = P (v′ ← E(v, ς)) iff P (⟨tape_{E,Z}, v′⟩ ∈ T r(Z|Q)_{k}^{S}) = p_{v′} · u_{S}, where Q has E = ⟦E⟧ as a subprocess. When private data-exchange is sequentialized, then u_{S} is always one.

Our last observation is that UC-equivalence is weaker than that in definition 6, i.e., Q_{1} ≃_{UC} Q_{2} does not necessarily imply Q_{1} ≃ Q_{2}, or colloquially, quantification over the class of UC-adversaries does not necessarily imply quantification over all contexts.

This is an expected effect, since the environments we are considering are constrained to the assumptions of the adversarial and communication models, e.g., activation of all parties once per round, message-delivery guaranteed, authenticated channels, threshold corruptions, etc. Nonetheless, this definition of security is not trivial at all, since useful realizations can be proved secure under such assumptions. Hence, by defining equivalence of processes in ppc restricted to the contexts induced by UC environments, we are not over-simplifying the notion of security in ppc.

4.2 Main Result

We can now prove a correspondence between the UC framework and the process calculus ppc under UC-observational equivalence:

Theorem 1 (Full Abstraction) Let n ∈ ℕ and t < n. Let π be a n-party reactive protocol, F be an ideal functionality, and T be an interface.

1. (Soundness) If ⟦π⟧ ≡_{UC} ⟦T ⟧ | ⟦F⟧ then T proves π t-realizes F; and reciprocally,

2. (Completeness) If T proves π t-realizes F, then ⟦π⟧ ≡_{UC} ⟦T ⟧ | ⟦F⟧.

Proof:

1. If it was not the case, there would exist an environment Z negating indistinguishability in UC. But this would refute the validity of ⟦T ⟧|[ ] in the hypothesis, since the context ⟦Z⟧|[ ] induced by Z would also negate indistinguishability in ppc. Indeed, by lemma 2, both Z and Z would observe ⟨guess, b⟩ with comparable probabilities, and this would be sufficient, according to lemma 1 to call for distinguishability in ppc.

2. If T is an interface proving π t-realizes F, then it should hold that ⟦π⟧ ≃_{UC} ⟦T ⟧| [⟦F⟧], since otherwise, there would exist according to lemma 1 ⟦Z⟧|[ ] ∈ Z_{UC} negating indistinguishability in ppc, and consequently inferring that Z would negate indistinguishability in UC. Indeed, if Z observes ⟨public tape, v⟩ with overwhelming distinct probabilities, then by lemma 2 Z does so too and at that point can halt and output the guessing bit b. ♢

References

[BPW04] M. Backes, B. Pfitzmann, and M. Waidner. A general composition theorem for secure reactive systems. In LNCS, volume 2951, pages 336–354, 2004. TCC’04.

[Can01] R. Canetti. Universally composable security: A new paradigm for cryptographic protocols. In Proceedings of the 42nd IEEE Symposium on Foundations of Computer Science, page 136, 2001.

[DKM^{+}04] A. Datta, R. K usters, J. Mitchell, A. Ramanathan, and V. Shmatikov. Unifying equivalence-based definitions of protocol security. In Workshop on Issues in the Theory of Security, 2004. WITS’04 Satellite Workshop at ETAPS’04.

[DKMR04] A. Datta, R. K usters, J. Mitchell, and A. Ramanathan. Sequential probabilistic process calculus and simulation-based security. Technical report, Stanford University and Christian-Albrechts-Universität zu Kiel, 2004. TR-SPPC-2004.

[DKMR05] A. Datta, R. K usters, J. Mitchell, and A. Ramanathan. On the relationships between notions of simulation-based security. In Proceedings of Theory of Cryptography Conference (to appear), 2005.

[DN03] Ivan Damgård and Jesper Buus Nielsen. Universally composable efficient multiparty computation from threshold homomorphic encryption. In LNCS, volume 2729, pages 247–264, 2003. CRYPTO’03.

[GMR89] S. Goldwasser, S. Micali, and C. Rackoff. The knowledge complexity of interactive proof systems. SIAM J. Comput., 18(1):186–208, 1989.

[Gol01] O. Goldreich. Foundations of Cryptography: Basic Tools, volume 1. Cambridge University Press, 2001.

[LMMS98] P. Lincoln, J. Mitchell, M. Mitchell, and A. Scedrov. A probabilistic poly-time framework for protocol analysis. In ACM Conference on Computer and Communications Security, pages 112–121, 1998.

[LMMS99] P. Lincoln, J. Mitchell, M. Mitchell, and A. Scedrov. Probabilistic polynomial-time equivalence and security analysis. In World Congress on Formal Methods, pages 776–793, 1999.

[MMS98] J. Mitchell, M. Mitchell, and A. Scedrov. A linguistic characterization of bounded oracle computation and probabilistic polynomial time. In Proceedings of the 39th IEEE Symposium on Foundations of Computer Science, pages 725–733, 1998. FOCS’98.

[MMS03] P. Mateus, J. Mitchell, and A. Scedrov. Composition of cryptographic protocols in a probabilistic polynomial-time process calculus. In LNCS, volume 2761, pages 327–349, 2003. CONCUR 2003.

[Nie04] Jesper Buus Nielsen. On Protocol Security in the Cryptographic Model. PhD thesis, BRICS, University of Aarhus, Department of Computer Science, IT-parken, Aabogade 34, DK-8200 Århus N, Denmark, 2004.

[PW00] B. Pfitzmann and M. Waidner. Composition and integrity preservation of secure reactive systems. In 7th ACM Conference on Computer and Communications Security, pages 245–254, 2000.

5 Appendix:

5.1 ∅-hybrid Model and Ideal Process

Figures 2 and 3 define the ∅-hybrid model and the ideal process, respectively. The code of each rule should be self-explanatory. The piece of code under the horizontal line is to be executed indivisibly, as a single transition.

However, we allow nested rules, hence, we assume resumption: If there is a point where the activation is handed over to another machine, then once recovered the execution resumes at the point it was left before.

We could be more succinct to the expense of rigorousity in regard to machines’ states. Our main purpose is to illustrate the interactive pattern of the UC model by means of our notation. In constrast, we have to prevent ourselves of this relaxation in a full translation from machines into processes. As an example, the first rule for Z reads: Upon activation in round r, check the condition whether all honest parties i ∈ H have sent their round r − 1’s outputs y_{i,r}. If it holds, then pick an honest party i, compute his round r’s input x_{i,r} and round r − 1’s messages from corrupt parties {m_{j,i,r−1}}_{j∈C}. Observe messages {m_{j,i,r−1}}_{j∈H} where sent by honest parties in the previous round. Write x_{i,r} on tape inToP_{i}, and (bgn rnd, i, {m_{j,i,r−1}}_{j∈C∪H}) on tape msgToP_{i}. Activate this party by writing P_{i} on tape activate, and switch to control state waiting.

This rule is to be executed as long as there are honest parties to be activated with command beg rnd. To do so, we use a variable com(r) ∈ {beg rnd, end rnd} that indicates which command is to be executed next. In addition, a set I contains the indices of remaining honest parties to be activated.

Note well that on every new activation of Z, the set I, from where an honest party is picked, may have changed, since Z may decide first to corrupt a party before executing this rule.

5.2 Encoding of Interactive Rules

Figures 4 and 5 define the encodings of the interactive rules for a party P_{i} and a functionality F, respectively.

5.3 Proof Proposition1

Proof: In UC framework deadlock is prevented because parties are linked only to the environment, and the environment is assumed not to activate two machines at a time. The remaining properties follow by checking the conditions of the interactive rules of each machine. ♢

5.4 Proof Lemma 1

Proof: Let S be any scheduler over multisets M of subprocesses of Z|Q. Then, given that S is a Markov chain and since data-exchange over public channels occur one at a time, it holds that S(M_{1}, M_{2}) = 1, where

i. {⟨v⟩_{c}, (x)_{c}.X} ⊂ M_{1} and there are no other probable transitions in M_{1};

ii. M_{2} = (M_{1} \ {⟨v⟩_{c}, (x)_{c}.X}) ∪ M_{X_{v}^{x}} and X_{v}^{x} is the process obtained by substituting all free occurrences of x by v in X; and

iii. c ∈ {inToP_{i}, outByP_{i}, msgToP_{i}, msgByP_{i}, corrToP_{i}, corrByP_{i}}. ♢

5.5 Proof Lemma 2

Proof:(Sketch) The proof proceeds by induction on the number of activations in the execution. The key fact is that machines and processes are scheduled in the same order by Z and its encoding Z. Thus, when machine E is activated with input value v, its corresponding process E is activated with the same input value and having, by induction hypothesis, the same state ς as E. Then, in virtue of our encoding, process E would initiate a tree of reduction involving solely private data-exchange in order to update its state. Assume the chosen branch in this tree has probability u_{S}. The branch ends at the point value v′ is computed by sending ⟨E(v, ς)⟩_{tape_{E,Z}}, with probability p_{v′}. Finally, the sent value is actually observed with probability one, as it is the unique public data-exchange at this point of the computation (reduction). Therefore, P (⟨tape_{E,Z}, v′⟩ ∈ T r(Z|Q)_{k}^{S}) = p_{v′} · u_{S} · 1. ♢

5.6 ppc-Composition Theorem

We provide a prove of the compositional theorem in ppc with respect to definition 8. In what follows we use ≡ to stand for protocol emulation.

Proposition 2 (Composition) Let Q ≡ I and R[I] ≡ J. Then R[Q] ≡ J.

Proof: The hypotheses can be rephrased as:

∃ D[ ] Q ≃ D[I]  (1)
∃ E[ ] R[I] ≃ E[J] ,  (2)

where ≃ means observational equivalence (cf. Definition 6). We will prove that D[E[ ]] is a context such that R[Q] ≃ D[E[J]], i.e., for all schedulers and for all contexts C[ ] it holds that

Tr(C[R[Q]]) ≈^{c} Tr(C[D[E[J]]]) .

Indeed, since ≈^{c} is transitive, it follows that

Tr(C[R[Q]])
≈^{c}  ( (1) with C[R[ ]] )
Tr(C[R[D[I]]])

=

Tr(C[D[R[I]]])
≈^{c}  ( (2) with C[D[ ]] )
Tr(C[D[E[J]]])

The second step above holds as long as contexts R[ ] and D[ ] are of form X|[ ] or ( )c.[ ] and there is no clash of free-names. We claim, albeit without further evidence here, this kind of composition is sufficient for modelling the interaction of ITM’s where linking tapes do not stand for actual communication devices. ♢

Init: Z(k, z, 𝔯_{Z}), P_{i}(k, 𝔯_{i}). Set r := 0, C := { }, H =^{def} [n] − C, I := H.

Environment Z:  Party P_{i}:
∀_{i∈H} ?_{outByP_{i}} y_{i,r−1}

precondition: comand(r)=beg rnd precondition:{I ⊇ H –1st call: =–}

I := I \ C i_{∈I} ← Z I := I \ {i} if I = { } then

com(r) := end rnd I := H

({m_{j,i,r−1}}_{j∈C}, x_{i,r}) ← Z !_{inToP_{i}} (i, x_{i,r}) !_{msgToP_{i}} (beg rnd, i, {m_{j,i,r−1}}_{j∈C∪H}) !_{activate} P_{i} waiting ?_{inToP_{i}} (i, x_{i,r}) ?_{msgToP_{i}} (beg rnd, i, {m_{j,i,r−1}}_{j∈C∪H})

({m_{i,j,r}}, y_{i,r}) = P_{i}({m_{j,i,r−1}}, x_{i,r}) !_{msgByP_{i}} {m_{i,j,r}}_{j≠i} waiting

∀_{i∈H} ?_{msgByP_{i}} {m_{i,j,r}}_{j≠i}

precondition: comand(r) = end rnd precondition:{I ⊇ H –1st call: =–}

I := I \ C i_{∈I} ← Z I := I \ {i} if I = { } then

r := r + 1

com(r) := beg rnd I := H

!_{msgToP_{i}} (end rnd) !_{activate} P_{i} waiting

?_{msgToP_{i}} (end rnd)

!_{outByP_{i}} y_{i,r} !_{activate} Z waiting

if |C| < t then i_{∈H} ← Z C := C ∪ {i} I := I \ C if I = { } then

com(r) := 1 − com(r) I := H

!_{corrToP_{i}} (corrupt i)

!_{activate} P_{i} waiting

?_{corrToP_{i}} (corrupt i)
!_{corrByP_{i}} 𝔯_{i} ; !_{activate} Z ; waiting

b ← Z ; !_{guess} b ; halt

Figure 2: Order of activations in ∅-hybrid model

Init: Z(k, z, 𝔯_{Z}), T (k, 𝔯_{T} ), F(k, 𝔯_{F}). Set r := 0, C := { }, H =^{def} [n] − C, I_{T} := H, I_{F} := H.

Interface T :  Functionality F:

?_{msgToP_{i}} (beg rnd, i, {m_{j,i,r−1}}_{j∈C∪H})

precondition:{I_{T} ⊇ H –1st call: =–}

I_{T} := I_{T} \ {i} !_{activate} F

?_{leaked} v_{F,i}^{inleak}

({m_{i,j,r}}_{j∈[n]}) ← T (k, {m_{j,i,r−1}}_{j∈C,i∈H}, v_{F,i}^{inleak} ; 𝔯_{T} ) if I_{T} = { } then

!_{probe} (beg rnd, v′) !_{activate} F

\begin{matrix}true \\ I_{T} := H \end{matrix}

!_{msgByP_{i}} {m_{i,j,r}}_{j≠i} !_{activate} Z waiting

?_{inToP_{i}} (i, x_{i,r})

v_{F,i}^{inleak} ← F(k, x_{i,r}; 𝔯_{F}) !_{leaked} v_{F,i}^{inleak} !_{activate} T waiting

?_{probe} (beg rnd, v′)

({y_{i,r}}_{i∈H}, v_{F}^{outleak} ) ← F(k, {x_{i,r}}_{i∈H}, v′; 𝔯_{F}) !_{activate} T waiting

?_{msgToP_{i}} (end rnd)

!_{probe} (end rnd, i) !_{activate} F

true ; !_{activate} Z waiting

?_{probe} (end rnd, i)

precondition:{I_{F} ⊇ H –1st call: =–}

I_{F} := I_{F} \ {i} !_{outByP_{i}} y_{i,r} if I_{F} = { } then

!_{leaked} v_{F}^{outleak} I_{F} := H

!_{activate} T waiting

?_{corrToP_{i}} (corrupt i) I_{T} := I_{T} \ {i} if I_{T} = { } then

!_{probe} v′ !_{activate} F

\begin{matrix}true \\ I_{T} := H \end{matrix}

!_{probe} (corrupt i) !_{activate} F ?_{leaked} v_{F,i}^{corrleak}

𝔯_{i} ← T ; !_{corrByP_{i}} 𝔯_{i} ; !_{activate} Z ; waiting

?_{probe} (corrupt i)

I_{F} := I_{F} \ {i} if I_{F} = { } then

!_{leaked} v_{F}^{outleak} I_{F} := H

v_{F,i}^{corrleak} ← F(k, i; 𝔯_{F}) !_{leaked} v_{F,i}^{corrleak} !_{activate} T waiting

Figure 3: Order of activations in ideal process

Rule Rnd =

(t)_{msgToP_{i}}
[t = (beg rnd, v′)]
( )_{msgToP_{i}}

⟨{m_{i,j,r}}_{j≠i}⟩_{msgByP_{i}} ⟨ ⟩_{updateStore_{P_{i}}}

⟨ ⟩_{unblock_{P_{i}}} ; ⟨Z⟩_{activate}

[t = (end rnd)]
⟨y_{i,r}⟩_{outByP_{i}} ⟨ ⟩_{updateStore_{P_{i}}}

⟨ ⟩_{unblock_{P_{i}}} ; ⟨Z⟩_{activate}

Rule Corrupt =

(t)_{corrToP_{i}}
⟨𝔯_{i}⟩_{corrByP_{i}} ⟨ ⟩_{updateStore_{P_{i}}}

⟨ ⟩_{unblock_{P_{i}}} ; ⟨Z⟩_{activate}

Figure 4: Enconding of P_{i}’s Interactive Rules

Rule Input =

( )_{inToP_{i}}
⟨v_{F,i}^{inleak} ⟩_{leaked} ⟨ ⟩_{updateStore_{F}}

⟨ ⟩_{unblock_{F}} ; ⟨T ⟩_{activate}

Rule Probe =

(t)_{probe}

[t = (beg rnd, v′)] ⟨ ⟩_{updateStore_{F}} ⟨ ⟩_{unblock_{F}} ; ⟨T ⟩_{activate}

[t = (end rnd, i)]
⟨y_{i,r}⟩_{outByP_{i}} ⟨ ⟩_{updateStore_{F}}

⟨ ⟩_{unblock_{F}} ; ⟨T ⟩_{activate}

[t = (corrupt, i)]
⟨v_{F,i}^{corrleak} ⟩_{leaked} ⟨ ⟩_{updSt._{F}}

\begin{matrix}⟨ ⟩_{unbl._{F}} \\ ⟨T ⟩_{act.} \end{matrix}

Figure 5: Enconding of F’s Interactive Rules

Recent BRICS Report Series Publications

RS-04-15 Jesús Fernando Almansa. The Full Abstraction of the UC Framework. August 2004. 26 pp.

RS-04-14 Jesper Makholm Byskov. Maker-Maker and Maker-Breaker Games are PSPACE-Complete. August 2004. 5 pp.

RS-04-13 Jens Groth and Gorm Salomonsen. Strong Privacy Protection in Electronic Voting. July 2004. 12 pp. Preliminary abstract presented at Tjoa and Wagner, editors, 13th International Workshop on Database and Expert Systems Applications, DEXA ’02 Proceedings, 2002, page 436.

RS-04-12 Olivier Danvy and Ulrik P. Schultz. Lambda-Lifting in Quadratic Time. June 2004. 34 pp. To appear in Journal of Functional and Logic Programming. This report supersedes the earlier BRICS report RS-03-36 which was an extended version of a paper appearing in Hu and Rodríguez-Artalejo, editors, Sixth International Symposium on Functional and Logic Programming, FLOPS ’02 Proceedings, LNCS 2441, 2002, pages 134–151.

RS-04-11 Vladimiro Sassone and Pawe� Sobociński. Congruences for Contextual Graph-Rewriting. June 2004. 29 pp.

RS-04-10 Daniele Varacca, Hagen Völzer, and Glynn Winskel. Probabilistic Event Structures and Domains. June 2004. 41 pp. Extended version of an article to appear in Gardner and Yoshida, editors, Concurrency Theory: 15th International Conference, CONCUR ’04 Proceedings, LNCS, 2004.

RS-04-9 Ivan B. Damgård, Serge Fehr, and Louis Salvail. Zero-Knowledge Proofs and String Commitments Withstanding Quantum Attacks. May 2004. 22 pp.

RS-04-8 Petr Jančar and Jiří Srba. Highly Undecidable Questions for Process Algebras. April 2004. 25 pp. To appear in Lévy, Mayr and Mitchell, editors, 3rd IFIP International Conference on Theoretical Computer Science, TCS ’04 Proceedings, 2004.

RS-04-7 Mojmír Křetínský, Vojtěch Řehák, and Jan Strejček. On the Expressive Power of Extended Process Rewrite Systems. April 2004. 18 pp.