extfieldsofstudy:
Physics
Mathematics
Computer Science

s2fieldsofstudy:
Computer Science
Physics

text:
Security of quantum key distribution using weak coherent states with nonrandom phases

We prove the security of the Bennett-Brassard (BB84) quantum key distribution protocol in the case where the key information is encoded in the relative phase of a coherent-state reference pulse and a weak coherent-state signal pulse, as in some practical implementations of the protocol. In contrast to previous work, our proof applies even if the eavesdropper knows the phase of the reference pulse, provided that this phase is not modulated by the source, and even if the reference pulse is bright. The proof also applies to the case where the key is encoded in the photon polarization of a weak coherent-state pulse with a known phase, but only if the phases of the four BB84 signal states are judiciously chosen. The achievable key generation rate scales quadratically with the transmission in the channel, just as for BB84 with phase-randomized weak coherent-state signals (when decoy states are not used). For the case where the phase of the reference pulse is strongly modulated by the source, we exhibit an explicit attack that allows the eavesdropper to learn every key bit in a parameter regime where a protocol using phase-randomized signals is provably secure.

Introduction
In quantum key distribution (QKD) [1], two parties (Alice and Bob) use quantum signals to establish a shared key that can be used to encrypt and decrypt classical messages. An eavesdropper (Eve) who collects information about the key by interacting with the signals produces a detectable disturbance; therefore Alice and Bob can detect the eavesdropper's activity, and they can reject the key if they fear that the eavesdropper knows too much about it. But if the detected disturbance is weak enough, then Alice and Bob can use classical error correction and privacy amplification protocols to extract a shared key that is very nearly uniformly distributed and almost certainly private [2,3,4,5,6,7,8]. The security of the QKD protocol is said to be unconditional, because the security can be proven for any attack consistent with the laws of quantum physics, and without any assumptions about computational hardness.
Experiments have recently demonstrated the feasibility of QKD over 150 km telecom fibers [9,10], and at least two firms are now marketing commercial QKD systems [11]. But how secure are these systems, really? To assess the security of practical implementations of QKD, it is important to consider how well the actual systems match the performance assumed in the security proofs. In particular, the signals used in typical practical realizations of QKD are dim laser pulses, which occasionally contain more than one photon. Multi-photon signals together with loss in the optical fiber can threaten security, but proofs of security for QKD using weak coherent states have been found [12,13]. (We note that for QKD protocols that use decoy states [14,15,16], security can be proven even for rather strong coherent-state signals. In this paper, however, we will focus on QKD with weak coherent states.) A key assumption in the security proofs in [12,13] (and also in [15]) is that the phase of the quantum signal is uniformly random. A coherent state of one mode of the electromagnetic field can be expressed as where |n denotes the state with photon number n. We may write α = √ νe iθ , where ν = |α| 2 denotes the mean photon number and e iθ is the phase of the coherent state. To an eavesdropper with no a priori knowledge of the phase, a signal whose phase is selected uniformly at random is indistinguishable from the state a Poisson distributed mixture of photon number eigenstates. Therefore, for a security analysis, we may suppose that a source emitting weak coherent state signals is actually emitting signals in the state ρ ν . With probability p 0 = e −ν , which is close to one for small ν, the source emits no photon; exactly one photon is emitted with probability p 1 = νe −ν . The probability that two or more photons are emitted is Multi-photons can pose a security risk, but if each signal has a random phase, p M is sufficiently small, and the loss in the channel is not too high, then it is possible to prove security of the Bennett-Brassard (BB84) protocol [1] against arbitrary eavesdropping attacks [12,13]. However, no previously known security proof applies if the eavesdropper has some a priori knowledge about the phase of the signal states. Conceivably, such phase information might be accessible in realistic implementations of QKD. For example, in a "plug-and-play" scheme [17], a strong signal is sent from Bob to Alice, who attenuates and modulates the signal before returning it to Bob; in unidirectional schemes as well, strong ancillary pulses are sometimes used to monitor the channel. The phase of a strong pulse is accurately measurable in principle, and could be correlated with the phase of the key-generating pulse. Furthermore, the key information itself might be encoded in the relative phase of a bright reference pulse and a weak signal pulse, in which case the eavesdropper could plausibly learn the phase of the reference pulse. Even if strong pulses are not used, the phase coherence of a realistic source might be maintained during the emission of many weak signals, allowing the phase to be determined accurately.
For all these reasons, it is worthwhile to investigate the security of QKD under the assumption that the eavesdropper knows something about the phase of the signals. Our main result in this paper is a proof of security for the BB84 protocol in the case where the key information is encoded in the relative phase of a reference pulse and a signal pulse. Our proof works even if the reference pulse is bright, with a phase known by the eavesdropper. It also applies if the key is encoded in the photon polarization of weak coherent states with nonrandom phases, provided the phases of the signal states are chosen appropriately. The proof is founded on the observation that, if the signal pulse is weak, Alice's source reveals relatively little information to Eve about the basis that Alice uses to encode her key bits. Privacy of the final key is demonstrated using an argument due to Koashi [18,19] that invokes the uncertainty principle. We also point out that this argument establishes that the key distribution protocol is universally composable -the key can be used in any subsequent application without compromising security.
We describe our quasi-realistic model for sources and detectors in Sec. 2, and present the security analysis (which relies heavily on Koashi's ideas [18,19]) in Sec. 3, Sec. 4, and Appendix A. In Sec. 5 we note that the key generation rate when the signals have nonrandom phases is comparable to the rate for phase randomized signals (when decoy states are not used). In Sec. 6 and Appendix B we point out that if the key is encoded in the photon polarization, and the (nonrandom) phases of the signals are not chosen judiciously, then BB84 is vulnerable to an unambiguous key discrimination attack, a measurement that, when conclusive, determines the key bit with certainty. Sec. 7 contains our conclusions.

The source
In the ideal BB84 protocol [1], each signal is carried by a single qubit sent by Alice and received by Bob. The qubit encodes a key bit in one of two conjugate orthonormal bases, which we will call the x basis and the y basis. When Alice uses the x basis, her signal states are the eigenstates with eigenvalues ±1 of the Pauli operator when Alice uses the y basis, her signal states are the eigenstates with eigenvalues ±1 of the Pauli operator Alice's source emits one of these four states, chosen equiprobably. Bob measures the qubit that he receives in either the x basis or the y basis, chosen equiprobably, to determine his key bit. Later, through public discussion, Alice and Bob "sift" their key by retaining only the key bits for which Bob measured in the same basis that Alice used. The final key is extracted from the sifted key via a classical protocol that reconciles Alice's key with Bob's and amplifies the privacy of the key.
In practice, the key information is carried by dim laser pulses transmitted through an optical fiber. In the protocol we will analyze, Alice's source emits one of four states of a pair of photon modes (described by annihilation operators a R and a S ): Here the phase of α is defined relative to a fixed classical phase reference frame that Eve can access. We will refer to the state of mode S as the "signal" pulse and to the state of mode R as the "reference" pulse. The key is encoded in the relative phase of the two pulses, and it is actually quite important for our analysis that the phase of the reference pulse is the same in all four of the signal statesonly the phase of the signal pulse is modulated by the source. (We will discuss in Sec. 6 and Appendix B how security can be compromised when the phase of the reference pulse is also modulated.) In some implementations, the two pulses are spatially separated in the optical fiber by a distance large compared to the pulse width; this scheme is called "phase encoding." In some implementations, the two modes represent the polarization states of the same spatial mode; this scheme is called polarization encoding. Phase encoding has been used in most fiber-based QKD experiments. Our security analysis will also apply to phase encoding in the case where the reference pulse is brighter than the signal pulse. We will return to this generalization in Sec. 4, but for now we will stick with the signals eq. (8), which could arise in either a phase-encoding or polarization-encoding scheme.
To summarize, the crucial features of our source model are: (1) the single-mode signal pulse assumption (the signal pulse is carried by a single bosonic mode, the same mode for all four of the signal states), and (2) the unmodulated reference pulse assumption (the state of the reference pulse is the same for all four signal states). These assumptions are reasonably well fulfilled by realistic sources used for the BB84 protocol with phase-encoded signals. Previous proofs of the security of BB84 have used (2 ′ ) the phase-randomization assumption (the phase of the reference pulse, but not of course the relative phase of signal and reference pulse that encodes the key information, is chosen uniformly at random and is not known by the eavesdropper). Our main new contribution in this paper is to prove security of BB84 using assumption (2) instead of assumption (2 ′ ).

The detectors
When Bob wants to measure the signal he receives in the x basis, he (in effect) combines the two modes in an interferometer, and directs modes a 0,X , a 1,X to two different "threshold" photon detectors, where Therefore, if Alice sends |0 X and the ideal (unattenuated) signal enters Bob's measurement device (which is configured for x measurement), then detector 0 receives a coherent state with mean photon number µ = 2|α| 2 (10) and detector 1 receives the vacuum state. Likewise, if Alice sends |1 X , then detector 0 receives the vacuum, and detector 1 receives the coherent state with mean photon number µ.
When Bob wants to measure in the y basis, the modes directed to the photon detectors are again, depending on the key bit, one mode receives mean photon number µ while the other receives vacuum. We assume that each detector used by Bob to measure the signal he receives is a "threshold" photon detector. This means that the detector cannot distinguish a single photon from many photons. An ideal threshold detector "clicks" (registers a count) if it collects one or more photons, and does not click if it receives no photon; thus it performs a POVM with the two outcomes E no click = |vac vac| , But in this paper we consider a threshold detector that is not ideal: we allow the detector to have imperfect efficiency (it sometimes fails to click even when it receives one or more photons) and to record occasional "dark counts" (it sometimes clicks even when it receives the vacuum state). Because Bob uses two threshold detectors, there are four possible outcomes when he measures a signal. If neither detector clicks, then the measurement is inconclusive and the signal is rejected. If detector b ∈ {0, 1} clicks and the other detector does not, then Bob records the key bit b. If both detectors click, then Bob records a key bit that he chooses uniformly at random. As noted in [12] and as we will explain below, it is important for the security analysis that double clicks are interpreted as key bits rather than regarded as inconclusive measurements. Actually, the security proof works the same way no matter how we map the double click events to key bits, but recording a random key bit is a particularly symmetric and natural choice. Given any fixed prescription for mapping double clicks to key bits, Bob's measurement realizes a POVM with three outcomes: 0, 1, and (when neither detector clicks) inconclusive.
Thus the protocol prescribes that Bob perform one of two possible POVMs, depending on whether Bob declares the x basis or the y basis, where each POVM has three outcomes. In fact, for our security proof we will not need to specify Bob's measurement in detail. All we require is that the measurement satisfy one assumption: Bob's three-outcome POVM is equivalent to a (basis-dependent) two-outcome POVM that determines the key bit, preceded by a basis-independent "filter" that allows the signal to pass if and only if Bob's measurement conclusively determines the key bit.
Following Koashi [19], we note that this property, that the inconclusive measurement outcome can be attributed to a basis-independent filter, follows if we adopt a particular wellmotivated model of dark counts and detector inefficiency, and if we suppose that both of Bob's detectors have the same efficiency. First we note that the inconclusive outcome can occur only if neither detector has a dark count. Let us model the dark counts as a random background process, where the rate of background counts is an intrinsic property of the detector, not dependent on the state of the mode that is being measured. That is, a background click occurs in detector 0 with probability d 0 , whether mode a 0,X or mode a 0,Y is being measured, and in detector 1 with probability d 1 , whether mode a 1,X or mode a 1,Y is being measured. Thus, each time a signal is received, the probability (1−d 0 )(1−d 1 ) that there is no background click in either detector does not depend on whether Bob declares the x basis or the y basis.
Furthermore, let us also assume [20] that when mode a 0,X (or a 0,Y ) contains n photons the probability that detector 0 fails to click is where ξ is the detector's efficiency, and similarly for detector 1. We may imagine that the detector induces decoherence in the photon number measurement before measuring -the real detector might not actually destroy the coherence of a superposition of states with two different nonzero photon numbers, but we are entitled to suppose that it does, because if so Eve's information and the measurement outcome would not be affected. Thus, each signal Bob receives can be regarded as a mixture of eigenstates of the total photon number n, where m ≤ n of the photons are directed to detector 0 and the remaining n − m photons are directed to mode 1. But if both detectors have the same efficiency ξ, and if the probability of no click is given by eq. (13), then the probability that neither detector clicks depends only on n, not on m, and therefore it makes no difference whether Bob's detectors receive modes a 0,X and a 1,X or a 0,Y and a 1,Y ; in other words the probability of an inconclusive outcome does not depend on whether Bob measures in the x basis or the y basis. We conclude, then, that when Bob receives an n photon signal, the probability that no click occurs in either detector, so that the measurement is inconclusive, is which does not depend on whether Bob declares the x basis or the y basis. Thus, we can imagine that a basis-independent filter is applied that measures the total photon number n and blocks the signal with probability Prob(n, inconclusive); if the signal passes the filter, Bob then performs a two-outcome POVM, either M x or M y depending on whether Bob declares the x basis or the y basis.
In order to describe Bob's measurement this way, we need a prescription for mapping the double click events to key bits. This prescription is needed because the probability of a double click event might depend on Bob's declared basis; therefore if the double clicks were regarded as inconclusive we would not be able to attribute the inconclusive outcome to a basisindependent filter. The prescription is incorporated into the definition of the measurements M x and M y , and for the security proof, the details of this prescription do not matter.
We note that if Bob receives a coherent state with mean photon number µ, then the inconclusive outcome occurs with probability In particular, eq. (15) applies if Bob receives one of the signal states in eq. (8) and performs the measurement specified in eq. (9) or eq. (11), where µ = 2|α| 2 . In that case, when Alice and Bob use the same basis, double clicks occur only because of dark counts, and when the measurement is conclusive and there are no dark counts Bob's key bit always agrees with Alice's. Attenuation in the channel reduces the probability of a conclusive outcome, but does not cause bit errors if the signals are otherwise unmodified and if Bob's measurement is ideal.
To summarize, the crucial feature of our detector model is the basis-independent filter assumption, which says that Bob's measurement can be modeled by a basis-independent filter that removes all the signals for which the measurement of the key bit is inconclusive, followed by a (basis-dependent) two-outcome POVM that always produces a conclusive result. This assumption is reasonably fulfilled by realistic measurement devices used in BB84 provided that (1) Bob uses two threshold detectors with the same efficiency, (2) the probability that the detector fails to click decays exponentially as a function of the number of photons received (as in the standard theory of photodetection), and (3) a prescription (either deterministic or probabilistic) is adopted for mapping double click events to key bits. We note that attacks have been proposed and analyzed [21,22] that exploit a mismatch in the efficiency of Bob's two photon detectors, highlighting the importance of assumption (1).
The basis-independent filter assumption limits Eve's ability to enhance her information about the signals by taking advantage of detector inefficiency. But we emphasize that our model still incorporates quite general flaws in the detection system (including for example a reduction in visibility due to an imperfect alignment of Bob's interferometer), because the POVMs M x and M y are arbitrary. Security is not compromised even if the detectors are very noisy, because in that case the bit error rate will be high and the key will almost certainly be rejected.

The unbalanced quantum coin
We can analyze the security of this protocol by applying the methods of [13,18], where security was proven for the case where Alice's source emits signals that, averaged over the key bits, have a small dependence on the basis. To apply this method, we must quantify the basis-dependence of the signal set eq. (8).
It is convenient to imagine that Alice launches each signal by performing a perfect measurement on a qubit that is entangled with the signal mode (the reference mode is always prepared in the state |α no matter which signal is being sent). When Alice wants to send one of the two signals {|0 X , |1 X }, we choose the entangled state of her qubit and the signal mode to be and we instruct Alice to determine her key bit by measuring her qubit in the basis {|0 X , |1 X }.
When Alice wants to send one of the two signals {|0 Y , |1 Y }, we choose the entangled state of her qubit and the mode to be and we instruct Alice to determine her key bit by measuring her qubit in the basis {|1 Y , |0 Y }. See Fig. 1. Now we notice that the states |Ψ x and |Ψ y are hard to distinguish when α is small. Using we find Ψ y |Ψ x = e −|α| 2 cos |α| 2 + sin |α| 2 = e −µ/2 (cos(µ/2) + sin(µ/2)) Note that there is no term linear in µ ≡ 2|α| 2 -that is, if we ignore the multi-photon contribution, the two states are indistinguishable. This happens because, to linear order in α, the two-dimensional subspace spanned by the two x-basis signals and the two-dimensional subspace spanned by the y-basis signals coincide. The large overlap of |Ψ x and |Ψ y indicates that, averaged over the value of the key bit, the states emitted by the source when the x basis is chosen are hard to distinguish from the states emitted when the y basis is chosen. (We have chosen the purifications |Ψ x and |Ψ y that have the maximal overlap compatible with the key-averaged signal states [23]; that is why we have paired |1 Y with |iα and |0 Y with | − iα in eq. (17).) A protocol such that the signals emitted by the source, averaged over the key bit, have a small dependence on Alice's basis choice can be analyzed by considering an equivalent protocol in which the basis-dependence of the signals can be related to the "balance" of a "quantum coin" [13,18]. In this equivalent protocol, Alice measures the coin in the basis {|0 Z , |1 Z } to determine whether her signal is encoded in the x basis or the y basis, and we may take the joint state of the coin and Alice's source states to be furthermore we may imagine that the measurement of the coin is delayed until after Eve is finished interacting with the signals. If she declares the y basis, she measures in the y basis and the entangled state is |Ψy . Bob's detector applies a basis-independent filter that determines whether his measurement has a conclusive outcome, followed by a two-outcome POVM, either Mx or My depending on Bob's declared basis. If Alice and Bob both declare the x basis, the probability that their measurement outcomes disagree is δx, and if both declare the y basis, the probability that they disagree is δy.
If |Ψ x and |Ψ y were equal, then the signals, averaged over the two possible values of the key bit, would be independent of whether Alice chose the x basis or the y basis. If |Ψ x and |Ψ y are nearly equal, then the source leaks a small amount of information about Alice's basis choice that Eve might exploit. A useful way to quantify the leaked basis information is to consider what would happen if Alice were to measure each of her coins in the basis of X eigenstates rather than the basis of Z eigenstates; then the outcome X = −1 would occur with probability ∆, where Thus we say that the coin is "∆-balanced," where ∆ quantifies the basis dependence of Alice's signals. For the signal states eq. (8), we have However, not all of the signals emitted by the source are detected; Eve, by carefully choosing which signals to block, might be able to enhance the basis dependence of the detected signals. Let us pessimistically assume that the detected signals are chosen to maximize the imbalance of the coin. For a perfect channel and for perfect detection efficiency, the fraction of signals detected would be 1 − e −µ ≈ µ, where µ is the mean photon number of the signals emitted by the source. The actual fraction of detected signals is ηµ, where η is an effective rate of loss due to absorption in the channel and imperfect detector performance. In the worst case, for all of the signals that are removed, the coin is an X = 1 eigenstate, which would enhance the probability of the outcome X = −1 by Thus we will use ∆ ′ to quantify the basis dependence in the signals that determine Alice's sifted key.
We will argue that for a fixed ∆ ′ that is sufficiently small, secure key can be extracted from sifted key at a fixed nonzero asymptotic rate. Therefore, the number of private key bits that can be generated per transmitted signal is proportional to ηµ ≈ 8∆ ′ η 2 and hence scales like η 2 -the same scaling as for a source with random phases [12,13] (assuming that decoy states are not used).

The uncertainty principle and privacy amplification
Koashi [18], generalizing the techniques in [13], explained how to relate the imbalance of the quantum coin to the privacy of a key that is generated by performing ideal measurements on qubits; here we wish to apply his reasoning to Alice's key bits, which we regard as determined by outcomes of measurements of (fictitious) qubits entangled with the signal states. For our argument, it is important that the imbalance of the coin arises solely from the basis dependence of Alice's signals. That is why we required that Bob's measurement be modeled by a basis-independent filter followed by a two-outcome measurement; if the probability of an inconclusive outcome actually depended on the basis, then the basis-dependence of the filter might have further enhanced the imbalance of the coins. As it is, after the inconclusive measurement results are discarded, we may imagine that Bob performs his two-outcome POVM on signals that are entangled with Alice's qubits and the quantum coins, where the imbalance ∆ ′ of the coins is determined only by the basis dependence of the source and the loss in the channel.
We recall that the BB84 protocol includes a verification test conducted by Alice and Bob. In the test, Alice and Bob publicly compare a randomly selected subset of their key bits to estimate a bit error rate, the fraction of the key bits for which Alice and Bob disagree. Signals sent in the x basis and the y basis can be tested separately, to estimate both a bit error rate δ x for signals sent in the x basis, and a bit error rate δ y for signals sent in the y basis. Let us consider the key bits that are generated by measuring in the x basis. Using Koashi's method [18], we may show that, in the asymptotic limit of a very long key, private key can be extracted from Alice's sifted key at a rate where δ x is the bit error rate, δ ′ y ≥ δ y is a function of δ y and ∆ ′ , and H(δ) = −δ log 2 δ − (1 − δ) log 2 (1 − δ) is the binary Shannon entropy. A similar formula applies for the key bits generated by measuring in the y basis, but with δ x and δ y interchanged. The term H(δ x ) is the rate at which sifted key must be sacrificed to perform error correction that reconciles Bob's key with Alice's (according to standard Shannon theory), and H(δ ′ y ) is the cost of performing privacy amplification to ensure that Eve has negligible information about Alice's final key.
What is the quantity δ ′ y ? Recall that when the x basis is declared, Alice measures her qubit in the x basis and Bob performs measurement M x , while if the y basis is declared, Alice measures her qubit in the y basis and Bob performs measurement M y . Furthermore, when the x basis is declared, the entangled state of Alice's qubit and the signal mode is |Ψ x , while when the y basis is declared, the entangled state is |Ψ y . The quantity δ ′ y is an upper bound on what the bit error rate would have been if Alice measured in the y basis and Bob performed measurement M y , but where the entangled state of the qubit and mode is |Ψ x

Eve
Filter

Bob measures My
Alice measures y qubit mode d d Fig. 2. Setting that defines the "phase error rate" δ ′ y . The entangled state of Alice's qubit and the signal mode is |Ψx as though Alice had declared the x basis, but Alice and Bob both measure in the "wrong" basis -Alice measures y instead of x, and Bob measures My instead of Mx. The probability that Bob's outcome disagrees with Alice's is δ ′ y . The quantity δ ′ y cannot be directly measured in the protocol, but an upper bound can be inferred from the observed bit error rate δy and the known basis dependence of Alice's signal states.
instead of |Ψ y . This hypothetical error rate is not known directly from the test, but because the state |Ψ x is close to |Ψ y when ∆ is small, the hypothetical "phase error rate" δ ′ y is close to the actual observed bit error rate δ y . See Fig. 2.
The estimate of δ ′ y is explained in Appendix 1. The result is that for any ε > 0, with high probability we may express δ ′ y as The upper bound on δ ′ y in the last line is obtained by retaining only the terms of lowest order in δ y and ∆ ′ , and gives a reasonable approximation to the tighter bound on the previous line. From the tighter bound and eq. (24), we see that the key generation rate R remains positive, in the limit of negligible bit error rates δ x , δ y , for ∆ ′ < 0.146, which corresponds to µ smaller than about (1.16)η when η is small.
Why does δ ′ y characterize the cost of amplifying privacy? Following Koashi [18] (and generalizing an idea used in [2] and [6]) we observe that when the x basis is declared, Eve's knowledge about Alice's key would not have been affected if Bob had chosen to measure in the wrong basis (to measure M y rather than M x ). Furthermore, neither the key nor Eve's knowledge of the key would have been affected if Alice had chosen to delay measuring her qubits until after Bob measured the signals that he received. Therefore, we may imagine that Alice generated her key by measuring in the x basis a string of qubits that, conditioned on the outcome of Bob's M y measurement, are close to y-basis eigenstates (if δ ′ y is small). If, after Bob's measurement, each of Alice's qubits were exactly a y-basis eigenstate, then Eve would be powerless to predict the key bits that Alice obtains by measuring the qubits in the x basis. In that case we could say that the privacy of the key is founded on the uncertainty principle: a qubit that produces a deterministic outcome when measured in the y basis will produce a uniformly random outcome when measured in the x basis. From this perspective, we may say that the purpose of the privacy amplification is to ensure that Alice's final key is very nearly equivalent to a key determined by measuring y-basis eigenstates in the x basis.
Let the n-component binary vector v denote Alice's sifted key for the signals in which the x basis was declared by Alice and Bob, and Bob reported successfully detecting the signal. Alice extracts her k-bit final key κ = vG by applying the random rank-k binary n × k matrix G to the sifted key. Equivalently, we may say that Alice's final key is obtained by measuring the k binary observablesX where X j denotes the Pauli matrix X acting on Alice's jth qubit. Before selecting the matrix G, we might have first selected a random rank-(n − k) binary n × (n − k) matrix H, and then chosen G subject to the constraint G T H = 0 (so that each column of G is orthogonal in the binary inner product to each column of H). In that case, each of the n − k binary observables (where Y j denotes the Pauli matrix Y acting on Alice's jth qubit) would commute with each of theX i 's. We may therefore imagine (since it would have no effect on Alice's final key or on Eve's information about the key) that Alice measured each of theȲ m 's before measuring theX i 's to determine her final key bits. Now, if Alice were to measure all of her qubits in the y basis, then with probability exponentially close to 1 for n large, her outcome would be one of N typ = 2 n(H(δ ′ y )+ε) typical n-bit strings. Note that if u and v are two distinct n-bit strings, and s is a randomly chosen n-bit string, then the bits us T and vs T are distinct with probability 1/2. Therefore if we choose the number of randomly chosen binary observables in the set {Ȳ m } (the number of columns in the matrix H) to be then the probability that more than one typical binary string is compatible with the outcomes of the {Ȳ m } measurements is at most N typ ·2 k−n = 2 −εn . This means that, conditioned on the results of measuring all the observables in the set {Ȳ m }, Alice's n qubits have been projected to a state that is exponentially close to a product of y-basis eigenstates. Thus Alice's final key is essentially the same as it would have been if the sifted key had been generated by measuring y-basis eigenstates in the x basis, and therefore is guaranteed to be private. Since k = n 1 − H(δ ′ y ) − 2ε , and n H(δ x ) + ε ′ key bits are sacrificed to reconcile Bob's sifted key with Alice's, we obtain the asymptotic key rate eq. (24).

Universal composability
This argument shows not just that Eve's mutual information with the final key is negligible, but also that a stronger definition of security is satisfied: the protocol is universally composable [24,25,26]. This means that the final key bits can be safely used in any subsequent application without compromising security. To demonstrate composability, we consider in more depth (following [26]) the joint state shared by Alice and Eve before Alice performs her x-basis measurements to generate her key. We have already seen that, after Alice's fictitious measurement of the observables {Ȳ m }, her density operator ρ A has high fidelity with the pure state |y 0 , where |y 0 denotes a particular product of y-basis eigenstates: where ζ is exponentially small. Therefore we may introduce an auxiliary system E, which we pessimistically assume to be under the eavesdropper's control, such that ρ A has a purification |Υ AE where |Υ AE has a large overlap with |y 0 A ⊗ |λ E and |λ E is a pure state of E: We can relate the large overlap to proximity in the trace norm, using the inequality Now when Alice measures the observables {X i } to determine her final key, the state |y 0 y 0 | yields a uniformly random key described by the maximally mixed density operator and the resulting state shared by Alice and Eve is a product state ρ uni A ⊗ σ E , where σ E = (|λ λ|) E . Quantum operations cannot increase the trace distance; therefore, if ρ AE is the state shared by Alice and Eve after Alice's measurement, we find that Eq. (34) is a security criterion shown to be universally composable in [25], which we have now seen is satisfied by a protocol where the signal states have nonrandom phases. This demonstration of universal composability for the BB84 quantum key distribution protocol also applies to the other cases addressed by Koashi in [18,19].

Bright reference pulse
Our security proof also applies if the reference pulse is bright. Suppose that, for each of the BB84 signals, the state of the reference pulse emitted by the source is |β R , while the emitted state of the signal pulse is as in eq. (8), where |β| ≥ |α|. Then we may calculate the imbalance of the quantum coin as before, except in eq. (22) we replace µ/2 by µ S = |α| 2 , the mean photon number of the signal pulse. When Bob receives the signals, he first attenuates the reference pulse so that its strength matches the strength of the signal pulse, and then performs the interferometric measurement described earlier. Thus we replace ηµ in eq. (23) by 2ηµ S , the mean total photon number of the two modes after the attenuation of the reference pulse (and taking loss into account). Therefore, in both formulas we replace µ by 2µ S , finding when the signal pulse is weak. It is obviously essential for this argument that the (possibly bright) reference pulse has exactly the same state (or at least very nearly the same state) for each of the BB84 signals, so that it conveys no information (or very little information) to Eve concerning which signal is emitted. Eve might tamper with Bob's measurement of the signal by attacking the reference pulse, but because she knows little about the basis in which the key bit is encoded, she is still incapable of collecting much information about the key without creating a detectable disturbance. Why is it that Eve seems to be no better off when the reference pulse is bright than when it is as dim as the signal pulse? The reason is that even when the reference pulse is dim we have pessimistically assumed that Eve knows the phase of the reference pulse perfectly. When we say that Eve "knows" that the state of the reference pulse is the coherent state |β R , we are taking it for granted that the phase of β has a fixed value relative to a classical phase reference that Eve controls. If the phase of β were not already known, then increasing |β| would make it easier for Eve to determine the phase relative to her reference frame, but if the phase is already known then increasing |β| does not give Eve any additional advantage.
The observation that the reference pulse can be bright without compromising security is relevant to, for example, the "double Mach-Zehnder" scheme for implementing phase encoding [27,28]. In this set-up, Alice uses an unbalanced interferometer to split a single pulse into two spatially separated pulses that travel to Bob through the same optical fiber; one of these pulses, whose phase is unmodulated, is the reference pulse, and the other, whose phase is modulated, is the signal pulse. Bob uses another unbalanced interferometer to combine the two pulses, with a modulated relative phase that determines his measurement basis.
For a given strength of the signal pulse, using a brighter reference pulse increases the key rate by reducing the probability that Bob fails to detect the signal. In particular, if the reference pulse is much brighter than the signal pulse, then nearly twice as many signals will be detected compared to the case where the reference and signal pulses have equal strength. Our proof shows that the key rate can be doubled by using a bright reference pulse, without reducing the privacy of the final key.
We can understand this doubling of the key rate by considering how Bob's detection system operates in the double Mach-Zehnder scheme. Let us suppose that the reference pulse follows the longer path in Alice's unbalanced interferometer and therefore lags behind the signal pulse during transmission through the fiber; we therefore use a L (L for "long") to denote the reference mode, and a S (S for "short" as well as "signal") to denote the signal mode. The two paths in Bob's interferometer also have unequal lengths, to compensate for the spatial separation in the fiber of the reference and signal pulses: the portion of the reference pulse that follows the short path in Bob's interferometer (let us call it the LS mode, since it follows the long path in Alice's interferometer and the short path in Bob's) interferes with the portion of the signal pulse that follows the long path in Bob's interferometer (the SL mode). The first beam splitter in Bob's interferometer is asymmetric, so that the reference and signal pulses are split according to where c 2 + s 2 = 1. Here LL refers to the part of the reference pulse that enters the long arm of Bob's interferometer, and SS refers to the part of the signal pulse that enters the short arm; these LL and SS modes are ignored by Bob. We denote the strengths of the reference and signal pulses byβ andα rather than β and α to take into account the attenuation of the pulses during transmission through the fiber; thus, if Eve does not intervene, |α|/|β| = |α|/|β|. Bob's first beam splitter is chosen so that s|β| = c|α|, or s/c = |α|/|β|; therefore the incoming LS and SL modes at Bob's second beam splitter have equal strength. This second beam splitter is symmetric, and Bob reads out his device by detecting the photons in the two output ports of this symmetric beam splitter. The probability of detection is proportional to the total mean photon number in the LS and SL modes as they arrive at Bob's second beam splitter, which is where The factor c 2 suppressing the detection rate arises because the strength of the signal pulse following the long path in Bob's interferometer is attenuated by the factor c at the first beam splitter; the rest of the signal pulse follows the short path and is wasted. This factor c 2 is 1/2 for |α| = |β| but close to 1 for |β| 2 ≫ |α| 2 . Thus when the reference pulse and signal pulse have the same strength half of the signal is wasted, but when the reference pulse is bright hardly any of the signal is wasted.

Comparison to phase-randomized signals
It is instructive to compare our estimate of the key generation rate with the rate that would be achievable if the phases of the signals were random. In that case, the quantum coin is undisturbed if the source emits a single photon, but it is strongly affected if two or more photons are emitted. Thus the fraction of the coins that are damaged is at worse where p M is the probability for emission of a multi-photon, and p D is the fraction of the signals that are detected. Therefore, for small µ we have [13] The key generation rate again has the form eq. (24), but for coins in this particular type of state (a fraction ∆ ′ badly damaged and a fraction 1 − ∆ ′ undisturbed), the estimate of δ ′ y can be improved to (Eq. (40) is an improvement found in [29] of the result δ ′ y − δ y = ∆ ′ found in [13].) For comparison, by combining eq. (23) with eq. (25) we find for the case where Eve knows the phase of the signals; thus we see that phase randomization improves the rate, but only by a relatively modest amount when the bit error rate is small. In fact, as shown in [13], for a phase-randomized source a higher key generation rate can be achieved than implied by eq. (24) and eq. (40), furthermore as shown in [19] this higher  The key generation rate in bits per pulse as a function of distance for sources with random and nonrandom phases, using experimental parameters from [10], and assuming an error-correction inefficiency f (e) = 1.22. Here for the phase-randomized case we assume that decoy states are not used. For each value of the distance, the signal strength has been chosen to optimize the rate.
rate applies for the detector model assumed in Sec. 2. The achievable number G of key bits per pulse can be expressed as Here Q is the fraction of pulses for which Bob detects the signal, e is the bit error rate observed in the verification test, and f (e) ≥ 1 parametrizes the inefficiency of the error correction used to perform key reconciliation; furthermore e 1 is the error rate for the single-photon signals emitted by the source and Q 1 is the fraction of the single-photon signals that result in a detection event. (The factor of 1 2 in front of the expression for G arises because half of the detected signals, those for which Alice and Bob used different bases, are discarded during sifting.) In a protocol that uses decoy states, Q 1 and e 1 can be estimated directly, but if decoy states are not used then we may pessimistically assume all the bit errors are due to single-photon signals, so that (with ∆ ′ = p M /Q), and that all the multi-photon signals are detected, so that For the case of a source with nonrandom phases, the achievable key rate per pulse is here e ph as a function of e is given as in eq. (25) by where ∆ ′ = ∆/Q = 1 2Q 1 − e −µ/2 (cos(µ/2) + sin(µ/2)) .
We have plotted the key rates per pulse given by eq. (42) and eq. (45) as a function of distance in Fig. 3. For this comparison, we have used experimental parameters (channel loss, dark count rate, and detector efficiency) from [10], and assumed an error-correction inefficiency f (e) = 1.22; for each value of the distance, the signal strength µ has been chosen to optimize the rate. The maximal distance for which secure key exchange is possible is about three times longer in the phase-randomized case.

Phase modulated reference pulse
The security proof works because the overlap of |Ψ x and |Ψ y is 1 − O(µ 2 S ). This property holds because, if we assume that the phase of the reference pulse is unmodulated, then the four BB84 signal states span a two-dimensional space when the multi-photons in the signal pulse are neglected. But, even when the reference pulse is weak, the story can change if the source modulates the phase of the reference pulse as well as the signal pulse. In [30] we studied such a source, and we concluded that the eavesdropper can exploit the modulation of the reference pulse to improve the effectiveness of her attack.
In particular, in Appendix B (see also [30]), we study the BB84 signal states in which the reference pulse for each signal has a distinct phase relative to Eve's classical phase reference. Thus key information is encoded not just in the relative phase of the signal and reference pulses, but also in the phase of the (dim) reference pulse relative to Eve's reference frame. The signal set eq. (48) seems more natural if we recognize that, when re-expressed in a different basis, it becomes the signal set eq. (B.1); thus it arises in a polarization encoding scheme where the single-photon component of each signal is the standard BB84 single-qubit signal, and where the relative phase of the vacuum and single-photon component is the same for all four signals. We note that, even if we ignore the (small) multi-photon component of the weak coherent state signals, these four BB84 signals belong to a three-dimensional Hilbert space spanned by the vacuum (no-photon) state and two distinguishable one-photon states. On the other hand, the two signals that convey a particular key bit value (0 or 1) span a two-dimensional space. Therefore, an eavesdropper who knows the relative phase of the vacuum and single photon component can launch an attack on the protocol that we call unambiguous key discrimination. She performs a POVM with three outcomes: 0, 1, and inconclusive; if either of the conclusive outcomes occurs, then Eve knows with certainty the key bit (0 or 1) encoded in the BB84 signal emitted by the source, though she does not gain any information about which of the two possible BB84 states compatible with that key bit was emitted.
For these signal states, we show in Appendix B that Eve's key discrimination has a conclusive outcome with probability p C ≈ .146µ when the mean photon number µ is small. If the signals had random phases, then only the multi-photon signals would be insecure, a fraction O(µ 2 ) of all the signals. But when the phase of α is known and the signals eq. (48) are used, this fraction increases to O(µ).
As van Enk [31] has astutely pointed out to us, the unambiguous key discrimination attack becomes much less effective if the encoding of the signals is chosen judiciously. And for the signal set eq. (8) in which the reference pulse has the same phase in all four signals, the signals span a two-dimensional space when the multi-photons are neglected, so that the conclusive key discrimination succeeds with probability p C = O(µ 2 ). (For polarization encoding, this corresponds to particular choices for the phases of the coherent states and for the orientation of the BB84 polarization states in the Bloch sphere.) Thus as we have seen, unconditional security is provable for this particular encoding, but the proof does not apply to the signal set eq. (48). Therefore, the protocol is vulnerable to a "Trojan horse" attack, in which a malicious manufacturer in cahoots with Eve provides Alice with a source that modulates the phase of the reference pulse [32].
There are other possible Trojan horse attacks that could be even more devastating -for example the source might encode the four BB84 states in four distinct bosonic modes so that Eve can distinguish the signals perfectly. It is useful, however to differentiate such multi-mode Trojan horse attacks from the more subtle attacks where the protocol is compromised because the source modulates the phase of a single mode. The single-mode Trojan horse might be harder for Alice and Bob to detect, and might be less susceptible to countermeasures [33] such as filtering out the unwanted modes.

Conclusion
In summary, we have shown that the BB84 quantum key distribution protocol with phaseencoded signals is secure if the signal pulse is weak. Our proof applies even if the reference pulse is bright and has a phase known by the adversary, provided that the phase of the reference pulse is the same for all four of the BB84 signals, and the measurement device satisfies the basis-independent filter assumption formulated in Sec. 2. Furthermore, our proof shows that the BB84 protocol is universally composable under these conditions. Our security proof also applies to polarization encoding, if the signal states are chosen appropriately. And we have discussed a new type of single-mode Trojan horse attack, in which security can be compromised because the source modulates the phase of the reference pulse depending on which signal is being emitted.
The achievable key rate established by our proof scales quadratically with the transmission η in the channel, as for BB84 with phase-randomized weak coherent-state signals. In the phase-randomized case, a key rate linear in η can be achieved with the decoy state method. An interesting open question is whether employing decoy states can also extend the range over which secure BB84 quantum key distribution is possible in the case where the eavesdropper knows the phase of the (possibly bright) reference pulse and the detector is modeled as in Sec. 2. We note that a key rate linear in η has been established for the B92 [27] protocol assuming that the reference pulse is bright and the detector has suitable properties (one proof requires Bob to have a local oscillator phase-locked with the reference pulse [34], another requires that Bob's detector can distinguish single-photon signals from multi-photons [35]), but these proofs do not apply to the threshold detectors used in current experiments. It may also be fruitful to investigate the impact on security of using imperfect sources and detectors for other quantum key distribution protocols, such as the six-state protocol [36] and SARG04 [37].
Finally we remark that, since a higher key generation rate has been established for the case where the reference pulse has a random phase than for the case where the phase is known, it may be advantageous to deliberately randomize the phases of the signals in order to reduce the eavesdropper's power. An experimental demonstration of quantum key distribution using active phase randomization was recently reported in [38].
for any ε > 0 and with probability exponentially (in n) close to 1, Thus, despite the possible correlations among the qubits, the results are constrained by the naive Bloch sphere bound in the limit of large n. It is convenient to rewrite this inequality (suppressing the ε) as We could apply the Bloch sphere bound to the quantum coin; the coin is measured in the z basis to determine whether Alice will encode her key bit in the x basis or the y basis. Thus γ z is the probability that Alice declares the y basis, 1 − γ z is the probability that Alice declares the x basis, and the "imbalance" of the coin is ∆ ′ = γ x .
However, our goal is to relate the bit error rate δ y that is observed when the y basis is declared to the bit error rate δ ′ y that would have been observed when the x basis is declared, if both Alice and Bob had measured in the "wrong" basis (the y basis rather than the x basis). Therefore, we will imagine that Alice and Bob always measure in the y basis, and we will divide the signals into two sets -the set for which Alice and Bob find key bits that agree (the set "n" for "no error") and the set for which Alice and Bob disagree (the set "e" for "error").
Let X coin denote the Pauli operator X acting on the coin, let Z coin denote the Pauli operator Z acting on the coin, and define Applying the Bloch sphere bound to the signals with a y-basis error we obtain and applying it to the signals with no y-basis error we obtain Using Bayes's rule, we have and likewise therefore, multiplying both sides of eq. (A.5) by Prob(Y error), we find By applying the same reasoning to the signals with no y-basis error, we find from eq. (A.6) that Prob(no Y error) − 2 Prob(X coin = −1, no Y error) Now adding together eq. (A.10) and eq. (A.11), we have This inequality says that δ ′ y must be close to δ y if ∆ ′ is small. After some algebra (and after reinstating ε), we may re-express eq. (A.12) in the form eq. (25).
In our analysis, we have allowed a basis asymmetry in the detected signals (γ z = 1/2). This asymmetry might occur because the source leaks a small amount of information about the basis choice, and Eve could use that basis information to (say) block more x-basis signals than y-basis signals. However, using the available basis information to enhance the basis asymmetry is not a good strategy for Eve. Rather, her attack is most effective when δ ′ y − δ y is largest, and eq. (A.12) indicates that the maximal possible value of δ ′ y − δ y occurs when x-basis and y-basis signals are detected with equal likelihood (γ z = 1/2).
In the end, the inequality eq. (A.12) has a simple form and in fact it admits a simple interpretation. Recall that if ρ x and ρ y are two density operators and the operators {E a } are the elements of a POVM, then there is an inequality relating the fidelity of the two density operators to the statistical overlap of the measurement outcomes: Ignore for the moment the correlations among the signal states that might be induced by Eve's attack, and suppose that, for each signal, the joint state of the qubit measured by Alice and of the bosonic modes measured by Bob is ρ x when Alice declares the x basis and ρ y when Alice declares the y basis. Recall that for the detector model formulated in Sec. 2, the probability that Bob's measurement yields a conclusive outcome does not depend on whether Bob measures in the x basis or the y basis; let us denote this probability that Bob's measurement is conclusive as Q x in the state ρ x and Q y in the state ρ y . Let {E a } be the threeoutcome POVM that outputs "inconclusive" when Bob's measurement is inconclusive, outputs "agree" when Bob's y measurement is conclusive and agrees with Alice's y measurement, and outputs "disagree" when Bob's y measurement is conclusive and disagrees with Alice's y measurement. Then eq. (A.13) becomes For a fixed value of Q x + Q y , the right-hand side of eq. (A.14) is maximized for Q x = Q y ; therefore, defining Q = (Q x + Q y )/2, we find But Eve's attack cannot improve the distinguishability of ρ x and ρ y ; thus and so we obtain where ∆ ′ = ∆/Q, in agreement with eq. (A.12). This fidelity argument establishes security against individual attacks, but we have not seen how to turn it into a rigorous proof of security against collective attacks. Recall that we need eq. (A.12) to hold with high probability even if (after Eve's attack) the signals are highly correlated with one another. For this purpose it would be natural to use the quantum de Finetti theorem [40,41] to show that the state of all the signals can be well approximated by a convex combination of product states. But unfortunately, because the Hilbert space of the signal and reference modes is infinite dimensional, the de Finetti theorem does not provide a useful approximation. Fortunately, though, the argument based on the imbalance of a quantum coin applies for any two-outcome POVM that Bob might apply (after the filtering), irrespective of the dimension of Bob's Hilbert space. key bit. The two conclusive outcomes of the POVM are projections onto the states: where N µ,0 , N µ,1 are normalization factors such that The vector |0 ⊥ is orthogonal to both of the two states |0 Z and |0 X that indicate the key bit 0. Hence, if this outcome is found, Eve knows for sure that the key bit could not be 0 and so must be 1. Similarly, the vector |1 ⊥ is orthogonal to both of the states |1 Z and |1 X that indicate the key bit 1. The vectors |0 ⊥ and |1 ⊥ are nearly parallel for small α. To ensure that all three POVM elements are positive, we may choose (For small positive µ, the strength of the conclusive POVM elements can be pushed up slightly, but this is a small effect that we ignore.) Thus we find the probability p C of a conclusive outcome (taking into account that Eve might detect multi-photons and reject the state) if the key bit is 0, and if the key bit is 1. We note that the conclusive outcome is slightly more likely when the key bit is 1. This asymmetry can be traced to the property that the overlap | 0 X |0 Z | of the two signals that indicate the key bit 0 is slightly larger than the overlap | 1 X |1 Z | of the two signals that indicate the key bit 1. (For other choices of the phase e iϕ that determines the plane in the Bloch sphere occupied by the BB84 signals, the asymmetry is substantially larger.) In any case, for either value of the key bit, the probability of a conclusive outcome obeys Now p C is the probability that Eve resends the signal to Bob, and therefore it is also the probability p D that Bob detects a signal, if his detector is perfectly efficient. If there were no interference by the eavesdropper (and no loss in the quantum channel connecting Alice and Bob), all non-vacuum signals would be detected, and then p D = 1 − e −µ = µ + O(µ 2 ). If Eve uses the unambiguous key discrimination POVM, then of course p C vanishes in the limit µ → 0, but what is noteworthy is that p C vanishes linearly with µ. Thus for µ small, a fraction η ≈ .146 of order one of all the non-vacuum signals sent by Alice are received by Bob. (Since multi-photon signals span a space of even higher dimension, there is a POVMunambiguous state discrimination -that, when conclusive, identifies not just the key bit but also the basis [42]; however for that POVM the probability of a conclusive outcome is higher order in µ.) Having characterized Eve's attack against a source that emits the signal set eq. (B.1), let us now consider the security analysis of a phase-randomized source. We will refer to the source that emits weak coherent states with a definite phase known by the eavesdropper as source P (for phase), and to a source that emits phase-randomized weak coherent states, with the same mean photon number µ, as source R (for random). If source P emits the signals eq. (B.1), and Eve launches the intercept/resend attack using unambiguous key discrimination, then Eve has perfect knowledge of every key bit, and Alice and Bob detect a bit error rate of δ = .146. But if source R is used instead, we will see that Alice and Bob can extract private key at a nonzero asymptotic rate for a bit error rate up to δ = .189. For the security analysis of source R, we will adopt a more restricted (and less realistic) model of the detector than the model described in Sec. 2: the detector applies a basis-independent "squash" that maps the incoming signal to a qubit, and then an ideal BB84 measurement is performed on that qubit in the appropriate basis.
We suppose that the source emits a multi-photon signal with probability p M , that Bob detects a fraction p D of all the signals sent by Alice, and that Eve's attack is unrestricted. Of the signals that are received, the fraction that were emitted as multi-photons is no more than ∆ = p M /p D ; the rest are single photon signals.
To establish a nonzero key generation rate for a relatively high bit error rate, we will need to consider schemes for key reconciliation and privacy amplification that involve twoway communication between Alice and Bob, for which the argument in [18] based on the uncertainty principle does not apply. Instead we can prove security following [5], by relating the BB84 protocol to a protocol in which the key is generated by measuring noisy entangled pairs shared by Alice and Bob. Private key can be extracted at a positive asymptotic rate if it is possible to distill high fidelity entanglement from the noisy entanglement. Entanglement distillation will succeed if the noisy entangled pairs have a bit error rate and a phase error rate that are both sufficiently small. The bit error rate δ is inferred directly from the verification test in the BB84 protocol; the phase error rate δ p is also inferred, but by a less direct argument.
If the source and detector used in the protocol were perfect, then a symmetry argument would suffice to show δ = δ p . This symmetry is broken if the equipment is imperfect, but it is still possible to bound the difference between the two error rates using an appropriate characterization of the imperfections. For the case where Bob has a perfect detector, but Alice's source sometimes emits multi-photons, it can be shown as in eq. (40) that |δ p − δ| < ∆/2 , (B.9) where ∆ is the fraction of all the detected signals that were emitted as multi-photons. Eq. (40) is an improvement found by Boileau [29] of the result |δ p − δ| = ∆ found in [13]. The security proof in [5], which relates one-way privacy amplification to one-way entanglement distillation using quantum error-correcting codes, does not apply for a bit error rate above δ = .110. But security of BB84 was established in [43] for a bit error rate as high as .189, by relating two-way privacy amplification to entanglement distillation with two-way communication between Alice and Bob. The original argument in [43] assumed a perfect source and detector. But the two-way entanglement distillation succeeds if both δ and δ p are below .189; therefore the argument can be applied to a protocol with imperfect equipment if there is a strong enough bound on |δ − δ p |.
If the bit error rate δ is .146, then the two-way BB84 protocol is secure for |δ − δ p | < .189 − .146 = .043. And for a source that emits phase-randomized coherent states, it suffices that ∆ < .086, where ∆ = p M p D ≤ (B.10) Thus ∆ < .086, and the protocol is provably secure, for µ < .0240. The security proof still applies if Bob's detector, rather than being perfectly efficient, has an efficiency that is independent of the basis in which the detector measures, where whether the detector fires is decided randomly, uninfluenced by the eavesdropper [44]. We have shown, therefore, that the BB84 QKD protocol is less secure using the phasecoherent source P than using the phase-randomized source R. Eve can exploit her knowledge of the phase of the signals emitted by the source P to implement a POVM that, when its outcome is conclusive, unambiguously identifies the key bit. But for the same bit error rate δ ≈ .146, signal strength µ (< .0240), and signal detection rate p D ≈ .146µ, if the signals have random phases then Alice and Bob can generate a final key about which Eve has negligible knowledge.
In fact, for source P using the signal set eq. (B.1) we do not have a security proof that establishes any positive bit error rate δ such that provably secure key can be generated at a positive asymptotic rate. However, as we have emphasized, it is a different story for the signal set eq. (8). In this paper, we have proven the security of BB84 using these signals, even when Eve knows the phase of the reference pulse.


RV 2005 Preliminary Version Steering of Discrete Event Systems: Control Theory Approach

Runtime verification involves monitoring the system at runtime to check for conformance of the execution trace to user defined safety properties. Typically, run-time verifiers do not assume a system model and hence cannot predict violations until they occur. This limits the practical applicability of runtime verification. Steering is the process of predicting the occurrence of violations and preventing them by controlling system execution. Steerers can achieve this using a limited knowledge of the system model even in situations where it is infeasible to store the entire model. In this paper, we explore a control-theoretic view of steering for discrete event systems. We introduce an architecture for steering and also describe different steering paradigms.

Introduction
Verification and validation are established techniques to ensure correctness of software systems. But, verification checks the specification rather than the implementation and validation does not provide guarantees for conformance. Also, verification and validation do not scale well to large systems. Runtime verification checks for conformance of execution traces to formally specified safety properties and hence exports the advantages of verification techniques to trace validation. Although runtime verifiers can efficiently detect nonconformance, they cannot predict violations in advance because they do not have information on the system model. Since any run-time technique deals with a single execution trace, limited knowledge (local to the execution trace) of the system model will be sufficient to predict violations with high confidence. Steering exploits this limited system knowledge to predict violations.
A steerer looks ahead into a partial system model to explore the state space in advance. It then invokes the runtime verifier to detect non conformance and generates control actions to prevent the system from reaching a violation. Steering can thus be defined as the process of analysis (using look ahead) of a partial system model to detect non-conformance (prediction) and application of control actions to the model (prevention). We assume, the steerer and the system to be residing on different machines and executing concurrently. This leads to communication delay in the transmission of event notifications and steering actions between the steerer and the system.
In this paper, we formulate the problem of steering of Discrete Event Systems (DES) as a supervisory control problem. Communication delay is accounted for by assuming partial observability of the system. We introduce a generic architecture for steering and propose four different steering paradigms. Constraints imposed on the system model and the steering overhead to the system are used to classify these paradigms. The paper then describes a subway system example to which a particular paradigm is applied.
Related Work: Stephane et. al. in their online control work [3], [4], [6] present a control-theory-based approach for control of DES with limited look ahead. We adapt this work to the steering problem where steerers must generate control actions with as little latency as possible in the presence of communication delays and concurrent execution. The steering framework described in [8], [10] is specific to a particular runtime verifier and assumes that a recovery after the occurrence of a violation is always possible. It assumes no knowledge of the system model and hence the user is required to specify steering actions. Papers [5], [7], [1] provide very domain specific solutions to simpler control problems and would be extremely inefficient in a general framework.
The rest of the paper is organized as follows. Section 2 lists motivating examples for steering and Section 3 formally defines the steering problem. Section 4 introduces the steering architecture and Section 5 formulates the steering problem as a control problem under partial observability. Section 6 describes four steering paradigms and Section 7 gives an illustrative example. Section 8 concludes the paper and indicates future research directions.

Motivation
When developing a software system, the designer and the users have at least an informal idea of properties that the system must satisfy. However, subtle errors throughout the software engineering process can lead to an incorrect implementation. Static analysis of an abstract model of the implementation to eliminate undesirable behaviors is a challenging problem when the state space  to be explored is large or time varying(dependent on external environment). Thus, in order to eliminate undesirable behaviors while preserving a rich set of allowable behaviors, we must use dynamic control. In this section, we list a few examples from different domains that support our claim for the need of a steerer.

Scheduling of real-time tasks using actual execution time
The paper [1] introduces a real-time task model in which the worst case execution times for each task, minimum and maximum execution periods for each task and the desired system utilization are given. The runtime verifier monitors task executions to determine their actual execution times and then evaluates the actual utilization of the system. The steerer uses this utilization estimate to adjust task periods so that the desired utilization may be achieved. This architecture is shown in Figure 1(a).

Reconciling System Requirements at run-time
At run-time, a software system can deviate from its expected behavior because of changes in the system environment. The paper [5] suggests two approaches for runtime steering. As shown in Figure 1(b), steering can be achieved by monitoring the system and modifying control parameters to minimize deviations. If the deviation is large, the steerer could also request that an alternate design model be used by the system. For example, consider a meeting scheduler scheduling a meeting based on the availability times of all the participants. One of the system requirements is that the scheduler should be able to get the availability times of the participants. One way of achieving this goal is by locating the agenda for each participant and extracting the availability times.
An alternate approach would be to send email requests to participants. Steering would then involve switching between these approaches depending on the accessibility of the agenda. When using the email model, the steerer can also monitor the delay in response of participants and adjust reminder frequencies accordingly.

Inverted Pendulum
Paper [8] describes a control system which consists of an inverted pendulum run by an experimental controller. The experimental controller generates random values for the motor speed of the pendulum. The runtime monitor checks if the experimental controller is maintaining the pendulum within a stable region. If the monitor detects a violation it switches the control to a safety controller which maintains the pendulum in the stable region. This experiment demonstrates the use of steering in a continuous-variable, constrained environment.

Problem Statement
As described in Section 2 steering is essential to detect certain errors in software, especially when the system state space is large or time varying. In this paper, we develop a steering architecture and steering paradigms for DES with large state spaces.

Steering for DES with large state spaces
Any steerer for a DES must satisfy the following properties, Light Weight: Steering must be light weight i.e., the steerer should not behave like a central controller.
Fast: Low response time is desirable because steering actions are state dependent. Low response time is also a desired property when steering realtime systems.
Minimally restrictive: Steering must restrict the system model minimally while ensuring that violations do not occur.
We now formulate the steering problem for DES with large state spaces. A DES is a transition system M = S, T, Σ , where S is the large state space, Σ is the event set and T is the transition function T : S × Σ −→ S. We assume that all the events Σ are controllable by the steerer. The state space S is discrete and hence finite or countably infinite. The state machine is event driven i.e., at each time instant at most one event can be generated. Let, n be the round-trip communication delay between the system and the steerer. This means that the system can generate a maximum of n events between the generation of an event e and the reception of steering action corresponding to e. We assume that the processing delay of the steerer is negligible compared to this delay. The steering problem can then be decomposed into the following problems: Given communication delay n, current state s 0 of the DES M and the system model M , (i) Predict non-conformance to user defined safety properties along different execution paths originating from s 0 in the partial system model (ii) Generate appropriate steering actions to ensure that the system does not reach violation by restricting the partial model (iii) Determine a steering paradigm for execution of the steering actions by the system Problem (i) can be formulated as a standard runtime verification problem once the partial system model has been generated. Problem (ii) has been addressed in this paper using supervisory control theory for DES. Steering paradigms designed later in the paper provide a solution to problem (iii). The same architecture and paradigms can be used for time varying systems if the partial system model for such systems can be generated at each step.

Steering Architecture for DES
The communication delay between the system and the steerer dictates the minimum amount of look ahead that the steerer must use to ensure that steering actions are transmitted to the system in time. Further, since steering actions are state dependent, each action must be executed by the system at the state for which that action was generated. In this section, we develop a steering architecture for DES which addresses these issues.

Steering Architecture
In response to an event notification, the steerer must generate a partial (n + 1) step DES originating from the current state as shown in Figure 2. n + 1 is the minimum amount of look ahead required to ensure that steering actions are received by the system in time. The states of this DES are known as runtime states and each state uniquely identifies an execution trace in the system. Formally, the runtime DES for a current state s 0 and system model M can be defined as G s 0 = S , R, Σ, s 0 , F, C, T . S is the set of runtime states and R defines a function, mapping runtime states in S to static states S in DES M . s 0 ∈ S is the initial state of G s 0 and Σ is the event set. T : where e ∈ Σ. F ⊂ S is the set of final states of the runtime DES and C ⊂ S is the set of control states defined as C = {s ∈ S |∃e ∈ Σ, f ∈ F, T (s , e) = f }. The steering action for s 0 will disable some of the transitions with source states in C.
In response to a request from the steerer, the runtime verifier finds a set of violating states F such that F ⊆ F . Let, G s 0 be the steered system for the original system G s 0 such that F is not reachable in G s 0 . Some steering paradigms might require that the steerer send activation and deactivation signals to the system for each steering action. These signals occur at points in the execution of the system and the steering action is applicable in the interval  of time between these points. These signals are necessary because there is no synchronization between the system and the steerer and steering actions are associated with specific system states. An activation signal is of the form A, N, Σ d , Σ e where A implies activation and N is the action number. The steerer uses this number(unique for every activation-deactivation pair) when sending the deactivation signal. Σ d is the set of events to be disabled and Σ e is the set of events to be enabled in the system model. The deactivation signal is of the form D, N where D implies deactivation.
The architecture of a DES with a steerer and a runtime verifier is shown in Figure 3. The functions of each of the modules in the architecture is described below.
• System(DES): When an event is generated, the system sends an event notification to the steerer. On receipt of a steering action, the system may either apply the action immediately or store it for future use depending on the steering paradigm employed. The system may also receive activation and deactivation signals from the steerer. When the system receives an activation signal, it executes the accompanying steering action. When it receives a deactivation signal, it deactivates the action corresponding to the action number accompanying the signal.
• Steerer: On receiving an event notification from the system, the steerer generates the partial runtime DES G s 0 . It then sends the set of final states F in G s 0 to the runtime verifier. For each state u ∈ C having transitions to F , the steerer generates the set Σ u d of events that need to be disabled(transitions leading to F ). The steering action for the state s 0 is then given by Similarly, the steerer could also generate a set of enabled events Σ e for C depending on the paradigm. • generating steering actions for G s 0 . This would involve determining the violating states in G s 0 using the runtime verifier and • determining a steering paradigm for the execution of steering actions.
Given system model M , current state s 0 and the steered runtime DES G s 0 from the previous iteration, the steerer can efficiently compute the new runtime DES G s 0 . If e ∈ Σ is the current event received from the system, the steerer updates its runtime state to s 0 = T (s 0 , e) where T is the transition relation in G s 0 . It then computes the states f ∈ F \ F of G s 0 that are reachable from s 0 . G s 0 is now generated by determining the successor states of this reachable set using M .

Control Theory based Steering
The runtime DES G s 0 for which we wish to generate steering actions is a finite state machine. This steering problem can be formulated as a static control problem for DES under partial observation. The partial observation is as a result of the fact that the steerer has limited knowledge of the current state of the system due to communication delay.

Steering of runtime DES as a Static Control Problem
Let, G be the finite DES for which we wish to design a controller and M = L(G) denote the language generated by G.L(G) = {s ∈ Σ * : (∃t ∈ Σ * ) ∧ (st ∈ L(G))} is the prefix closure of L(G). Let, S denote the finite DES(supervisor) we wish to design such that L(S × G) ⊆ L(G) where L(S × G) is the language generated by the supervised system. Σ o ⊆ Σ denotes the set of observable events and Σ u = Σ \ Σ o denotes the set of unobservable events. P is a projection function defined on event strings denoted as P : Σ * −→ Σ * o . Figure 4 shows the architecture for control of finite DES under partial observation. The supervisor S can be defined by a function SC : P (L(S × G)) −→ 2 Σ given by s ∈ L(S × G) ∧ sσ ∈ L(G) ∧ σ ∈ SC(P (s)) ⇒ sσ ∈ L(S × G). Two different strings can be equivalent under partial observation and hence the control actions required for these two strings in order to generate the controlled language must be the same. The observability condition is used to determine whether a controlled language is admissible for a given system under given partial observability. Let, where N ⊆ Σ * . Basically, supP (N ) is given by the set {s|(s ∈ N ) ∧ (All pref ixes of s are in N )}. Let K be any language such that K ⊆ L(G) and K = φ. We wish to decide if we can design a supervised system S generating K(K = L(S × G)) and admissible for M under the projection P . The observability condition given in [2] can be stated as, K is said to be observable with respect to M and P if The observability condition given in [9] can be defined as, K is observable with respect to M and P if and only if supP (P i (K)) ∩ M ⊆K Proof of equivalence of these two observability conditions is given in Appendix A. Steering paradigms described later in the paper will restrain the system model using these observability conditions to ensure correctness of the paradigm. Generation of steering actions for the runtime DES G s 0 can now be formulated as a static control problem under partial observation. G s 0 is the finite DES for which we wish to design a steerer and G s 0 denotes the steered DES. The steering problem can now be stated as, Given G s 0 and the set F ⊆ F of violating states, design G s 0 such that F is not reachable in the controlled system G s 0 . G s 0 and G s 0 must satisfy observability conditions specified in the particular steering paradigm used.

Steering Paradigms
In this section we describe different steering paradigms that can be adopted under the architecture defined in Section 4. Since the steerer and the system have inconsistent views of the current state of the system, the steerer must assist the system in determining the state at which a particular steering action must be executed.

Paradigm 1: Unconstrained System Model(Hashing based Steering)
Steering paradigms under this classification do not impose any restrictions on the system model. Hashing based execution of steering actions is one such paradigm. In this approach, the steerer sends hashed values of event strings(states u in C that have transitions to violating states in F ) and the corresponding set of disabled events(Σ u d ) to the system. The system stores these values in a hash table. When an event occurs, the system generates a new hash value(incrementally) for the event string seen so far and hashes into this table. On a hit, the system activates the steering action associated with that slot. This action can be deactivated on the occurrence of any further event.
We now design a hash function for this paradigm. Let, (k − 1) denote the number of different events in the system model. We will then use a radix-k representation for event strings. Each event e ∈ Σ will be associated with a unique integer i e ∈ (1, k − 1). For every event string es = e 1 e 2 · · · e l where i e 1 , i e 2 , · · · , i e l are the unique integers for events e 1 , e 2 , · · · , e l respectively, its radix-k representation r es = i e l + i e l−1 × k + · · · + i e 1 × k l−1 . Given es and its radix-k representation r es , the radix-k representation of the event string es = es.e l+1 (. represents string append) is r es = i e l+1 + (r es × k).
This representation splits event strings into different ranges of natural numbers depending on string lengths. The hash function we design, will ensure that event strings with different lengths do not hash into the same slot. We split the entire hash table into n regions numbered 0, · · · , (n − 1) each of the same size. Event string es ∈ Σ * will hash into the (|es| mod n) th region in the hash table where |es| denotes the string length. Splitting the hash table into n regions is sufficient because n is the communication delay. When steering action for a string of length 2n is received by the system, the system must have executed the action for strings of length n(steerer generates steering actions for strings of length 2n after the system reaches states corresponding to strings of length n). All strings of length less than n cannot be associated with any steering action and hence will hash into a single slot.
Let, m + 1 be the total size of the hash table where m/n is an integer. The size of each region is m/n and slot 0 will be used to hash all strings of length less than n. The hash function is then given by, h(r es , i) = 0 i ≤ (n − 1) = (r es mod m/n) + ((i mod n)(m/n)) + 1 otherwise The relation between r es and i in the hash function is given by (k i − 1)/(k − 1) ≤ r es ≤ (k i − 1). The average chain length at each slot is α = O(((k − 1) n )n/m) because the maximum number of strings that can hash into a single region is always (k − 1) n (steerer generates steering actions for runtime states in C using G s 0 and has complete knowledge of the execution trace upto s 0 . The length of any event string originating from s 0 and terminating in some state in C is always n).
Splitting the hash table into n regions up front can lead to under utilization of the hash table. The modified hash function which splits the hash table dynamically is given by, h(r es , i, j) = 0 i ≤ (n − 1) = (r es mod m/j) + ((i mod n)(m/j)) + 1 otherwise The steerer will now send the entire hash table to the system every time it generates new steering actions. In practice, violating states are a small subset of the state space and hence the number of entries in the hash table will be small. The steerer also sends the number of regions j into which the hash table is currently split. Advantages This paradigm does not impose any restrictions on the system model. Disadvantages There is an overhead on the system for storing the hash table and for computing the hash function.

System correctness
System correctness depends on the interaction between event strings that participate in a collision in the hash table. A conflict occurs between two colliding strings only when an event disabled by the steering action of one string is required to be enabled in the other. We make a pessimistic assumption that two colliding strings lead to incorrect control when either of them have any steering action associated with them. Let, h denote the number of hash slots in each region of the hash table, p the average number of strings hashing into a region and d the average number of strings that have steering actions associated with them. Let the set of event strings that have steering actions associated be denoted by D. Assuming simple uniform hashing, the probability of collision between any two strings r es1 , r es2 hashing into the same region and having same length i is P rob{h(r es1 , i) = h(r es2 , i)} = 1/h. The probability that the system during its execution generates one of the strings from r es1 and r es2 is P rob{ System generates r es1 ∨ r es2 } = 2/p. Using our assumption, the probability that r es1 and r es2 conflict is given by, Given n is the number of regions in the hash table and P rob{Region f ails} is the probability of failure(colliding and conflicting strings) in one region, the probability that the steered system is correct is, P rob{System correct} = [1 − P rob{Region f ails}] n Now, P rob{Region f ails} = P rob{h(r es1 , i) = h(r es2 , i)} × P rob{ System generates r es1 ∨ r es2 } × P rob{r es1 , r es2 conflict } = 1/h × 2/p × [P rob{r es1 , r es2 conflict |r es1 ∈ D or r es2 ∈ D}× P rob{r es1 ∈ D or r es2 ∈ D}+P rob{r es1 , r es2 conflict |r es1 ∈ D and r es2 ∈ D}× P rob{r es1 ∈ D and r es2 ∈ D}] Therefore, P rob{Region f ails}

Constrained System Model
In this steering paradigm we reduce the steering overhead on the system by constraining the system model. A constrained model will provide opportunities for automated activation and deactivation of steering actions. Let, P n 1 ,n 2 (s) = s.s such that n 1 ≤ |s | ≤ n 2 where s, s ∈ Σ * and |s | denotes length of string s . Also, let G s 0 be the original system, F be the final states of G s 0 and G s 0 be the steered system.

Paradigm 2: Event Trace based Steering
In this approach, the steerer sends the disabled event set Σ d and its observed event trace s 0 to the system. The system compares its own event trace with the trace sent by the steerer and determines the distance to C(states where steering actions must be executed) for that steering action. It stores this distance along with the steering action and decrements the distance at the occurance of each event. When this distance reduces to zero, the corresponding steering action is executed. Deactivation can be done at the occurance of any further event. When the steering action is executed, the system could be in any state in C. To ensure correctness, the system model must satisfy the observability condition given in Section 5.1 whereK = G s 0 , M = G s 0 and all strings in G s 0 are equivalent under projection P . Advantages This paradigm imposes less overhead on the system as compared to hashing.
Disadvantages The system must store its event trace and also update the distance metric for all the stored steering actions at the occurance of every event. The system model is also constrained by the observability condition.

Paradigm 3: Steering with Observability Condition and Minimum Separation
In this paradigm, the system will disable all the events in Σ d as soon as it receives the steering action A, N, E d , E e (N not required). To ensure admissibility of the steering action, the system model must satisfy the observability condition as in paradigm 2. The system will deactivate the steering action as soon as any event in Σ d ∪Σ e occurs. A minimum separation property of events in the model will ensure correctness of this deactivation procedure. Minimum separation is given by, This property ensures that no event in Σ d ∪ Σ e will occur in any of the transitions with source states in S \ (F ∪ C).
Advantages Event traces are not required to be stored by the system in this paradigm. The steering overhead on the system is also minimal.
Disadvantages The steerer is required to send both the event sets Σ d and Σ e . The system model is also severely constrained.

Paradigm 4: Steering with Stringent Observability Condition
In this approach, the system will disable all the events in Σ d as soon as it receives the steering action A, N, Σ d , Σ e (Σ e is empty). When the steerer sends the activation signal, it stores the action number N alongwith the corresponding set of final states F of G s 0 . When the steerer receives an event notification, it checks if the current state matches with any state in F for any action number. If such a match occurs for action number N , the steerer sends the deactivation signal D, N . On receiving a deactivation signal, the system deactivates the steering action specified by the action number. To ensure admissibility of steering actions, the system model must satisfy a modified observability condition given by, s 0 is the steered runtime DES originating from s 0 and having depth 2n + 1. When the system receives the activation signal, it could be in any of the states in S \ F and when it receives the deactivation signal it could be in any state which is at a distance of atmost n steps from some state in F . The modified observability condition ensures that if σ ∈ Σ d , then all the σ transitions in this entire region are disabled.
Advantages This paradigm induces minimal steering overhead on the system. The restriction on the system model is less stringent than in paradigm 3.
Disadvantages The steerer has to send deactivation signals and also needs additional storage for previously sent activation signals.

Illustrative Example
In this section, we apply steering paradigm 4 to an example of a simple subway system [3]. We demonstrate the ability of our architecture to prevent the subway system from entering violations and highlight the constraints that the steering paradigm enforces on the system model.

Simple Subway System
As shown in Figure 5, a subway system consists of stations, junctions, trains and a set of tracks with directions. Each train is represented by its source station, destination station and a route. We assume each track is further divided into 4 sections. This is a good example for dynamic control because the state space grows with the number of trains in the system and this in general can be very large. Safety properties for this subway system may include, (i) Limit on the maximum number of trains at any given time at any junction. For example, let one safety property be "Junction J1 has capacity for only 2 trains at any given time" (ii) Balanced usage of tracks in the system. For example, let the system be constrained by the property that "The difference in loads(number of trains that have used the track) in tracks T6 and T7 must never exceed 4".
We would like to steer the system and prevent it from violating any of these safety properties. We assume that the round-trip communication delay between the steerer and the subway system is n = 1.

Steering of Subway System
Let, α(i, j, k) represent the event that train k enters section j of track i and α(i, 5, k) represent the event that train k left track i and entered a junction or a station. Let for example, the system consist of three trains X, Y and Z. Assume train X executed event α(1, 4, X) and Y executed event α(2, 4, Y ) most recently. Let train Z be currently at junction J1 and let s represent this state of the combined system. At this state, the system can violate safety property 1 in n + 1 = 2 steps(both X and Y decide to enter J1 without train Z leaving it). Hence the steerer, under paradigm 4, will disable events α(1, 5, X) and α(2, 5, Y ) at state s as shown in Figure 6. Train Z could move to section 1 of track T 3 before trains X and Y arrive at junction J1 and this will ensure that property 1 is not violated. But for admissibility of the steering action under paradigm 4, the system must satisfy observability condition specified in section 6.2.3. This condition would require that events α(1, 5, X) and α(2, 5, Y ) be disabled in all states which are at most n + 1 = 2 steps from s as shown in Figure 6. If we use hashing based steering(Paradigm Let, β k represent the event that train k enters track T 7 from S2 and γ k be the event that train k enters track T 7 from J2 . Safety property 2 can now be written as −4 ≤ (|β| + |γ| − |α(6, 1, * )|) ≤ 4 where |e| represents the number of occurrences of event e(ignoring train numbers) in the system execution history. Let, the system currently consist of trains A and B only where train A has executed event α(3, 4, A) most recently and train B is at station S2. Also, let the current value of (|β| + |γ| − |α(6, 1, * )|) be −4. Now, if train A enters track T 6 before train B enters track T 7, safety property 2 will be violated. To prevent this, the steerer will disable event α(6, 1, A) at the current state. The observability condition in section 6.2.3 does not block safe states in this case as shown in Figure 7.

Conclusion and Future Work
In this paper, we have introduced an architecture for steering of DES with large state spaces and also described different steering paradigms for execution of steering actions. Runtime monitors equipped with steerers will be able to predict occurrence of violations well in advance to be able to steer the system away from them. The paper, essentially views the steerer as a dynamic controller that uses the runtime verifier as a sub-module to predict violations. If the violations are restricted to a small subset of the state space, then this architecture will provide efficient steering for DES with large state spaces.
Generation of the partial system model for time varying systems is an important extension for this steering architecture. Extending the steering architecture to models where not all transitions are controllable is also a natural area to explore because in a typical system not all execution points are controllable. Reducing steering overhead by using probabilistic prediction of violations is another direction for further work.

A Equivalence of Observability Conditions
The observability condition given in [2] can be stated as, K is said to be observable with respect to M and P if ∀s ∈K ∧ ∀σ ∈ Σ, (sσ ∈K) ∧ (sσ ∈ M ) ⇒ P −1 [P (s)]σ ∩K = φ (A.1) The observability condition given in [9] can be defined as, K is observable with respect to M and P if and only if supP (P i (K)) ∩ M ⊆K (A.2) We first prove some lemmas which will then be used to prove the equiva- Lemma A.2 sσ ∈ P i (s σ) ⇔ s σ ∈ P i (sσ) Proof. We now prove that sσ ∈ P i (s σ) implies s σ ∈ P i (sσ). From the definition of P i (.), sσ ∈ P i (s σ) ⇒ s ∈ P −1 [P (s )] ⇒ s ∈ P −1 [P (s)] ⇒ s σ ∈ P −1 [P (s)]σ ⇒ s σ ∈ P i (sσ).