基于ASLan++的OAuth2.0協(xié)議授權(quán)碼模型形式化建模與分析

摘要： OAuth2.0協(xié)議被廣泛應(yīng)用的同時(shí)，其安全性備受爭(zhēng)議。針對(duì)授權(quán)碼泄露和跨站請(qǐng)求偽造問題，對(duì)OAuth2.0協(xié)議中的授權(quán)碼模型進(jìn)行安全性研究。根據(jù)OAuth2.0協(xié)議標(biāo)準(zhǔn)，采用形式化建模語言ASLan++對(duì)授權(quán)碼模型中的用戶瀏覽器、第三方應(yīng)用服務(wù)器和授權(quán)服務(wù)器進(jìn)行形式化建模，分析模型的安全目標(biāo)，并采用線性時(shí)態(tài)邏輯描述授權(quán)碼模型的安全性質(zhì)。使用基于SAT的模型檢查器對(duì)授權(quán)碼形式化... （共8頁）