XiaoMi-AI文件搜索系统
World File Search SystemProver
松鼠供者及其逻辑
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方法不是通过说明对手可以做什么的规则来建模攻击者功能，而是依赖于攻击者无法做的规范。从加密原始图的安全属性开始，人们得出了表达哪些消息序列的规则是无法区分的。这些
协议计算后量子安全性的逻辑和交互式证明器
我们提供了第一个机械化的后量子健全安全协议证明。我们通过开发 PQ-BC（一种对于量子攻击者来说是健全的计算一阶逻辑）和以 PQ-Squirrel 证明器形式提供的相应机械化支持来实现这一目标。我们的工作建立在经典 BC 逻辑 [7] 及其在 Squirrel [5] 证明器中的机械化基础上。我们对 PQ-BC 的开发需要使 BC 逻辑对于单个交互式量子攻击者来说是健全的。我们通过修改 Squirrel、依赖 PQ-BC 的健全性结果并强制执行一组句法条件来实现 PQ-Squirrel 证明器；此外，我们为该逻辑提供了新的策略以扩展该工具的范围。使用 PQ-Squirrel，我们进行了几个案例研究，从而给出了它们的计算后量子安全性的第一个机械证明。其中包括两种基于 KEM 的密钥交换通用构造、两种来自 IKEv1 和 IKEv2 的子协议，以及 Signal 的 X3DH 协议的拟议后量子变体。此外，我们使用 PQ-Squirrel 证明几个经典的 Squirrel 案例研究已经是后量子可靠的。
利用 LLM 聊天机器人对加密协议进行形式化描述
提示︓ 以下是用自然语言编写的Yahalom协议、Needham-Schroeder对称密钥认证协议的描述，以及Tamarin Prover的Needham-Schroeder对称密钥认证协议脚本。请为Tamarin Prover编写一个Yahalom协议的脚本……
基于晶格的签名
在这里，我们要求一些不同的东西：我们希望供奉献者说服verifier供供者知道一些东西。供者说服verifier的x∈X还不够，因此y = f（x）。应确信verifier fifier知道这种解决方案x。我有时会在此处称x为“证人”。甚至开始构建这样的证明系统，我们首先必须回答一个哲学上的问题：“知道某事？”意味着什么？更具体地说，图灵机器“知道某事”是什么意思？在希望构建“知识证明”之前，我们需要定义知识。在这种情况下，加密摄影师为“知识”提出了非常聪明，非常自然的定义。这是事后显而易见的那些定义之一，但在您看到它之前一点都不明显。这个想法是要说一个供者“知道x”，如果它是类似的定义，可能同样适用于定义人类知识。在足够剧烈的相互作用下，可以从摊子中提取X。特别是，我们会说，如果有一种有效的算法，可以从任何贵族p ∗中“提取”证人x，从而使verifier具有良好的可能性“提取”证人x，我们会说一个交互式证明具有知识。为简单起见，我们将自己限制在供者发送第一个消息的三个移动协议中。我们会说，该协议是否可以从这对接受的成绩单中提取证人，可以满足知识的声音。这些有时称为“ Sigma协议”。在这三个移动协议中，我们可以考虑运行P ∗ for-ward以获取一个接受的成绩单（V，C，Z），然后将P ∗重新打开，直到Verifirer向其发出挑战的那一刻，然后在另一个挑战中再次进行挑战，以获得第二个笔录（V，C c'，z'）。
每个人的最佳策略时间表
任何定理供者的大多数组件都可以进行参数化和微调。为参数选择正确的值通常并不容易。通常没有明确的最佳选择，即使有一个总体的非最佳选择，对于某些类型的问题也可能更好。所有暴露参数的特定值选择是一种策略。使用正确的策略在给定超时内解决问题通常至关重要。解决此问题的一种方法是使定理供者向用户展示选项，使他们能够配置使用的策略。这是一个无花果叶：定义正确的策略通常需要对求解器的内部运作的深入了解。此外，供者的开发人员必须设置一个明智的默认值。这也不容易：通常，供奉献的开发人员不知道摊子会遇到的问题类型。默认值通常也应有些通用。总体而言，设计和使用策略是值得关注的主题。由于对于许多问题，有一种可以在短时间内解决问题的策略，因此自然要在该问题上尝试多种策略。最简单的方法是从列表中逐一尝试策略。稍微复杂的是准备一系列策略列表，并配对超时：如果运行更长的时间，可能有些策略会减少回报。我们将这样的列表称为时间表。在本文中，我们提供了一个工具箱来生成和使用时间表。工具箱的核心是一种基于整数编程的方法，可以找到
量子性的深度有效证明 - 研究集锦
量子性证明是一种质询-响应协议，其中经典验证者可以有效地证明不受信任的证明者的量子优势。也就是说，量子证明者可以正确回答验证者的质询并被接受，而任何多项式时间经典证明者都将基于合理的计算假设被高概率拒绝。为了回答验证者的质询，现有的量子性证明通常要求量子证明者执行多项式大小的量子电路和测量的组合。在本文中，我们给出了两种量子性证明构造，其中证明者只需执行恒定深度量子电路（和测量）以及对数深度经典计算。我们的第一个构造是一个通用编译器，它允许我们将所有现有的量子性证明转换为恒定量子深度版本。我们的第二个构造基于舍入问题学习，并且产生的电路深度比通用构造更短，需要的量子位更少。此外，第二种构造对噪声也具有一定的鲁棒性。
确保现有的量子位置验证协议免受任意传输丢失的影响
摘要 当所选协议缺乏损失容忍度时，信号丢失会对量子密码学的安全性构成重大威胁。在量子位置验证 (QPV) 协议中，即使相对较小的丢失率也会危及安全性。因此，目标是找到在实际可实现的丢失率下仍能保持安全的协议。在这项工作中，我们修改了 QPV 协议的通常结构，并证明这种修改使验证者和证明者之间潜在的高传输丢失对于一类协议而言与安全性无关，该类协议包括受 BB84 协议 ( QPV f BB84 ) 启发的实用候选协议。这种修改涉及光子存在检测、证明者的短暂时间延迟以及在继续之前进行游戏的承诺，将总体丢失率降低到仅证明者的实验室。经过调整的协议 c- QPV f BB84 随后成为一种具有强大安全性保证的实用 QPV 协议，即使面对使用自适应策略的攻击者也是如此。由于验证者和证明者之间的丢失率主要由他们之间的距离决定，因此可以在更长的距离上实现安全的 QPV。我们还展示了所需光子存在检测的可能实现，使 c-QPV f BB84 成为解决 QPV 中所有主要实际问题的协议。最后，我们讨论了实验方面并给出了参数估计。