Hot answers tagged

12

Disclaimer: I use Coq on daily basis... I have seen in some places that people use formal verification and/or computer-aided verification for cryptography. To my knowledge, there aren't that many places that do such a thing. :) First lets make sure we talk about the same concepts: Formal Verification: The act of proving the correctness of ...


8

Just looking for a Turing machine vs circuit is a bit misleading. The important distinction is uniform (complexity class BPP) vs non-uniform (complexity class P/poly) adversaries. You can characterize P/poly in terms of circuit families, but also in terms of Turing machines with arbitrary "advice strings." In fact, the latter is the more traditional ...


3

I am stuck at the point where I proved that the complexity is $O(2^\rho)$ using brute-force approach. How shall I proceed? Well, a proof that assumed a specific attack strategy is of limited use, as that proof would be inapplicable if the attacker used some other strategy. Instead, what we typically do in a proof is assume that the adversary had some ...


3

Your questions can be split in two: What is the meaning of IND-CCA secure? What have an adversary access in a challenger-adversary game? This basically means that the scheme achieves the indistinguishability notion, even if an attacker has access to a decryption oracle. See Easy explanation of "IND-" security notions? for more detail on ...


3

Formal verification is used to verify the security services of your algorithm or your protocol. It uses specific high level modeling specification to specify your security solution and uses a back end formal verification tools to see whether or not there are security breaches or not. The outcome of the formal verification will tell you if your protocol is ...


2

I will answer this part specifically: Are there any practical differences between circuits and turing machines for cryptographic research (i.e. are there systems that are secure against PPT turing machines, but not polynomial-size circuits?) or does it exclusively come down to personal preference / convenience which one you use for your proofs? In ...


1

Here is an example of a proof. This proves why CBC mode needs an IV that is random: (fyi many people think a nonce will suffice, but it won't, it needs to be random) Our definition of a probabilistically secure encryption scheme: Imagine two oracles taking two inputs: a plaintext $P$ and initialization vector $IV$. The 1st oracle $Enc_{k}(P, IV)$ performs ...



Only top voted, non community-wiki answers of a minimum length are eligible