Towards Secrecy for Rewriting in Weakly Adhesive Categories

Inspired by the scope extrusion phenomenon of name passing calculi that allow to reason about knowledge of (secret) names, we propose an abstract formulation of the concept of secret in any weakly adhesive category. The guiding idea is to mark part of a system state as visible or publicly accessible; further, in principle, something that has become public knowledge will stay accessible indefinitely.The main technical contribution consists in providing a proof which shows that a recently proposed categorical construction, which produces a category having monomorphisms as objects and pullback squares as morphisms, preserves weak adhesivity. Finally we sketch how it is possible to verify certain secrecy properties using unfolding based verification approaches that lately have been generalized to rewriting systems in weakly adhesive categories