4 ms·

I am one of the authors of the paper. Feel free to ask questions about our work, I'll try to monitor this thread and come back to answer.

by bblipp 7y ago

fuklief 7y ago
The abstract says cryptoverif is a proof assistant, but the cryptoverif page says it's an automatic protocol prover. Which is it ? (my understanding is that a proof assistant is interactive, like Coq, Agda, etc)
- bblipp 7y ago
  CryptoVerif [1] is called “automatic” because 1) it generates intermediate games automatically during the proof [see footnote1 for a brief explanation of “games”]. This is in contrast to the other major tool that works in the computational model, EasyCrypt [2], where the user has to write down these games manually. 2) it has an automatic mode in which the tool is able to perform certain proof steps on its own, using a built-in proof strategy. For “simple” protocols in “simple” attacker models, it can even finish the entire proof automatically, where “simple” depends on the capabilities of CryptoVerif. CryptoVerif also has an interactive mode that allows the user to guide the proof. This is necessary for more complex protocols and attacker models like the one we developed for WireGuard. Once you found the necessary proof steps in interactive mode, you put them into your proof/model file. Then, CryptoVerif can re-check the entire proof in one go. As CryptoVerif only works with protocols, it's not a general proof assistant like for example Coq, and that's why it's sometimes called “protocol prover”. [1] CryptoVerif https://cryptoverif.inria.fr https://cryptoverif.inria.fr [2] EasyCrypt https://www.easycrypt.info/ https://www.easycrypt.info/ [footnote1] “Games” are a concept of the proof technique, which is used to prove cryptographic security: security properties are expressed as a game; if the adversary wins the game, the security property would be broken. We prove that the adversary wins the game only with a negligible probability. We do this by transforming the game more and more, until we reach a game where we can easily prove that the adversary cannot win it, or only with a small (negligible) probability.
  - Loq 7y ago
    “Games” are a ... I think the terminology of games is a bit misleading. A better term would be program but in a (probabilistic) programming language that specifies interaction by message passing (such as process calculi). CryptoVerif outputs what might be seen as program transformations: P = Q such that the probability that a polynomially bounded adversary can 'crack' P is only negligibly different from the probability for Q. This can be seen as a probabilistic generalisation of e.g. the program transformations that an optimising compiler does, except that in compilation you need that P and Q have exactly the same (observable) behaviour. Verifying crypto protocols is essentially the production of a chain P1 = P2 = ... = Pn where P1 is the protocol in question, and Pn is some "obviously secure" protocol (e.g. existence of one-way functions). Note that Pn might be doing something different from P1. What's important is that the probabilities remain 'similar' (this can be made precise). This proves that P1 is as secure as Pn, so we can break the latter if we can break the former. The reason for the "game" terminology is historical. Von Neumann's theory of economic games [1] preceeds the development of programming languages for interactive behaviour [2] by many decades. [1] https://en.wikipedia.org/wiki/Theory_of_Games_and_Economic_Behavior https://en.wikipedia.org/wiki/Theory_of_Games_and_Economic_B... [2] https://en.wikipedia.org/wiki/Process_calculus https://en.wikipedia.org/wiki/Process_calculus
    - bblipp 7y ago
      Games is the terminology of cryptographers, that's why we use it in our work; we need it to interface with this community. The reason this term is used in cryptography might be historical, but also, speaking of an adversary that should not be able to win a security game stays intuitive and thus useful for the definition of security properties. The language of CryptoVerif is a probabilistic process calculus with interaction by message passing. Your description of CryptoVerif's output and the proof technique is accurate, thanks that you detailed it for fellow readers. I like the comparison to optimising compilers. In our case, we look at the distribution of messages that are observable by the adversary, and prove that these distributions are only distinguishable with negligible probability. The computations done are actually changed such that they would no longer be useful in a real-world protocol. Like, in one proof step we replace the result of an encryption by a randomly generated bitstring. And if the encryption scheme is secure, the adversary is not able to distinguish these two cases.
nickpsecurity 7y ago
Props to your team's great work doing useful analysis on an important protocol. I appreciate it. :) I do have some questions about the assurance CryptoVerif provides. I'm a non-mathematician that does research in high-assurance security that tracks formal verification results. What I've read indicates problems can kick in at places like this: 1. The logic or modelling used isn't proven sound. There's been tons of analysis into things like set theory or HOL Light. Is CryptoVerif using a proven logic? 2. Recent designs favor kernelized models where about every step or transition can be proven consistent or just not mess up to begin with. Does CryptoVerif do this or is there a lot of complexity in it? 3. The solvers might themselves make mistakes. One mitigation was them simply driving the steps in 2 that were easy to check and/or providing a log of work for a trusted checker. Any risks on automated part to worry about? 4. Small, verifiable TCB. HOL Light and Milawa were explicitly designed for this. Does CryptoVerif have a trusted checker? Are the design and implementation of above done in a tiny, easy-to-verify fashion? The EasyCrypt paper's comparisons to CryptoVerif and CertiCrypt made me think it doesn't. 5. Verification activities on the code itself, source and/or binary, from static analysis to property-based testing. Empirical evidence suggests these catch problems proofs sometimes miss, esp due to specification errors. Even CompCert had a few. Any of this on CryptoVerif's building blocks? The answers to these questions might be helpful to people interested in boosting the assurance of this or other tools in the future. After all, the proofs can only be as strong as the foundations they're built on.
- bblipp 7y ago
  Thanks for your appreciation :) These are excellent questions, let me come back to them tomorrow.
- bblipp 7y ago
  - CryptoVerif uses a probabilistic process calculus adapted to its use case, detailed in [1]; - There is no verified kernel. All algorithms, including an equational prover for simplification of games, are implemented in ~30k to 40k LOC of OCaml. The correctness of CryptoVerif’s game transformations has been proved manually [1]. A formal link between these proofs and the OCaml code is not established; - During a proof, after each game transformation, CryptoVerif checks a list of invariants. This already allowed to find implementation errors in the past. - There are regression tests using proofs that have been done before with CryptoVerif, with both proofs that are supposed to succeed and proofs that are supposed to fail. To conclude, CryptoVerif has no high-assurance guarantees on its code like Coq and others, but is the only tool that is capable to treat complex real-world protocols. [1] https://prosecco.gforge.inria.fr/personal/bblanche/publications/BlanchetTDSC07.html https://prosecco.gforge.inria.fr/personal/bblanche/publicati...
deleted 7y ago
[deleted]

I am one of the authors of the paper. Feel free to ask questions about our work, I'll try to monitor this thread and come back to answer.

by bblipp 7y ago

I am one of the authors of the paper. Feel free to ask questions about our work, I'll try to monitor this thread and come back to answer.

fuklief 7y ago

The abstract says cryptoverif is a proof assistant, but the cryptoverif page says it's an automatic protocol prover. Which is it ? (my understanding is that a proof assistant is interactive, like Coq, Agda, etc)

bblipp 7y ago
CryptoVerif [1] is called “automatic” because 1) it generates intermediate games automatically during the proof [see footnote1 for a brief explanation of “games”]. This is in contrast to the other major tool that works in the computational model, EasyCrypt [2], where the user has to write down these games manually. 2) it has an automatic mode in which the tool is able to perform certain proof steps on its own, using a built-in proof strategy. For “simple” protocols in “simple” attacker models, it can even finish the entire proof automatically, where “simple” depends on the capabilities of CryptoVerif. CryptoVerif also has an interactive mode that allows the user to guide the proof. This is necessary for more complex protocols and attacker models like the one we developed for WireGuard. Once you found the necessary proof steps in interactive mode, you put them into your proof/model file. Then, CryptoVerif can re-check the entire proof in one go. As CryptoVerif only works with protocols, it's not a general proof assistant like for example Coq, and that's why it's sometimes called “protocol prover”. [1] CryptoVerif https://cryptoverif.inria.fr https://cryptoverif.inria.fr [2] EasyCrypt https://www.easycrypt.info/ https://www.easycrypt.info/ [footnote1] “Games” are a concept of the proof technique, which is used to prove cryptographic security: security properties are expressed as a game; if the adversary wins the game, the security property would be broken. We prove that the adversary wins the game only with a negligible probability. We do this by transforming the game more and more, until we reach a game where we can easily prove that the adversary cannot win it, or only with a small (negligible) probability.
- Loq 7y ago
  “Games” are a ... I think the terminology of games is a bit misleading. A better term would be program but in a (probabilistic) programming language that specifies interaction by message passing (such as process calculi). CryptoVerif outputs what might be seen as program transformations: P = Q such that the probability that a polynomially bounded adversary can 'crack' P is only negligibly different from the probability for Q. This can be seen as a probabilistic generalisation of e.g. the program transformations that an optimising compiler does, except that in compilation you need that P and Q have exactly the same (observable) behaviour. Verifying crypto protocols is essentially the production of a chain P1 = P2 = ... = Pn where P1 is the protocol in question, and Pn is some "obviously secure" protocol (e.g. existence of one-way functions). Note that Pn might be doing something different from P1. What's important is that the probabilities remain 'similar' (this can be made precise). This proves that P1 is as secure as Pn, so we can break the latter if we can break the former. The reason for the "game" terminology is historical. Von Neumann's theory of economic games [1] preceeds the development of programming languages for interactive behaviour [2] by many decades. [1] https://en.wikipedia.org/wiki/Theory_of_Games_and_Economic_Behavior https://en.wikipedia.org/wiki/Theory_of_Games_and_Economic_B... [2] https://en.wikipedia.org/wiki/Process_calculus https://en.wikipedia.org/wiki/Process_calculus
  - bblipp 7y ago
    Games is the terminology of cryptographers, that's why we use it in our work; we need it to interface with this community. The reason this term is used in cryptography might be historical, but also, speaking of an adversary that should not be able to win a security game stays intuitive and thus useful for the definition of security properties. The language of CryptoVerif is a probabilistic process calculus with interaction by message passing. Your description of CryptoVerif's output and the proof technique is accurate, thanks that you detailed it for fellow readers. I like the comparison to optimising compilers. In our case, we look at the distribution of messages that are observable by the adversary, and prove that these distributions are only distinguishable with negligible probability. The computations done are actually changed such that they would no longer be useful in a real-world protocol. Like, in one proof step we replace the result of an encryption by a randomly generated bitstring. And if the encryption scheme is secure, the adversary is not able to distinguish these two cases.

nickpsecurity 7y ago

Props to your team's great work doing useful analysis on an important protocol. I appreciate it. :) I do have some questions about the assurance CryptoVerif provides. I'm a non-mathematician that does research in high-assurance security that tracks formal verification results. What I've read indicates problems can kick in at places like this: 1. The logic or modelling used isn't proven sound. There's been tons of analysis into things like set theory or HOL Light. Is CryptoVerif using a proven logic? 2. Recent designs favor kernelized models where about every step or transition can be proven consistent or just not mess up to begin with. Does CryptoVerif do this or is there a lot of complexity in it? 3. The solvers might themselves make mistakes. One mitigation was them simply driving the steps in 2 that were easy to check and/or providing a log of work for a trusted checker. Any risks on automated part to worry about? 4. Small, verifiable TCB. HOL Light and Milawa were explicitly designed for this. Does CryptoVerif have a trusted checker? Are the design and implementation of above done in a tiny, easy-to-verify fashion? The EasyCrypt paper's comparisons to CryptoVerif and CertiCrypt made me think it doesn't. 5. Verification activities on the code itself, source and/or binary, from static analysis to property-based testing. Empirical evidence suggests these catch problems proofs sometimes miss, esp due to specification errors. Even CompCert had a few. Any of this on CryptoVerif's building blocks? The answers to these questions might be helpful to people interested in boosting the assurance of this or other tools in the future. After all, the proofs can only be as strong as the foundations they're built on.

bblipp 7y ago
Thanks for your appreciation :) These are excellent questions, let me come back to them tomorrow.
bblipp 7y ago
- CryptoVerif uses a probabilistic process calculus adapted to its use case, detailed in [1]; - There is no verified kernel. All algorithms, including an equational prover for simplification of games, are implemented in ~30k to 40k LOC of OCaml. The correctness of CryptoVerif’s game transformations has been proved manually [1]. A formal link between these proofs and the OCaml code is not established; - During a proof, after each game transformation, CryptoVerif checks a list of invariants. This already allowed to find implementation errors in the past. - There are regression tests using proofs that have been done before with CryptoVerif, with both proofs that are supposed to succeed and proofs that are supposed to fail. To conclude, CryptoVerif has no high-assurance guarantees on its code like Coq and others, but is the only tool that is capable to treat complex real-world protocols. [1] https://prosecco.gforge.inria.fr/personal/bblanche/publications/BlanchetTDSC07.html https://prosecco.gforge.inria.fr/personal/bblanche/publicati...

deleted 7y ago

[deleted]