Non-interference ensures no unauthorized data leaks during system execution. Verifying security policies is complex, requiring analysis of multiple execution paths. Hyperproperties provide a framework to describe security policies like non-interference. However, existing methods like HyperLTL are limited to finite-state models. This paper introduces a case study illustrating the use of HyperFOLTL, designed for infinite-state systems, and presents a formal approach to verify security policies in such systems.