I am trying to understand timer interrupts in Arduino.
I am finding a major difficulty in retrieving documentation.
Sources online refer to apparently "magical" constants (like TIMSK1 for example) but I am unable to find where they are defined.
Do they come from some sort of header file?
Is there some reference documentation anywhere?
You've already answered, but I'd like to fill in some gaps, perhaps.
Those symbols are not magical, they are the names of the processor and I/O registers and values for the bit-fields inside those registers. As you found, the processor datasheet explains the layout of the I/O registers. This is standard for all microcontroller vendors.
Here's the home page for the Mega328P: https://www.microchip.com/en-us/product/ATmega328p since the datasheet PDF might change some day. Note that farther down the page there are many very helpful "application notes" that describe how to do things...
How does a C program, or an Arduino script, get the values of the registers and fields? From the vendor supplied header files. See here for Microchips "packs": http://packs.download.atmel.com
The compiler that comes with the Arduino IDE distribution has included the headers for the boards it supports. They're buried pretty deeply - we go to the datasheet to find the register and field names, not usually to the header files.
For the mega328, the header file is here (macos): ~/Arduino.app/Contents/Java/hardware/tools/avr/avr/include/avr/iom328p.h
I'm not sure why you said "(although not explained in full detail)". There's really not much to it - it just holds a few bits that enable interrupts when certain things happen in Timer/Counter 1.
From the 328P datasheet 01/2015, TIMSK1 is described on page 90 "All interrupts are individually masked with the Timer Interrupt Mask Register (TIMSK1)." The register layout is on page 112. And its position within the I/O register set on page 278. A programmer doesn't need more than that! :-)
(I wish I could attach a pdf... it has a big table of the registers, fields, interrupt vectors, DIP pins, ... all generated from that header file.)