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

fmod PROTOCOL-EXAMPLE-ALGEBRAIC is protecting PROTOCOL-EXAMPLE-SYMBOLS .
eq exp ( exp ( W:Gen , Y:NeNonceSet ) , Z:NeNonceSet ) = exp ( W:Gen , Y:NeNonceSet * Z:NeNonceSet ) [ variant ] .
eq e ( K:Key , d ( K:Key , M:Msg ) ) = M:Msg [ variant ] .
eq d ( K:Key , e ( K:Key , M:Msg ) ) = M:Msg [ 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:NeNonceSet), 
   -(NS1:NeNonceSet), 
   +(NS1:NeNonceSet * NS2:NeNonceSet), nil]  & 
:: nil ::
[ nil | 
   -(GE:GenvExp), 
   -(NS1:NeNonceSet), 
   +(exp(GE:GenvExp, NS1:NeNonceSet)), 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 = 
:: r1:Fresh ::
[ nil | 
   -(ANAME1:Name ; BNAME:Name ; XEB:Exp), 
   +(ANAME1:Name ; BNAME:Name ; exp(g, n(BNAME:Name, r1:Fresh))), 
   -(e(exp(XEB:Exp, n(BNAME:Name, r1:Fresh)), S:Secret)), nil]  & 
:: r:Fresh,r':Fresh ::
[ nil | 
   +(ANAME:Name ; BNAME:Name ; exp(g, n(ANAME:Name, r:Fresh))), 
   -(ANAME:Name ; BNAME:Name ; XEA:Exp), 
   +(e(exp(XEA:Exp, n(ANAME:Name, r:Fresh)), sec(ANAME:Name, r':Fresh))), nil] [nonexec].
var LIST : SMsgList-R . var K : IntruderKnowledge . var S : StrandSet . eq ATTACK-STATE(0)= 
:: r1:Fresh ::
[ nil, 
   -(a ; b ; XEB:Exp), 
   +(a ; b ; exp(g, n(b, r1:Fresh))), 
   -(e(exp(XEB:Exp, n(b, r1:Fresh)), sec(a, r':Fresh))) | nil] 
|| empty
|| 
nil
|| 
nil
|| never((S & 
:: r:Fresh,r':Fresh ::
[ nil, 
   +(a ; b ; exp(g, n(a, r:Fresh))), 
   -(a ; b ; XEA:Exp), 
   +(e(exp(XEA:Exp, n(a, r:Fresh)), sec(a, r':Fresh))) | nil] ) || K)[nonexec].
 eq ATTACK-STATE(1)= 
:: r1:Fresh ::
[ nil, 
   -(a ; b ; XEB:Exp), 
   +(a ; b ; exp(g, n(b, r1:Fresh))), 
   -(e(exp(XEB:Exp, n(b, r1:Fresh)), sec(a, r':Fresh))) | nil] 
|| 
sec(a, r':Fresh) inI
|| 
nil
|| 
nil
|| 
nil[nonexec].
 endfm
select MAUDE-NPA .