XiaoMi-AI文件搜索系统
World File Search SystemProverif
安全协议验证者proverif及其喇叭子句分辨率算法
安全协议的验证是自1990年代以来非常活跃的研究领域。安全协议无处不在：Internet（特别是用于https：// connections使用的TLS协议），WiFi，移动电话，信用卡，。。。。众所周知，他们的设计容易出错，并且未通过测试检测到错误：仅当对手试图攻击协议时，它们才会出现。因此，正式验证它们很重要。为了使安全协议形式化，需要为其数学模型。通常会考虑一个活跃的对手，可以收听网络上发送的消息，计算自己的媒介，然后将它们发送到网络上，就好像它们来自诚实的参与者一样。为了促进协议的自动验证，大多数协议验证者都考虑了加密的符号模型，也称为“ dolev-yao模型” [18，15]。在此模型中，加密原语（例如加密）被视为理想的黑盒，以功能符号为代表。消息是通过这些原始词的术语建模的；并且对手仅限于应用定义的原语。这也称为完美的加密假设：对手解密消息的唯一途径是将解密函数与正确的密钥一起使用。在这样的模型中，协议验证的主要任务之一是计算对手的知识，即对对手可以获得的一组术语。这仍然是并非繁琐的，因为该集合通常是无限的，但是它比有关斑点和概率的推理要简单得多。两个最广泛使用的符号协议验证者可能是proverif [11]和tamarin [17]。有关协议验证领域的更多详细信息，我们将读者转移到调查[10，6]。在本文中，我们专注于协议验证者proverif，可以从https://proverif.inria.fr下载。我们在下一节中介绍了王朝的概述，并关注其喇叭条款分辨率算法。
hax：使用多个...
摘要。我们提出了HAX，这是针对安全至关重要软件（例如加密库，协议实施，身份验证和授权机制）以及解析和消毒代码的验证工具链。HAX背后的关键思想是务实的观察者，即不同的验证工具可以更好地处理各种验证目标。因此，HAX支持多个证明后端，包括特定领域的安全分析工具，例如Proverif和Sprove，以及Coq和F*等通用证明助理。在本文中，我们介绍了HAX工具链，并展示如何使用它将Rust Code转换为不同抛弃的输入语言。我们描述了我们如何系统地测试翻译模型和生锈系统库的模型，以增强其正确性的信心。最后，我们简要概述了依赖HAX的各种正在进行的验证项目。
Quantum后安全通道协议
摘要。国家机构和组织的过渡不得不授权，通常会涉及一个阶段，其中经典和PQ原语将合并为混合解决方案。在这种情况下，必须对现有协议进行调整，以确保量子阻力在维护其安全目标的同时。这些适应可以显着影响性能，尤其是在设备上。在本文中，我们专注于标准化协议，这些协议支持跨不同模式的ESIM进行应用管理。这是一个复杂的用例，涉及具有严格安全要求的受限设备。我们介绍了所有模式的PQ适应，包括混合和完全PQ版本。使用Proverif，我们提供自动证明，以验证这些PQ变体的安全性。此外，我们分析了在设备上实施PQ协议，运行时和带宽消耗的性能影响。我们的发现突出了与实现ESIM管理后的量词后安全性相关的资源开销。
对标准 QKD 协议的 ETSI 提案进行形式化验证
密钥交换协议允许事先互不相识的双方共享一个公共加密密钥，以便随后交换对称加密消息。当前的密钥交换协议基于公钥加密。因此，它们的安全性基于知道公钥、找到私钥或用公钥加密的密钥的难度。随着量子计算机的出现，当前的非对称算法将不再提供这样的保证 [1]。量子密钥分发协议（量子密钥分发，QKD）的安全性基于量子物理的特性，特别是不可克隆定理 [2]；该定理指出，不可能完美地克隆粒子（量子比特）的量子态。如果攻击者试图读取两个参与者交换的量子比特（通常是光子的偏振态），那么她必然会修改量子态，因此可以即时检测到。然而，QKD 的局限性之一仍然是双方可以交换的最大地理距离，目前为几百公里 [3]。ETSI 提出了 QKD 网络的协议标准 [4]。在这里，我们建议使用 ProVerif 工具对其进行正式验证。
OPC UA
OPC UA是一种旨在确保安全的关键基础架构中的标准化工业控制系统（ICS）协议。即将发布的1.05版包括基础加密设计的重大更改，包括基于Diffie-Hellmann的密钥交换，而不是以前的基于RSA的版本。版本1.05应该提供更强大的安全性，包括完美的前锋保密（PFS）。我们使用最先进的符号协议验证程序proverif对OPC UA V1.05和V1.04中指定的安全协议进行正式安全分析。与以前的研究相比，我们的模型更加全面，包括新协议版本，包括建立安全渠道，会话及其管理的不同子协议的组合，涵盖了大量可能的配置。这导致了有史以来最大的模型之一，这是由于状态机器的复杂性而引起的许多挑战，主要是由于状态机的复杂性。我们讨论了如何缓解这种复杂性以获得有意义的分析结果。我们的分析发现了OPC基金会已报告并承认的几个新漏洞。我们设计并提出了证明是安全的修复程序，其中大多数包含在该标准的即将版本中。
5G-AKA-HPQC：用于量子弹性5G主要身份验证的混合后量子加密协议
摘要-5G通过在我们的日常生活中与各种服务融合，可以作为变革性数字创新的催化剂。这种范式移动的成功无可否认地取决于稳健的安全措施，并具有主要的身份验证 - 符合对5G网络的访问权限 - 至关重要。两个协议，5G身份验证和关键协议（5G-AKA）以及用于身份验证和关键协议Prime（EAP-AKA'）的可扩展的身份验证协议，已为此目的进行了标准化，前者是为第三代合作项目（3GPP）设备设计的，而非3GPP设备的后者则为非3GPP设备。但是，最近的研究暴露了5G-AKA协议中的漏洞，使其容易受到安全漏洞的影响，包括可连接性攻击。此外，量子计算的广告构成了巨大的量子威胁，强调了迫切需要采用抵抗量子的加密机制。尽管已标准化了量子后加密（PQC），但缺乏现实部署限制了其可靠的鲁棒性。相比之下，在数十年的实际应用中，便会加密方案表现出可靠性。为了解决这一差距，互联网工程工作组（IETF）启动了混合PQC算法（HPQC）的标准化，结合了经典和抗量子的技术。因此，确保在5G-AKA协议中确保对量子威胁的前瞻性和弹性至关重要。为了应对这些安全挑战，我们提出了5G-AKA-HPQC协议。结果证实了协议的安全性和正确性。我们的协议旨在通过结合通过椭圆曲线集成的加密方案（ECIE）与源自PQC-key封装机制（KEM）进行协商的密钥来维持与现有标准的兼容性。为了严格而全面地验证5G-AKA-HPQC的安全性，我们采用了正式的验证工具，例如SVO Logic和Proverif。此外，性能评估突出了5G-AKA-HPQC固有的计算和通信开销。此分析表明该协议如何有效地平衡安全性和效率。总而言之，我们的研究提供了对安全，量子安全身份验证协议设计的重要见解，并为移动电信的安全身份验证和关键协议协议的未来标准化奠定了基础。
松鼠供者及其逻辑
1。简介安全协议如今已广泛用于确保通过Internet等公共渠道进行的交易。常见用途包括敏感信息的安全传输，例如信用卡号或系统上的用户身份验证。因为它们在许多广泛使用的应用中存在（例如电子商务，政府发行的ID），开发验证安全协议的方法和工具已成为重要的研究挑战。这样的工具有助于提高我们对协议的信任，从而对依靠它们的应用程序进行信任。正式的方法已经带来了各种方法，以证明加密促进确实保证了预期的安全性。在这一研究领域的一种有效方法是将密码信息作为一阶术语建模，以及代表攻击者能力的方程理论。最初在[Dolev and Yao 1981]中提出的这个想法多年来得到了完善，导致了各种所谓的符号模型。这些模型包括攻击者的广泛类别，并促进了协议的自动验证。他们导致了成功的工具的开发，例如Proverif [Blanchet 2001]和Tamarin [Meier等。2013]。但是，重要的是要注意，符号模型中的安全性并不一定意味着密码师标准模型中的安全性，称为计算模型。与符号模型相比，验证计算模型的验证技术虽然至关重要，但与符号模型相比通常具有较小的灵活性或自动化。 2023]。验证计算模型的验证技术虽然至关重要，但与符号模型相比通常具有较小的灵活性或自动化。2023]。在该模型中，攻击者由概率多项式时间图灵机（PPTMS）表示，并且证明协议与理想化的，显然是安全的版本没有区别。作为一个例证，秘密键是在计算模型中忠实地建模的，因为长斑点是随机均匀绘制的，而它们是在符号模型中使用抽象名称进行建模的。在符号模型中，两个不同的秘密键由不同的名称表示，这些键不能相等。然而，在计算模型中，就像实际上一样，采样的斑点是相等的（尽管不太可能）。在此列中，我们提出了一种基于逻辑的方法，用于验证计算模型中的加密协议，以及在松鼠工具中实现的一些实际方面[Baelde等。2021; Baelde等。该系统建立在[Bana and Comon-Lundh 2012的计算完整符号攻击者（C CSA）方法上； Bana and Comon-lundh 2014]，依赖于逻辑的象征环境，但避免了上述符号模型的局限性。CSA方法不是通过说明对手可以做什么的规则来建模攻击者功能，而是依赖于攻击者无法做的规范。从加密原始图的安全属性开始，人们得出了表达哪些消息序列的规则是无法区分的。这些