Calibrating The Power Of Schedulers For Probabilistic Systems
Calibrating the power of schedulers forprobabilistic systems Srečko Brlek1 , Sardaouna Hamadou2 , and John Mullins2,112Laboratoire LaCIM, Dép. d’Informatique, Université du Québec à Montréal.brlek@lacim.uqam.ca,Laboratoire CRAC, Dép. de Génie Informatique, École Polytechnique de Montréal{sardaouna.hamadou, john.mullins}@polymtl.caAbstract. When modelling security protocols by means of process calculi that express both nondeterministic and probabilistic behavior, it iscustomary to view the scheduler as an intruder. It has been establishedthat the traditional scheduler needs to be carefully calibrated in orderto more accurately reflect the intruder’s real power. We propose such aclass of schedulers through a variant of the Probabilistic Poly-time Calculus (PPC) of Mitchell et al. [12] called PPCνσ . To this end, we definetwo levels of schedulers: adversarial schedulers which schedule a class ofindistinguishable actions, i.e. actions that we do not want an attacker todistinguish, and internal schedulers, called task schedulers, that resolvethe remaining nondeterminism within the chosen class. We also show howto apply it in order to design schedulers for the analysis of cryptographicprotocols that will accurately reflect an intruder’s capacity for controlling communication networks, without controlling the internal reactionsof the protocol under attack. We illustrate the aptness of our approachby an extensive study of the Dining Cryptographers (DCP) [9] protocol.Along these lines, we also define a new characterization of the asymptotic observational equivalence of Mitchell et al. [12] that is more suitedfor taking into account any observable trace instead of just one singleaction. Finally we prove that our asymptotic observational equivalenceis congruent in accordance with the new schedulers.Key words: Process algebra, observational equivalence, probabilisticscheduling, analysis of cryptographic protocols1IntroductionSystems that combine both probability and nondeterminism are very convenientfor modelling probabilistic security protocols. In order to model such systems,possibilistic models based on process algebras (such as either the π-calculus orthe CSP) have been extended to include probabilities. One can distinguish twoclasses of such models. On the one hand, we have all-purpose probabilistic modelsadding probabilities to nondeterministic models [1, 7, 3]. On the other hand, we Research partially supported by individual NSERC research grants (Canada)
2S. Brlek, S. Hamadou and J. Mulinshave process algebra frameworks that define probabilistic models to make themmore suitable for cryptographic protocol applications [12, 4, 11].While it is customary to use schedulers for resolving non-determinism inprobabilistic systems, scheduling processes have to be carefully designed to reflectas accurately as possible an intruder’s capacity for controlling the communicationnetworks without controlling the internal reactions of the system. Consider theprotocol c(a).0 c(b).0 transmitting the messages a and b over c, with the intruderc(x).0 eavesdropping on this channel. As the protocol is purely non-deterministic,the probability of the intercepted message being either a or b should be the same.A scheduler that could assign an arbitrary probabilistic distribution to these twomessages could also force the protocol to transmit either a or b. Such schedulersare too strong however, and are therefore not admissible; but care also mustbe taken in restricting the power of schedulers so that we do not end up withadversaries that are overly weak. Forcing schedulers to give priority to internalactions, for example, makes internal actions completely invisible to attackers.An intruder is then unable to distinguish a process P from another process thatmight perform some internal action and then behave like P . Consider, however,the following process:P νc′ (c(x).c′ (x).0 c′ (1).0 c′ (y).[y 0]c(secret ).0).In this obviously unsecure protocol, an intruder could send 0 to P over c and thusallow P to reveal the secret. Such a flaw would never be detected in semanticsgiving priority to internal actions, because P would never broadcast secret onpublic channel c.Contribution. Our contribution is threefold. Firstly, we define a variant of theProbabilistic Polynomial-time Process Calculus PPC [12], called PPCνσ , to copewith the problem of characterizing the intruders’s capacity. Contrary to mostprobabilistic models, our operational semantics does not normalize probabilities.The reason is that normalizing has the effect of removing the intruder’s controlof its own actions. Consider the process P c(m).Q1 c(m).Q2 . Depending onwhether P represents a protocol or an intruder, the scheduling of a component isrespectively either equiprobable, or arbitrarily chosen by the intruder. A solutionmight be to semantically distinguish between a protocol and an intruder, but thisrapidly becomes quite unmenageable since synchronization actions could involveboth. This problem is dealt with in [5], where actions are indexed at the semanticlevel according the positions of the parallel components that they belong to.This leads to a characterization of probabilistic schedulers for cryptographicprotocols that gives the attacker full control of its own actions but does notallow it to control either the internal actions of the protocol or the protocol’sinternal reactions to its stimulus. This is implemented by having schedulersequiprobabilistically choose all actions we do not want an attacker to distinguish.All internal transitions of the protocol are equiprobabilistically scheduled, forexample. In the same way, all outputs of the protocol on the same channelare equiprobable. This paper generalizes this technique by defining two levelsof schedulers: adversarial schedulers which choose a class of indistinguishable
Calibrating schedulers’ power for probabilistic systems3actions, and internal schedulers, called task schedulers, that resolve the remainingnondeterminism in a class according to a fixed and predetermined probabilitydistribution. In order to define this equivalence relation over actions in a morenatural way, we use here the syntactic approach presented in [8] where processesare labelled at the syntactic level.Secondly, we reformulate the observational asymptotic equivalence of [12]into a more amenable form that take into account any observable trace insteadof just one single action. We prove that in accordance with the new schedulers,this asymptotic equivalence is a congruence, extending in that way the resultsof [5].Finally, to illustrate the appropriateness of our approach, we conclude the paper with an extensive case study: the analysis of Chaum’s Dining Cryptographersprotocol [9]. We give a probabilistic version of the possibilistic specification ofthe anonymity property, as per Schneider and Sidiropoulos [13], and prove thatoverly restricting the scheduler’s power may lead to very weak models that cannot detect flawed specifications of the protocol.Related work. The technical precursor of our framework is the process calculus of Mitchell et al. [12]. Although it is a formal model, it is still close to thecomputational setting of modern cryptography since it works directly on thecryptographic level. Indeed it defines an extension of the CCS process algebrawith finite replication and probabilistic polynomial-time terms denoting cryptographic primitives. It turns out that these probabilistic polynomial functionsare useful for modelling the probabilistic behaviour of security systems. Unlikeformalisms such as [7, 4, 11], the scheduling is probabilistic, thus better reflectingthe ability of an attacker to control the communication networks. Finally it isalso a natural formal framework for capturing and reasoning about a variety offundamental cryptographic notions.The problem of characterizing schedulers’ capacities has recently been considered in [6, 8, 10]. In [6] the authors treated the problem of overly powerfulschedulers in the context of systems modelled in a Probabilistic I/O Automataframework. They restricted the scheduler by defining two levels of scheduler.A high-level scheduler called adversarial scheduler is a component of the system, and controls the communication network (i.e. it schedules public channels).This component has limited knowledge of the behaviour of other componentsin the system: their internal choices and secret information is hidden. On theother hand, a low-level scheduler called tasks scheduler resolves the remainingnon-determinism by using a task schedule. These tasks are equivalence classes ofactions that are independent of high-level scheduler choices.In Garcia et. al. [10] a dual problem to the one we have considered here,namely the problem that arises when traditional schedulers are overly powerful,is addressed. In the context of security protocols modelled by probabilistic automata, they define a probabilistic scheduler that assigns, in the current state, aprobability distribution to the possible nondeterministic next transitions. Unlikeour scheduler, it is history-dependent since it defines equiprobable paths, andit is not stochastic, and might therefore halt execution at any time. Roughly
4S. Brlek, S. Hamadou and J. Mulinsspeaking, admissible schedulers are defined w.r.t bisimulation equivalence: anyobservably trace-equivalent paths are equiprobably scheduled and lead to bisimilar states.Another recent paper on the scheduling issue is presented in [8]. Unlike ourscheduler and that of [10] which are both defined on the semantic level, [8] proposes a framework in which schedulers are defined and controlled on the syntacticlevel. They make random choices in the protocol invisible to the adversary. Notethat we achieve the same goal by using the operational semantics Eval rule,which reduces unblocked processes, as well as our strategically equivalent classesof actions.Finally an alternate approach is proposed in [4, 11]. Instead of schedulinga single action (like ours), or a path (like the one of [10]), a process is scheduled. The problems of, discriminating between a protocol’s actions and an intruder’s ones, and the privileging of internal actions, is meaningless in thesemodels because scheduling is implicitly included in the specification. In otherwords, the protocol designer determines when control passes from the protocolto the attacker and vice versa. This can be explained by considering the protocol P ν(c)(c(1). c(x).c′ (0).) which, after an internal communication, outputs0 on public channel c′ . In frameworks [4, 11], it may be specified in two differentmannersP1 ν(c)(start().c(1).0 c(x).c′ (0).0)andP2 ν(c)(start().c(1).0 c(x).contr2Intr().getContr().c′ (0).0)depending on whether or not we want to make the internal action completelyinvisible to the attacker. In this way the user has full control and can eliminateundesirable schedulers at the specification level. The drawback is that the protocol designer who has incomplete knowledge about the system, may specify hisintuition of the protocol, and so get some properties that might not be satisfiedby the actual protocol.Content of the paper. The PPC calculus is presented in Section 2. ThePPCνσ is presented in Section 3 together with the definitions of adversarial andtask schedulers. These are used in Section 4 to design a particular class of schedulers for the analysis of cryptographic protocols. Section 5 is devoted to probabilistic behavioral equivalences. The case study is presented in Section 6. Weconclude the paper in Section 7.2The PPC CalculusThe Probabilistic Polynomial-time Process Calculus PPC [12] extends the CCSprocess algebra with finite replication and probabilistic polynomial-time terms(functions) denoting cryptographic primitives to better take into account theanalysis of cryptographic protocols. Although it is a formal model, it is still closeto the computational setting of modern cryptography since it works directly onthe cryptographic level. It turns out that these probabilistic polynomial functions
Calibrating schedulers’ power for probabilistic systems5are useful for modelling the probabilistic behaviour of security systems. In thissection we present a small variant of the PPC model. On a syntactic level, thereis very little difference: while in [12] terms are probabilistic polynomial-timefunctions with constants denoting messages, in our setting these functions aretreated as guards. On the semantic level, we do not normalize probabilities,leaving that task to the scheduling process instead.2.1Syntax of PPCTerms. The set of terms T of the process algebra PPC consists of variables V,numbers N, pairs, and a specific term N standing for the security parameter.The security parameter may be understood as the cryptographic primitives’ keylength, and may appear in the probabilistic polynomial functions defined below.Formally we havet :: n (integer ) x (variable ) N (secur. param.) (t, t) (pair )For each term t, f v(t) is the set of variables in t. A message is a closed term(i.e. not containing variables). The set of messages is denoted M.Functions. Probabilistic, as well as deterministic, cryptographic primitives’computations, such as keys and nonces generation, encryption, decryption, etc.,are modelled by probabilistic polynomial functions3 Λ {λ : Mk M k N}which satisfy (m1 , . . . , mk ) Mk , m M, λ Λ, p [0, 1] such thatProb[λ(m1 , · · · , mk ) m] p.We denote by λ(m1 , · · · , mk ) ֒ x the assignment of the value λ(m1 , · · · , mk )pto the variable x. The notation λ(m1 , · · · , mk )֒ m means that λ(m1 , · · · , mk )evaluates to m with probability p. From Definition 17 (see Appendix A), the setpIm(λ(m1 , · · · , mk )) {m p ]0.1] λ(m1 , · · · , mk )֒ m}of m s.t. λ(m1 , · · · , mk ) evaluates to m with non-zero probability, is a finite set.For instance, RSA encryption that takes as parameters, a message m toencrypt and an encryption key formed of the pair (e, n), and returns the numberme mod n, is the function λRSA (m, e, n) returning c with probability 1 if c me mod n, and 0 otherwise. Similarly, we can model the key guessing attack ofa cryptosystem by the product [rand(1k ) ֒ key][dec(c, key) ֒ x] where 1k isthe size of the key randomly generated by the function rand, and the decryptionfunction dec returns m with probability 1 if c is the cryptogram of m encrypted1. Theseby k and key k. The success of such an attack has probability p 2 k few examples illustrate the expressive power offered by these functions. We limitourselves to probabilistic polynomial functions in order to model all realizableattacks in polynomial time.Processes. Let C be a countable set of public channels. We assume that eachchannel is equipped with a bandwidth given by the polynomial function bw :3See Appendix A for a formal definition of a probabilistic polynomial function
6S. Brlek, S. Hamadou and J. MulinsC N. We say that a message m belongs to the domain of a channel c,written m dom(c), if the message length m is less than or equal to thechannel bandwidth, i.e. m dom(c) m bw(c). Note that (m, m′ ) m m′ r where r is the length of a fixed bits string, which allows us toconcatenate and decompose two terms without any ambiguity.Processes in PPC are constructed as follows :P :: 0 c(x).P !q(N) P c(m).P P P (νc)P [λ(t1 , · · · , tn ) ֒ x]P [t t]P Given a process P , the set f v(P ) of free variables is the set of variables x in Pthat are not in the scope of any prefix input (of the form c(x)) nor in the scopeof any probabilistic evaluation (of the form [λ(t1 , · · · , tn ) ֒ x]). A processwithout free variables is called closed and the set of closed processes is denotedby Proc. Hereafter, all processes are considered closed.The mechanisms for reading, emitting, parallel composition, restriction andmatching are all standard. The finite replication process !q(N) P , is the q(N) foldparallel composition of P with itself, in which q is a polynomial function. Theinnovation is the call and return of probabilistic polynomial functions[λ(t1 , · · · , tn ) ֒ x]PThis feature allows us to model (probabilistic) polynomial cryptographic primitives as well as the probabilistic character of a protocol. In fact it is the mainsource of probability in this model.The following examples illustrate the way PPC can be used to model protocols.Example 1. Let Kgen be a (probabilistic) polynomial function that, given thesecurity parameter N, generates a secret encryption key, and let enc be a (probabilistic) encryption function that, given a secret key K and a message M , returnsthe cryptogram of M under K. The process P that receives a message over thepublic channel c generates an encryption key and returns the cryptogram of thismessage over the same public channel. This is modeled in PPCνσ as follows:P : c(x).[Kgen(N) ֒ y][enc(x, y) ֒ z]c(z).0Example 2. Though the calculus does not consider the probabilistic alternativechoice operator “ ”, it is possible to simulate it by means of the parallel composition operator and some special probabilistic functions.Let f lips be the probabilistic polynomial function which, given a coin, returnHead with probability p and T ail with probability 1 p. Then the process Q,which flips a coin and then behaves as the process Q′ if the result of the coinflipping is Head and as the process Q′′ otherwise, is modelled in our calculus asfollows:Q : [f lips(coin) ֒ x]([x Head]Q′ [x T ail]Q′′)
Calibrating schedulers’ power for probabilistic systems7p′P 6 BlockedEval. eval(P )֒ Pτ [p]P P ′m dom(c)m dom(c)InputOutputc(m)[1]c(m)[1]c(m).P Pc(x).P P [m/x]α[p]α[p]P2 P2′(P1 P2 ) BlockedP1 P1′(P1 P2 ) BlockedParR.ParL.α[p]α[p]P1 P2 P1′ P2P1 P2 P1 P2′SyncL.RestCL.Restc(m)[p1 ]c(m)[p1 ]c(m)[p2 ]c(m)[p2 ]P1 P1′P2 P2′ P1′ P2 P2′SyncR.c(m).c(m)[p1 .p2 ]c(m).c(m)[p1 .p2 ]P1 P2P1 P2 P1′ P2′ P1′ P2′c(m).c(m)[p]c(m).c(m)[p]′′ P PPRestCR. Pτ [p]τ [p](νc)P (νc)P ′(νc)P (νc)P ′α[p]P P ′α6 {c(m),c(m),c(m)·c(m),c(m)·c(m):m M}P Blockedα[p]′(νc)P (νc)PP1Table 1. Operational semantics of PPC2.2Operational semanticsThe set of actionsAct {c(m), c(m), c(m) · c(m), c(m) · c(m), τ m M and c C}consists of the set of partial input and output actions, and the set of synchronization actions on public channels, and the internal action τ :Partial {c(m), c(m) m M and c C}Actual {c(m) · c(m), c(m) · c(m), τ m M and c C}The set of observable actions is given by Vis Act {τ }. The operationalsemantics of PPC is a probabilistic transition system (E, T , E0 ) generated bythe inference rules given in Table 1 where E Proc is the set of states, T E Act [0, 1] E the set of transitions and E0 Proc the initial state. Theα[p]notation P P ′ stands for (P, α, p, P ′ ) T .The PPC semantics are an extension of the CCS semantics, with a mechanismfor calling probabilistic polynomial functions. We sketch it briefly here.To make sure that internal computations of functions do not interfere withcommunication actions (in particular with those on public channels controlled bythe intruder), all exposed functions in a process (Eval rule) are simultaneouslyevaluated by the probabilistic polynomial function eval defined in Table 2 below,as illustrated in Example 3. This evaluation step allows us to get what we call ablocked process, i.e. a process having no more internal computations to perform.The set of blocked processes is denoted by Blocked .Example 3. If processes Q′ and Q′′ of Example 2 are blocked processes then Qreduces to Q′ with probability p and to Q′′ with probability 1 p. In other words,Prob[eval (Q) Q′ ] p and Prob[eval (Q) Q′′ ] 1 p.
8S. Brlek, S. Hamadou and J. MulinsProb[eval (0) 0] 1Prob[eval (c(x).P ) c(x).P ] 1 and Prob[eval (c(m).P ) c(m).P ] 1Prob[eval ((νc)P )
The Probabilistic Polynomial-time Process Calculus PPC [12] extends the CCS process algebra with finite replication and probabilistic polynomial-time terms (functions) denoting cryptographic primitives to better take into account the analysis of cryptographic protocols. Although it is a formal model, it is still close
May 02, 2018 · D. Program Evaluation ͟The organization has provided a description of the framework for how each program will be evaluated. The framework should include all the elements below: ͟The evaluation methods are cost-effective for the organization ͟Quantitative and qualitative data is being collected (at Basics tier, data collection must have begun)
Silat is a combative art of self-defense and survival rooted from Matay archipelago. It was traced at thé early of Langkasuka Kingdom (2nd century CE) till thé reign of Melaka (Malaysia) Sultanate era (13th century). Silat has now evolved to become part of social culture and tradition with thé appearance of a fine physical and spiritual .
On an exceptional basis, Member States may request UNESCO to provide thé candidates with access to thé platform so they can complète thé form by themselves. Thèse requests must be addressed to esd rize unesco. or by 15 A ril 2021 UNESCO will provide thé nomineewith accessto thé platform via their émail address.
̶The leading indicator of employee engagement is based on the quality of the relationship between employee and supervisor Empower your managers! ̶Help them understand the impact on the organization ̶Share important changes, plan options, tasks, and deadlines ̶Provide key messages and talking points ̶Prepare them to answer employee questions
Dr. Sunita Bharatwal** Dr. Pawan Garga*** Abstract Customer satisfaction is derived from thè functionalities and values, a product or Service can provide. The current study aims to segregate thè dimensions of ordine Service quality and gather insights on its impact on web shopping. The trends of purchases have
Chính Văn.- Còn đức Thế tôn thì tuệ giác cực kỳ trong sạch 8: hiện hành bất nhị 9, đạt đến vô tướng 10, đứng vào chỗ đứng của các đức Thế tôn 11, thể hiện tính bình đẳng của các Ngài, đến chỗ không còn chướng ngại 12, giáo pháp không thể khuynh đảo, tâm thức không bị cản trở, cái được
Le genou de Lucy. Odile Jacob. 1999. Coppens Y. Pré-textes. L’homme préhistorique en morceaux. Eds Odile Jacob. 2011. Costentin J., Delaveau P. Café, thé, chocolat, les bons effets sur le cerveau et pour le corps. Editions Odile Jacob. 2010. Crawford M., Marsh D. The driving force : food in human evolution and the future.
Le genou de Lucy. Odile Jacob. 1999. Coppens Y. Pré-textes. L’homme préhistorique en morceaux. Eds Odile Jacob. 2011. Costentin J., Delaveau P. Café, thé, chocolat, les bons effets sur le cerveau et pour le corps. Editions Odile Jacob. 2010. 3 Crawford M., Marsh D. The driving force : food in human evolution and the future.
