Difference between revisions of "BGV"
(27 intermediate revisions by the same user not shown) | |||
Line 6: | Line 6: | ||
Until recently, the BGV scheme was considered to be the most efficient homomorphic encryption scheme when performing the same operations on multiple ciphertexts at once. | Until recently, the BGV scheme was considered to be the most efficient homomorphic encryption scheme when performing the same operations on multiple ciphertexts at once. | ||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
== Leveled Fully Homomorphic Encryption == | == Leveled Fully Homomorphic Encryption == | ||
Line 29: | Line 21: | ||
Let <math>\lambda </math> be a security parameter, representing <math> 2^{\lambda}</math> security against known attacks. | Let <math>\lambda </math> be a security parameter, representing <math> 2^{\lambda}</math> security against known attacks. | ||
− | Let <math>R | + | Let <math>R </math> be a ring. For any integer <math>q </math>, we write <math>R_q </math> for the quotient <math>R/qR </math>. |
Let <math> q=q(\lambda) </math> be an odd modulus and <math>\chi = \chi(\lambda) </math> a ``noise" distribution over <math> R</math>. Let <math>N=N(\lambda)</math> be an additional parameter of the system which is larger than <math>3 \cdot \log{q} </math>. | Let <math> q=q(\lambda) </math> be an odd modulus and <math>\chi = \chi(\lambda) </math> a ``noise" distribution over <math> R</math>. Let <math>N=N(\lambda)</math> be an additional parameter of the system which is larger than <math>3 \cdot \log{q} </math>. | ||
Let us assume that the plaintext is <math>R_2 = R/2R </math>. | Let us assume that the plaintext is <math>R_2 = R/2R </math>. | ||
+ | |||
+ | * E.Setup(<math>1^{\lambda}, 1^{\mu} </math>): Choose a <math> \mu</math>-bit modulus <math> q </math> and choose the other parameters <math>d= d(\lambda, \mu) </math>, and <math>N = \lceil 3 \log q \rceil </math>, <math>\chi(\lambda, \mu) </math> appropriately to ensure that the scheme is based on a Ring-LWE instance that achieves <math> 2^{\lambda}</math> security against known attacks. Let <math>R= \mathbb Z[X]/(x^{d}+1) </math> and let params = <math>(q, d, N, \chi) </math>. | ||
+ | |||
+ | * E.SecretKetGen(params): Draw <math>s' \leftarrow \chi</math>. Set <math>sk=s \leftarrow (1,s') \in R_{q}^2</math>. | ||
+ | |||
+ | * E.PublicKeyGen(params, sk): Recall that the secret key is <math>sk=s=(1,s') </math>. This algorithm generates a (column) vector <math>A' \leftarrow R_q^{N} </math>, uniformly and a vector <math>e \leftarrow \chi^N </math>. The algorithm computes | ||
+ | <math>b = A's' + 2 e </math>. Then, set <math>A</math> to be the <math>N \times 2</math> matrix obtained by setting <math>b</math> on the first column followed by the entries of <math>-A'</math>. We remark that <math>A \cdot s = 2e </math>. The algorithm outputs the public key <math>pk=A</math>. | ||
+ | |||
+ | * E.Enc(params, pk,m): To encrypt a message <math>m \in R_2 = R/2R </math>, set <math> m \leftarrow (m,0) \in R_q^2 </math>, sample <math>r \leftarrow R_2^N </math> uniformly and output the ciphertext <math>c \leftarrow m+A^T \cdot r \in R_q^2 </math>. | ||
+ | |||
+ | * E.Dec(params, sk, c): Output <math>m \leftarrow [[<c,s>]_q]_2 </math>. Where <math> [\cdot]_q</math> denotes reduction into the range <math>(- q/2,q/2] </math>. | ||
+ | |||
+ | Correctness is easy to verify, whereas we refer to the paper for details upon security. | ||
+ | |||
+ | == Key switching (Dimension reduction)== | ||
+ | |||
+ | Recall that in the above scheme, the decryption equation for a ciphertext <math> c </math> that encrypts a message <math> m </math> under the secret key <math> s</math> can be written as | ||
+ | <math>m = E.Dec(params, s,c) = [[L_{c}(s)]_q]_2,</math> where <math>L_c </math> is a linear operator which depends on <math>c </math>. To be precise, the latter is just the inner product <math>L_c(s) = <c,s> </math> between two vectors in <math>R_q^2</math>. | ||
+ | |||
+ | To understand the key switching procedures, we have to (at least briefly) describe the following subroutines first: | ||
+ | |||
+ | * BitDecomp(<math>x \in R_q^n,q </math>): decomposes <math>x </math> into its bit representation, namely <math>x= \sum_{j=0}^{\lfloor \log q \rfloor} 2^j u_j,</math> where all of the <math>u_j \in R_2^n </math>. The procedure outputs the vector | ||
+ | |||
+ | <center><math> (u_0, u_1, \dots, u_{\lfloor \log q \rfloor}) \in R_2^{n\cdot \lceil \log q \rceil} </math> </center> | ||
+ | |||
+ | * Powersof2(<math>x \in R_q^n,q</math>): outputs the vector | ||
+ | |||
+ | <center><math>(x, 2 \cdot x, \dots, 2^{\lfloor \log q \rfloor} \cdot x) \in R_q^{n \cdot \lceil \log q \rceil}.</math></center> | ||
+ | |||
+ | It is easy to see that for vectors <math>c,s </math> of the same length <math> n</math>, we have: | ||
+ | |||
+ | <center><math> <BitDecomp(c,q), Powersof2(s,q)> = <c,s> \pmod{q} </math>.</center> | ||
+ | |||
+ | Now, key switching consists of two procedures: | ||
+ | |||
+ | * SwitchKeyGen(<math>s_1 \in R_q^{n_1}, s_2 \in R_q^{n_2} </math>): | ||
+ | |||
+ | ** Run <math>A \leftarrow E.PublicKeyGen(s_2,N)</math> for <math>N = n_1 \cdot \lceil \log q \rceil</math>. | ||
+ | |||
+ | ** Set <math>B \leftarrow A+ Powersof2(s_1)</math> (Add Powersof2(<math>s_1 </math>)), which is an element of <math>R_q^N </math> to <math>A</math>'s first column. Output <math> \tau_{s_1 \to s_2} = B</math>. | ||
+ | |||
+ | * SwitchKey(<math>\tau_{s_1 \to s_2}, c_1 </math>): Output <math>c_2 = BitDecomp(c_1)^T \cdot B \in R_q^{n_2}</math>. | ||
+ | |||
+ | Note that, in SwitchKeyGen, the matrix <math>A</math> consists of encryptions of <math> 0</math> under the key <math> s_2</math>. Then, pieces of the key <math> s_1 </math> are added to these encryptions of <math> 0 </math>. Thus, in some sense, the matrix <math> B </math> consists of encryptions of pieces of <math> s_1</math> (in a certain format) under the key <math>s_2 </math>. | ||
+ | |||
+ | The authors establish the following correctness result (See Lemma 3 in the paper): | ||
+ | |||
+ | <center><math> [[<c_2,s_2>]_{q}]_2 = [[<c_1,s_1>]_q]_2 </math> </center> | ||
+ | |||
+ | <math>c_2 </math> is a valid encryption of <math> m</math> under the key <math> s_2 </math>, and one can see that the noise of <math>c_2 </math> is larger by a small additive factor. | ||
+ | |||
+ | == Modulus switching == | ||
+ | |||
+ | |||
+ | If <math>c</math> is a valid encryption of <math> m</math> under the key <math> s </math>, and <math>s</math> is (what the authors call) a ``short vector" and <math>c' </math> is a simple scaling of <math> c </math>, i.e. <math>c' </math> is the <math> R</math>-vector closest to <math>(p/q) \cdot c </math> under the additional constraint that | ||
+ | <center><math>c' = c \pmod 2 </math>,</center> | ||
+ | it turns out that (under some conditions) the vector <math>c' </math> is a valid encryption of <math>m </math>, under the secret key <math>s </math> using the modulus <math> p</math>. | ||
+ | |||
+ | In other words, under some conditions, one can change the modulus <math> q </math> in the decryption equation to another (maybe smaller) modulus <math> p</math>, while preserving the correctness of decryption under the same secret key <math> s</math>. | ||
+ | |||
+ | For an integer vector <math> x </math> and integers <math>q>p>m </math>, the authors define | ||
+ | <center><math> x' \leftarrow \mathrm{Scale}(x,q,p,r) </math> </center> | ||
+ | to be the <math>R</math>-vector closest to <math>(p/q) \cdot x </math> which satisfies <math>x' = x \pmod r.</math> | ||
+ | |||
+ | For the details concerning the conditions on <math>p,q </math> and the vector <math> s</math> required for the preservation of decryption correctness, we refer to Lemma 4 and its Corollary 1 in [1]. | ||
+ | |||
+ | The aforementioned results assert that assuming <math>p </math> is smaller than <math> q </math> and <math> s </math> has coefficients that are small in relation to <math> q </math> , this ``modulus swithcing" procedure | ||
+ | permits the evaluator to reduce the magnitude of the noise without knowing the secret key. The evaluator only has to know a bound on <math>\vert \vert s \vert \vert </math>. | ||
+ | |||
+ | == Leveled FHE == | ||
+ | |||
+ | We will only present the version of the scheme which is based on Ring version of LWE (R-LWE) and we reffer to Section 3.4 in [1] for an analogous construction of a scheme based on the classical LWE. | ||
+ | |||
+ | In the scheme, the authors use a parameter <math> L </math> indicating the number of levels of arithmetic circuit that the FHE scheme should be able of evaluating. | ||
+ | |||
+ | <b> FHE without Bootstrapping:</b> | ||
+ | |||
+ | * FHE.Setup(<math>1^{\lambda}, 1^L </math>): Takes as imput the security parameter and a number of levels <math>L</math>. Let <math>\mu := \mu(\lambda, L) = \theta(\log{\lambda}+ \log{L})</math> be a parameter (see the original paper [1] for details about its choice). | ||
+ | |||
+ | For <math>j = L </math> to <math> 0</math> (output level), run | ||
+ | <math>params_j \leftarrow E.Setup(1^{\lambda}, 1^{(j+1)\mu}) </math> to obtain a ladder of decreasing moduli from <math>q_L</math> - which has <math>(L+1) \cdot \mu </math> bits - down to <math>q_0 = \mu</math> bits. | ||
+ | |||
+ | For <math>j = L-1 </math> to <math> 0 </math>, replace the value of <math> d_j </math> in <math> params_j </math> with <math> d=d_L </math> and the distribution <math>\chi_j </math> with <math>\chi_L </math>. By this, one ensures that the ring dimension and the noise distribution do not depend on the circuit level, but the vector dimension <math> n_j</math> might depend. | ||
+ | |||
+ | * FHE. KeyGen(<math> \{params_j : j =\overline{0,L} \} </math> ): For <math>j = L </math> down to <math> 0 </math>, do the following: | ||
+ | |||
+ | 1. Run <math>s_j \leftarrow</math> E.SecretKeygen(<math>params_j </math>) and <math>A_j \leftarrow </math> E.PublicKeyGen(<math>params_j, s_j</math>). | ||
+ | |||
+ | 2. Set <math>s_j' \leftarrow s_j \otimes s_j </math>, namely <math> s_j </math> tensored with itself. | ||
+ | |||
+ | 3. Set <math>s_j'' \leftarrow</math> BitDecomp(<math>(s_j', q_j) </math>). | ||
+ | |||
+ | 4. Run <math>\tau_{s_{j+1}'' \to s_j} \leftarrow</math> SwitchKeyGen(<math>s_j'', s_{j-1} </math>). Omit this step when <math>j = L</math>. | ||
+ | |||
+ | * FHE.Enc(<math>params, pk, m </math>): Take a message in <math> R_2 </math> and run <math> E. Enc(A_L,m)</math>. | ||
+ | |||
+ | * FHE.Dec(<math>params, sk, c </math>): Suppose the ciphertext is encrypted under the key <math>s_j</math>. Run <math>E.Dec(s_j,c)</math>. The authors mention (and in fact this is the case for the implementation), that the ciphertext could be augmented with an index indicating which level it belongs to. | ||
+ | |||
+ | * FHE.Add(<math>pk, c_1, c_2 </math>): The ciphertexts <math>c_1,c_2 </math> must be encrypted under the same <math> s_j </math>. If they are not, one uses FHE.Refresh detailed below to make it so. Set <math>c_3 \leftarrow c_1 + c_2 \pmod{q_j} </math>. | ||
+ | |||
+ | One should interpret <math>c_3 </math> as a ciphertext under <math>s_j' = s_j \otimes s_j </math>. Recall that the first coefficient of <math>s_j</math> is equal to <math> 1 </math>. | ||
+ | |||
+ | Output | ||
+ | <center><math> c_4 \leftarrow FHE.Refresh(c_3, \tau_{s_{j}'' \to s_{j-1}}, q_j, q_{j-1}).</math> </center> | ||
+ | |||
+ | * FHE. Mult(<math>pk, c_1, c_2 </math>): As before, the ciphertexts must be encrypted under the same <math> s_j</math>. If they are not, one uses FHE.Refresh to make it so. | ||
+ | |||
+ | First, multiply: the new ciphertext, under the secret key <math>s_j' = s_j \otimes s_j </math>, is the coefficient vector <math>c_3 </math> of the linear equation | ||
+ | |||
+ | <center><math>L^{long}_{c_1,c_2}(x \otimes x).</math></center> | ||
+ | |||
+ | Remember one can see <math>L_{c_1}(x) \cdot L_{c_2}(x) = <c_1,x> \cdot <c_2,x> </math> as a linear equation over the coefficients of <math>x \otimes x</math>, the tensoring of <math>x </math> with itself. This is the meaning of the linear functional <math>L_{c_1,c_2}</math>. Then, output | ||
+ | |||
+ | <center><math>c_4 \leftarrow</math> FHE.Refresh(<math>c_3 \tau_{s_{j}'' \to s_{j-1}}, q_j, q_{j-1}</math> ).</center> | ||
+ | |||
+ | * FHE.Refresh(<math>c, \tau_{s_j'' \to s_{j-1}}, q_j, q_{j-1} </math>): Takes a ciphertext encrypted under <math>s_j' </math>, the auxiliary key switching information <math> \tau_{s_j'' \to s_{j-1}}</math> and the current and next moduli <math>q_j </math> and <math>q_{j-1}</math>, respectively. The procedure does the following: | ||
+ | |||
+ | 1. It expands <math>c_1 \leftarrow</math> Powersof2(<math>c,q_j </math>). We recall that | ||
+ | <math><c_1, s_j''> = <c, s_j'> \pmod{q_j} </math>. | ||
+ | |||
+ | 2. It switches the moduli: Set <math>c_2 \leftarrow</math> Scale(<math>c_1, q_j, q_{j-1},2</math> ). This <math>c_2 </math> is now a ciphertext under the key <math>s_j'' </math> for the modulus <math> q_{j-1} </math>. | ||
+ | |||
+ | 3. Finally, it switches keys: Output | ||
+ | |||
+ | <center><math>c_3 \leftarrow</math>SwitchKey(<math>\tau_{s_j'' \to s_{j-1}}, c_2, q_{j-1} </math>),</center> | ||
+ | which is a ciphertext under the key <math>s_{j-1}</math> for the modulus <math> q_{j-1}</math>. | ||
+ | |||
+ | As one can observe, a key step in this FHE scheme is the Refresh procedure. | ||
+ | |||
+ | We mention that, as the addition noise increases only linearly one does not necessarily need to refresh after addition (even after high fan-in ones). | ||
+ | |||
+ | |||
+ | We refer to the original article [1] for details on correctness, parameter tuning, performance and security. | ||
+ | |||
+ | There are significant ways in improving the performance of this scheme, for example Batching (see section 5 of the article). The scheme is also bootstrappable. | ||
+ | |||
+ | == Implementation == | ||
+ | |||
+ | [https://github.com/homenc/HElib HElib] is an open-source software library that implements homomorphic encryption (HE) which contains the implementation of the Brakerski-Gentry-Vaikuntanathan (BGV) scheme with bootstrapping. | ||
+ | |||
+ | The implementation incorporates many optimizations that make homomorphic evaluation run faster, focusing mostly on effective use of the [https://eprint.iacr.org/2011/133 Smart-Vercauteren ciphertext packing] techniques and the [https://eprint.iacr.org/2012/099 Gentry-Halevi-Smart optimizations]. The latter were introduce in the seminal paper "Homomorphic Evaluation of the AES circuit"<ref>C. Gentry, S. Halevi, N. Smart. Homomorphic Evaluation of the AES Circuit, Advances in Cryptology – CRYPTO 2012, pp. 850-867.</ref>. | ||
+ | |||
+ | ==Example use of HElib== | ||
+ | |||
+ | We refer to | ||
+ | |||
+ | https://tommd.github.io/posts/HELib-Intro.html | ||
+ | |||
+ | for short tutorial on how to use HElib for simple computations. More precisely, at the above link the reader can find an example of program which fills two vectors with integers, encrypts them using the [BGV] implementation and adds them (component by component) homomorphically. | ||
== References == | == References == |
Latest revision as of 16:04, 7 February 2021
In 2011, Brakerski, Gentry and Vaikuntanathan (BGV) published the paper [1] in which they introduce a new (leveled) fully homomorphic encryption (FHE) that improves performance and bases security on weaker assumptions than schemes from the previous generation.
A central conceptual contribution of this work is a new way of constructing leveled fully homomorphic encryption schemes (capable of evaluating arbitrary polynomial-size circuits), without Gentry’s bootstrapping procedure.
Until recently, the BGV scheme was considered to be the most efficient homomorphic encryption scheme when performing the same operations on multiple ciphertexts at once.
Contents
Leveled Fully Homomorphic Encryption
Most of the work done by the will focus on the construction of a leveled fully homomorphic scheme, in the sense that the parameters of the scheme depend (polynomially) on the depth of the circuits that the scheme is capable of evaluating.
Definition. We say that a family of homomorphic encryption schemes is leveled fully homomorphic if, for all , they all use the same decryption circuit, compactly evaluates all circuits of depth at most (that use some specified complete set of gates), and the computational complexity of 's algorithms is polynomial (a fixed polynomial for all ) in the security parameter , and the size of the circuit (in the case of the evaluation algorithm).
The construction: FHE without bootstrapping
The authors base the security of their scheme on the hardness of Ring-Learning with errors problems, a generalisation of the classical LWE problem.
Let be a security parameter, representing security against known attacks.
Let be a ring. For any integer , we write for the quotient .
Let be an odd modulus and a ``noise" distribution over . Let be an additional parameter of the system which is larger than .
Let us assume that the plaintext is .
- E.Setup(): Choose a -bit modulus and choose the other parameters , and , appropriately to ensure that the scheme is based on a Ring-LWE instance that achieves security against known attacks. Let and let params = .
- E.SecretKetGen(params): Draw . Set .
- E.PublicKeyGen(params, sk): Recall that the secret key is . This algorithm generates a (column) vector , uniformly and a vector . The algorithm computes
. Then, set to be the matrix obtained by setting on the first column followed by the entries of . We remark that . The algorithm outputs the public key .
- E.Enc(params, pk,m): To encrypt a message , set , sample uniformly and output the ciphertext .
- E.Dec(params, sk, c): Output . Where denotes reduction into the range .
Correctness is easy to verify, whereas we refer to the paper for details upon security.
Key switching (Dimension reduction)
Recall that in the above scheme, the decryption equation for a ciphertext that encrypts a message under the secret key can be written as where is a linear operator which depends on . To be precise, the latter is just the inner product between two vectors in .
To understand the key switching procedures, we have to (at least briefly) describe the following subroutines first:
- BitDecomp(): decomposes into its bit representation, namely where all of the . The procedure outputs the vector
- Powersof2(): outputs the vector
It is easy to see that for vectors of the same length , we have:
Now, key switching consists of two procedures:
- SwitchKeyGen():
- Run for .
- Set (Add Powersof2()), which is an element of to 's first column. Output .
- SwitchKey(): Output .
Note that, in SwitchKeyGen, the matrix consists of encryptions of under the key . Then, pieces of the key are added to these encryptions of . Thus, in some sense, the matrix consists of encryptions of pieces of (in a certain format) under the key .
The authors establish the following correctness result (See Lemma 3 in the paper):
is a valid encryption of under the key , and one can see that the noise of is larger by a small additive factor.
Modulus switching
If is a valid encryption of under the key , and is (what the authors call) a ``short vector" and is a simple scaling of , i.e. is the -vector closest to under the additional constraint that
it turns out that (under some conditions) the vector is a valid encryption of , under the secret key using the modulus .
In other words, under some conditions, one can change the modulus in the decryption equation to another (maybe smaller) modulus , while preserving the correctness of decryption under the same secret key .
For an integer vector and integers , the authors define
to be the -vector closest to which satisfies
For the details concerning the conditions on and the vector required for the preservation of decryption correctness, we refer to Lemma 4 and its Corollary 1 in [1].
The aforementioned results assert that assuming is smaller than and has coefficients that are small in relation to , this ``modulus swithcing" procedure permits the evaluator to reduce the magnitude of the noise without knowing the secret key. The evaluator only has to know a bound on .
Leveled FHE
We will only present the version of the scheme which is based on Ring version of LWE (R-LWE) and we reffer to Section 3.4 in [1] for an analogous construction of a scheme based on the classical LWE.
In the scheme, the authors use a parameter indicating the number of levels of arithmetic circuit that the FHE scheme should be able of evaluating.
FHE without Bootstrapping:
- FHE.Setup(): Takes as imput the security parameter and a number of levels . Let be a parameter (see the original paper [1] for details about its choice).
For to (output level), run to obtain a ladder of decreasing moduli from - which has bits - down to bits.
For to , replace the value of in with and the distribution with . By this, one ensures that the ring dimension and the noise distribution do not depend on the circuit level, but the vector dimension might depend.
- FHE. KeyGen( ): For down to , do the following:
1. Run E.SecretKeygen() and E.PublicKeyGen().
2. Set , namely tensored with itself.
3. Set BitDecomp().
4. Run SwitchKeyGen(). Omit this step when .
- FHE.Enc(): Take a message in and run .
- FHE.Dec(): Suppose the ciphertext is encrypted under the key . Run . The authors mention (and in fact this is the case for the implementation), that the ciphertext could be augmented with an index indicating which level it belongs to.
- FHE.Add(): The ciphertexts must be encrypted under the same . If they are not, one uses FHE.Refresh detailed below to make it so. Set .
One should interpret as a ciphertext under . Recall that the first coefficient of is equal to .
Output
- FHE. Mult(): As before, the ciphertexts must be encrypted under the same . If they are not, one uses FHE.Refresh to make it so.
First, multiply: the new ciphertext, under the secret key , is the coefficient vector of the linear equation
Remember one can see as a linear equation over the coefficients of , the tensoring of with itself. This is the meaning of the linear functional . Then, output
- FHE.Refresh(): Takes a ciphertext encrypted under , the auxiliary key switching information and the current and next moduli and , respectively. The procedure does the following:
1. It expands Powersof2(). We recall that .
2. It switches the moduli: Set Scale( ). This is now a ciphertext under the key for the modulus .
3. Finally, it switches keys: Output
which is a ciphertext under the key for the modulus .
As one can observe, a key step in this FHE scheme is the Refresh procedure.
We mention that, as the addition noise increases only linearly one does not necessarily need to refresh after addition (even after high fan-in ones).
We refer to the original article [1] for details on correctness, parameter tuning, performance and security.
There are significant ways in improving the performance of this scheme, for example Batching (see section 5 of the article). The scheme is also bootstrappable.
Implementation
HElib is an open-source software library that implements homomorphic encryption (HE) which contains the implementation of the Brakerski-Gentry-Vaikuntanathan (BGV) scheme with bootstrapping.
The implementation incorporates many optimizations that make homomorphic evaluation run faster, focusing mostly on effective use of the Smart-Vercauteren ciphertext packing techniques and the Gentry-Halevi-Smart optimizations. The latter were introduce in the seminal paper "Homomorphic Evaluation of the AES circuit"[2].
Example use of HElib
We refer to
https://tommd.github.io/posts/HELib-Intro.html
for short tutorial on how to use HElib for simple computations. More precisely, at the above link the reader can find an example of program which fills two vectors with integers, encrypts them using the [BGV] implementation and adds them (component by component) homomorphically.
References
- ↑ Z. Brakerski, C. Gentry, and V. Vaikuntanathan. 2014. (Leveled) Fully Homomorphic Encryption without Bootstrapping. ACM Trans. Comput. Theory 6, 3, Article 13 (July 2014), 36 pages. DOI:https://doi.org/10.1145/2633600
- ↑ C. Gentry, S. Halevi, N. Smart. Homomorphic Evaluation of the AES Circuit, Advances in Cryptology – CRYPTO 2012, pp. 850-867.