• 
    

    
    

      99热精品在线国产_美女午夜性视频免费_国产精品国产高清国产av_av欧美777_自拍偷自拍亚洲精品老妇_亚洲熟女精品中文字幕_www日本黄色视频网_国产精品野战在线观看 ?

      滿足對應(yīng)性屬性的平臺配置證明

      2018-04-12 07:17:54徐明迪高雪原
      計算機應(yīng)用 2018年2期
      關(guān)鍵詞:攻擊者完整性全局

      徐明迪,高 楊,高雪原,張 帆

      (1.武漢數(shù)字工程研究所,武漢 430205; 2.武漢輕工大學(xué) 數(shù)學(xué)與計算機學(xué)院,武漢 430023)(*通信作者電子郵箱whpuzf@whpu.edu.cn)

      0 引言

      遠(yuǎn)程證明是可信計算提供的核心功能之一,能夠為云計算應(yīng)用提供可信的計算環(huán)境。然而,遠(yuǎn)程證明過程中的完整性度量、完整性存儲和完整性報告,都存在著不同程度的安全缺陷[1]。國內(nèi)外眾多學(xué)者對完整性報告協(xié)議(Integrity Report Protocol, IRP)的安全性問題進(jìn)行了廣泛研究[2],發(fā)現(xiàn)該協(xié)議在抵御重放攻擊、篡改攻擊和假冒攻擊上存在安全缺陷。IRP包含了平臺身份證明和平臺配置證明(Platform Configuration Attestation, PCA)。在IRP的平臺配置證明研究方面,文獻(xiàn)[3-4]提出了IRP的平臺配置證明過程存在著平臺配置寄存器(Platform Configuration Register, PCR)可被任意讀寫操作,以及存儲度量日志(Stored Measurement Log, SML)可被任意修改的問題。在IRP形式化建模與驗證方面,Xu等[5]開發(fā)出了基于信息流完整性模型的遠(yuǎn)程證明系統(tǒng)DR@FT,在CW-Lite模型的完整性度量框架基礎(chǔ)上,DR@FT將系統(tǒng)的可信性歸結(jié)為系統(tǒng)狀態(tài)變化的可信性。Arapinis等[6]用Horn子句對TPM的內(nèi)部狀態(tài)寄存器PCR進(jìn)行建模,并分析了PCR狀態(tài)的變化對BitLocker協(xié)議帶來的攻擊。Datta等[7]用LS2系統(tǒng)對靜態(tài)和動態(tài)完整性度量協(xié)議進(jìn)行了形式化建模和證明。

      文獻(xiàn)[8]圍繞授權(quán)策略給出了安全增強后的完整性報告協(xié)議,在協(xié)議應(yīng)答者與平臺配置證明信息之間建立授權(quán)約束,解決包含全局攻擊者和局部攻擊者對IRP的平臺配置證明發(fā)起的四類攻擊,并通過原型系統(tǒng)進(jìn)行了有效驗證,該文側(cè)重通過增加授權(quán)auth防止PCR和SML的篡改和假冒導(dǎo)致破壞平臺配置證明過程的攻擊。針對PCR和SML的篡改和假冒問題,文獻(xiàn)[4]通過安全進(jìn)程代數(shù)對可信計算平臺內(nèi)部子系統(tǒng)之間的安全可復(fù)合性進(jìn)行了理論證明,得出了一些有意義的結(jié)論,但未對授權(quán)操作對應(yīng)的理論問題進(jìn)行探討。

      IRP的參與方包括挑戰(zhàn)者和應(yīng)答者,本文根據(jù)攻擊者所在位置的不同,將攻擊者分為全局攻擊者和局部攻擊者:全局攻擊者通過截獲、篡改、重放等攻擊手段對挑戰(zhàn)者或應(yīng)答者進(jìn)行中間人攻擊、偽裝攻擊和平臺配置隱私竊取等;局部攻擊者對應(yīng)答者所在平臺的完整性度量架構(gòu)(Integrity Measurement Architecture, IMA)和可信平臺模塊(Trusted Platform Module, TPM)發(fā)起攻擊,包括度量與加載時間差(Time of Check Time of Use, TOCTOU)攻擊、信任鏈攻擊和TPM硬件攻擊等[9]。針對IRP中的平臺配置證明存在的安全問題,為從理論上分析和解決該問題,本文擬從對應(yīng)性屬性出發(fā)進(jìn)行安全形式化驗證:首先對形式化描述語言StatVerif進(jìn)行語法擴(kuò)展,增加與完整性度量相關(guān)的構(gòu)造和析構(gòu)算子;然后基于對應(yīng)性屬性給出局部和全局攻擊者的形式化描述,以及全局可靠和局部可靠的條件;最后通過對攻擊者能力進(jìn)行建模,用形式化驗證工具Proverif對IRP的對應(yīng)性進(jìn)行證明,得出有意義的命題結(jié)論。

      1 StatVerif語法擴(kuò)展

      StatVerif演算是對應(yīng)用π演算的擴(kuò)展[10],在其基礎(chǔ)上通過新擴(kuò)展的狀態(tài)進(jìn)程對全局狀態(tài)變量進(jìn)行描述,能夠?qū)Υ嬖谌譅顟B(tài)的安全協(xié)議和系統(tǒng)進(jìn)行建模。在StatVerif演算中,進(jìn)程由項和進(jìn)程算子構(gòu)造而成。其中,項是用來表示數(shù)據(jù),包括變量、名字、構(gòu)造算子和析構(gòu)算子。構(gòu)造算子f(M1,M2,…,Mn)能夠根據(jù)一些已知項構(gòu)造出新項。析構(gòu)算子letx=g(M1,M2,…,Mn) inPelseQ表示進(jìn)行析構(gòu)操作g(M1,M2,…,Mn),若成功則用析構(gòu)結(jié)果替換進(jìn)程P中所有x的出現(xiàn)后再運行進(jìn)程P,否則運行進(jìn)程Q。對于敵手attacker來說,若attacker已知消息m和公鑰pk,那么構(gòu)造算子pencrypt為attacker(m)∧attacker(pk) ? attacker(pencrypt(m,pk)),相應(yīng)地,析構(gòu)算子pdecrypt為attacker(pencrypt(m,pk(sk)))∧attacker(sk) ? attacker(m)。

      與ProVerif相同,StatVerif演算中與密碼相關(guān)的操作是通過構(gòu)造子和析構(gòu)子完成的,除了密碼學(xué)函數(shù)外,本文擴(kuò)展了與平臺配置證明相關(guān)的構(gòu)造算子,見表1。readpcr(x)表示讀取TPM中第x個PCR的值;extendpcr(x,y)表示用y對TPM的第x個PCR進(jìn)行迭代;readsml(x)表示讀取SML中第x個eventlog結(jié)構(gòu);logsml(x)表示用eventlog結(jié)構(gòu)x對SML進(jìn)行追加;eventlog(x1,x2,y1,y2,z)表示構(gòu)造出一個新的eventlog結(jié)構(gòu),(x1,x2,y1,y2,z)分別表示PCR索引、事件類型、事件摘要、事件長度和事件數(shù)據(jù)。

      表1 與完整性度量相關(guān)的構(gòu)造算子Tab. 1 Constructors for integrity measurement

      與完整性度量相關(guān)的析構(gòu)算子見表2。其中:前5條規(guī)則表示通過元組操作從事件日志中獲取單個項;calsml()表示從SML中獲取PCRi對應(yīng)的eventlog結(jié)構(gòu)并對其進(jìn)行迭代計算;checkevent()表示對SML的單個eventlog結(jié)構(gòu)進(jìn)行驗證;checksml()表示對PCR和SML進(jìn)行驗證。

      表2 與完整性度量相關(guān)的析構(gòu)算子Tab. 2 Destructors for integrity measurement

      ProVerif是能夠接收應(yīng)用π演算作為輸入的自動定理證明工具,已被用于驗證各種安全協(xié)議和安全系統(tǒng)的安全屬性,包括可達(dá)屬性(reachability properties)、一致性斷言(correspondence assertions)和可觀察等價性(observational equivalence),這些有助于分析秘密性屬性和認(rèn)證性屬性(secrecy and authentication properties)。文獻(xiàn)[10]指出:ProVerif是有效的,如果ProVerif驗證了安全協(xié)議滿足安全性質(zhì),則安全協(xié)議不存在實際的攻擊序列;同時ProVerif是不完備的,可能產(chǎn)生誤報(false attack),但是實驗證明在實際使用中ProVerif誤報率很低,并且ProVerif輸出非常詳細(xì),適用于檢查是否有誤報發(fā)生。

      2 平臺配置證明安全

      2.1 局部攻擊和全局攻擊

      Sailer等[11]提出的完整性報告協(xié)議見表3,應(yīng)答者PB為了向挑戰(zhàn)者PA證明平臺身份和平臺配置完整性,需要經(jīng)過一系列的協(xié)議交互,其中nonce為不可預(yù)知的隨機數(shù),AIKpriv和AIKpub為證明身份密鑰對,loadkey(AIKpriv)表示從可信平臺模塊TPM中裝載證明身份密鑰AIKpriv,SML為平臺完整性度量的存儲日志,cert(AIKpub)為PrivacyCA向平臺簽發(fā)的AIKpub證書,sign{PCR,nonce}AIKpriv表示用AIKpriv作為私鑰對PCR和收到的隨機數(shù)nonce進(jìn)行簽名。

      表3 TCG完整性報告協(xié)議Tab. 3 TCG integrity report protocol

      在TCG完整性報告協(xié)議中,平臺配置證明涉及到表3中步驟3b、3c以及5b、5c:步驟3b和3c用于獲取應(yīng)答者PB的PCR和SML,步驟5b和5c用于對應(yīng)答者PB的PCR和SML進(jìn)行安全驗證。在應(yīng)答者PB獲得本地平臺PCR和SML的過程中,TCG規(guī)范沒有對PCR和SML的訪問或操作進(jìn)行安全約束,這使得應(yīng)答者PB中的局部攻擊者attackerl可直接進(jìn)行惡意修改或破壞,造成應(yīng)答者PB獲取的PCR和SML的可信狀態(tài)不可控,攻擊路徑見表4和表5;同時,全局攻擊者attackerg能夠直接對明文SML進(jìn)行替換攻擊,導(dǎo)致挑戰(zhàn)者PA對PCR和SML的驗證結(jié)果與應(yīng)答者PB的本地實際狀態(tài)并不一致,攻擊路徑見表6。

      表4 局部攻擊者攻擊PBTab. 4 Local attackers tamper PB

      表5 局部攻擊者欺騙PATab. 5 Local attackers deceit PA

      表6 全局攻擊者攻擊SMLTab. 6 Global attackers tamper SML

      2.2 攻擊者能力建模

      根據(jù)Dolev-Yao模型,攻擊者能夠監(jiān)聽所有消息,通過重寫規(guī)則來修改消息并發(fā)送它所擁有的消息。下面給出攻擊者具有的初始知識Init-adversary的定義。

      定義1令I(lǐng)nit為有限名集,如果Q是不包含事件的閉進(jìn)程且fn(Q)?Init,那么Q為Init-adversary。

      Init表示了攻擊者Q可獲得的初始知識。在完整性報告協(xié)議中,對于平臺配置完整性而言,TPM命令執(zhí)行引擎、BIOS服務(wù)中斷和可信軟件棧(TCG Software Stack, TSS)核心服務(wù)提供者接口都提供了多個直接對PCR和SML進(jìn)行操作的命令,這些命令集合InitPCR和InitSML構(gòu)成了攻擊者Q的初始知識,具體命令見表7。

      從跡語義的角度出發(fā),若一條跡滿足attacker(M),說明攻擊者擁有M,或者M(jìn)被Init中的公有通道發(fā)送;跡滿足message(M,M′),說明消息M′被通過通道M發(fā)送;跡滿足event(M),說明事件event(M)已被執(zhí)行?;谯E的原子語法見表8。

      表7 攻擊者具有的初始知識Tab. 7 Attacker’s initial knowledge

      表8 基于跡的原子語法Tab. 8 Atom grammar based on trace

      定義4X|→f表示:通過已知的事實X能夠獲得事實f,其中|→為推導(dǎo)算子。

      定義5令C為破壞平臺配置證明的攻擊者,那么:

      C=vx.vy.vz.

      letxh=hash(x) in

      letyp=readpcr(y) in

      letzs=eventlog(z) in

      extendpcr(y,yp|xh).logsml(zs).

      通過定義5可以看出,攻擊者通過破壞應(yīng)答者的平臺配置完整性證明過程,最終讓挑戰(zhàn)者認(rèn)為應(yīng)答者的平臺配置完整性不滿足安全約束。攻擊者破壞平臺配置信息有三種方式:攻擊者將構(gòu)造子應(yīng)用在已有的知識上構(gòu)造出新的消息;攻擊者將析構(gòu)子應(yīng)用在已有的消息上分析出新的知識;攻擊者在公共信道上發(fā)送消息和偷聽消息。攻擊者可通過構(gòu)造子、析構(gòu)子、名字生成并形成攻擊者知識,進(jìn)而對平臺配置證明過程進(jìn)行攻擊,攻擊者的構(gòu)造算子和析構(gòu)算子見表9。

      2.3 平臺配置證明的局部攻擊

      通過上文可以看出,在局部和全局攻擊者存在的情況下,應(yīng)答者PB并不能向挑戰(zhàn)者PA證明自身的真實平臺配置信息,原因在于沒有對PCR和SML設(shè)置安全訪問策略,導(dǎo)致了局部攻擊者能夠?qū)CR和SML進(jìn)行任意非授權(quán)寫操作,以及全局攻擊者對明文SML進(jìn)行任意篡改操作,造成了IRP中的應(yīng)答者PB和挑戰(zhàn)者PA之間難以滿足對應(yīng)性關(guān)系。

      平臺配置證明的局部攻擊包括對PCR和SML的攻擊,圖3列出了攻擊者具備的所有對PCR、SML和eventlog的初始知識。這里需要解釋說明的是,在平臺配置證明中,存儲度量日志SML由多個事件結(jié)構(gòu)(Event Structure, ES)組成,每個ESi, j都是一個五元組,包括平臺配置寄存器索引idxi、事件類型typei, j、事件摘要digesti, j、事件長度sizei, j和數(shù)據(jù)eventi, j。其中digesti, j::=hash(eventi, j),挑戰(zhàn)者對接收到的SML進(jìn)行平臺配置證明。圖1給出了應(yīng)答者PB上的局部攻擊者Init-adversary對平臺配置完整性的破壞。

      表9 攻擊者的構(gòu)造子和析構(gòu)子Tab. 9 Attacker’s constructors and destructors

      圖1 攻擊者利用局部接口的平臺配置完整性攻擊Fig. 1 Attacker’s compromising to platform configuration integrity by using local API

      定義6令PA、PB分別表示挑戰(zhàn)者和應(yīng)答者,ζ=ε,S∪{p,s},P表示PB運行協(xié)議時使用的平臺配置,p和s分別表示PCR和SML,那么對PA的認(rèn)證性表示為p,s|→PA:φ。如果PB完成了協(xié)議,那么PB認(rèn)為已經(jīng)給PA發(fā)送了運行協(xié)議時使用的p和s,且PA收到了PB發(fā)送的p和s。

      定義7令PA、PB分別表示挑戰(zhàn)者和應(yīng)答者,p和s分別表示PCR和SML,那么對PB的認(rèn)證性表示為p,s|→PB:φ。如果PA完成了協(xié)議,那么PA獲得的p和s的確是PB發(fā)送出來的。

      文獻(xiàn)[2]提出完整性報告協(xié)議存在平臺替換攻擊,并指出其主要原因是用戶與平臺之間沒有綁定關(guān)系。同樣,在平臺配置證明過程中,PCR和SML的值與平臺之間也沒有綁定關(guān)系,任意主體都能夠?qū)CR和SML進(jìn)行操作,因此,應(yīng)答者PB進(jìn)行平臺配置證明所使用的PCR和SML并不能反映PB當(dāng)前的真實運行狀態(tài)。同時,也無法說明挑戰(zhàn)者PA接收的SML與應(yīng)答者PB的對應(yīng)性。因此,從對應(yīng)性安全屬性出發(fā),定義6和定義7給出了應(yīng)答者PB向挑戰(zhàn)者PA證明自身平臺配置信息需滿足的條件。

      定義8令應(yīng)答者的平臺配置為ζ0=ε0,S0,P0,其中S0包含平臺配置寄存器P和存儲度量日志S,令p、s分別為P和S的當(dāng)前會話實例,若存在locks和lockp,ε0,S0∪{lockp,s},P0→E0,S0,P0∪{p,s},則稱P和S都是寫保護(hù)的。

      通過定義8可以看出,若P和S的當(dāng)前會話實例存在加鎖或者策略保護(hù),那么可以通過加鎖機制或授權(quán)策略機制,實現(xiàn)平臺配置證明過程中p和s對應(yīng)答者保持的唯一性。

      3 滿足對應(yīng)性屬性的平臺配置證明

      安全協(xié)議的認(rèn)證性是用對應(yīng)性進(jìn)行描述的,對應(yīng)性一般使用兩個事件event1(M)和event2(M),它們位于安全協(xié)議不同的角色子進(jìn)程,event1(M)在消息M的發(fā)送者子進(jìn)程中,event2(M)在消息M的接收者子進(jìn)程中。對應(yīng)性又可分為單射對應(yīng)性、非單射對應(yīng)性和一般對應(yīng)性。

      命題1令p和s分別表示PCR和SML,若p,s|→PA:φ且p,s|→PB:φ,則平臺配置證明過程是全局可靠但局部不可靠的。

      從安全協(xié)議的認(rèn)證性角度出發(fā),命題1給出了對挑戰(zhàn)者PA的認(rèn)證性和對應(yīng)答者PB的認(rèn)證性,如果PB運行完了協(xié)議,那么PB認(rèn)為已經(jīng)給PA發(fā)送了正確的SML和PCR,且PA的確收到了PB發(fā)送的SML和PCR;同時,如果PA運行完了協(xié)議,那么PA獲得的SML和PCR的確是PB發(fā)送出來的。

      證畢。

      命題1的現(xiàn)實意義在于,在認(rèn)證性安全屬性約束下,IRP協(xié)議中的變量p和s不會受到全局攻擊,也就是不會出現(xiàn)篡改和假冒攻擊,但是在局部攻擊存在的情況下,p和s并不能代表PB的真實配置情況。

      從命題1可知,p和s的狀態(tài)在全局可靠的情況下存在著局部不可靠的安全隱患,這是由于局部攻擊者具有的初始知識讓p和s的狀態(tài)發(fā)生了改變,而這種狀態(tài)改變在IRP中是無法表達(dá)的,造成局部攻擊者發(fā)起的攻擊難以被發(fā)現(xiàn)。為更好地對平臺配置證明過程進(jìn)行安全描述,下面將用對應(yīng)性屬性描述局部狀態(tài)變化引起的一致性關(guān)系。對應(yīng)性屬性也稱為對應(yīng)性斷言,用于描述多個事件之間發(fā)生的邏輯關(guān)系,即:“如果事件e發(fā)生了,那么事件e′在此之前也發(fā)生了”。下面將通過對應(yīng)性屬性描述平臺配置證明。

      表10 利用局部接口攻擊平臺配置完整性的形式化描述Tab. 10 Formulized description for local compromising to platform configuration integrity

      則平臺配置證明過程存在平臺配置全局攻擊和局部攻擊。

      證明當(dāng)m=1時,

      證畢。

      則平臺配置證明過程存在局部攻擊。

      證明當(dāng)m=1時,

      當(dāng)m>1時,證明過程同上,不再贅述。

      證畢。

      對命題2和命題3的證明采用形式化驗證工具Proverif,證明結(jié)果如下:

      query event(completedA(nonce,pcr,idx1,sml,idx2))==>

      event(startedB(nonce,pcr,sml)).

      The event completedA(n_512,p_513,i_514,s_515,i_516)

      is executed.

      A trace has been found.

      RESULT event(completedA(x_271,y_272,z_273,m_274,

      n_275))==>

      event(startedB(x_271,y_272,m_274)) is false.

      證明從命題條件

      因此平臺配置證明是局部可靠的。

      證畢。

      則稱平臺配置證明是全局可靠的,即

      證明從命題條件

      因此平臺配置證明是全局可靠的。

      證畢。

      對命題4和命題5的證明同樣采用形式化驗證工具Proverif,證明結(jié)果如下:

      Starting query event(completedA(x_265,y_266,z_267,

      m_268,n_269))==>

      event(startedB(x_265,y_266,m_268)).

      goal reachable: begin(startedB(n_9,

      p_10[!1=@sid_476],s_11[!2=@sid_477]->

      end(completedA(n_9,p_10[!1=@sid_476],

      @sid=@sid_476,s_11[!2=@sid_477],

      @sid=@sid_477))

      RESULT event(completedA(x_265,y_266,z_267,m_268,

      n_269))==>

      event(startedB(x_265,y_266,m_268)) is true.

      4 結(jié)語

      針對可信計算的完整性報告協(xié)議存在的安全問題,首先對形式化描述語言StatVerif進(jìn)行了語法擴(kuò)展,增加了與完整性度量相關(guān)的構(gòu)造和析構(gòu)算子,以對IRP進(jìn)行形式化分析。對平臺配置證明安全進(jìn)行分析后,發(fā)現(xiàn)其存在的局部攻擊和全局攻擊問題,通過對攻擊者能力進(jìn)行建模,用形式化驗證工具Proverif對IRP的對應(yīng)性進(jìn)行了證明。

      參考文獻(xiàn):

      [1]徐明迪,張煥國,張帆,等.可信系統(tǒng)信任鏈研究綜述[J].電子學(xué)報,2014,42(10):2024-2031. (XU M D, ZHANG H G, ZHANG F, et al. Survey on chain of trust of trusted system [J]. Acta Electronica Sinica, 2014, 42(10): 2024-2031.)

      [2]馬卓.無線網(wǎng)絡(luò)可信接入理論及其應(yīng)用研究[D].西安:西安電子科技大學(xué),2010:23-44. (MA Z. Trusted access in wireless network theory and applications [D]. Xi’an: Xidian University, 2010: 23-44)

      [3]徐明迪,張煥國,趙恒,等.可信計算平臺信任鏈安全性分析[J].計算機學(xué)報,2010,33(7):1165-1176. (XU M D, ZHANG H G, ZHAO H, et al. Security analysis on trust chain of trusted computing platform [J]. Chinese Journal of Computers, 2010, 33(7): 1165-1176.)

      [4]ZHANG H, YAN F, FU J, et al. Research on theory and key technology of trusted computing platform security testing and evaluation [J]. Science China: Information Sciences, 2010, 53(3): 434-453.

      [5]XU W, ZHANG X, HU H, et al. Remote attestation with domain-based integrity model and policy analysis [J]. IEEE Transactions on Dependable and Secure Computing, 2012, 9(3): 429-442.

      [6]ARAPINIS M, RITTER E, RYAN M D. StatVerif: verification of stateful processes [C]// CSF 2011: Proceedings of the 24th IEEE Computer Security Foundations Symposium. Washington, DC: IEEE Computer Society, 2011: 33-47.

      [7]DATTA A, FRANKLIN J, GARG D, et al. A logic of secure systems and its application to trusted computing [C]// SP 2009: Proceedings of the 30th IEEE Symposium on Security and Privacy. Washington, DC: IEEE Computer Society, 2009: 221-236.

      [8]徐明迪,張煥國,張帆,等.授權(quán)約束下的平臺配置證明研究[J].電子學(xué)報,2017,45(6):1389-1395. (XU M D, ZHANG H G, ZHANG F, et al. Authorization restriction-based platform configuration attestation [J]. Acta Electronica Sinica, 2017, 45(6): 1389-1395.)

      [9]JAIN L, VYAS J. Security analysis of remote attestation, CS259 Project Report [R]. Palo Alto: Stanford University, 2008: 1-8.

      [10]BLANCHET B, ABADI M, FOURNET C. Automated verification of selected equivalences for security protocols [J]. The Journal of Logic and Algebraic Programming, 2008, 75(1): 3-51.

      [11]SAILER R, ZHANG X L, JAEGER T, et al. Design and implementation of a TCG-based integrity measurement architecture [C]// SSYM 2004: Proceedings of the 13th Conference on USENIX Security Symposium. Berkeley, CA: USENIX Association, 2004, 13: 223-238.

      猜你喜歡
      攻擊者完整性全局
      Cahn-Hilliard-Brinkman系統(tǒng)的全局吸引子
      量子Navier-Stokes方程弱解的全局存在性
      稠油熱采水泥環(huán)完整性研究
      云南化工(2021年9期)2021-12-21 07:44:00
      基于微分博弈的追逃問題最優(yōu)策略設(shè)計
      落子山東,意在全局
      金橋(2018年4期)2018-09-26 02:24:54
      正面迎接批判
      愛你(2018年16期)2018-06-21 03:28:44
      莫斷音動聽 且惜意傳情——論音樂作品“完整性欣賞”的意義
      精子DNA完整性損傷的發(fā)生機制及診斷治療
      有限次重復(fù)博弈下的網(wǎng)絡(luò)攻擊行為研究
      新思路:牽一發(fā)動全局
      兴仁县| 若羌县| 绥化市| 太保市| 西昌市| 浠水县| 德令哈市| 灵寿县| 苗栗市| 镇远县| 兖州市| 台东市| 仲巴县| 达拉特旗| 新乡市| 陆良县| 溆浦县| 皮山县| 本溪市| 旌德县| 连江县| 宁晋县| 上栗县| 克山县| 祁东县| 申扎县| 南京市| 绥宁县| 泸州市| 台北市| 安远县| 汨罗市| 西充县| 台中县| 通化市| 贺兰县| 萨迦县| 漳浦县| 格尔木市| 庆城县| 长海县|