[WIP]: Add sections on formal verification and Tamarin #12
Conversation
|
|
|
||
| ## Ideal use case | ||
|
|
||
| - If you need to define custom primitives or prove more complex security properties. |
There was a problem hiding this comment.
Period should be a comma:
properties, not supported by
| #### Include function signatures with descriptive type names when declaring new functions | ||
|
|
||
| We recommend always including the full function signature when introducing new functions. This makes function | ||
| definitions easier to parse, allows you to take full advantage of Tamarin's build-in typing checking, and avoid |
| reviewing in a language understood by the tool, and we also need to describe the security properties that we would like | ||
| the protocol to have. The tool will then automatically search for a formal proof that the properties we have specified | ||
| are upheld by the protocol, and if it terminates, it will output either a proof showing that the properties hold, or a | ||
| counterexample showing how some property fails to hold. |
There was a problem hiding this comment.
It might be worth highlithing somehwere that Cryptoverif doesn't find attacks/counter-examples when it can't find a proof. At the same time, when if it doesn't find a proof that doesn't necesariy imply insecurity.
| **Anyone who is composing different cryptographic primitives (like encryption, signatures, and hashes) in a way that has | ||
| not been previously specified by a standards document like an IETF RFC or NIST standard, and has not been analyzed in a | ||
| public academic paper, is designing a new cryptographic protocol.** |
| bitstrings, and the adversary is modeled as an arbitrary probabilistic polynomial-time Turing Machine. The probability | ||
| of the attacker successfully breaking the security of a given primitive has to be provided up-front by the user. The |
There was a problem hiding this comment.
I thinking this part could use same treatment as in the symbolic model("On the one hand, it provides clean
abstractions that allows us to specify the high-level building blocks of cryptographic protocols without having to worry
too much about how each cryptographic primitive is implemented"). The reasoning is: in some sense the probability of breaking a primitive isn't really a "responsiblity" of the user. That probability or advantage can be arbitary and Cryptoverif will find a proof(if possible) regardless. What the user should specify is the abstract security guarantee of the primitive which includes an advantage that can be arbitrary. So in this way cryptoverif allows to work with clean abstractions say of an AEAD and the real instanciation is given by the advantage. In the end, the advantages become important later for evaluating the concerete security. This might also be a good warning to users to carefully interpret these results.
| The output is given as a bound on the probability of a successful attack as a function of the security parameters of the | ||
| individual primitives used, and the number of protocol executions. A key benefit of the computational model is that this |
There was a problem hiding this comment.
"Function of the advantages of the individual primitives" might work better here. In practice there's mainly a single security parameter for the entire protocol. AFAIK, by default Cryptoverif performs a concrete analysis rather than asympotic one, which would also justify omitting security parameters from the discussion.
| The computational model is clearly more expressive than the symbolic model. However, it is also presupposes a deep | ||
| understanding of provable security and game-based proofs, which is not required when working in the symbolic model. | ||
|
|
||
| Ultimately, which tool to use depends as much on your background as on the protocol you are trying to analyze. If you |
There was a problem hiding this comment.
Should we consider framing them as complementary? I probably need to re-read again, but currently, it reads as if the tools are, to some extent, opposites.
Maybe we can point out that (as already done now) thatfor most users, especially those with little cryptographic analysis background, symbolic tools will provide the most value very fast. On the other hand, one could do everything in the computational model, but that’s painful. Power users like Inria tend to do tons of symbolism first and conclude the analysis with computational.
| components, or sub-protocols, like _registering a new device_ or _sending and receiving a single message_, and try to | ||
| prove that these individual components provide the expected security guarantees. | ||
|
|
||
| This approach clearly limits what the attacker can do since each sub-protocol is analyzed in a vacuum. However, it makes |
There was a problem hiding this comment.
This could also be a great place to highlight the complementarity of tools. In the computation model we can find composability results allowing to easily break down protocols in subprotocol withouth worrying about composition. So if such a composition result exist it's nice then to focus symbolic effort on a subprotocol without worrying either.
|
|
||
| # Tamarin | ||
|
|
||
| Tamarin is a symbolic verification tool that can be used to model the security properties of cryptographic protocols. |
There was a problem hiding this comment.
Include a link to the tool here
| leaked at some time `#i` before `#j`." | ||
|
|
||
| Terms may be composed using functions. These are either user defined, or defined by importing a predefined theory (known as a `builtin`). | ||
|
|
There was a problem hiding this comment.
Can we get a very simple example before we continue? I think readers would like to know what they're getting into =)
| This section presents a number of tools that can be used to formally verify | ||
| cryptographic protocols. It currently covers the symbolic protocol verifier | ||
| Tamarin, but our long-term goal is to cover both symbolic and computational | ||
| verifiers. For each tool, we go though: |
| ## Linear and persistent facts | ||
|
|
||
| By default, Tamarin rules consume the set of input facts when they are executed. This means that if the global state is | ||
| given by `{DeviceState(~x, pk(~x)), F(~y)}` and we execute the following rule, then `Fr(~y)` would be consumed and the |
There was a problem hiding this comment.
DeviceState(~x, pk(~x)), F(~y) -> DeviceState(~x, pk(~x)), Fr(~y)
Do not merge.
This PR is a WIP and adds content on formal verification in general and Tamarin in particular.