A previous study showed how control ow analysis can be applied to analyse key distribution protocols based on symmetric key cryptography. We have extended both the theoretical treatment and our fully automatic verifier to deal with protocols based on asymmetric cryptography. This paper reports on the application of our technique exemplified on the Beller-Chang-Yacobi MSR protocol, which uses both symmetric and asymmetric cryptography and show how we discover an undocumented flaw.
Control Flow Analysis Can Find New Flaws Too
BODEI, CHIARA;DEGANO, PIERPAOLO;
2004-01-01
Abstract
A previous study showed how control ow analysis can be applied to analyse key distribution protocols based on symmetric key cryptography. We have extended both the theoretical treatment and our fully automatic verifier to deal with protocols based on asymmetric cryptography. This paper reports on the application of our technique exemplified on the Beller-Chang-Yacobi MSR protocol, which uses both symmetric and asymmetric cryptography and show how we discover an undocumented flaw.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.
