ABSTRACT

The paper presents first how we can compute sheaf tools for accomplishing our goals, i.e. a method of authentication by sheaves. By handling the concepts of Goguen, the behaviour of a system is computed in the internal language of a (pre)sheaf topos. Non-interference by Goguen is also computed in the internal language of a presheaf topos by using predicates.