2020年8月21日,，計(jì)算機(jī)與信息學(xué)院老師包象琳通過線上（騰訊會議））+線下的形式作題為“關(guān)于比特幣形式化安全性分析方法”的交流報(bào)告,。該報(bào)告是我校物聯(lián)網(wǎng)協(xié)會和中科大區(qū)塊鏈協(xié)會校際交流又一次活動,。報(bào)告由物聯(lián)網(wǎng)工程系劉三民老師主持,，我校計(jì)算機(jī)與信息學(xué)院部分老師、兩個協(xié)會的部分學(xué)生參加了本次交流報(bào)告,。

包象琳老師首先介紹了網(wǎng)絡(luò)安全現(xiàn)狀以及形式化安全分析方法的背景,，并通過案例向大家展示如何對簡單的形式化模型進(jìn)行安全屬性驗(yàn)證的人工推理,。在此基礎(chǔ)上,，重點(diǎn)分析比特幣消息交互模型,、敵手模型的建模過程以及安全屬性的形式化定義過程，并且對比特幣形式化模型的自動化驗(yàn)證結(jié)果進(jìn)行展示,。最后總結(jié)了比特幣形式化安全分析所面臨的困境,。

報(bào)告結(jié)束,，包象琳老師在線回答了學(xué)生的提問，同時(shí)線下與參會老師就區(qū)塊鏈技術(shù)的相關(guān)問題和想法進(jìn)行交流討論,。

（文：劉三民,，包象琳；圖：劉三民,；審核：劉濤 ）