Symbolic approaches have proved their usefulness for analyzing security protocols. Automatic tools have been often used for discovering previously unknown flaws. Abstracting messages by terms seems to be a good level of abstraction since it is possible to show that security proof in symbolic models actually implies stronger guarantees in computational models under classical assumptions under the implementation of the primitives.rnThere are still several open directions of research. Symbolic approaches currently allow to check classical security properties such as confidentiality and authentication. For more recent protocols such as e-voting protocols and contract-signing protocols, the properties that should be achieved are more involved and cannot be encoded in existing tools. In addition, these recent protocols make use of less classical primitives such as re-randomizable encryption scheme or blind signatures. New decision techniques have to be developed for these particular primitives and security properties.rnBridging the gap between symbolic and computation models is a promising line a research since it enables to prove strong security guarantees, benefiting from the simplicity of symbolic models. However, current results require strong assumptions on the security of the cryptographic primitives (e.g. IND-CCA2 encryption schemes). Weaker security assumptions like IND-CPA secure encryption schemes may not suffice to ensure security of protocols. Using weaker encryption schemes may thus require to adapt both symbolic models and protocols accordingly.
展开▼
