This answer consists of three parts. The first part comes closest to an actual answer, by referencing an isomorphism testing problem which is harder than graph isomorphism (but sadly not NP-hard). The second part mentions Emil Jeřábek's explanation about why isomorphism will often be in coAM, and how broadly it applies (thereby preventing most natural isomorphism testing problems from being NP-hard). The third part finally mentions some NP-hard equivalence test problems (like the IBDD problem mentioned in the question). It calls them distinction problems, which better captures their real nature (that is different from isomorphism testing problems). The link between these three parts is the role of input encoding and compression, especially if a canonical compression (like the straight line program representation) exists.
This question reminds me of how annoyed I was about an unexpected definition of the ring isomorphism problem by Kayal and Saxena:
Group Isomorphism $\leq_m$ Graph Isomorphism $\leq_m$ Ring Isomorphism. Also Integer Factoring $\leq_m$ Ring Isomorphism [Kayal and Saxena]. Also Graph Automorphism $\leq_m$ Graph Isomorphism.
I was annoyed about Integer Factoring $\leq_m$ Ring Isomorphism, because it used a compressed representation for rings, and hence used an unexpected measure for the length of the input:
The ring is given by addition/mult tables, but these have a canonical compressed representation for rings (because the additive group is Abelian), so the GI-completeness result for finite structures is not relevant.
Even so testing isomorphism for this example (Ring Isomorphism) isn't NP-hard, it is harder than GI, and the can of worms provided by allowing compressed input might make it possible to come up with actual examples of NP-hard isomorphism testing problems. The paper implicitly assumes that the orders $d_k$ and the coefficients $a_{ij}^k$ are encoded in binary representation. But why not use unary representation (less compressed) or straight line program representation (more compressed) instead? The straight line program representation for Abelian groups (only addition, no multiplication) is actually equivalent to binary encoding, so using binary encoding might be indeed justified as a canonical compression here.
Emil Jeřábek's comment about isomorphism being in coAM still applies even to this compressed representation (at least if you ignore the part with the base set). We can randomly select a basis, and everything else is uniquely determined from that basis, so the standard IP protocol works. (There are actually many subtleties, even beyond the proof of claim 3.1.2. $RI\in coAM$ given in the paper, but it is true nevertheless.)
I often learn more from Emil Jeřábek's comments than from the actual answers. He's probably a great teacher, and uses the comments for more interaction with the asker and more focused teaching, than would be possible by a mere static answer.
If we allow straight line program representation as a valid compression of the input, then we can easily come up with many NP-hard equivalence test problems similar to the indexed binary decision diagrams problem given in the question. Asking whether two boolean formulas (given as straight line programs for the free Boolean ring, using the constants $0$, $1$, the unary minus operation, and the binary addition and multiplication operations) are distinct (non-equivalent) is actually NP-complete (and closely related to SAT). One could call this problem of distinguishing two elements of a free algebra given in straight line program representation the slp distinction problem. This problem is undecidable for the free modular lattice (on 4 or more generators). But for undecidable problems, it doesn't even matter whether we compressed the input or not, hence some people wrongly believe that it doesn't matter how the input is encoded (if it is only compressed).
