rollback_car_attack_proverif

Rollback 攻击形式化验证 ProVerif 对汽车遥控钥匙上 Rollback 攻击的概念验证（CVE-2022-37418、CVE-2022-36945 和 CVE-2022-37305），详见1 免责声明 我与 1 的作者没有任何关联。感谢他们使其论文开放获取。 ProVerif 安装 官方方式 要运行 ProVerif 形式化验证 PoC，请先按照官方网站上的说明安装 ProVerif。 预编译二进制 另外，我预编译了适用于 amd64 架构 Linux 的静态二进制文件，可在仓库的发布页面获取，同时还有适用于 Windows 的可执行文件。...

Cryptographic Choreographies

We present CryptoChoreo, a choreography language for the specification of cryptographic protocols. Choreographies can be regarded as an extension of Alice-and-Bob notation, providing an intuitive high-level view of the protocol as a whole rather than specifying each protocol role in isolation. Th...

Active Attack Resilience in 5G: a New Take on Authentication and Key Agreement

As 5G networks expand into critical infrastructure, secure and efficient user authentication is more important than ever. The 5G-AKA protocol, standardized by 3GPP in TS 33.501, is central to authentication in current 5G deployments. It provides mutual authentication, user privacy, and key secrec...

One for All: Formally Verifying Protocols Which Use Aggregate Signatures (Extended Version)

Aggregate signatures are digital signatures that compress multiple signatures from different parties into a single signature, thereby reducing storage and bandwidth requirements. BLS aggregate signatures are a popular kind of aggregate signature, deployed by Ethereum, Dfinity, and Cloudflare...