运用SPIN对开放授权协议OAuth 2.0的分析与验证

来源：计算机工程与科学杂志2015年第11期北京时间：

作者：程道雷,肖美华,刘欣倩,梅映天,李伟

单位：（华东交通大学软件学院，江西 南昌 330013）

摘要：OAuth 2.0协议是一种开放授权协议，主要用于解决用户账号关联与资源共享问题。但是，其弱安全性导致各网络公司海量用户信息泄露,且OAuth 2.0传输数据采用的https通道效率低下,成为黑客攻击对象。提出采用http通道传输OAuth 2.0协议数据，基于Promale语言及DolevYao攻击者模型对OAuth 2.0协议建模，运用SPIN进行模型检测。形式化分析结果表明，采用公钥加密体系对OAuth 2.0协议进行加密不安全。上述建模方法对类似的授权协议形式化分析有重要借鉴意义。

关键词：OAuth 2.0协议,信息泄露,公钥加密体系,模型检测,

基金资助：国家自然科学基金资助项目(61163005)；计算机软件新技术国家重点实验室开放课题资助项目(KFKT2012B18)；江西省自然科学基金资助项目(20132BAB201033)；江西省高校科技落地计划项目(KJLD13038)；江西省对外科技合作技术资助项目（20151BDH80005）；华东交通大学研究生创新计划资助项目（YC2014X007）