fmod PROTOCOL-EXAMPLE-SYMBOLS is protecting DEFINITION-PROTOCOL-RULES .
sorts Name  Nonce  MultipliedNonces  Generator  Exp  Key  GeneratorOrExp  Secret .
subsorts Generator  Exp < GeneratorOrExp .
subsorts Exp < Key .
subsorts Name  Generator < Public .
subsorts Nonce < MultipliedNonces .
ops a  b  i : -> Name .
ops e  d : Key  Msg -> Msg [ frozen ] .
op _;_ : Msg  Msg -> Msg [ gather  (  e  E  )  frozen ] .
op _*_ : MultipliedNonces  MultipliedNonces -> MultipliedNonces [ assoc  comm  frozen ] .
op g : -> Generator .
op exp : GeneratorOrExp  MultipliedNonces -> Exp [ frozen ] .
op n : Name  Fresh -> Nonce [ frozen ] .
op sec : Name  Fresh -> Secret [ frozen ] .
subsorts Name  Nonce  MultipliedNonces  Generator  Exp  Key  GeneratorOrExp  Secret < Msg .
op _$;_ : Msg Msg -> Msg [ctor gather(e E) frozen].
endfm

fmod PROTOCOL-EXAMPLE-ALGEBRAIC is protecting PROTOCOL-EXAMPLE-SYMBOLS .
eq exp ( exp ( G:Generator , Y:MultipliedNonces ) , Z:MultipliedNonces ) = exp ( G:Generator , Y:MultipliedNonces * Z:MultipliedNonces ) [ variant ] .
endfm
fmod PROTOCOL-SPECIFICATION is protecting PROTOCOL-EXAMPLE-SYMBOLS .
protecting DEFINITION-PROTOCOL-RULES .
protecting DEFINITION-CONSTRAINTS-INPUT .
eq STRANDS-DOLEVYAO = 
:: nil ::
[ nil | 
   +(g), nil]  & 
:: nil ::
[ nil | 
   +(NAME:Name), nil]  & 
:: nil ::
[ nil | 
   -(M2:Msg), 
   -(M1:Msg), 
   +(M1:Msg ; M2:Msg), nil]  & 
:: nil ::
[ nil | 
   -(K:Key), 
   -(M:Msg), 
   +(e(K:Key, M:Msg)), nil]  & 
:: nil ::
[ nil | 
   -(K:Key), 
   -(M:Msg), 
   +(d(K:Key, M:Msg)), nil]  & 
:: nil ::
[ nil | 
   -(NS2:MultipliedNonces), 
   -(NS1:MultipliedNonces), 
   +(NS1:MultipliedNonces * NS2:MultipliedNonces), nil]  & 
:: nil ::
[ nil | 
   -(GE:GeneratorOrExp), 
   -(NS1:MultipliedNonces), 
   +(exp(GE:GeneratorOrExp, NS1:MultipliedNonces)), nil]  & 
:: nil ::
[ nil | 
   -(M1:Msg ; M2:Msg), 
   +(M1:Msg), nil]  & 
:: nil ::
[ nil | 
   -(M1:Msg ; M2:Msg), 
   +(M2:Msg), nil]  & 
:: r:Fresh ::
[ nil | 
   +(n(i, r:Fresh)), nil] [nonexec].
eq STRANDS-PROTOCOL = 
:: r2:Fresh ::
[ nil | 
   -(A1Name:Name ; BName:Name ; XEB:Exp), 
   +(A1Name:Name ; BName:Name ; exp(g, n(BName:Name, r2:Fresh))), 
   -(e(exp(XEB:Exp, n(BName:Name, r2:Fresh)), S:Secret)), nil]  & 
:: r1:Fresh,r3:Fresh ::
[ nil | 
   +(AName:Name ; BName:Name ; exp(g, n(AName:Name, r1:Fresh))), 
   -(AName:Name ; BName:Name ; XEA:Exp), 
   +(e(exp(XEA:Exp, n(AName:Name, r1:Fresh)), sec(AName:Name, r3:Fresh))), nil] [nonexec].
var LIST : SMsgList-R . var K : IntruderKnowledge . var S : StrandSet . eq ATTACK-STATE(0)= 
:: r2:Fresh ::
[ nil, 
   -(a ; b ; XEB:Exp), 
   +(a ; b ; exp(g, n(b, r2:Fresh))), 
   -(e(exp(XEB:Exp, n(b, r2:Fresh)), sec(a, r3:Fresh))) | nil] 
|| empty
|| 
nil
|| 
nil
|| never((S & 
:: r1:Fresh,r3:Fresh ::
[ nil, 
   +(a ; b ; exp(g, n(a, r1:Fresh))), 
   -(a ; b ; XEA:Exp), 
   +(e(exp(XEA:Exp, n(a, r1:Fresh)), sec(a, r3:Fresh))) | nil] ) || K)[nonexec].
 endfm
select MAUDE-NPA .