協(xié)議組合邏輯安全的4G無(wú)線網(wǎng)絡(luò)接入認(rèn)證方案

王麗麗，馮濤,2,，馬建峰

(1. 蘭州理工大學(xué) 計(jì)算機(jī)與通信學(xué)院, 甘肅 蘭州 730050;2. 福建師范大學(xué) 網(wǎng)絡(luò)安全與密碼技術(shù)重點(diǎn)實(shí)驗(yàn)室, 福建 福州 350007;3. 西安電子科技大學(xué) 計(jì)算機(jī)網(wǎng)絡(luò)與信息安全教育部重點(diǎn)實(shí)驗(yàn)室, 陜西 西安 710071)

1 引言

在多種無(wú)線通信技術(shù)及異構(gòu)網(wǎng)絡(luò)共存、融合的趨勢(shì)下，4G無(wú)線網(wǎng)絡(luò)移動(dòng)終端的安全接入問(wèn)題變得更加復(fù)雜和重要[1]。2009年，ITU-R確立了兩大4G候選標(biāo)準(zhǔn)：LTE-Advanced和IEEE 802.16m。文獻(xiàn)[2,3] 中介紹了關(guān)于 LTE RAN(radio access network)的安全決策，但沒(méi)有給出具體的接入認(rèn)證協(xié)議。文獻(xiàn)[4]中，IEEE 802.16m工作組針對(duì)4G網(wǎng)絡(luò)的安全機(jī)制提出了PKMv3(privacy key management version 3)協(xié)議，但也沒(méi)有給出具體的接入認(rèn)證過(guò)程。

1991年，Girault首次提出自證實(shí)公鑰系統(tǒng)[5]。同基于證書(shū)的公鑰密碼體制相比，自證實(shí)公鑰系統(tǒng)更適用于移動(dòng)環(huán)境。首先，AN(access network)和ME(mobile equipment)的認(rèn)證參數(shù)中不包含公鑰證書(shū)，協(xié)議交互之前，不需要存儲(chǔ)和傳送自己的公鑰證書(shū)，不需要驗(yàn)證彼此公鑰證書(shū)的合法性和有效性，節(jié)省了存儲(chǔ)空間和通信帶寬，減輕了網(wǎng)絡(luò)負(fù)載和傳輸時(shí)延，減少了移動(dòng)終端的計(jì)算負(fù)擔(dān)；此外，對(duì)公鑰的驗(yàn)證隱藏在簽名驗(yàn)證或加密過(guò)程中，當(dāng)網(wǎng)絡(luò)存在階層關(guān)系時(shí)也不需要通過(guò)其他網(wǎng)絡(luò)實(shí)體轉(zhuǎn)發(fā)認(rèn)證信息，提高了公鑰驗(yàn)證效率和認(rèn)證效率。

Zheng等人[6]基于自證實(shí)公鑰系統(tǒng)提出了一個(gè)4G網(wǎng)絡(luò)用戶認(rèn)證方案，但方案還存在不足之處。第一，方案中，網(wǎng)絡(luò)端的公鑰并不是基于自證實(shí)公鑰系統(tǒng)構(gòu)建的，對(duì)該公鑰的驗(yàn)證是利用基站聯(lián)合廣播，并在ME中設(shè)立緩沖區(qū)，通過(guò)概率統(tǒng)計(jì)方法實(shí)現(xiàn)的。但是驗(yàn)證結(jié)果存在風(fēng)險(xiǎn)，如局部出現(xiàn)偽基站密度超過(guò)合法基站的可能等。而且，方案中沒(méi)有明確指出如何確定終端緩沖區(qū)的長(zhǎng)度、如何確定偽基站與合法基站的數(shù)量同識(shí)別成功的概率之間的關(guān)系。第二，該方案的首次接入認(rèn)證和切換認(rèn)證協(xié)議中，用戶的歸屬環(huán)境和訪問(wèn)網(wǎng)絡(luò)之間需要交互部分認(rèn)證信息，接入時(shí)延會(huì)增加，對(duì)實(shí)時(shí)應(yīng)用很不利。第三，Zheng沒(méi)有對(duì)該方案的安全屬性進(jìn)行形式化分析和證明。

考慮到4G網(wǎng)絡(luò)中ME的安全接入問(wèn)題，以及ME的移動(dòng)性和漫游性，本文基于自證實(shí)公鑰設(shè)計(jì)了一個(gè)新的4G無(wú)線網(wǎng)絡(luò)終端接入方案，方案包括首次/切換接入認(rèn)證協(xié)議和再次接入認(rèn)證協(xié)議。由于安全協(xié)議的分析和證明對(duì)于現(xiàn)代安全網(wǎng)絡(luò)系統(tǒng)至關(guān)重要，通過(guò)運(yùn)用DDMP理論[7]，本文給出新方案的演繹推導(dǎo)，并對(duì)其安全屬性進(jìn)行了形式化證明和分析。DDMP理論由A.Datta等人[7]提出，它包括協(xié)議演繹系統(tǒng)PDS和協(xié)議組合邏輯PCL，該理論既可以作為協(xié)議設(shè)計(jì)的新方法，又為協(xié)議的安全性證明和分析提供了一種全新的形式化方法。

2 預(yù)備知識(shí)

2.1 自證實(shí)公鑰系統(tǒng)

TA(trust authority)公開(kāi)模數(shù)n及其公鑰e，秘密保留私鑰d，用戶的注冊(cè)過(guò)程如下[5,8]。

1) 用戶選定長(zhǎng)度為160bit以上的私鑰x，并計(jì)算出V=g-xmodn，n是長(zhǎng)度為1 024bit以上的模數(shù)，然后將V和自己身份ID傳給TA。

2) TA計(jì)算用戶的公鑰Y，Y=(V-ID)dmodn，并將Y傳給用戶。

3) 用戶驗(yàn)證V=(Ye+ID)modn，若等式成立，則用戶的公鑰為Y，私鑰為x。

在自證實(shí)公鑰系統(tǒng)中，用戶的身份、公鑰和私鑰滿足一種計(jì)算上不可偽造的數(shù)學(xué)關(guān)系，在利用密鑰執(zhí)行加解密、簽名驗(yàn)證、密鑰協(xié)商或其他密碼操作的同時(shí)，就可以驗(yàn)證該數(shù)學(xué)關(guān)系，從而驗(yàn)證公鑰的合法性和有效性。用戶的私鑰是自己選定的，其安全性基于解離散對(duì)數(shù)困難問(wèn)題，TA無(wú)法從傳送過(guò)來(lái)的數(shù)據(jù)中得到用戶的私鑰，不能冒充用戶偽造他們的簽名，相比于基于身份的公鑰密碼體制，具有更高的安全性，更適合于開(kāi)放系統(tǒng)環(huán)境中的應(yīng)用。此外，TA無(wú)法完全掌握公鑰的產(chǎn)生和驗(yàn)證，即使TA偽造出相同用戶的另一個(gè)公鑰也會(huì)被檢測(cè)出來(lái)。

2.2 協(xié)議演繹系統(tǒng)和協(xié)議組合邏輯

協(xié)議演繹系統(tǒng)(PDS)由構(gòu)件集合和操作集合組成，構(gòu)件是用于構(gòu)造復(fù)雜協(xié)議的簡(jiǎn)單協(xié)議，操作集合包含3類(lèi)不同的演繹操作：組合、求精和轉(zhuǎn)換。組合操作用于2個(gè)協(xié)議的組合，包括并行組合和串行組合。求精操作用于一個(gè)簡(jiǎn)單協(xié)議構(gòu)件上，為協(xié)議添加必要的安全屬性，且不會(huì)改變協(xié)議的消息數(shù)或協(xié)議的基礎(chǔ)結(jié)構(gòu)，例如用加密的隨機(jī)數(shù)代替原來(lái)沒(méi)有加密的隨機(jī)數(shù)。轉(zhuǎn)換操作則是通過(guò)移動(dòng)消息、組合協(xié)議步驟、插入一個(gè)或多個(gè)協(xié)議步驟等操作完成對(duì)協(xié)議的修改，例如將數(shù)據(jù)從一個(gè)消息移動(dòng)到另外一個(gè)較早的消息中。本文中主要使用的演繹操作包括串行組合操作、轉(zhuǎn)換操作T1以及求精操作R3、R4和R6(具體含義在本文設(shè)計(jì)的安全協(xié)議演繹過(guò)程中說(shuō)明)。

協(xié)議組合邏輯(PCL)可用于安全協(xié)議的形式化證明和分析，同BAN邏輯及其他的邏輯方法相比，PCL支持安全協(xié)議的組合證明；由于包含了協(xié)議的執(zhí)行過(guò)程，PCL不需要對(duì)協(xié)議進(jìn)行抽象；PCL采用的是標(biāo)準(zhǔn)邏輯概念，而不需要使用“管轄(jurisdiction)”和“信念(belief)”等不清晰規(guī)則。此外，PCL加入了密碼學(xué)原語(yǔ)，并重點(diǎn)刻畫(huà)了消息的發(fā)送和接收，這些概念體現(xiàn)了安全協(xié)議的基本要素。目前，PCL已經(jīng)被成功用于形式化證明多個(gè)協(xié)議的正確性，如SSL/TLS協(xié)議[7]、IEEE 802.11i協(xié)議[9]、Kerberos V5 協(xié)議[10]等。

PCL的基本語(yǔ)法元素是前置斷言—后置斷言表達(dá)式，即幾乎所有的安全協(xié)議證明步驟都遵循θ[P]Xφ規(guī)則，該規(guī)則表明協(xié)議的執(zhí)行實(shí)例X執(zhí)行動(dòng)作序列P以后，狀態(tài)由θ轉(zhuǎn)變?yōu)棣铡１疚挠玫降牟糠止砗头▌t如下[7,11,12]。

Contains(t1,t2)：表示t1包含t2。

Fresh(X,t)：表示在實(shí)例X中產(chǎn)生的t是新鮮的。

Has(X,t)：秘密屬性的一種描述，表示實(shí)體X?在實(shí)例X中擁有信息t。

Honest(X?)：表示實(shí)體X?在當(dāng)前輪中是誠(chéng)實(shí)的，其執(zhí)行的所有動(dòng)作都是協(xié)議所規(guī)定的。

Send(X,t)/New(X,t)/Sign(X,t)/Encrypt(X,t)：分別表示發(fā)生了發(fā)送、生成隨機(jī)數(shù)、簽名和加密動(dòng)作。

3 4G無(wú)線網(wǎng)絡(luò)接入認(rèn)證新方案

3.1 參數(shù)描述

相關(guān)參數(shù)要求[5,8]：|x|表示x的長(zhǎng)度，整數(shù)A、B、S滿足其中，|S|表示私鑰長(zhǎng)度。TA為ME產(chǎn)生自證實(shí)公鑰的過(guò)程如下。

1) ME選定私鑰MEx，計(jì)算并將IDME、IDHE和VME發(fā)送給TA，其中，IDME是ME的身份標(biāo)識(shí)符(IMSI)，IDHE是ME的歸屬環(huán)境HE(home environment)的標(biāo)識(shí)符。

同理，AN通過(guò)TA獲得公鑰YAN，私鑰ANx。

3.2 移動(dòng)終端的首次/切換接入認(rèn)證協(xié)議

為了滿足移動(dòng)網(wǎng)絡(luò)的需求和特性，針對(duì)用戶在首次接入、再次接入和漫游切換等不同場(chǎng)景，本文基于自證實(shí)公鑰系統(tǒng)提出了首次/切換接入場(chǎng)景下的認(rèn)證與密鑰交換協(xié)議(AKEBSP,authentication and key exchange protocol based on self-certified public key)和再次接入場(chǎng)景下的認(rèn)證協(xié)議，在確保安全接入的前提下，提高了認(rèn)證效率。首次/切換接入場(chǎng)景下的認(rèn)證過(guò)程如圖1所示。

圖1 首次/切換接入認(rèn)證過(guò)程

此過(guò)程說(shuō)明如下。

1) ME收到AN廣播的IDAN和公鑰YAN后，選擇隨機(jī)數(shù)并將cME、IDAN、IDHE發(fā)送給AN。

2) AN驗(yàn)證IDAN后，選擇隨機(jī)數(shù)rAN∈[ 0,A]和cAN∈[ 0 ,B]，分別計(jì)算TAN=rAN+xANcME和RAN=grANmodn，并將消息cAN、RAN、RAN、SigAN發(fā)送給ME，其中SigAN= {cME,cAN,RAN,TAN}xAN。

3) ME首先驗(yàn)證SigAN，如果正確，則驗(yàn)證下面式子是否成立：和TAN∈[0,A+(B-1)(S-1)]。如果成立，則選擇隨機(jī)數(shù)rME∈ [ 0,B]，并計(jì)算然后將消息發(fā)送給AN。

5) ME收到消息并解密，獲得了自己的臨時(shí)身份TIDME，供再次接入該網(wǎng)絡(luò)使用。

認(rèn)證結(jié)束后，AN會(huì)在數(shù)據(jù)庫(kù)中存儲(chǔ)TIDME和（IDME,YME,KAM）的對(duì)應(yīng)關(guān)系，向ME提供服務(wù)后可以將作為不可否認(rèn)憑證發(fā)送給ME的歸屬環(huán)境HE。其中，bill為計(jì)費(fèi)信息，

3.3 移動(dòng)終端再次接入認(rèn)證協(xié)議

首次/切換接入認(rèn)證通過(guò)后，ME需要再次接入到同一網(wǎng)絡(luò)時(shí)，可以利用TIDME代替協(xié)議中的IDME進(jìn)行再次接入認(rèn)證，保護(hù)了ME的身份隱私，其認(rèn)證交互過(guò)程如圖2所示。其中，TIDME′是AN為ME生成的新的臨時(shí)身份，KAM′是AN生成的新的會(huì)話密鑰，作為ME和AN下次交互使用，減少了攻擊者通過(guò)已攻陷的會(huì)話密鑰同網(wǎng)絡(luò)交互的風(fēng)險(xiǎn)。

圖2 再次接入認(rèn)證過(guò)程

4 新協(xié)議的演繹

由于篇幅限制，本文僅對(duì)首次/切換接入場(chǎng)景下的認(rèn)證與密鑰交換協(xié)議 AKEBSP進(jìn)行演繹推導(dǎo)和形式化證明。在新協(xié)議的演繹過(guò)程和步驟中，為了簡(jiǎn)潔和清晰，分別用X?和?表示協(xié)議的2個(gè)參與方：移動(dòng)終端ME和接入網(wǎng)絡(luò)AN，其相應(yīng)的實(shí)體分別用X和Y表示。此外，AN的公鑰也可用?表示，終端的歸屬環(huán)境標(biāo)識(shí)符用IDH表示。

首先，選取3個(gè)簡(jiǎn)單的基本協(xié)議，一個(gè)是基于簽名的挑戰(zhàn)應(yīng)答協(xié)議P1，另外2個(gè)是基于加密的挑戰(zhàn)應(yīng)答協(xié)議P2 和P3（其中，?是AN的公鑰，密鑰K是ME通過(guò)RY計(jì)算得到的）。

對(duì)協(xié)議P1 和P2進(jìn)行串行組合（串行組合操作是通過(guò)適當(dāng)?shù)奶娲襟E，使前一協(xié)議模塊的輸出代替后一協(xié)議模塊的輸入來(lái)完成協(xié)議的組合），用協(xié)議P1 的輸出代替P2的輸入，從而得到協(xié)議P4。

對(duì)協(xié)議P4應(yīng)用轉(zhuǎn)換操作T1（通過(guò)將數(shù)據(jù)從一個(gè)消息移動(dòng)到另外一個(gè)較早的消息中），將cY移動(dòng)到較早的消息中，從而得到協(xié)議P5，其主要目的是減少消息數(shù)量。

由于ME驗(yàn)證AN時(shí)需要使用2個(gè)參數(shù)，分別是由RAN=grANmodn和TAN=rAN+xANcME計(jì)算得到的RAN和TAN，但協(xié)議P5中并未給出，根據(jù)轉(zhuǎn)換操作的定義，這里可以應(yīng)用轉(zhuǎn)換操作在協(xié)議第二步中加入RAN和TAN，從而得到協(xié)議P6。

為了讓X確信消息是由Y新鮮生成的，對(duì)協(xié)議P6應(yīng)用轉(zhuǎn)換操作T2，得到協(xié)議P7，其主要目的是為了防止重放攻擊。

由于ME要明確接收消息的AN，并需要同歸屬環(huán)境進(jìn)行交互，根據(jù)轉(zhuǎn)換操作的定義，在協(xié)議第一步中加入IDY和TIDH，從而得到協(xié)議P8。

對(duì)協(xié)議P8 和P3進(jìn)行串行組合，用協(xié)議P8 輸出代替協(xié)議P3的輸入，從而得到協(xié)議P9。

對(duì)協(xié)議P9應(yīng)用轉(zhuǎn)換操作T1，將消息RX移動(dòng)到較早的消息中，從而得到協(xié)議P10，其主要目的也是減少消息數(shù)量。

由于AN驗(yàn)證ME時(shí)還需要參數(shù)TX、X的身份標(biāo)識(shí)IDX以及X的公鑰YX，但協(xié)議P10中并未給出，根據(jù)轉(zhuǎn)換操作的定義，這里可以應(yīng)用轉(zhuǎn)換操作在協(xié)議第3步中加入TX、IDX和YX，從而得到協(xié)議P11。

為了保護(hù)用戶的身份隱私，首次認(rèn)證或切換認(rèn)證之后，用戶再次接入該網(wǎng)絡(luò)時(shí)是借助一個(gè)臨時(shí)身份TIDX，但協(xié)議P11中并未給出，根據(jù)轉(zhuǎn)換操作的定義，這里可以應(yīng)用轉(zhuǎn)換操作在協(xié)議第4步中加入TIDX，從而得到協(xié)議P12。

到此為止，通過(guò)協(xié)議演繹系統(tǒng)(PDS)演繹得到了新協(xié)議AKEBSP。

5 新協(xié)議安全性的形式化證明和分析

5.1 協(xié)議流程表示

PCL標(biāo)記法表示的協(xié)議角色如下。

其中，InitAKEBSP是發(fā)起者角色(對(duì)應(yīng)于 ME)的動(dòng)作序列，RespAKEBSP是響應(yīng)者角色(對(duì)應(yīng)于AN)的動(dòng)作序列。

5.2 安全屬性的形式化證明

定理 1 AKEBSP安全認(rèn)證協(xié)議具有會(huì)話認(rèn)證性。

根據(jù)協(xié)議組合邏輯PCL，需要證明的發(fā)起者角色會(huì)話認(rèn)證性的形式化表示為

當(dāng)上式成立時(shí)，AKEBSP協(xié)議的發(fā)起者角色能夠保證會(huì)話認(rèn)證性。這里僅給出ME端的證明情況，AN端的證明情況類(lèi)似。

證明

定理2 AKEBSP安全認(rèn)證協(xié)議具有密鑰機(jī)密性。

根據(jù)協(xié)議組合邏輯PCL，需要證明的發(fā)起者角色密鑰機(jī)密性的形式化表示為

當(dāng)上式成立時(shí)，AKEBSP協(xié)議的發(fā)起者角色能夠保證密鑰機(jī)密性。這里僅給出ME端的證明情況，AN端的證明情況類(lèi)似。

證明

5.3 新方案的綜合分析

從認(rèn)證協(xié)議的可證明安全性、通信效率和計(jì)算效率等方面對(duì)新方案中的 AKEBSP協(xié)議和文獻(xiàn)[6]提出的SPAKA協(xié)議進(jìn)行比較，結(jié)果如表1所示，其中有關(guān)符號(hào)說(shuō)明如下：|SV|表示一次簽名驗(yàn)證操作，|SED|表示一次對(duì)稱(chēng)密鑰加解密操作，|PED|表示一次非對(duì)稱(chēng)密鑰加解密操作。

新方案是基于自證實(shí)公鑰系統(tǒng)提出的，節(jié)省了存儲(chǔ)空間，減少了ME的計(jì)算量和認(rèn)證時(shí)延。根據(jù)協(xié)議的演繹過(guò)程可知，ME和AN之間傳遞的所有消息均具有新鮮性和不可預(yù)測(cè)性，所以新方案能抵御重放攻擊。

表1 本方案與相關(guān)方案的比較

新方案能提供不可否認(rèn)服務(wù)，整個(gè)系統(tǒng)中只有擁有正確私鑰的終端用戶才可以根據(jù)cAN構(gòu)造出合法的TME，一旦終端用戶通過(guò)了認(rèn)證，則不能否認(rèn)自己的接入。當(dāng)出現(xiàn)糾紛的時(shí)候，AN可以提供RAN、TME和cAN進(jìn)行驗(yàn)證，以作為不可否認(rèn)憑證。

新方案中，ME的身份（IDME/IMSI）是在用戶驗(yàn)證接入網(wǎng)絡(luò)的身份之后發(fā)送出去的，沒(méi)有以明文形式在空中接口和有線鏈路傳輸，且只有TA知道用戶公鑰和用戶身份的對(duì)應(yīng)關(guān)系，攻擊者無(wú)法對(duì)用戶進(jìn)行非法跟蹤，提供了身份保護(hù)。每次認(rèn)證后，AN都會(huì)動(dòng)態(tài)更換用戶的臨時(shí)身份，使得用戶身份的安全性大大增強(qiáng)。

6 結(jié)束語(yǔ)

本文分析了4G無(wú)線網(wǎng)絡(luò)中移動(dòng)終端的安全接入認(rèn)證問(wèn)題，基于自證實(shí)公鑰設(shè)計(jì)了一個(gè)新的終端接入認(rèn)證方案。新方案包括首次/切換接入場(chǎng)景下的認(rèn)證及密鑰交換 AKEBSP協(xié)議和再次接入場(chǎng)景下的認(rèn)證協(xié)議，適應(yīng)了4G無(wú)線網(wǎng)絡(luò)的移動(dòng)和漫游特性。本文應(yīng)用DDMP理論中的協(xié)議演繹系統(tǒng)PDS對(duì)新協(xié)議進(jìn)行了演繹推導(dǎo)，用協(xié)議組合邏輯 PCL對(duì)協(xié)議進(jìn)行了形式化證明，并綜合分析了協(xié)議的安全性能。結(jié)果表明，新方案具有會(huì)話認(rèn)證性和密鑰機(jī)密性，不僅能抵御偽基站攻擊和重放攻擊，還能提供不可否認(rèn)服務(wù)和身份隱私性，同時(shí)提高了移動(dòng)終端的接入效率。

[1] PIYUSH G,PRIYADARSHAN P.4G-A new era in wireless telecommunication[EB/OL]. http://www.idt.mdh.se/kurser/ct3340/ht09/ADMI NISTRATION/IRCSE09-submissions/ircse09_submission_13.pdf, 2009.

[2] AQSACOM S,AQSACOM I. Lawful interception for 3G and 4G networks[EB/OL].http://www.aqsacomna.com/us/articles/Aqsacom_White_paper_4G_LI_v1.pdf,2010.

[3] 3GPP. Technical Specification Group Services and System Aspects;Rationale and Track of Security Decisions in Long Term Evolved(LTE) RAN/3GPP System Architecture Evolution(SAE)(Release 9)[S]. Tech Spec 3GPP TS 33.102 V9.0.0. 2009.

[4] IEEE P802.16m. Part 16:air interface for fixed and mobile broadband wireless access systems[EB/OL].http://lichun.cm.nctu.edu.tw/pa pers/P80216m_D4.pdf,2010.

[5] GIRAULT M. Self-certified public keys[A]. Eurocrypt’91 [C]. Brighton UK,1991.490-497.

[6] HE D K, WANG J,ZHENG Y. User authentication scheme based on self-certified public key for next generation wireless network[A].IEEE International Symposium on Biometrics and Security Technologies [C]. Islamabad, Pakistan, 2008.

[7] DATTA A. Security Analysis of Network Protocol: Compositional Reasoning and Complexity Theoretic Foundations[D]. Computer Science Department, Stanford University, 2005.8-72.

[8] POUPARD C,STERN J. Security analysis of a practical on the fly authentication and signature generation[A]. Eurocrypt’1998[C]. Espoo Finland, 1998. 422-436.

[9] HE C,SUNDARARAJAN M,DATTA A. A modular correctness proof of IEEE 802.11i and TLS[A]. CCS2005-12th ACM Conference on Computer and Communications Security[C].Alexandria,VA, United States,2005.2-15.

[10] ROY A,DATTA A, DEREK A. Secrecy analysis in protocol composition logic[A]. The 11th Asian Computing Science Conference [C].Tokyo,Japan,2006.197-213.

[11] DATTA A, ROY A, MITCHELL J. Protocol composition logic(PCL)[J]. Electronic Notes in Theoretical Computer Science, 2007,172(1): 311-358.

[12] CAS C. On the protocol composition logic PCL[A]. Preceedings of 2008 ACM Symposium on Information, Computer and Communications Security[C].Tokyo, Japan, 2008.18-20.