Nächste Seite: Wortbausteine (Atoms)
Aufwärts: Spezifizierung eines Protokolls für
Vorherige Seite: Übergangsregeln
  Inhalt
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