Analyzed Protocols

In this section you may find all the protocol encodings written until now with a brief description of the related resources (see the download section for information on the rule systems).

protocol type validation rules
Amended Needham-Schroeder
TTP based key-exchange with shared key syntactic analysis
Amended SPLICE/AS
mutual entity and message authentication with public key

type system (typed nonce)

Untyped Amended SPLICE/AS

type system (message)

F Woo-Lam
TTP based unilateral authentication with shared key syntactic analysis

Flawed Example

intended unilateral authentication with shared key

syntactic analysis
Flawed Woo-Lam
intended TTP based unilateral authentication with shared key syntactic analysis

ISO Two-Pass

unilateral authentication with shared key syntactic analysis, type system (entity)

ISO Two-Steps

unilateral authentication with shared key syntactic analysis, type system (entity)
Wide Mouthed Frog
TTP based key-exchange with shared key syntactic analysis
Simplified Woo-Lam
TTP based unilateral authentication with shared key syntactic analysis
Untyped Example
unilateral entity and message authentication with public key type system (message)

Double Tagging Example

unilateral authentication with public key type system (entity)