Strong Normalization of Extended Calculus of Constructions (CC with cumulative universes)
I guess this is just an extension of my comment, but I've heard Luo cite Goguen's paper The metatheory of UTT which uses typed operational semantics. I'm afraid I can't find a free online version though, and typed operational semantics doesn't exactly take all the sting from the technical hassles.

A completely different, and IMO under-appreciated paper is Sacchini &amp; Gregoire's On Strong Normalization of the Calculus of Constructions with Type-Based Termination, which treats a system with Prop + 1 universe and natural numbers. Already a feat!

Addressing your other concerns: Weak normalization does imply consistency! I don't think it's significantly easier to prove than strong normalization, though, so usually people will go for gold and try to prove SN directly. It's a well-known conjecture that weak normalization implies strong normalization in "reasonable" theories anyways.

If you're only interested in consistency, you might try building a model of your theory directly! This seems to be quite a bit easier than normalization, and might be seen as a stepping stone if you're going to try to build a proof yourself. One reference I enjoy is  Werner and Lee Proof-irrelevant model of CC with predicative induction and judgmental equality
. I think this easily generalizes to cumulative universes. And if you think their construction is technical, imagine the full normalization proof!