From Wikipedia, the free encyclopedia
In mathematical logic, a metatheorem is a statement about theorems or about some axiomatic theory. It is crucial to realize that a metatheorm is not a statement in the theory.
[edit] Examples
[edit] Security Property as a Metatheorem
In security protocol analysis using formal methods, a security protocol specification can be seen as a theory and the refinement of this theory would correspond to a theory extension, for instance the addition of new axioms regarding adversary capabilities such as algebraic manipulation of cryptographic terms. These analysis results are usually counter-intuitive and difficult to accomplish without the help of formal methods because a security property is a metatheorem about the security system: it states that the adversary is not able to deduce certain facts (for instance, a session key) from the underlying theory, and adding new adversary capabilities can invalidate the security (see properties below). The concrete implementation of a security protocol is always a refinement of its theory, and therefore an implementation is always suscetible to vulnerabilities that are not present in the security protocol abstract theory. Such vulnerabilities correspond to the invalidation of the metatheorem of the security property.
[edit] Properties
- Metatheorems are not preserved by theory extensions (e.g. after adding new axioms to some theory, the metatheorem may not hold anymore.)
[edit] See also
[edit] References
