Related Research Articles
In computer science, formal methods are mathematically rigorous techniques for the specification, development, analysis, and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.
Electronic design automation (EDA), also referred to as electronic computer-aided design (ECAD), is a category of software tools for designing electronic systems such as integrated circuits and printed circuit boards. The tools work together in a design flow that chip designers use to design and analyze entire semiconductor chips. Since a modern semiconductor chip can have billions of components, EDA tools are essential for their design; this article in particular describes EDA specifically with respect to integrated circuits (ICs).
In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification. This is typically associated with hardware or software systems, where the specification contains liveness requirements as well as safety requirements.
In cryptography, a zero-knowledge proof or zero-knowledge protocol is a method by which one party can prove to another party that a given statement is true, while avoiding conveying to the verifier any information beyond the mere fact of the statement's truth. The intuition underlying zero-knowledge proofs is that it is trivial to prove the possession of certain information by simply revealing it; the challenge is to prove this possession without revealing the information, or any aspect of it whatsoever.
In cryptography, a password-authenticated key agreement (PAK) method is an interactive method for two or more parties to establish cryptographic keys based on one or more party's knowledge of a password.
A system architecture is the conceptual model that defines the structure, behavior, and more views of a system. An architecture description is a formal description and representation of a system, organized in a way that supports reasoning about the structures and behaviors of the system.
In computer science and mathematical logic, satisfiability modulo theories (SMT) is the problem of determining whether a mathematical formula is satisfiable. It generalizes the Boolean satisfiability problem (SAT) to more complex formulas involving real numbers, integers, and/or various data structures such as lists, arrays, bit vectors, and strings. The name is derived from the fact that these expressions are interpreted within ("modulo") a certain formal theory in first-order logic with equality. SMT solvers are tools that aim to solve the SMT problem for a practical subset of inputs. SMT solvers such as Z3 and cvc5 have been used as a building block for a wide range of applications across computer science, including in automated theorem proving, program analysis, program verification, and software testing.
Distance bounding protocols are cryptographic protocols that enable a verifier V to establish an upper bound on the physical distance to a prover P.
In computer networking, an Ethernet frame is a data link layer protocol data unit and uses the underlying Ethernet physical layer transport mechanisms. In other words, a data unit on an Ethernet link transports an Ethernet frame as its payload.
Non-interactive zero-knowledge proofs are cryptographic primitives, where information between a prover and a verifier can be authenticated by the prover, without revealing any of the specific information beyond the validity of the statement itself. This makes direct communication between the prover and verifier unnecessary, effectively removing any intermediaries.
In cryptography, the Fiat–Shamir heuristic is a technique for taking an interactive proof of knowledge and creating a digital signature based on it. This way, some fact can be publicly proven without revealing underlying information. The technique is due to Amos Fiat and Adi Shamir (1986). For the method to work, the original interactive proof must have the property of being public-coin, i.e. verifier's random coins are made public throughout the proof protocol.
ProVerif is a software tool for automated reasoning about the security properties of cryptographic protocols. The tool has been developed by Bruno Blanchet and others.
Quantum cryptography is the science of exploiting quantum mechanical properties to perform cryptographic tasks. The best known example of quantum cryptography is quantum key distribution, which offers an information-theoretically secure solution to the key exchange problem. The advantage of quantum cryptography lies in the fact that it allows the completion of various cryptographic tasks that are proven or conjectured to be impossible using only classical communication. For example, it is impossible to copy data encoded in a quantum state. If one attempts to read the encoded data, the quantum state will be changed due to wave function collapse. This could be used to detect eavesdropping in quantum key distribution (QKD).
PragmaDev Studio is a modeling and testing software tool introduced by PragmaDev in 2002 dedicated to the specification of communicating systems. It was initially called Real Time Developer Studio or RTDS. Its primary objective was to support SDL-RT modeling technology. Since V5.0 launched on October 7, 2015 RTDS is called PragmaDev Studio, and it is organized in four independent modules: Specifier, Developer, Tester and Tracer. V5.1 launched on November 29, 2016 introduces a freemium licensing model.
RIPE Atlas is a global, open, distributed Internet measurement platform, consisting of thousands of measurement devices that measure Internet connectivity in real time.
Tamarin Prover is a computer software program for formal verification of cryptographic protocols. It has been used to verify Transport Layer Security 1.3, ISO/IEC 9798, DNP3 Secure Authentication v5, WireGuard, and the PQ3 Messaging Protocol of Apple iMessage.
Algorand is a cryptocurrency protocol providing pure proof-of-stake on a blockchain. Algorand's native cryptocurrency is called ALGO.
Kyber is a key encapsulation mechanism (KEM) designed to be resistant to cryptanalytic attacks with future powerful quantum computers. It is used to establish a shared secret between two communicating parties without an (IND-CCA2) attacker in the transmission system being able to decrypt it. This asymmetric cryptosystem uses a variant of the learning with errors lattice problem as its basic trapdoor function. It won the NIST competition for the first post-quantum cryptography (PQ) standard. NIST calls its draft standard Module-Lattice-Based Key-Encapsulation Mechanism (ML-KEM).
IoT forensics is a branch of digital forensics that has the goal of identifying and extracting digital information from devices belonging to the Internet of things field, using a forensically sound and legally acceptable process.
Nervos Network is a proof-of-work blockchain platform which consists of multiple blockchain layers that are designed for different functions. The native cryptocurrency of this layer is called CKB. Smart contracts and decentralized applications can be deployed on the Nervos blockchain. The Nervos Network was founded in 2018.
References
- ↑ Dowling, Benjamin; Rösler, Paul; Schwenk, Jörg (2020), "Flexible Authenticated and Confidential Channel Establishment (fACCE): Analyzing the Noise Protocol Framework", Lecture Notes in Computer Science, Cham: Springer International Publishing, pp. 341–373, doi:10.1007/978-3-030-45374-9_12, hdl: 20.500.11850/399156 , ISBN 978-3-030-45373-2 , retrieved 2024-05-17
- ↑ Kobeissi, Nadim; Nicolas, Georgio; Bhargavan, Karthikeyan (June 2019). "Noise Explorer: Fully Automated Modeling and Verification for Arbitrary Noise Protocols". 2019 IEEE European Symposium on Security and Privacy (EuroS&P). IEEE: 356–370. doi:10.1109/eurosp.2019.00034. ISBN 978-1-7281-1148-3.
