使用Maude进行后量子密钥封装机制的建模和验证
Víctor García1, Santiago Escobar1, Kazuhiro Ogata2
1Universidad Politécnica de Valencia, Valencia, Spain.
PeerJ. Computer science
|October 9, 2023
概括
量子计算威胁着当前的网络安全. 本研究引入了分析后量子密码学的正式框架,揭示了中间人攻击和比特翻转密钥封装中的漏洞.
科学领域:
- 计算机科学 计算机科学
- 密码学 密码学 密码学 密码学
- 信息安全 信息安全
背景情况:
- 当前的通信系统依赖于经典密码学,易受量子计算的影响.
- 国家标准与技术研究所的后量子密码学项目旨在开发抗量子解决方案.
- 正式验证对于评估加密协议的安全性至关重要.
研究的目的:
- 在Maude中开发一个正式的框架来分析后量子密钥封装机制.
- 在Dolev-Yao模型下评估这些机制的安全性.
- 识别漏洞,并为后量子密码学提出解决方案.
主要方法:
- 使用Maude在网络中构建了参与者行为的象征模型.
- 执行可访问性分析以检测安全漏洞.
- 利用莫德线性时间逻辑模型检查器进行安全,活力和公平性分析.
主要成果:
- 确定了影响所有分析后量子密钥封装机制的中间人攻击.
- 在Bit Flipping Key Encapsulation协议中发现了一个设计漏洞.
- 证实安全属性受到损害,而生命力和公平性属性保持.
结论:
- 开发的莫德框架有效地识别了后量子密码学中的安全漏洞.
- 中间人攻击和Bit Flipping Key Encapsulation漏洞需要进一步研究强大的解决方案.
- 正式方法对于确保未来量子抗性加密系统的安全至关重要.
更多相关视频
06:44Quantitative Analysis of Mitochondria-Associated Endoplasmic Reticulum Membrane (MAM) Stabilization in a Neural Model of Alzheimer's Disease (AD)
Published on: January 10, 2025
521
05:51Isotopic Effect in Double Proton Transfer Process of Porphycene Investigated by Enhanced QM/MM Method
Published on: July 19, 2019
6.3K
相关概念视频
The Quantum-Mechanical Model of an Atom
42.4K
Shortly after de Broglie published his ideas that the electron in a hydrogen atom could be better thought of as being a circular standing wave instead of a particle moving in quantized circular orbits, Erwin Schrödinger extended de Broglie’s work by deriving what is now known as the Schrödinger equation. When Schrödinger applied his equation to hydrogen-like atoms, he was able to reproduce Bohr’s expression for the energy and, thus, the Rydberg formula governing hydrogen spectra.
42.4K
Maxam-Gilbert Sequencing
11.2K
In the same year as the discovery of the Sanger sequencing method, another group of scientists, Allan Maxam and Walter Gilbert, demonstrated their chemical-cleavage method for DNA sequencing. The Maxam-Gilbert method relies on using different chemicals that can cleave the DNA sequence at specific sites, the separation of resulting DNA fragments of variable size using electrophoresis, and deciphering the DNA sequence from the resulting gel bands.
Challenges of the Maxam-Gilbert Method
The...
Challenges of the Maxam-Gilbert Method
The...
11.2K
Mechanistic Models: Compartment Models in Algorithms for Numerical Problem Solving
66
Mechanistic models play a crucial role in algorithms for numerical problem-solving, particularly in nonlinear mixed effects modeling (NMEM). These models aim to minimize specific objective functions by evaluating various parameter estimates, leading to the development of systematic algorithms. In some cases, linearization techniques approximate the model using linear equations.
In individual population analyses, different algorithms are employed, such as Cauchy's method, which uses a...
In individual population analyses, different algorithms are employed, such as Cauchy's method, which uses a...
66
Propagation of Uncertainty from Random Error
709
An experiment often consists of more than a single step. In this case, measurements at each step give rise to uncertainty. Because the measurements occur in successive steps, the uncertainty in one step necessarily contributes to that in the subsequent step. As we perform statistical analysis on these types of experiments, we must learn to account for the propagation of uncertainty from one step to the next. The propagation of uncertainty depends on the type of arithmetic operation performed on...
709
Norton's Theorem
609
Norton's theorem is a fundamental principle stating that a linear two-terminal circuit can be substituted with an equivalent circuit, which comprises a current source (ⅠN) in parallel with a resistor (RN). Here, ⅠN represents the short-circuit current flowing through the terminals, and RN stands for the input or equivalent resistance at the terminals when all independent sources are deactivated. This implies that the circuit illustrated in Figure (a) can be exchanged with the...
609
Hückel's Rule Diagram of π MOs: Frost Circle
4.5K
The Frost circle or the inscribed polygon method is a graphical method for determining the relative energies of π molecular orbitals (MOs) for planar, fully conjugated, and monocyclic compounds. This method was first described by A. A. Frost and Boris Musulin in 1953.
A Frost circle is constructed by drawing a polygon whose number of edges is equal to the number of carbons of the given cyclic system, with one of the vertices pointing down. Then, a circle is drawn enclosing the polygon so...
A Frost circle is constructed by drawing a polygon whose number of edges is equal to the number of carbons of the given cyclic system, with one of the vertices pointing down. Then, a circle is drawn enclosing the polygon so...
4.5K
