A Logic and an Interactive Prover for the Computational Post-Quantum Security of Protocols.
该论文提出了首个面向协议计算后量子安全性的机械化证明体系。核心贡献是设计了一个新的计算一阶逻辑 PQ-BC，该逻辑相对量子攻击者是可靠的，并基于此实现了机械化证明工具 PQ-SQUIRREL（通过修改经典的 SQUIRREL 证明器并加入新
#security-protocol
共收录 5 条相关情报。
← 返回所有主题Secure Long-Range Autonomous Valet Parking: A Reservation Scheme With Three-Factor Authentication and Key Agreement
远程自主代客泊车（LAVP）系统旨在缓解城市交通拥堵与停车困难，但大规模停车需求下的预约服务面临身份合法性和通信安全方面的挑战。现有方案大多聚焦于停车请求验证和入场检查，未能充分保护乘客上下车过程中的身份认证与会话安全。针对这一问题，论文提
Practical EMV Relay Protection.
本论文针对 EMV 非接触式支付系统中存在的中继攻击（relay attack）问题展开研究。中继攻击允许攻击者在持卡人与读卡器之间转发消息，从而在用户不知情的情况下完成支付，例如通过无线方式窃取资金。论文首先评估了现有的防护措施：Appl
The Secrets Must Not Flow: Scaling Security Verification to Large Codebases.
现有程序验证器能够证明安全协议实现的高级属性，但由于需要大量人工努力，难以扩展到大型代码库。针对这一挑战，本文提出了一种名为Diodon的新方法。Diodon通过将代码库分割为协议实现（核心）和其余部分（应用程序）来解决扩展性问题。这种分割
Pepper: High-bandwidth and Scalable Anonymous Broadcast with Cryptographic Privacy
本文提出Pepper，一种高带宽匿名广播协议，针对全局敌手提供加密发送者匿名性。Pepper基于双服务器DC-net架构，但引入三项关键创新：1）使用可验证分布式点函数的自包含匿名注册子协议，无需外部拨号服务；2）通过分布式多点函数支持批量