next up previous contents
Nächste Seite: Wortbausteine (Atoms) Aufwärts: Spezifizierung eines Protokolls für Vorherige Seite: Übergangsregeln   Inhalt

Operationen

Hier werden die Operationen als Funktionssymbole definiert, die von ehrlichen Teilnehmern als auch von Angreifern ausgeführt werden können. Kann sie vom Angreifer ausgeführt werden, so wird sie mit pen markiert, andernfalls mit nopen. Mit Hilfe der Operationen die der Angreifer ausführen kann, werden weiter Übergansregeln definiert, die zuvor (wie oben beschrieben) noch selbsterstellt werden mussten.


fsd1:pke(X,Y):length(X)=1:length(pke(X,Y))=length(Y):pen.

Der erste Teil steht für ,,function symbol definition``, der Zweite gibt die Operation und deren Argumente, der Dritte die Bedingungen an die Argumente und der Vierte die Länge des entstehenden Wortes an.


2003-01-22