This paper proposes five market models for the procurement of flexibility by transmission (TSO) and distribution system operators (DSOs), based on several TSO-DSO coordination schemes, including a disjoint distribution, disjoint transmission, common, fragmented, and multi-level market. The properties of these models are then analyzed. In particular, the common market is first proven to be more efficient than the other market models. Then, different methods are proposed to adequately price TSO/DSO interface flows, when procuring cross-grid flexibility. It is then shown that, when interface flows are optimally priced, the fragmented and multi-level market solutions converge to those of the common market, reaching optimal efficiency. To prevent the need for any network information sharing among system operators in the different coordination schemes, decomposition methods based on bi-level programming and the alternating direction method of multipliers (ADMM) are proposed. A developed case study, considering an interconnected transmission-distribution system, corroborates the mathematical findings by highlighting the greater efficiency of the common market, the effect of adequate interface pricing on reducing procurement costs, and the capability of the decomposition methods to reach optimal market solutions with limited information exchange.