The most straightforward conclusion seems to be that the analysis of a protocol brings about a lot of subtleties. Even for simple protocols like OpenPGP, one should be careful with drawing any conclusions without some proof.
GNY logic gives us a method to define what anyone can know at a given point in the protocol. The logic as described here was not complete; GNY also deals with effects like freshness and "not-originated-from-here" messages, which might be important for some protocols.
Being able to deduce assertions based only on assumptions already defined, and some rules, one is able to analyse a protocol more efficiently. After the analysis is done, one only has to wonder whether the defined assumptions are reasonable, whether the given rules are sound and complete and whether the conclusions are acceptable.
However, even with a protocol proven to be secure in GNY logic, one has to be careful. GNY can only assert as much as its rules allow. There might be other forms of attack (like short time window attacks) that GNY cannot detect (since it only has two timeframes, the present and the past, a fact that hasn't really been shown here). Also, a secure protocol does not mean the implementation is equally secure, or that the users use it in the correct way.
For example, in the course of this project, we discovered a bug in the implementation of OTR in the Mac OS X messaging client Adium. This bug made it impossible to correctly verify that a key fingerprint belongs to the user. Even such a radical bug was unnoticed by the program authors; one should place serious consideration in trusting a party to write secure software. Users that are not careful with their private keys may also form a security risk.
Furthermore, non-reputability as defined by the OTR might not hold in any jurisdiction. While the protocol might provide non-reputability, other aspects like the time a message was sent, logs by providers and the trust in an expert might be enough for a legal system to still accredit someone as the writer of a message in OTR.
Both the OpenPGP and the OTR protocols have their own use. Reputability vs plausible deniability is not a question of good versus bad. One should be aware of the consequences however. Signing a message with your private key in OpenPGP is non-revokable and might be used against you. Also, the OTR protocol is forward secure while OpenPGP messages might be decrypted afterwards, something you might want to keep in mind.
The OTR protocol also has some flaws. However, even with a perfect protocol, one should keep in mind that real security is always in the hands of the users.
The following applets were used for demonstration:
In addition, the following papers were consulted:
Borisov, N., Goldberg, I., and Brewer, E. (2004). Off-the-record communication, or, why not to use PGP. Proceedings of the 2004 ACM workshop on Privacy in the electronic society, pages 77–84.
Burrows, M., Abadi, M., and Needham, R. (1990). A logic of authentication. ACM Transactions on Computer Systems (TOCS), 8(1):18–36.
Di Raimondo, M., Gennaro, R., and Krawczyk, H. (2005). Secure off-the-record messaging. Proceedings of the 2005 ACM workshop on Privacy in the electronic society, pages 81–89.
Gong, L., Needham, R., and Yahalom, R. (1990). Reasoning about belief in cryptographic protocols. Proceedings 1990 IEEE Symposium on Research in Security and Privacy, pages 234–248.