Maude> (search)
1 : N(princ-msg(tcs-princ(client-tcs C))& princ-msg(tcs-princ(ts-tcs(TGS-ts TS)))& nonce-msg F1),START-CSE C,START-TGE C,
    T_clientASE_resp C F0,F0 C TS F1
2 : N(princ-msg(tcs-princ(client-tcs C))& encrypt(dbK-key kTS)(shK-msg F2 & princ-msg(tcs-princ(client-tcs C)))& encrypt(
    dbK-key kC)(shK-msg F2 & nonce-msg F1 & princ-msg(tcs-princ(ts-tcs(TGS-ts TS))))),START-CSE C,START-TGE C,
    T_clientASE_resp C F0,F0 C TS F1
3 : START-CSE C,START-TGE C,Auth C(encrypt(dbK-key kTS)(shK-msg F2 & princ-msg(tcs-princ(client-tcs C))))TS F2
4 : N(encrypt(dbK-key kTS)(shK-msg F2 & princ-msg(tcs-princ(client-tcs C)))& encrypt(shK-key F2)(princ-msg(tcs-princ(
    client-tcs C)))& princ-msg(tcs-princ(client-tcs C))& princ-msg(tcs-princ(ts-tcs(server-ts S)))& nonce-msg F4),START-CSE
    C,T_clientTGE_resp C F3,Auth C(encrypt(dbK-key kTS)(shK-msg F2 & princ-msg(tcs-princ(client-tcs C))))TS F2,F3 C S TS F4
5 : N(princ-msg(tcs-princ(client-tcs C))& encrypt(dbK-key kS)(shK-msg F5 & princ-msg(tcs-princ(client-tcs C)))& encrypt(
    shK-key F2)(shK-msg F5 & nonce-msg F4 & princ-msg(tcs-princ(ts-tcs(server-ts S))))),START-CSE C,T_clientTGE_resp C F3,
    Auth C(encrypt(dbK-key kTS)(shK-msg F2 & princ-msg(tcs-princ(client-tcs C))))TS F2,F3 C S TS F4
6 : START-CSE C,Auth C(encrypt(dbK-key kTS)(shK-msg F2 & princ-msg(tcs-princ(client-tcs C))))TS F2,Service C(encrypt(
    dbK-key kS)(shK-msg F5 & princ-msg(tcs-princ(client-tcs C))))S F5
7 : N(encrypt(dbK-key kS)(shK-msg F5 & princ-msg(tcs-princ(client-tcs C)))& encrypt(shK-key F5)(princ-msg(tcs-princ(
    client-tcs C))& time-msg F7)),T_clientCSE_resp C F6,Auth C(encrypt(dbK-key kTS)(shK-msg F2 & princ-msg(tcs-princ(
    client-tcs C))))TS F2,Service C(encrypt(dbK-key kS)(shK-msg F5 & princ-msg(tcs-princ(client-tcs C))))S F5,F6 C S F5 F7(
    encrypt(dbK-key kS)(shK-msg F5 & princ-msg(tcs-princ(client-tcs C))))
8 : N(encrypt(shK-key F5)(time-msg F7)),T_clientCSE_resp C F6,Auth C(encrypt(dbK-key kTS)(shK-msg F2 & princ-msg(tcs-princ(
    client-tcs C))))TS F2,Mem S C F5 F7,Service C(encrypt(dbK-key kS)(shK-msg F5 & princ-msg(tcs-princ(client-tcs C))))S
    F5,F6 C S F5 F7(encrypt(dbK-key kS)(shK-msg F5 & princ-msg(tcs-princ(client-tcs C))))
9 : DoneMut C S F5,Auth C(encrypt(dbK-key kTS)(shK-msg F2 & princ-msg(tcs-princ(client-tcs C))))TS F2,Mem S C F5 F7,Service
    C(encrypt(dbK-key kS)(shK-msg F5 & princ-msg(tcs-princ(client-tcs C))))S F5

Maude> (search !)
1 : DoneMut C S F5,Auth C(encrypt(dbK-key kTS)(shK-msg F2 & princ-msg(tcs-princ(client-tcs C))))TS F2,Mem S C F5 F7,Service
    C(encrypt(dbK-key kS)(shK-msg F5 & princ-msg(tcs-princ(client-tcs C))))S F5

Maude>