Sketches of Expected Theorems and Proofs

In the following, some theorems are sketched that should be provable if the formalization is adequate. 

This subsection sketches theorems that are not specific to signature schemes. 

if the requirements are restricted to temporal logic, general temporal validity (i.e., the fact that a formula holds for all sequences over the given domain) should trivially imply security validity with every degree of security. 

As to proof rules, modus ponens is not trivial. It can be seen as a test for robust classes of very small functions Let requirements / i, / 2 and R = (Ri - R2) be given. Modus ponens means that the validity of R and R for a scheme with a certain degree of security implies the validity of R2. For given parameters A, sys pars, and i group, let Pj, P2, and P denote the probabilities P 5(5ys pars, i group) for the respective requirements. Obviously, (1 - P2) (1 - Pj) + (1 - P). Hence modus ponens can be used if the sum of two very small functions is still very small . 

Whenever a requirement holds for a scheme in the interest of a certain interest group, it also holds in the interest of any larger interest group with the same degree of security. This should be clear because more entities are correct if the interest group is larger, and correct entities are a special case of an attacker strategy. 

---