A QUANTIFIED MODEL OF SECURITY: A PROGRAMMING LOGIC A--- The predicate model: definitions A1-- Generalised predicates Programs have type G*DIST(L) -> POW(DIST(G*DIST(L))). As usual we investigate the result sets by calculating the least expected output of a random variable ("expectation function"). These expectation functions are the generalised predicates, and examining the result set of a program we deduce that the generalised predicates should suitably be of type G*DIST(L) -> Real . We lift standard ppt predicates A: G*L -> Real by defining the evaluation ev of such a predicate A over a generalised state (G,D) to be ev.A.(g,D) := (+ l . D.l * A.g.l) , where D is a distribution over the state space L. Standard ppt predicates though are insufficient to make the distinction between external and internal semantics. We introduce a new operator, SM (for "supermin") as follows: for standard predicates A,B define A SM B by ev.(A SM B).(g,D) := ev.A.(g,D) MIN ev.B.(g,D) . Notice that this takes the minimum -after- integration over D (that is, summation as above when the state space is finite), whereas the normal MIN operator of ppt first minimises statewise over the functions A and B and -afterwards- applies the integration. The expressions involving SM are generated (as we shall see) when external nondeterministic choice is present in the program. The generalised predicates that seem to be sufficient in this context are the standard ppt predicates closed under addition, scalar multiplication and taking SM's. Addition and scalar multiplication are defined as follows for generalised predicates: ev.(p*(A SM B) + C).(g,D) := p*(ev.A.(g,D) MIN ev.B.(g,D)) + ev.C.(g,D) . A2-- Testing Programs We investigate the result set of a program executed from a (generalised) initial state (g,D). As usual for a (generalised) predicate, post, we calculate the weighted average with respect to each possible output distribution and select the minimum value, representing the "worst case" expected value. Doing that for each possible initial (g,D) generates the precondition. In detail the calculations for a single output distribution are made as follows: first the postcondition is averaged individually over each row of a result distribution (see matrix below); then the results for each row are weighted according to the "external" row distribution; finally those results are summed. When the postcondition is -standard- this is equivalent to converting the distributions of type DIST(G*DIST(L)) to the usual "flattened" form of type DIST(G*L) and integrating as usual. For example, consider a "result" function F:DIST(G*DIST(L)) summarised by the matrix: (l=0) (l=1) (g=0) 0.5 0.5 @ 0.25 (g=0) 0.25 0.75 @ 0.25 (g=1) 0.4 0.6 @ 0.5 When used to test against a -standard- ppt postcondition, form the usual joint distribution over G*L obtained by combining the conditional distributions. Note (below) how the rows (g=0) are amalgamated --- thus testing against standard postconditions ignores the difference between internal and external probabilistic choice. The "flattened" joint distribution becomes: (l=0) (l=1) (g=0) 0.19 0.32 (g=1) 0.2 0.3 A postcondition involving SMs requires a different kind of calculation: it represents a set of standard postconditions, each of which must be integrated against the full output distributions and the minimum value taken. Define for example A := [g=0 AND l=1] + [g=1 AND l=0] B := [g=0 AND l=0] + [g=1 AND l=1] Then A SM B represents the set of standard postconditions { [g=0 AND l=1] + [g=1 AND l=0], [g=0 AND l=0] + [g=1 AND l=1], [g=0 AND l=1] + [g=1 AND l=1], [g=0 AND l=0] + [g=1 AND l=0] } . The new functions C belonging to the resulting set are those that satisfy C[g:=g'] equals A[g:=g'] or B[g:=g'] , for each value g' of the global variable. For the matrix above we must calculate the minimum expected output along each row of the matrix separately for each standard postcondition in the set. For example for the first row the expected return for each of the four standard postconditions is the same (value 0.5). For the second and third rows the minimum occurs at [g=0 AND l=0] + [g=1 AND l=1] for row 2 (value 0.25) [g=0 AND l=0] + [g=1 AND l=0] for row 1 (value 0.4). Thus the total -least- expectation is the weighted sum: 0.5*0.25 + 0.25*0.25 + 0.4*0.5 . SMs arise because of external nondeterministic choice which cannot take advantage of the -actual- value of the internal variables, but only its current distribution. Each possible resolution of an external nondeterministic choice generates a precondition to be handed on to the rest of the program, thus each possible precondition must be retained until the distribution over the internal variables is revealed. For example the external assignment g:=0 [] g:=1 applied to the postcondition [g=l] generates two preconditions [0=l] and [1=l] --- one for each possible resolution of the choice. Given an initial assigment l:=0 {1/4} l:=1 (since the external demon has no -absolute- knowledge of l but only of its distribution) both predicates must be averaged over l's distribution separately producing 1/4 , 3/4 respectively. The external demon, only knowing the initial l-distribution, would seek to minimise the expectation and therefore choose the left branch. [ Aside --- an internal demon would have complete knowledge of l and be able to avoid l every time. On application of wp.(g:=0 {} g:=1) to the postcondition [g=l] the preconditions [0=l] and [1=l] are combined with MIN and the expression reduces to zero immediately. ] A3-- Predicate transformer semantics We need three operators: wp, iwp, ewp which repectively denote weakest precondition, internal weakest precondition and external weakest precondition dealt with separately below. For a complete program, prog, we will always be interested in calculating ewp.prog.post for some postcondition post. We will need (see below) to alternate between iwp and ewp in the case of calculating preconditions for module calls. We denote an explicit call to an internal operation by CALL, and when this occurs within a program fragment then internal semantics is used. Thus ewp.(CALL prog) := iwp.prog. The five basic rules for reducing expressions are as follows: (1) Standard wp applies for standard postconditions and deterministic programs. (2) For a deterministic program prog, iwp.prog.(SM x. post) := (+g':G . (SM x. wp.prog.(post AND [g=g'])) . (3) Internal nondeterministic choice is converted to an an external nondeterministic choice: ewp.(CALL ({}x. prog(x))) := ewp.([]f:L->X. CALL prog(f.l)) . (4) External probabilistic choice: ewp.(prog [p] prog').post := p*(ewp.prog.post) + ~p*(ewp.prog'.post) . (5) External nondeterministic choice: ewp.([]x. prog).post := (SM x. ewp.prog.post) . B--- The predicate model: Simplifying calculations The following results are all designed to reduce the complexity of the expressions. Expressions become complicated when external nondeterminism and internal probabilistic choice interact, as for example expressions involving SM are generated by an external nondeterministic choice, and they can only be reduced later when the internal distribution is declared. Knowing when it is possible to remove the SMs from an expression is a useful technique. The following lemmas describe some rules for simplification. Lemma 1 If for all values g', ===== wp.prog.(post MIN [g=g']) = (wp.prog.post) MIN [g=g'] for any standard postcondition and some deterministic prog then for that prog iwp.prog.(SM x.post) = (SM x. wp.prog.post) . This says that if prog does not assign to g (but may read from it) then Rule 2 may be simplified by not referring to g explicitly. Intuitively one reasons that since only the local variables are changed, and there is no nondeterminism the global variables cannot pass any information outside the module. Proof iwp.prog.(SM x.post) = "Rule 2" (+g'. (SM x. wp.prog.(post MIN [g=g']))) = "hypothesis" (+g'. (SM x. (wp.prog.post) MIN [g=g'])) = "(A MIN [g=g']) SM (B MIN [g=g']) = (A SM B) MIN [g=g']" (+g'. (SM x. wp.prog.post) MIN [g=g']) = (SM x. wp.prog.post) . @@@ Lemma 2 If there is some function f, depending only on the deterministic ===== program prog (and not on the incoming l-distribution), such that for all post, g' wp.prog.(post MIN [g=g']) = [g'=f.g] MIN wp.prog.post then iwp.prog.(SM x.post) = (SM x. wp.prog.post) . This says that if the program can assign to g, but only to a single value then Rule 2 simplifies --- since the output value of g is always the same that information cannot be used to deduce more information about the local variables. Proof iwp.prog.(SM x. post) = "Rule 2" (+g'. (SM x. wp.prog.(post MIN [g=g']))) = "hypothesis" (+g'. (SM x. [g'= f.g] MIN wp.prog.post)) = (+g'.(SM x. wp.prog.post) MIN [g'=f.g]) = "f a function, independent of l, obvious?" (SM x. wp.prog.post) . @@@ Note that Lemma 1 is a special case of Lemma 2, when f is the identity. In fact Rule 2 simplifies even for nondeterministic programs. Lemma 3 If either of the conditions of Lemmas 1,2 hold then ===== iwp.({}y. prog) .(SM x.post) = (SM x. wp.([]y.prog)). Proof We present only the calculation for a binary choice. So let prog, prog' be deterministic programs so that for -any- boolean function, f:L -> B prog prog' satisfies the conditions for Lemma 2. We now reason as follows: iwp.(prog {} prog').(SM x. post) = "Rule 3, Rule 5" (SM f:L->B .iwp.(prog prog').(SM x. post)) = "hypothesis, Lemma 2" (SM f:L->B. (SM x. iwp.(prog prog').post)) = "swap SM" (SM x. (SM f:L->B .iwp.(prog prog').post)) = "nondet lemma, see below" (SM x. wp.prog.post MIN wp.prog'.post) = (SM x. wp.(prog {} prog').post) . The nondet lemma is stated as follows: for any type T and predicate pre --- without SM --- referring to f only in the form f.l, we have (SM f:L->T . pre(f.l)) = (MIN t:T. pre(t)) . @@@ Any deterministic probabilistic assignment that only changes global variables can be made externally or internally --- the intuition here is that probabilistic choice is not influenced by demons, be they internal or external, and if the local variables remain unchanged no extra information is passed to the outside. The next lemma is the simplest instance of this, though the result is more generally true. Lemma 4 For global variable, g we have ===== g:=0 {p} g:=1 = g:=0 [p] g:=1 Proof iwp.(g:=0 {p} g:=1).(SM x. post) = "Rule 2" (SM x. wp.(g:=0 {p} g:=1).(post MIN [g=0])) + (SM x. wp.(g:=0 {p} g:=1).(post MIN [g=1])) = "standard ppt" (SM x. p*post[g:=0]) + (SM x. ~p*post[g:=1]) = p*(SM x. post[g:=0]) + ~p*(SM x. post[g:=1]) = "Rule 4" ewp.(g:=0 [p] g:=1). (SM x. post) . @@@ Knowing when standard (ppt) reasoning can be used will be a useful technique. Clearly if one knows in advance that no expression containing SM will be generated then standard reasoning can be used throughout. Two obvious situations are (A) when all the operations are internal, (B) when there is no external nondeterministic choice. But the problem really occurs when internal probabilistic choice and external nondeterministic choice are present; thus if the internal variables are never assigned to probabilistically then, once again, standard reasoning alone should apply. For deterministic programs the result is again intutitively clear: if the internal state is always a point distribution then the external demon knows all there is to know. The condition in Lemma 5 captures the property that the behaviour of the internal variables is nonprobabilistic. Lemma 5 For deterministic prog, if wp.prog.[l=l'] is 0 or 1 then ===== iwp.prog.(SM x. post) = wp.prog.(MIN x. post) . Proof iwp.prog.(SM x. post) = "Rule 2" (+g'. (SM x. wp.prog.(post MIN [g=g']))) = "prog is deterministic" (+g'. (SM x. (+l'. wp.prog.(post MIN [g=g'] MIN [l=l'])))) = "see below" (+g'.(+l'.(SM x. wp.prog.(post MIN [g=g'] MIN [l=l'])))) = "swap +" (+l'.(+g'.(SM x. wp.prog.(post MIN [g=g'] MIN [l=l'])))) = "Rule 2" (+l'. iwp.prog.(SM x. (post MIN [l=l']) = "post MIN [l=l'] nonzero for single value of l" (+l'. iwp.prog.(MIN x. (post MIN [l=l']) = "prog deterministic, Rule 1" wp.prog.(MIN x. post) . For the "see below" step we reason as follows: (SM x. (+l'. wp.prog.(post MIN [g=g'] MIN [l=l']))) = "[l=l'] nonprobabilistic" (SM x. (+l'. wp.prog.(post MIN [g=g'] & [l=l']))) = "prog deterministic, wp.prog is linear and terminating" (SM x. (+l'. wp.prog.(post MIN [g=g']) & wp.prog.[l=l'])) = "hypothesis" (SM x. (+l'. wp.prog.(post MIN [g=g']) MIN wp.prog.[l=l'])) = "prog deterministic, hypothesis" (+l'.(SM x. wp.prog.(post MIN [g=g'])) MIN wp.prog.[l=l']) . @@@ Lemma 5 also holds for nondeterministic programs. Lemma 6 If prog, prog' satisfy the hypotheses for Lemma 5 then ===== iwp.(prog {} prog').(SM x. post) = iwp.(prog {} prog').(MIN x. post) . Proof Apply Rule 3 to convert the program into an external choice over deterministic programs progprog', where f is a boolean valued function. Now note that wp.(prog prog').[l=l'] is either 0 or 1 if wp.prog.[l=l'] and wp.prog'.[l=l']. The result now follows from Lemma 5. @@@ C--- The predicate model: examples We rework the examples set out in the relational model, this time using the logic. C1-- -Internal- prob is -not- detectable by external nondet. For the program CALL l:= (0 {p} 1); g:= (0 [] 1) we calculate for the postcondition [l<>g] [l<>g] = "apply ewp.(g:= (0 [] 1)), Rule 5" ewp.(g:= 0).[l<>g] SM ewp.(g:= 1).[l<>g] = "standard ppt, global assignments" [l<>0] SM [l<>1] = "apply ewp.(CALL l:=0 {p} l:=1), following Lemma 1" wp.(l:= (0 {p} 1)).[l<>0] SM wp.(l:= (0 {p} 1)).[l<>1] = "apply wp.(l:= (0 {p} 1)) twice" ~p SM p = "SM reduces to MIN if l not mentioned" ~p MIN p . The interpretation is that g can guess l with probability at least p MAX ~p. C2-- -External- prob -is- detectable by external nondet For the program CALL l:= 0 [p] CALL l:= 1; g:= (0 [] 1) , again we test with the postcondition [l<>g]: [l<>g] = "apply ewp.(g:= (0 [] 1)) [l<>0] SM [l<>1] = "apply ewp.(CALL l:= 0 [p] CALL l:= 1), Rule 4" p*(ewp.(CALL l:= 0).([l<>0] SM [l<>1]) + ~p*(ewp.(CALL l:= 1).([l<>0] SM [l<>1]) = "lemma 1 twice" p*([0<>0] SM [0<>1]) + ~p*([1<>0] SM [1<>1]) = "arithmetic" p*0 + ~p*0 = 0 . Thus the probability is 0 in this case: the interpretation is that g can guess l with probability at least 1. C3-- Mixture of internal and external prob Consider the program CALL l:= (0{p}1) [q] CALL l:= (0{r}1); g:= (0[]1) . As usual we calculate [g<>l] = "apply ewp.(g:= (0[]1))" [0<>l] SM [1<>l] = "apply ewp.(CALL l:= (0{p}1) [q] CALL l:= (0{r}1)), Rule 4" q*(iwp.(l:= (0{p}1)).([0<>l] SM [1<>l])) + ~q*(iwp.(l:= (0{r}1)).([0<>l] SM [1<>l])) = "Lemma 1 twice" (~p MIN p) [q] (~r MIN r) . C4-- Internal versus external nondet: sometimes equal. We show that the two programs l:= (0 {} 1) and CALL l:= 0 [] CALL l:= 1 give the same result on all postconditions. Thus consider a general postcondition over l and g, and let B be the Boolean type. We have iwp.(l:= (0 {} 1).(SM x. post) = "Rule 3" ewp.([]f: L->B . CALL l:=0 < f.l > l:=1).(SM x. post) = "Rule 5" (SM f: L->B . iwp.(l:=0 < f.l > l:=1).(SM x. post)) = "Lemma 1" (SM f: L->B . (SM x. post[l:=0] < f.l > post[l:=1])) = "Swap SM's; nondet lemma" (SM x. (MIN b:B. post[l:= 0] post[l:= 1])) = (SM x. post[l:= 0] MIN post[l:= 1]) = "post[l:= ?] contains no l" = (SM x. post[l:= 0] SM post[l:= 1]) = (SM x. post[l:= 0]) SM (SM x. post[l:= 1]) = "Rule 5; Lemma 1" ewp.(CALL l:= 0 [] CALL l:= 1).(SM x. post) . [ Aside --- this calculation shows that the logic cannot distinguish between the two programs, and thus provides one reason for including the internal convex closure described in the relational section. ] C5-- Internal versus external nondet: sometimes not equal. We repeat C4 but this time we allow predicates to be expressions over g,l and a new local variable, m. This time internal choice can be distinguished from external. Let post be [l<>m], and calculate: iwp.(l:= (0 {} 1)).[l<>m] = (SM f: L*M->B . [l<>m][l:=0] [l<>m][l:=1]) = (SM f: L*M->B . [0<>m] [1<>m]) <= "assume M={0,1}; take f.l.m := (m=0)" = 0 . For external choice however we have ewp.(l:= (0 [] 1)).[l<>m] = ewp.(CALL l:=0).[l<>m] SM ewp.(CALL l:=1).[l<>m] = [m<>0] SM [m<>1] = "again assume M={0,1}" [m=1] SM [m=0] , and evaluating that expression at an initial m-valued distribution m:=0 {1/2} m:=1 gives for example 1/2, not 0. C6-- Case analysis over global variables is essential This example illustrates why we need to introduce an explicit global variable in Rule 2, even when the postcondition does not refer explicitly to the global variables. Consider the program CALL (l:=0 {0.5} l:=1); CALL g:=l; h:= (0[]1) where (as usual) l is a local variable and g and h are global. Here we have a variable h which tries to guess the local variable l. That should be possible every time: the preceeding statement assigns to g exactly the value of l, which can then be seen externally. As before we calculate for the postcondition [h<>l] [h<>l] = "apply ewp.(h:= (0[]1))" [0<>l] SM [1<>l] = "apply ewp.(CALL g:=l)" ... In the standard ppt logic, since the post condition contains no explicit reference to g, and the statement g:=l would leave all variables but g unchanged, application of wp.(g:=l) has no effect on the postconditon. With that incorrect use of Rule 2, we would then continue the reasoning ... [0<>l] SM [1<>l] = "apply ewp.(CALL (l:=0 {0.5} l:=1))" 0.5 , which says that the variable h can guess l (and avoid it) only half the time. This is obviously not the intended meaning since g (a global variable) copies l exactly, making that information available to an external demon. The calculation has failed to introduce the dependence of l's distribution on the value of g. Continuing now with the correct application of Rule 2 instead, we have ... (+h',g' . wp.(g:= l).[0<>l AND g=g' AND h=h'] SM wp.(g:= l).[1<>l AND g=g' AND h=h']) = "apply wp.(g:= l); one-point rule for h'" (+g' . [0<>l AND l=g'] SM [1<>l AND l=g']) = "nonzero values occur only for 0<>g' AND 1<>g'" [0<>l AND 1<>l] = "apply ewp.(CALL (l:=0 {0.5} l:=1))" = 0 . C7-- The `spy' example. Consider the structure VAR g: G; h: L; MODULE Secure VAR l: L; PROC Secrets == l:@ D --- Set l according to distribution D PROC Spy == g:< G --- Choose g internally nondet from G END Secure; Secret; Spy; h:< L --- Choose h externally nondet from L, trying to guess l Module Secure contains a secret l that is set probabilistically by operation Secrets, representing the overall effect of `secret' activity inside the module. Variable l is not externally observable. Operation Spy uses external variable g to pass out information about l; it does so by making an internal nondeterministic choice from an arbitrary set G. (Clearly the size of the otherwise arbitrary set G is related to the amount of information the spy can disclose.) The externally nondeterministic h:< L --- the enemy --- tries to guess the value of l, using (implicitly) the information in g passed out by the spy. Success for the spy and the enemy depends on their coming to an arrangement beforehand on the use of their respective nondeterministic choices. To discover the (maximum) probability of a successful guess we use postcondition [h<>l] --- we want the spy/enemy to -fail- to guess l, and so set that as a postcondition --- and calculate as follows: [h<>l] = "apply ewp.(h:< L)" (SM l':L . [l'<>l]) = "apply iwp.(g:< G)" (SM f:L->G. (+g':G. (SM l':L. wp.(g:= f.l).[l'<>l AND g'=g]))) = "wp of assignment" (1) (SM f:L->G. (+g':G. (SM l':L . [l'<>l AND g'=f.l]))) = "distribute inner SM through +" (SM f:L->G. (SM n:G->L. (+g':G . [n.g'<>l AND g'=f.l]))) = "commute SM's" (SM n:G->L. (SM f:L->G. (+g':G . [n.g'<>l AND g'=f.l]))) = "nondet lemma: see below" (SM n:G->L. (MIN g'':G. (+g':G . [n.g'<>l AND g'=g'']))) = "one-point rule" (SM n:G->L. (MIN g'':G . [n.g''<>l])) = "collapse MIN" (SM n:G->L . [l NOTIN n.G]) = "introduce L' to replace n.G" (SM L': POW(L) | #L'<=#G . [l NOTIN L']) = "assume #G<=#L; exploit taking of minima" (SM L': POW(L) | #L'=#G . [l NOTIN L']) . (2) The deferred "nondet lemma" is that for any type T and predicate pre --- without SM --- referring to f only in the form f.l, we have (SM f:L->T . pre(f.l)) = (MIN t:T. pre(t)) . That lemma seems to be an important way of simplifying SM expressions to those involving just MIN instead. To conclude, we go one step further from (2), using the lemma iwp.(l:@ D) = ev.D , so that the overall precondition becomes iwp.(l:@ D).(2) = "above" ev.D.(2) = ev.D.(SM L': POW(L) | #L'=#G . [l NOTIN L']) , thus simply the evaluation of (2) over the distribution D. With a bit of thought (?) that leads us to conclude that the probability of establishing [h<>l] --- the least guaranteed probability of the spy's -failing- to guess the secret --- is the sum of all but the #G greatest probabilities in the (known) distribution D over the (unknown) internal l. Thus the probability of the spy's -succeeding- to guess the secret is the complement of that: the sum of the #G greatest probabilities in D. If D is uniform --- with each probability 1/#L --- that reduces to just (#G/#L) MIN 1 , where the MIN 1 simply handles the situation in which #G>#L. As special cases, note that when #G=1 the spy can pass out no information, and so the probability of a correct guess is 1/#L --- no better than an oblivious guess; when #G=#L the spy can pass out the exact value of l, and the probability is then 1. (What happens when #G=0? Then the statement g:< G is miraculous, and cannot execute --- and neither can its successor h:< L, giving that the probability is then 0 because the guess can't even be made.) [ Aside --- If we return to (1) and strip off the outer quantification over f, we get (+g':G . (SM l':L . [l'<>l AND g'=f.l])) , in which f is now free. That as a precondition gives the probability of the enemy's failing to guess l when the spy's policy is given -explicitly- as a function f (and with our growing familiarity with these idioms that precondition can almost be written down directly). The operation becomes PROC Spy == g:< f.l --- Communicate -something- about l . Compare the even/odd example C8 below, in which f is given explicitly as (DIV 2). Returning now to our current example, we see that the minimisation over f in (1) is effectively a minimising over all possible `revelation' functions that the two demons might have agreed beforehand. ] C8-- The `even/odd' example Consider the structure VAR g: [0,N); --- integers from 0 inc. to N exc. h: [0,2N); MODULE Secure VAR l: [0,2N); PROC Traitor == --- Details below PROC Spy == g:= l DIV 2 --- Choose g internally nondet from G END Secure; Traitor; Spy; h:< [0,2n) --- Choose h externally nondet, trying to guess l Note that it contains no probabilistic statements (and that hence this is in part a `pure' security example). Module Secure contains a secret l that is almost entirely exposed by Spy --- only one bit remains hidden. On the basis of the exposure (into g), the external h then tries to guess the value of l. For the moment the behaviour of Traitor is unspecified. To evaluate h's chance of successful guessing, we calculate as usual from the postcondition that the guess is -wrong- : [h<>l] = "apply ewp.(h:< L)" (SM l':[0,2N) . [l'<>l]) = "apply iwp.(g:= l DIV 2)" (+g':[0,N). (SM l':[0,2N). wp.(g:= l DIV 2).[l'<>l AND g=g'])) = "wp of assignment" (+g':[0,N). (SM l':[0,2N). [l'<>l AND (l DIV 2)=g'])) = "specialise to just the two effective l' values" (+g':[0,N). [2g'<>l AND (l DIV 2)=g'] SM [2g'+1<>l AND (l DIV 2)=g']) = (+g':[0,N) . [l=2g'+1] SM [l=2g']) , (1) from which we can see that if the incoming distribution is L, say, a function from the integers [0,2N) into the probabilities [0,1], then the probability of establishing [h<>l] is L.0 MIN L.1 + L.2 MIN L.3 +...+ L.(2N-2) MIN L.(2N-1) . Clearly, therefore, if the incoming distribution is uniform (L.k = 1/2N) then the probability is 1/2 --- just the probability of choosing the missing low-order bit at random. Suppose now that a Traitor is inserted into the module who can ensure that l is even --- we specify that by writing ewp.Traitor.[odd l] = 0 , which does not however require any particular -distribution- of the l values among the even integers in [0,2n). [ Aside --- To use the more straightforward specification ewp.Traitor.[even l] = 1 would in fact be saying too much: it says that the traitor -must- make l even "every time". The specification we gave says instead that the traitor -can- ensure that l is even "if/when he wants to", and is weaker. Pursuing the metaphor, that freedom allows the traitor to permit odd values of l on occasion, when perhaps he is under suspicion. ] To analyse the new situation we carry on from (1) above, noting (1) <= "drop a SM term" (+g':[0,N) . [l=2g'+1]) = [odd l] , so that we can reason overall (2) ewp.(Traitor; Spy; h:< [0,2N)).[h<>l] = "sequential composition" ewp.Traitor.(ewp.(Spy; h:< [0,2N)).[h<>l]) <= "above, and monotonicity of ewp.Traitor" ewp.Traitor.[odd l] = "specification of Traitor" 0 , so that in fact ewp.(Traitor; Spy; h:< [0,2N)).[h<>l] = 0 . The conclusion is that if the traitor -can- ensure that the secret l is even, then we must assume (with probability 1-0 = 1) that the secret can be completely compromised. Note that the looseness of the traitor's specification is important --- given his situation there may be many other constraints he must satisfy at the same time. Finally, consider a traitor who can ensure only that l has probability 2/3 of being even --- he can `bias' its parity, but not completely control it. Again we specify that `backwards' by ewp.Traitor.[odd l] <= 1 - 2/3 = 1/3 , and the reasoning at (2) would become (only the last step changes) ewp.(Traitor; Spy; h:< [0,2N)).[h<>l] = "sequential composition" ewp.Traitor.(ewp.(Spy; h:< [0,2N)).[h<>l]) <= "above, and monotonicity of ewp.Traitor" ewp.Traitor.[odd l] <= "specification of Traitor" 1/3 , so that overall ewp.(Traitor; Spy; h:< [0,2N)).[h<>l] <= 1/3 . We conclude that the likelihood of the secret's being kept is no more than 1/3 --- it has thus probability (at least) 2/3 of being revealed. The analysis would be the same for any bias --- not just 2/3 --- and would apply whether that bias were towards even or towards odd. [ Aside --- Concluding on the basis of the example that the secret is revealed with probability "the maximum of the even/odd biases" is tempting, but incorrect: since g's value is known at the point the guess is made (at the point h is chosen), there is more information available than simply the overall bias. It might be for that particular g value that the bias is particularly high, for example. Nevertheless we can return to (1) and reason (+g':[0,N) . [l=2g'+1] SM [l=2g']) (1) <= "super-distribute SM through +" (+g':[0,N) . [l=2g'+1]) SM (+g':[0,N) . [l=2g']) = [odd l] SM [even l] , which is the -minimum- of the two biases --- thus the probability of h's guessing incorrectly is -no more- than the lesser bias. The probability of h's guessing correctly is thus shown to be -no less- than the greater of the two biases. But (as we saw above), unless the bias is uniform the probability of l's being guessed is probably greater still, since h can use g's actual value to inform its guess on each occasion. ]