原文标题:Terrorist Attacks for Fake Exposure Notifications in Contact Tracing Systems
原文地址:https://eprint.iacr.org/2020/1150.pdf
原文作者:Gennaro Avitabile, Daniele Friolo, and Ivan Visconti
笔记作者:qY2jts9hEJGy
新冠病毒全球爆发,为了通知那些与后来检测病毒呈阳性的人有密切接触的个人的风险暴露,谷歌和苹果公司联合开发了 Google-Apple Exposure Notifications (GAEN)系统,被广泛应用,并且最近已经实现了跨境兼容性。包括美国在内的多个国家已经采用了基于GAEN的系统。GAEN允许在政府控制非常低的地方运行分散的联系人跟踪,这使得来自第三方的攻击通常更容易发起,并更难防御。
基于GAEN的接触跟踪系统使用蓝牙低能量(BLE)来检测智能手机之间的近距离接触。每个智能手机都通过BLE广播随机的假名,这些信息与一些加密的元数据一起被智能手机近距离接收。如果公民检测呈阳性,并决定通知其他人,她将上传一组名为临时暴露密钥的密钥TEK,对应于她可能传染的前几天。从TEK开始,可以生成用户在一天中广播的所有假名。然后,这些假名的接收者将设法解密存储的元数据,然后评估风险因素。TEK通过后端服务器分发给用户,后端服务器定期发布数字签名TEK的列表。
针对GAEN的原理,作者建立一个中介自由市场的智能合约,在这个市场上,各方在不认识对方、不见面、不冒被欺骗的风险的情况下,可以滥用GAEN系统的曝光通知程序,以实现对接触者追踪系统实施虚假曝光通知攻击。
作者通过分析GAEN系统工作原理,对比设计了一个基于区块链技术的智能合约Take Tek,将接触者追踪系统中故意散布假消息的攻击者比作智能合约中的Buyer,将上传TEK秘钥的受感染者比作Seller。作者提出了一种与以往研究不同的购买/出售TEK的方法,其主要思想是要求卖家证明与服务器的TLS会话成功地上传了买家的TEK。基于这种设计,作者分别介绍了GANE系统中的TEK交易和如何将智能合约与TLS 回话联系研究,证明攻击的可能性。
每当一个用户检测呈阳性时,她就有权将自己的TEK上传到服务器上,以便通知其他用户有感染的风险。该机制可以实现可以有不同的方式。一个简单的方法包含一个由应用程序生成的代码,该代码首先提供给运行状况操作员,以便在服务器上激活它。然后,一旦服务器授权了代码,应用程序就会将tek和代码一起上传。为了评估传染风险,GAEN提供了适当的方法,将包含最后的tek和相关签名的两个文件作为输入,如果签名没有在谷歌和apple之前已知的公钥下进行验证,则不执行匹配。
名词解释如下:
序号 | 名称 | 简称 |
---|---|---|
1 | buyer | B |
2 | seller | P |
智能合约的功能如下:
攻击概述
包含4个主要的功能函数:
名词解释如下:
序号 | 符号 | 含义 |
---|---|---|
1 | pk~B~ | B的钱包 |
2 | pk~P~ | P的钱包 |
3 | S | Server服务器 |
4 | T~B~:= (tek^B^~i~,date^B^~i~)i∈[n] | tek^B^~i~表示B的第i个TEK,date^B^~i与~表示第i个TEK相关的时间,n的取值小于等于最大TEk |
5 | vk~S~ | 用来认证TEKs签名的密钥 |
6 | t | 卖方P必须提供正确清单和签名的最长时间 |
7 | d~P~ | 卖方P必须存入的价值为抵押品 |
8 | σ~T~ | TEK的签名 |
9 | T= (tek~i~,date~i~)i∈[N] | N表示发布的TEKs的数量 |
协议流程:
Take-TEK攻击依赖于使用数字签名来授权上传,从签名消息中提取公钥也至关重要。作者研究证明了TLS 预言机可以用来向智能合约证明上传已成功执行,而无需依赖TEKs的签名。
1.去中心化预言机
去中心化密钥交换。DECO中的密钥交换机制称为三方握手(3PHS)。包含3个实体,分别为证明者P,验证者V,服务器S。DECO的总体思想是,证明者和验证者在执行某些两方计算之后,计算交换密钥的共享,而服务器计算整个密钥,未区分P和V两个不同的交互实体。
当使用CBC-HMAC时,P和V分别掌握密钥k~p~^MAC^ 和k~v~^MAC^,并有k~p~^MAC^ +k~v~^MAC^=k^MAC^,同时只有P知道k^Enc^。
当使用AES-GCM时,P和V共享相同密钥,并且P和V只知道他们自己共享的密钥,S同时掌握k^Enc^和k^MAC^。
密钥交换工作流程如下:
最后,S计算交换密钥Z=s~S~·Y,P和V分别计算共享密钥Z~p~=s~p~·Y和Z~v~=s~v~·Y~v~,同时又Z=
加密通信。在3PHS阶段结束时,P和V必须使用2PC协议来正确计算MAC和发送到服务器的明文加密,而不向对方透露共享。明文的隐私也得到了保证。对于CBC-HMAC,此类明文的加密由持有加密密钥的P独占计算。
证明。DECO一个重要特点就是是,P可以在零知识的情况下,以一种更有效的方式证明交流记录本上的陈述。作者为了使他们的协议实现目标,不会试图保持转录本的私有性。
作者的目标是让智能合约扮演DECO验证者的角色。通过这种方式,智能合约将能够验证卖方和服务器之间是否进行了预期的通信,并相应地奖励卖方。
作者提出一种方法,将证明者和验证者之间的DECO运行与智能合约的状态联系起来,这样当检测到偏离规定的诚实行为时,智能合约最终将能够作为公正的法官惩罚恶意方。
协议描述。分别定义买方为证明者P,卖方为验证者V,服务器S。密码套件CBC-HMAC的详细攻击过程如下:
P在智能合约上预留时间段t~1~,在此时间段内,DECO协议必须与V和S一起运行,并且兑换奖励所需的数据必须由P发布在智能合约上。如果超时,P将不能再上传。
通过添加保留机制,可以确保恶意V在执行DECO协议运行时不能在智能合约中播放模拟的脚本。
由于服务器和验证程序之间的上传通信仅由单个查询和单个响应组成,因此欺骗验证程序不可能使计时器过期,从而避免在成功完成TEKs上传的同时向验证程序付款。一旦V与P合作建立了一个有效的请求,此时无论V做什么操作,S将独立回复P,并将奖品给V。
在执行3PHS时,P检查握手时V发送的值是否与智能合约上发布的值Y一致。如果不一致,P立即终止操作;如果一致,则参与通信的各方在P生成的上传请求上共同计算MAC。如果通信正常结束,则将以下信息上传至智能合约:
智能合约开始一个时间t~2~,指V显示其秘密S~v~的最大时间。如果V未完成,奖品将自动转移到卖家,如果完成,智能合约将执行以下操作:
智能合约检查消息内容m~c~(从验证程序到服务器)中的字段是否正确(即,存在买方的TEK)、响应消息(从服务器到验证程序)是否正确以及验证MAC~s~(θ~c~,θ~s~)是否等于k^MAC^,若果所有检查通过,则P获得奖品,否则,退回V。
作者以Vaudenay提出的在加密工具和能够执行智能合约的区块链的帮助下,可以针对GAEN系统具体实施攻击为研究内容。设计了Take-TEK攻击模型,详细描述了GAEN系统Teks交易过程,以及将智能合约与TLS会话联系,以此表明攻击的可行性。
安全学术圈招募队友-ing, 有兴趣加入学术圈的请联系secdr#qq.com