The basis of IBC is the ability to verify in the on-chain consensus ruleset of chain _B_ that a message packet received on chain _B_ was correctly generated on chain _A_. This establishes a cross-chain linearity guarantee: upon validation of that packet on chain _B_ we know that the packet has been executed on chain _A_ and any associated logic resolved (such as assets being escrowed), and we can safely perform application logic on chain _B_ (such as generating vouchers on chain _B_ for the chain _A_ assets which can later be redeemed with a packet in the opposite direction).
It is possible to make use of the structure of BFT consensus to construct extremely lightweight and provable messages _U<sub>h'</sub>_ and _X<sub>h'</sub>_. The implementation of these requirements with Tendermint consensus is defined in Appendix E. Another algorithm able to provide equally strong guarantees (such as Casper) is also compatible with IBC but must define its own set of update and change messages.
The merkle proof _M<sub>k,v,h</sub>_ is a well-defined concept in the blockchain space, and provides a compact proof that the key value pair (_k, v)_ is consistent with a merkle root stored in _H<sub>h</sub>_. Handling the case where _k_ is not in the store requires a separate proof of non-existence, which is not supported by all merkle stores. Thus, we define the proof only as a proof of existence. There is no valid proof for missing keys, and we design the algorithm to work without it.
Establishing a bidirectional initial root-of-trust between the two blockchains (_A_ to _B_ and _B_ to _A_) — _HA<sub>h</sub>_ and _CA<sub>h</sub>_ stored on chain _B_, and _HB<sub>h</sub>_ and _CB<sub>h</sub_ stored on chain _A_ — is necessary before any IBC packets can be sent.
Any header may be from a malicious chain (e.g. shadowing a real chain state with a fake validator set), so a subjective decision is required before establishing a connection. This can be performed permissionlessly, in which case users later utilizing the IBC channel must check the root-of-trust themselves, or authorized by on-chain governance.
We define two messages _U<sub>h</sub>_ and _X<sub>h</sub>_, which together allow us to securely advance our trust from some known _H<sub>n</sub>_ to some future _H<sub>h</sub>_ where _h > n_. Some implementations may require that _h = n + 1_ (all headers must be processed in order). IBC implemented on top of Tendermint or similar BFT algorithms requires only that Δ_<sub>vals</sub>(C<sub>n</sub>, C<sub>h</sub> ) < ⅓_ (each step must have a change of less than one-third of the validator set)[[4](./references.md#4)].
Either requirement is compatible with IBC. However, by supporting proofs where _h_-_n > 1_, we can follow the block headers much more efficiently in situations where the majority of blocks do not include an IBC packet between chains _A_ and _B_, and enable low-bandwidth connections to be implemented at very low cost. If there are packets to relay every block, these two requirements collapse to the same case (every header must be relayed).
Since these messages _U<sub>h</sub>_ and _X<sub>h</sub>_ provide all knowledge of the remote blockchain, we require that they not just be provable, but also attributable. As such, any attempt to violate the finality guarantees in headers posted to chain _B_ can be submitted back to chain _A_ for punishment, in the same manner that chain _A_ would independently punish (slash) identified Byzantine actors.
Define _max(T)_ as _max(h, where H<sub>h</sub>_∈_T)_. For any _T_ with _max(T) = h-1_, there must exist some _X<sub>h </sub>|<sub> </sub>U<sub>h</sub>_ so that _max(update(T, X<sub>h </sub>|<sub> </sub>U<sub>h </sub>)) = h_.
By induction, there must exist a set of proofs, such that _max(update…(T,...)) = h+n_ for any n.
Bisection can be used to discover this set of proofs. That is, given _max(T) = n_ and _valid(T, X<sub>h </sub>|<sub> </sub>U<sub>h </sub>) = unknown_, we then try _update(T, X<sub>b </sub>|<sub> </sub>U<sub>b </sub>)_, where _b = (h+n)/2_. The base case is where _valid(T, X<sub>h </sub>|<sub> </sub>U<sub>h </sub>) = true_ and is guaranteed to exist if _h=max(T)+1_.
IBC implementations may optionally include the ability to close an IBC connection and prevent further header updates, simply causing _update(T, X<sub>h </sub>|<sub> </sub>U<sub>h </sub>)_ as defined above to always return _false_.
Closing a connection may break application invariants (such as fungiblity - token vouchers on chain _B_ will no longer be redeemable for tokens on chain _A_) and should only be undertaken in extreme circumstances such as Byzantine behavior of the connected chain.
Closure may be permissioned to an on-chain governance system, an identifiable party on the other chain (such as a signer quorum, although this will not work in some Byzantine cases), or any user who submits a connection-specific fraud proof of Byzantine behavior. When a connection is closed, application-specific measures may be undertaken to recover assets held on a Byzantine chain. We defer further discussion to { an appendix }.
