theory Sorts
begin
/*
* Variables are of different sorts:
*
* ~x denotes x:fresh
* $x denotes x:pub
* #i denotes i:temporal
* m denotes m:msg
*
* Temporal variables are typically used to specify the security properties.
* The other sorts appear both in the properties (called "lemmas" in Tamarin)
* and in the rules.
*
* For example:
*/
functions: f/3
rule SillyRuleWithVariablesOfDifferentSorts:
[ Fr(~n), In(X) ] // Generate a nonce n and wait for an arbitrary incoming message X
-->
[ Out(f(~n, X, $P)) ] // Output a function of n, X, and a new public name P
/*
* Public names can be introduced anywhere. In the rule above, when $P is
* encountered, a new public name is defined. See also Example 7.
*/
end