We introduce the νspi-calculus that strengthens the notion of “perfect symmetric cryptography” of the spi-calculus by making encryption history dependent. We give our calculus an operational and a static semantics. The latter is a control flow analysis (CFA), defined in the form of a flow logic, and it is proved semantically correct. We then apply our CFA to check security properties; in particular, we show that secrecy à la Dolev–Yao can be expressed in terms of the CFA.
Flow Logic for Dolev-Yao Secrecy in Cryptographic Processes
BODEI, CHIARA;DEGANO, PIERPAOLO;
2002-01-01
Abstract
We introduce the νspi-calculus that strengthens the notion of “perfect symmetric cryptography” of the spi-calculus by making encryption history dependent. We give our calculus an operational and a static semantics. The latter is a control flow analysis (CFA), defined in the form of a flow logic, and it is proved semantically correct. We then apply our CFA to check security properties; in particular, we show that secrecy à la Dolev–Yao can be expressed in terms of the CFA.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
