Chip designers outsource chip fabrication to external foundries, but at the risk of IP theft. Logic locking, a promising solution to mitigate this threat, adds extra logic gates (key gates) and inputs (key bits) to the chip so that it functions correctly only when the correct key, known only to the designer but not the foundry, is applied. In this paper, we identify a new vulnerability in all existing logic locking schemes. Prior attacks on logic locking have assumed that, in addition to the design of the locked chip, the attacker has access to a working copy of the chip. Our attack does not require a working copy and yet we successfully recover a significant fraction of key bits from the design of the locked chip only. Empirically, we demonstrate the success of our attack on eight large benchmark circuits from a benchmark suite that has been tailored specifically for logic synthesis research, for two different logic locking schemes. Then, to address this vulnerability, we initiate the study of provably secure logic locking mechanisms. We formalize, for the first time to our knowledge, a precise notion of security for logic locking. We establish that any locking procedure that is secure under our definition is guaranteed to counter our desynthesis attack, and all other such known attacks. We then devise a new logic locking procedure, Meerkat, that guarantees that the locked chip reveals no information about the key or the designer's intended functionality. A main insight behind Meerkat is that canonical representations of boolean functionality via Reduced Ordered Binary Decision Diagrams (ROBDDs) can be leveraged effectively to provide security. We analyze Meerkat with regards to its security properties and the overhead it incurs. As such, our work is a contribution to both the foundations and practice of securing digital ICs.