3 ms·

“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 speci

by 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.

by Loq 7y ago

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.