Nous étudions une propriété de non-interférence temporisée pour les systèmes de sécurité modélisés sous forme d'automates temporisés, dans lesquels un utilisateur de bas niveau de sécurité ne doit pas être en mesure de déduire l'occurrence d'une action d'un niveau de sécurité élevé.

Nous supposons deux modèles d'attaque différents : dans le premier, l'utilisateur malveillant (de bas niveau) a la capacité d'observer totalement l'état du système mais pas de le mémoriser ; dans le deuxième, il ne peut qu'observer partiellement l'état du système mais peut le mémoriser au cours de son exécution.

Nous commençons par présenter une propriété de non-interférence existant dans la littérature garantissant la sécurité du système vis-à-vis du premier modèle d'attaque. Nous montrons que les preuves de décidabilité de cette propriété sont à ce jour incomplètes et en fournissons une nouvelle.

Nous formalisons ensuite une propriété de non-interférence qui garantit la sécurité du système vis-à-vis du second modèle d'attaque et nous prouvons l'indécidabilité de cette propriété lorsque l'attaquant peut avoir une mémoire arbitrairement grande, c'est-à-dire lorsqu'il est capable de mémoriser des séquences d'observations, ainsi que la durée entre deux observations successives, de n'importe quelle longueur. Nous supposons ensuite une mémoire limitée pour l'attaquant et montrons que la propriété peut alors être décidée. Finalement, nous montrons que la propriété peut être décidée avec une complexité PSPACE pour une sous-classe d'automates temporisés assurant une durée finie entre deux observations distinctes mémorisées par l'attaquant.