theory Tuples
begin
/*
* The pair/2 function can be used to compose messages (think of it as
* concatenation of messages). Instead of repeated application of pair/2, you
* may use <...>. The functions fst/1 and snd/1 can be used to extract parts
* of a composite message. For example:
*/
rule R1:
[ Fr(~a), Fr(~b) ]
-->
/*
* In this example, we do not want the attacker to interfere. So, instead
* of sending the message to the public channel with Out(), we define a
* custom fact that establishes a private secure channel, inaccessible to
* the adversary.
*/
[ PrivChannel(<~a, 'C', ~b>) ] // Symbols in quotes denote global constants
rule R2:
[ PrivChannel(tuple) ]
--[ Snd(fst(snd(tuple))) ]-> // Extract the second component of the 3-tuple
[ ]
// Verify that the tuple is processed correctly:
lemma R2_extracts_the_second_component:
" ∀ t #i. Snd(t) @ i ⇒ t = 'C' "
/*
* Btw, Tamarin accepts Unicode symbols for the logical connectives
* (if you know how to input them in your editor!)
*/
end