Validating firewalls using flow logics

Citations of this article
Mendeley users who have this article in their library.


The ambient calculus is a calculus of computation that allows active processes to communicate and to move between sites. A site is said to be a protective firewall whenever it denies entry to all attackers not possessing the required passwords. We devise a computationally sound test for validating the protectiveness of a proposed firewall and show how to perform the test in polynomial time. The first step is the definition of a flow logic for analysing the flow of control in mobile ambients; it amounts to a syntax-directed specification of the acceptability of a control flow estimate. The second step is to define a hardest attacker and to determine whether or not there exists a control flow estimate that shows the inability of the hardest attacker to enter; if such an estimate exists, then none of the infinitely many attackers can enter unless they contain at least one of the passwords, and consequently the firewall cannot contain any trap doors. © 2002 Elsevier Science B.V. All rights reserved.




Nielson, F., Nielson, H. R., & Hansen, R. R. (2002). Validating firewalls using flow logics. Theoretical Computer Science, 283(2), 381–418.

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free