Using logics to detect implementation-dependent flaws [cryptographic protocol design]

Vulnerabilities may be introduced at all stages of cryptographic protocol design. Reasoning about a protocol at a functional level does not unveil flaws which are inherently implementation-dependent. This paper uncovers a potential implementation-dependent flaw in a previously published protocol. Formal techniques should be able to analyse protocols with respect to such flaws. The epistemic logic CKT5 is modified and shown to operate at a sufficiently detailed bevel to capture implementation-dependent flaws