Browse Source

Import of originally published version of isabelle-ofmc.

master
Achim D. Brucker 11 years ago
commit
0407d94abd
52 changed files with 12743 additions and 0 deletions
  1. +1
    -0
      AUTHORS
  2. +35
    -0
      COPYING
  3. +3
    -0
      ChangeLog
  4. +12
    -0
      README
  5. +0
    -0
      bin/.empty
  6. +19
    -0
      examples/AnB/Bilateral-Key_Exchange.AnB
  7. +284
    -0
      examples/AnB/Bilateral-Key_Exchange.fp
  8. +24
    -0
      examples/AnB/Denning-Sacco.AnB
  9. +213
    -0
      examples/AnB/Denning-Sacco.fp
  10. +18
    -0
      examples/AnB/ISOpubKeyOnePassUnilateralAuthProt.AnB
  11. +222
    -0
      examples/AnB/ISOpubKeyOnePassUnilateralAuthProt.fp
  12. +15
    -0
      examples/AnB/ISOsymKeyTwoPassUnilateralAuthProt.AnB
  13. +154
    -0
      examples/AnB/ISOsymKeyTwoPassUnilateralAuthProt.fp
  14. +19
    -0
      examples/AnB/WideMouthFrog.AnB
  15. +209
    -0
      examples/AnB/WideMouthFrog.fp
  16. +26
    -0
      examples/AnB/nsl-ks.AnB
  17. +401
    -0
      examples/AnB/nsl-ks.fp
  18. +18
    -0
      examples/AnB/nsl.AnB
  19. +275
    -0
      examples/AnB/nsl.fp
  20. +608
    -0
      examples/Bilateral-Key_Exchange.thy
  21. +488
    -0
      examples/Denning-Sacco.thy
  22. +484
    -0
      examples/ISOpubKeyOnePassUnilateralAuthProt.thy
  23. +376
    -0
      examples/ISOsymKeyTwoPassUnilateralAuthProt.thy
  24. +83
    -0
      examples/IsaMakefile
  25. +76
    -0
      examples/ROOT.ML
  26. +466
    -0
      examples/WideMouthFrog.thy
  27. +38
    -0
      examples/document/root.tex
  28. +814
    -0
      examples/nsl-ks.thy
  29. +592
    -0
      examples/nsl.thy
  30. +95
    -0
      src/IsaMakefile
  31. +75
    -0
      src/ROOT.ML
  32. +82
    -0
      src/config.sml
  33. +82
    -0
      src/config.sml.in
  34. +68
    -0
      src/encoder/anb2thy.cm
  35. +323
    -0
      src/encoder/ml-yacc-lib/base.sig
  36. +118
    -0
      src/encoder/ml-yacc-lib/join.sml
  37. +83
    -0
      src/encoder/ml-yacc-lib/lrtable.sml
  38. +566
    -0
      src/encoder/ml-yacc-lib/parser2.sml
  39. +29
    -0
      src/encoder/ml-yacc-lib/root.sml
  40. +43
    -0
      src/encoder/ml-yacc-lib/stream.sml
  41. +208
    -0
      src/encoder/ofmc-fp.grm
  42. +54
    -0
      src/encoder/ofmc-fp.grm.sig
  43. +1434
    -0
      src/encoder/ofmc-fp.grm.sml
  44. +131
    -0
      src/encoder/ofmc-fp.lex
  45. +2223
    -0
      src/encoder/ofmc-fp.lex.sml
  46. +137
    -0
      src/encoder/ofmc_abstraction.sml
  47. +138
    -0
      src/encoder/ofmc_connector.sml
  48. +70
    -0
      src/encoder/ofmc_encoder.sml
  49. +489
    -0
      src/encoder/ofmc_thygen.sml
  50. +117
    -0
      src/encoder/ofmcfp.sml
  51. +57
    -0
      src/encoder/root.sml
  52. +148
    -0
      src/ofmc.thy

+ 1
- 0
AUTHORS View File

@@ -0,0 +1 @@
Achim D. Brucker <brucker@member.fsf.org>

+ 35
- 0
COPYING View File

@@ -0,0 +1,35 @@
Isabelle-OFMC --- Connecting OFMC and Isabelle/HOL
==================================================

Copyright (c) 2009 Achim D. Brucker, Germany

All rights reserved.

Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are
met:

* Redistributions of source code must retain the above copyright
notice, this list of conditions and the following disclaimer.

* Redistributions in binary form must reproduce the above
copyright notice, this list of conditions and the following
disclaimer in the documentation and/or other materials provided
with the distribution.

* Neither the name of the copyright holders nor the names of its
contributors may be used to endorse or promote products derived
from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.


+ 3
- 0
ChangeLog View File

@@ -0,0 +1,3 @@

2009-11-02 Achim D. Brucker <brucker@member.fsf.org>
* Isabelle/OFMC: first public release (development version)

+ 12
- 0
README View File

@@ -0,0 +1,12 @@
Isabelle/OFMC - Linking OFMC and Isabelle/HOL
=============================================

This is a developer release for Isabelle/OFMC, i.e., while it may be
of interested to experts, it is not yet useable by the general
public. This development version comprises a small set of Isabelle
theories and a prototypical tool, called anb2thy. Using OFMC's
fixed-point module, anb2thy generates Isabelle theory files for
protocols that haven been successfully validated by OFMC.



+ 0
- 0
bin/.empty View File


+ 19
- 0
examples/AnB/Bilateral-Key_Exchange.AnB View File

@@ -0,0 +1,19 @@
Protocol: BilateralKeyExchange
Types: Agent A,B;
Number NA,NB;
Symmetric_key K;
Function pk,f
Knowledge: A: A,B,pk(A),pk(B),inv(pk(A)),f;
B: A,B,pk(A),pk(B),inv(pk(B)),pk,f
Actions:
B->A: B,{NB,B}pk(A)
A->B: {f(NB),NA,A,K}pk(B)
B->A: {|f(NA)|}K
Goals:
A *->* B: K

+ 284
- 0
examples/AnB/Bilateral-Key_Exchange.fp View File

@@ -0,0 +1,284 @@
Backend: Open-Source Fixedpoint Model-Checker version 2009c
Protocol: BilateralKeyExchange
Types:
[(Purpose,["purposeK"]),(Agent False False,["A","B"]),(Number,["NA","NB"]),(SymmetricKey,["K"]),(Function,["pk","f"])]
section rules:
step rule_0:
iknows(crypt(K,M));
iknows(inv(K))

=>
iknows(M)

step rule_1:
iknows(crypt(inv(K),M));
iknows(K)

=>
iknows(M)

step rule_2:
iknows(scrypt(K,M));
iknows(K)

=>
iknows(M)

step rule_3:
iknows(pair(M1,M2))

=>
iknows(M1);
iknows(M2)

step rule_4:
secret(M,Agent (honest a));
iknows(M)

=>
attack(pair(secrecy,M))

step rule_5:
request(A,B,Purpose (purposeNB),M,(SID sid))
| B/=Agent (dishonest i);
M/=Nonce (absNB(pair(B,A)))
=>
attack(pair(authentication,pair(A,pair(B,M))))

step rule_6:
request(A,B,Purpose (purposeNA),M,(SID sid))
| B/=Agent (dishonest i);
M/=Nonce (absNA(pair(B,A)))
=>
attack(pair(authentication,pair(A,pair(B,M))))

step rule_7:
request(A,B,Purpose (purposeK),M,(SID sid))
| B/=Agent (dishonest i);
M/=SymKey (absK(pair(B,A)))
=>
attack(pair(authentication,pair(A,pair(B,M))))

step rule_8:
State (rB,[Agent (B),Step 0,inv(pk(Agent (B))),pk(Agent (B)),pk(Agent (A)),Agent (A),(SID sid)])

=>
State (rB,[Agent (B),Step 1,inv(pk(Agent (B))),pk(Agent (B)),pk(Agent (A)),Agent (A),Nonce (absNB(pair(Agent (B),Agent (A)))),pair(Agent (B),crypt(pk(Agent (A)),pair(Nonce (absNB(pair(Agent (B),Agent (A)))),Agent (B)))),(SID sid)]);
iknows(pair(Agent (B),crypt(pk(Agent (A)),pair(Nonce (absNB(pair(Agent (B),Agent (A)))),Agent (B)))))

step rule_9:
State (rA,[Agent (A),Step 0,inv(pk(Agent (A))),pk(Agent (B)),pk(Agent (A)),Agent (B),(SID sid)]);
iknows(Agent (B));
iknows(crypt(pk(Agent (A)),pair(Nonce (NB),Agent (B))))

=>
secret(SymKey (absK(pair(Agent (A),Agent (B)))),Agent (B));
witness(Agent (A),Agent (B),Purpose (purposeK),SymKey (absK(pair(Agent (A),Agent (B)))));
State (rA,[Agent (A),Step 1,inv(pk(Agent (A))),pk(Agent (B)),pk(Agent (A)),Agent (B),Nonce (NB),crypt(pk(Agent (A)),pair(Nonce (NB),Agent (B))),pair(Agent (B),crypt(pk(Agent (A)),pair(Nonce (NB),Agent (B)))),Nonce (absNA(pair(Agent (A),Agent (B)))),SymKey (absK(pair(Agent (A),Agent (B)))),crypt(pk(Agent (B)),pair(f(Nonce (NB)),pair(Nonce (absNA(pair(Agent (A),Agent (B)))),pair(Agent (A),SymKey (absK(pair(Agent (A),Agent (B)))))))),(SID sid)]);
iknows(crypt(pk(Agent (B)),pair(f(Nonce (NB)),pair(Nonce (absNA(pair(Agent (A),Agent (B)))),pair(Agent (A),SymKey (absK(pair(Agent (A),Agent (B)))))))))

step rule_10:
State (rA,[Agent (A),Step 0,inv(pk(Agent (A))),pk(Agent (B)),pk(Agent (A)),Agent (B),(SID sid)]);
iknows(Agent (B));
iknows(pk(Agent (A)));
iknows(Nonce (NB))

=>
secret(SymKey (absK(pair(Agent (A),Agent (B)))),Agent (B));
witness(Agent (A),Agent (B),Purpose (purposeK),SymKey (absK(pair(Agent (A),Agent (B)))));
State (rA,[Agent (A),Step 1,inv(pk(Agent (A))),pk(Agent (B)),pk(Agent (A)),Agent (B),Nonce (NB),crypt(pk(Agent (A)),pair(Nonce (NB),Agent (B))),pair(Agent (B),crypt(pk(Agent (A)),pair(Nonce (NB),Agent (B)))),Nonce (absNA(pair(Agent (A),Agent (B)))),SymKey (absK(pair(Agent (A),Agent (B)))),crypt(pk(Agent (B)),pair(f(Nonce (NB)),pair(Nonce (absNA(pair(Agent (A),Agent (B)))),pair(Agent (A),SymKey (absK(pair(Agent (A),Agent (B)))))))),(SID sid)]);
iknows(crypt(pk(Agent (B)),pair(f(Nonce (NB)),pair(Nonce (absNA(pair(Agent (A),Agent (B)))),pair(Agent (A),SymKey (absK(pair(Agent (A),Agent (B)))))))))

step rule_11:
State (rA,[Agent (A),Step 0,inv(pk(Agent (A))),pk(Agent (B)),pk(Agent (A)),Agent (B),(SID sid)]);
iknows(Agent (B));
iknows(Agent (A));
iknows(Nonce (NB))

=>
secret(SymKey (absK(pair(Agent (A),Agent (B)))),Agent (B));
witness(Agent (A),Agent (B),Purpose (purposeK),SymKey (absK(pair(Agent (A),Agent (B)))));
State (rA,[Agent (A),Step 1,inv(pk(Agent (A))),pk(Agent (B)),pk(Agent (A)),Agent (B),Nonce (NB),crypt(pk(Agent (A)),pair(Nonce (NB),Agent (B))),pair(Agent (B),crypt(pk(Agent (A)),pair(Nonce (NB),Agent (B)))),Nonce (absNA(pair(Agent (A),Agent (B)))),SymKey (absK(pair(Agent (A),Agent (B)))),crypt(pk(Agent (B)),pair(f(Nonce (NB)),pair(Nonce (absNA(pair(Agent (A),Agent (B)))),pair(Agent (A),SymKey (absK(pair(Agent (A),Agent (B)))))))),(SID sid)]);
iknows(crypt(pk(Agent (B)),pair(f(Nonce (NB)),pair(Nonce (absNA(pair(Agent (A),Agent (B)))),pair(Agent (A),SymKey (absK(pair(Agent (A),Agent (B)))))))))

step rule_12:
State (rB,[Agent (B),Step 1,inv(pk(Agent (B))),pk(Agent (B)),pk(Agent (A)),Agent (A),Nonce (NB),pair(Agent (B),crypt(pk(Agent (A)),pair(Nonce (NB),Agent (B)))),(SID sid)]);
iknows(crypt(pk(Agent (B)),pair(f(Nonce (NB)),pair(Nonce (NA),pair(Agent (A),SymKey (K))))))

=>
request(Agent (B),Agent (A),Purpose (purposeK),SymKey (K),(SID sid));
State (rB,[Agent (B),Step 2,inv(pk(Agent (B))),pk(Agent (B)),pk(Agent (A)),Agent (A),Nonce (NB),pair(Agent (B),crypt(pk(Agent (A)),pair(Nonce (NB),Agent (B)))),crypt(pk(Agent (A)),pair(Nonce (NB),Agent (B))),SymKey (K),Nonce (NA),f(Nonce (NB)),crypt(pk(Agent (B)),pair(f(Nonce (NB)),pair(Nonce (NA),pair(Agent (A),SymKey (K))))),scrypt(SymKey (K),f(Nonce (NA))),(SID sid)]);
iknows(scrypt(SymKey (K),f(Nonce (NA))))

step rule_13:
State (rB,[Agent (B),Step 1,inv(pk(Agent (B))),pk(Agent (B)),pk(Agent (A)),Agent (A),Nonce (NB),pair(Agent (B),crypt(pk(Agent (A)),pair(Nonce (NB),Agent (B)))),(SID sid)]);
iknows(pk(Agent (B)));
iknows(f(Nonce (NB)));
iknows(Nonce (NA));
iknows(Agent (A));
iknows(SymKey (K))

=>
request(Agent (B),Agent (A),Purpose (purposeK),SymKey (K),(SID sid));
State (rB,[Agent (B),Step 2,inv(pk(Agent (B))),pk(Agent (B)),pk(Agent (A)),Agent (A),Nonce (NB),pair(Agent (B),crypt(pk(Agent (A)),pair(Nonce (NB),Agent (B)))),crypt(pk(Agent (A)),pair(Nonce (NB),Agent (B))),SymKey (K),Nonce (NA),f(Nonce (NB)),crypt(pk(Agent (B)),pair(f(Nonce (NB)),pair(Nonce (NA),pair(Agent (A),SymKey (K))))),scrypt(SymKey (K),f(Nonce (NA))),(SID sid)]);
iknows(scrypt(SymKey (K),f(Nonce (NA))))

step rule_14:
State (rB,[Agent (B),Step 1,inv(pk(Agent (B))),pk(Agent (B)),pk(Agent (A)),Agent (A),Nonce (NB),pair(Agent (B),crypt(pk(Agent (A)),pair(Nonce (NB),Agent (B)))),(SID sid)]);
iknows(pk(Agent (B)));
iknows(Nonce (NB));
iknows(Nonce (NA));
iknows(Agent (A));
iknows(SymKey (K))

=>
request(Agent (B),Agent (A),Purpose (purposeK),SymKey (K),(SID sid));
State (rB,[Agent (B),Step 2,inv(pk(Agent (B))),pk(Agent (B)),pk(Agent (A)),Agent (A),Nonce (NB),pair(Agent (B),crypt(pk(Agent (A)),pair(Nonce (NB),Agent (B)))),crypt(pk(Agent (A)),pair(Nonce (NB),Agent (B))),SymKey (K),Nonce (NA),f(Nonce (NB)),crypt(pk(Agent (B)),pair(f(Nonce (NB)),pair(Nonce (NA),pair(Agent (A),SymKey (K))))),scrypt(SymKey (K),f(Nonce (NA))),(SID sid)]);
iknows(scrypt(SymKey (K),f(Nonce (NA))))

step rule_15:
State (rB,[Agent (B),Step 1,inv(pk(Agent (B))),pk(Agent (B)),pk(Agent (A)),Agent (A),Nonce (NB),pair(Agent (B),crypt(pk(Agent (A)),pair(Nonce (NB),Agent (B)))),(SID sid)]);
iknows(Agent (B));
iknows(f(Nonce (NB)));
iknows(Nonce (NA));
iknows(Agent (A));
iknows(SymKey (K))

=>
request(Agent (B),Agent (A),Purpose (purposeK),SymKey (K),(SID sid));
State (rB,[Agent (B),Step 2,inv(pk(Agent (B))),pk(Agent (B)),pk(Agent (A)),Agent (A),Nonce (NB),pair(Agent (B),crypt(pk(Agent (A)),pair(Nonce (NB),Agent (B)))),crypt(pk(Agent (A)),pair(Nonce (NB),Agent (B))),SymKey (K),Nonce (NA),f(Nonce (NB)),crypt(pk(Agent (B)),pair(f(Nonce (NB)),pair(Nonce (NA),pair(Agent (A),SymKey (K))))),scrypt(SymKey (K),f(Nonce (NA))),(SID sid)]);
iknows(scrypt(SymKey (K),f(Nonce (NA))))

step rule_16:
State (rB,[Agent (B),Step 1,inv(pk(Agent (B))),pk(Agent (B)),pk(Agent (A)),Agent (A),Nonce (NB),pair(Agent (B),crypt(pk(Agent (A)),pair(Nonce (NB),Agent (B)))),(SID sid)]);
iknows(Agent (B));
iknows(Nonce (NB));
iknows(Nonce (NA));
iknows(Agent (A));
iknows(SymKey (K))

=>
request(Agent (B),Agent (A),Purpose (purposeK),SymKey (K),(SID sid));
State (rB,[Agent (B),Step 2,inv(pk(Agent (B))),pk(Agent (B)),pk(Agent (A)),Agent (A),Nonce (NB),pair(Agent (B),crypt(pk(Agent (A)),pair(Nonce (NB),Agent (B)))),crypt(pk(Agent (A)),pair(Nonce (NB),Agent (B))),SymKey (K),Nonce (NA),f(Nonce (NB)),crypt(pk(Agent (B)),pair(f(Nonce (NB)),pair(Nonce (NA),pair(Agent (A),SymKey (K))))),scrypt(SymKey (K),f(Nonce (NA))),(SID sid)]);
iknows(scrypt(SymKey (K),f(Nonce (NA))))

step rule_17:
State (rA,[Agent (A),Step 1,inv(pk(Agent (A))),pk(Agent (B)),pk(Agent (A)),Agent (B),Nonce (NB),crypt(pk(Agent (A)),pair(Nonce (NB),Agent (B))),pair(Agent (B),crypt(pk(Agent (A)),pair(Nonce (NB),Agent (B)))),Nonce (NA),SymKey (K),crypt(pk(Agent (B)),pair(f(Nonce (NB)),pair(Nonce (NA),pair(Agent (A),SymKey (K))))),(SID sid)]);
iknows(scrypt(SymKey (K),f(Nonce (NA))))

=>
State (rA,[Agent (A),Step 2,inv(pk(Agent (A))),pk(Agent (B)),pk(Agent (A)),Agent (B),Nonce (NB),crypt(pk(Agent (A)),pair(Nonce (NB),Agent (B))),pair(Agent (B),crypt(pk(Agent (A)),pair(Nonce (NB),Agent (B)))),Nonce (NA),SymKey (K),crypt(pk(Agent (B)),pair(f(Nonce (NB)),pair(Nonce (NA),pair(Agent (A),SymKey (K))))),scrypt(SymKey (K),f(Nonce (NA))),(SID sid)])

step rule_18:
State (rA,[Agent (A),Step 1,inv(pk(Agent (A))),pk(Agent (B)),pk(Agent (A)),Agent (B),Nonce (NB),crypt(pk(Agent (A)),pair(Nonce (NB),Agent (B))),pair(Agent (B),crypt(pk(Agent (A)),pair(Nonce (NB),Agent (B)))),Nonce (NA),SymKey (K),crypt(pk(Agent (B)),pair(f(Nonce (NB)),pair(Nonce (NA),pair(Agent (A),SymKey (K))))),(SID sid)]);
iknows(SymKey (K));
iknows(f(Nonce (NA)))

=>
State (rA,[Agent (A),Step 2,inv(pk(Agent (A))),pk(Agent (B)),pk(Agent (A)),Agent (B),Nonce (NB),crypt(pk(Agent (A)),pair(Nonce (NB),Agent (B))),pair(Agent (B),crypt(pk(Agent (A)),pair(Nonce (NB),Agent (B)))),Nonce (NA),SymKey (K),crypt(pk(Agent (B)),pair(f(Nonce (NB)),pair(Nonce (NA),pair(Agent (A),SymKey (K))))),scrypt(SymKey (K),f(Nonce (NA))),(SID sid)])

step rule_19:
State (rA,[Agent (A),Step 1,inv(pk(Agent (A))),pk(Agent (B)),pk(Agent (A)),Agent (B),Nonce (NB),crypt(pk(Agent (A)),pair(Nonce (NB),Agent (B))),pair(Agent (B),crypt(pk(Agent (A)),pair(Nonce (NB),Agent (B)))),Nonce (NA),SymKey (K),crypt(pk(Agent (B)),pair(f(Nonce (NB)),pair(Nonce (NA),pair(Agent (A),SymKey (K))))),(SID sid)]);
iknows(SymKey (K));
iknows(Nonce (NA))

=>
State (rA,[Agent (A),Step 2,inv(pk(Agent (A))),pk(Agent (B)),pk(Agent (A)),Agent (B),Nonce (NB),crypt(pk(Agent (A)),pair(Nonce (NB),Agent (B))),pair(Agent (B),crypt(pk(Agent (A)),pair(Nonce (NB),Agent (B)))),Nonce (NA),SymKey (K),crypt(pk(Agent (B)),pair(f(Nonce (NB)),pair(Nonce (NA),pair(Agent (A),SymKey (K))))),scrypt(SymKey (K),f(Nonce (NA))),(SID sid)])


section initial state:
init_0: iknows(Nonce (ni));
init_1: iknows(Agent (dishonest i));
init_2: State (rA,[Agent (honest a),Step 0,inv(pk(Agent (honest a))),pk(Agent (dishonest i)),pk(Agent (honest a)),Agent (dishonest i),(SID sid)]);
init_3: State (rA,[Agent (honest a),Step 0,inv(pk(Agent (honest a))),pk(Agent (honest a)),pk(Agent (honest a)),Agent (honest a),(SID sid)]);
init_4: iknows(Step 0);
init_5: iknows(inv(pk(Agent (dishonest i))));
init_6: iknows(pk(Agent (dishonest i)));
init_7: iknows((SID sid));
init_8: iknows(pk(Agent (honest a)));
init_9: iknows(Agent (honest a));
init_10: State (rB,[Agent (honest a),Step 0,inv(pk(Agent (honest a))),pk(Agent (honest a)),pk(Agent (dishonest i)),Agent (dishonest i),(SID sid)]);
init_11: State (rB,[Agent (honest a),Step 0,inv(pk(Agent (honest a))),pk(Agent (honest a)),pk(Agent (honest a)),Agent (honest a),(SID sid)]);

section fixedpoint:
fp_0: iknows(pair(Agent (honest a),crypt(pk(Agent (honest a)),pair(Nonce (absNB(pair(Agent (honest a),Agent (honest a)))),Agent (honest a)))));
fp_1: iknows(pair(Agent (honest a),crypt(pk(Agent (dishonest i)),pair(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),Agent (honest a)))));
fp_2: State (rB,[Agent (honest a),Step 1,inv(pk(Agent (honest a))),pk(Agent (honest a)),pk(Agent (dishonest i)),Agent (dishonest i),Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),crypt(pk(Agent (dishonest i)),pair(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),Agent (honest a)))),(SID sid)]);
fp_3: State (rB,[Agent (honest a),Step 1,inv(pk(Agent (honest a))),pk(Agent (honest a)),pk(Agent (honest a)),Agent (honest a),Nonce (absNB(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),crypt(pk(Agent (honest a)),pair(Nonce (absNB(pair(Agent (honest a),Agent (honest a)))),Agent (honest a)))),(SID sid)]);
fp_4: secret(SymKey (absK(pair(Agent (honest a),Agent (dishonest i)))),Agent (dishonest i));
fp_5: witness(Agent (honest a),Agent (dishonest i),Purpose (purposeK),SymKey (absK(pair(Agent (honest a),Agent (dishonest i)))));
fp_6: State (rA,[Agent (honest a),Step 1,inv(pk(Agent (honest a))),pk(Agent (dishonest i)),pk(Agent (honest a)),Agent (dishonest i),Nonce (ni),crypt(pk(Agent (honest a)),pair(Nonce (ni),Agent (dishonest i))),pair(Agent (dishonest i),crypt(pk(Agent (honest a)),pair(Nonce (ni),Agent (dishonest i)))),Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),SymKey (absK(pair(Agent (honest a),Agent (dishonest i)))),crypt(pk(Agent (dishonest i)),pair(f(Nonce (ni)),pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),SymKey (absK(pair(Agent (honest a),Agent (dishonest i)))))))),(SID sid)]);
fp_7: secret(SymKey (absK(pair(Agent (honest a),Agent (honest a)))),Agent (honest a));
fp_8: witness(Agent (honest a),Agent (honest a),Purpose (purposeK),SymKey (absK(pair(Agent (honest a),Agent (honest a)))));
fp_9: State (rA,[Agent (honest a),Step 1,inv(pk(Agent (honest a))),pk(Agent (honest a)),pk(Agent (honest a)),Agent (honest a),Nonce (ni),crypt(pk(Agent (honest a)),pair(Nonce (ni),Agent (honest a))),pair(Agent (honest a),crypt(pk(Agent (honest a)),pair(Nonce (ni),Agent (honest a)))),Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),SymKey (absK(pair(Agent (honest a),Agent (honest a)))),crypt(pk(Agent (honest a)),pair(f(Nonce (ni)),pair(Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),SymKey (absK(pair(Agent (honest a),Agent (honest a)))))))),(SID sid)]);
fp_10: iknows(crypt(pk(Agent (honest a)),pair(f(Nonce (ni)),pair(Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),SymKey (absK(pair(Agent (honest a),Agent (honest a)))))))));
fp_11: iknows(crypt(pk(Agent (dishonest i)),pair(f(Nonce (ni)),pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),SymKey (absK(pair(Agent (honest a),Agent (dishonest i)))))))));
fp_12: iknows(crypt(pk(Agent (honest a)),pair(Nonce (absNB(pair(Agent (honest a),Agent (honest a)))),Agent (honest a))));
fp_13: iknows(crypt(pk(Agent (dishonest i)),pair(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),Agent (honest a))));
fp_14: iknows(pair(Agent (honest a),crypt(pk(Agent (honest a)),pair(Nonce (absNB(pair(Agent (honest a),Agent (honest a)))),Agent (honest a)))));
fp_15: iknows(pair(Agent (honest a),crypt(pk(Agent (dishonest i)),pair(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),Agent (honest a)))));
fp_16: iknows(pair(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),Agent (honest a)));
fp_17: iknows(pair(Agent (honest a),SymKey (absK(pair(Agent (honest a),Agent (dishonest i))))));
fp_18: iknows(pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),SymKey (absK(pair(Agent (honest a),Agent (dishonest i)))))));
fp_19: iknows(pair(f(Nonce (ni)),pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),SymKey (absK(pair(Agent (honest a),Agent (dishonest i))))))));
fp_20: State (rA,[Agent (honest a),Step 1,inv(pk(Agent (honest a))),pk(Agent (honest a)),pk(Agent (honest a)),Agent (honest a),Nonce (absNB(pair(Agent (honest a),Agent (honest a)))),crypt(pk(Agent (honest a)),pair(Nonce (absNB(pair(Agent (honest a),Agent (honest a)))),Agent (honest a))),pair(Agent (honest a),crypt(pk(Agent (honest a)),pair(Nonce (absNB(pair(Agent (honest a),Agent (honest a)))),Agent (honest a)))),Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),SymKey (absK(pair(Agent (honest a),Agent (honest a)))),crypt(pk(Agent (honest a)),pair(f(Nonce (absNB(pair(Agent (honest a),Agent (honest a))))),pair(Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),SymKey (absK(pair(Agent (honest a),Agent (honest a)))))))),(SID sid)]);
fp_21: iknows(crypt(pk(Agent (honest a)),pair(f(Nonce (absNB(pair(Agent (honest a),Agent (honest a))))),pair(Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),SymKey (absK(pair(Agent (honest a),Agent (honest a)))))))));
fp_22: iknows(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))));
fp_23: iknows(SymKey (absK(pair(Agent (honest a),Agent (dishonest i)))));
fp_24: iknows(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))));
fp_25: iknows(f(Nonce (ni)));
fp_26: iknows(pair(Agent (honest a),crypt(pk(Agent (honest a)),pair(Nonce (absNB(pair(Agent (honest a),Agent (honest a)))),Agent (honest a)))));
fp_27: iknows(pair(Agent (honest a),crypt(pk(Agent (dishonest i)),pair(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),Agent (honest a)))));
fp_28: iknows(pair(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),Agent (honest a)));
fp_29: iknows(pair(Agent (honest a),SymKey (absK(pair(Agent (honest a),Agent (dishonest i))))));
fp_30: iknows(pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),SymKey (absK(pair(Agent (honest a),Agent (dishonest i)))))));
fp_31: iknows(pair(f(Nonce (ni)),pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),SymKey (absK(pair(Agent (honest a),Agent (dishonest i))))))));
fp_32: State (rA,[Agent (honest a),Step 1,inv(pk(Agent (honest a))),pk(Agent (dishonest i)),pk(Agent (honest a)),Agent (dishonest i),Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),crypt(pk(Agent (honest a)),pair(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),Agent (dishonest i))),pair(Agent (dishonest i),crypt(pk(Agent (honest a)),pair(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),Agent (dishonest i)))),Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),SymKey (absK(pair(Agent (honest a),Agent (dishonest i)))),crypt(pk(Agent (dishonest i)),pair(f(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i))))),pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),SymKey (absK(pair(Agent (honest a),Agent (dishonest i)))))))),(SID sid)]);
fp_33: State (rA,[Agent (honest a),Step 1,inv(pk(Agent (honest a))),pk(Agent (dishonest i)),pk(Agent (honest a)),Agent (dishonest i),Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),crypt(pk(Agent (honest a)),pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),Agent (dishonest i))),pair(Agent (dishonest i),crypt(pk(Agent (honest a)),pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),Agent (dishonest i)))),Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),SymKey (absK(pair(Agent (honest a),Agent (dishonest i)))),crypt(pk(Agent (dishonest i)),pair(f(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i))))),pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),SymKey (absK(pair(Agent (honest a),Agent (dishonest i)))))))),(SID sid)]);
fp_34: State (rA,[Agent (honest a),Step 1,inv(pk(Agent (honest a))),pk(Agent (honest a)),pk(Agent (honest a)),Agent (honest a),Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),crypt(pk(Agent (honest a)),pair(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),Agent (honest a))),pair(Agent (honest a),crypt(pk(Agent (honest a)),pair(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),Agent (honest a)))),Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),SymKey (absK(pair(Agent (honest a),Agent (honest a)))),crypt(pk(Agent (honest a)),pair(f(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i))))),pair(Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),SymKey (absK(pair(Agent (honest a),Agent (honest a)))))))),(SID sid)]);
fp_35: State (rA,[Agent (honest a),Step 1,inv(pk(Agent (honest a))),pk(Agent (honest a)),pk(Agent (honest a)),Agent (honest a),Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),crypt(pk(Agent (honest a)),pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),Agent (honest a))),pair(Agent (honest a),crypt(pk(Agent (honest a)),pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),Agent (honest a)))),Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),SymKey (absK(pair(Agent (honest a),Agent (honest a)))),crypt(pk(Agent (honest a)),pair(f(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i))))),pair(Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),SymKey (absK(pair(Agent (honest a),Agent (honest a)))))))),(SID sid)]);
fp_36: request(Agent (honest a),Agent (honest a),Purpose (purposeK),SymKey (absK(pair(Agent (honest a),Agent (honest a)))),(SID sid));
fp_37: State (rB,[Agent (honest a),Step 2,inv(pk(Agent (honest a))),pk(Agent (honest a)),pk(Agent (honest a)),Agent (honest a),Nonce (absNB(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),crypt(pk(Agent (honest a)),pair(Nonce (absNB(pair(Agent (honest a),Agent (honest a)))),Agent (honest a)))),crypt(pk(Agent (honest a)),pair(Nonce (absNB(pair(Agent (honest a),Agent (honest a)))),Agent (honest a))),SymKey (absK(pair(Agent (honest a),Agent (honest a)))),Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),f(Nonce (absNB(pair(Agent (honest a),Agent (honest a))))),crypt(pk(Agent (honest a)),pair(f(Nonce (absNB(pair(Agent (honest a),Agent (honest a))))),pair(Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),SymKey (absK(pair(Agent (honest a),Agent (honest a)))))))),scrypt(SymKey (absK(pair(Agent (honest a),Agent (honest a)))),f(Nonce (absNA(pair(Agent (honest a),Agent (honest a)))))),(SID sid)]);
fp_38: request(Agent (honest a),Agent (dishonest i),Purpose (purposeK),SymKey (absK(pair(Agent (honest a),Agent (dishonest i)))),(SID sid));
fp_39: State (rB,[Agent (honest a),Step 2,inv(pk(Agent (honest a))),pk(Agent (honest a)),pk(Agent (dishonest i)),Agent (dishonest i),Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),crypt(pk(Agent (dishonest i)),pair(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),Agent (honest a)))),crypt(pk(Agent (dishonest i)),pair(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),Agent (honest a))),SymKey (absK(pair(Agent (honest a),Agent (dishonest i)))),Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),f(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i))))),crypt(pk(Agent (honest a)),pair(f(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i))))),pair(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (dishonest i),SymKey (absK(pair(Agent (honest a),Agent (dishonest i)))))))),scrypt(SymKey (absK(pair(Agent (honest a),Agent (dishonest i)))),f(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))))),(SID sid)]);
fp_40: State (rB,[Agent (honest a),Step 2,inv(pk(Agent (honest a))),pk(Agent (honest a)),pk(Agent (dishonest i)),Agent (dishonest i),Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),crypt(pk(Agent (dishonest i)),pair(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),Agent (honest a)))),crypt(pk(Agent (dishonest i)),pair(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),Agent (honest a))),SymKey (absK(pair(Agent (honest a),Agent (dishonest i)))),Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),f(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i))))),crypt(pk(Agent (honest a)),pair(f(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i))))),pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (dishonest i),SymKey (absK(pair(Agent (honest a),Agent (dishonest i)))))))),scrypt(SymKey (absK(pair(Agent (honest a),Agent (dishonest i)))),f(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))))),(SID sid)]);
fp_41: State (rB,[Agent (honest a),Step 2,inv(pk(Agent (honest a))),pk(Agent (honest a)),pk(Agent (dishonest i)),Agent (dishonest i),Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),crypt(pk(Agent (dishonest i)),pair(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),Agent (honest a)))),crypt(pk(Agent (dishonest i)),pair(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),Agent (honest a))),SymKey (absK(pair(Agent (honest a),Agent (dishonest i)))),Nonce (ni),f(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i))))),crypt(pk(Agent (honest a)),pair(f(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i))))),pair(Nonce (ni),pair(Agent (dishonest i),SymKey (absK(pair(Agent (honest a),Agent (dishonest i)))))))),scrypt(SymKey (absK(pair(Agent (honest a),Agent (dishonest i)))),f(Nonce (ni))),(SID sid)]);
fp_42: State (rA,[Agent (honest a),Step 2,inv(pk(Agent (honest a))),pk(Agent (dishonest i)),pk(Agent (honest a)),Agent (dishonest i),Nonce (ni),crypt(pk(Agent (honest a)),pair(Nonce (ni),Agent (dishonest i))),pair(Agent (dishonest i),crypt(pk(Agent (honest a)),pair(Nonce (ni),Agent (dishonest i)))),Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),SymKey (absK(pair(Agent (honest a),Agent (dishonest i)))),crypt(pk(Agent (dishonest i)),pair(f(Nonce (ni)),pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),SymKey (absK(pair(Agent (honest a),Agent (dishonest i)))))))),scrypt(SymKey (absK(pair(Agent (honest a),Agent (dishonest i)))),f(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))))),(SID sid)]);
fp_43: iknows(scrypt(SymKey (absK(pair(Agent (honest a),Agent (dishonest i)))),f(Nonce (ni))));
fp_44: iknows(scrypt(SymKey (absK(pair(Agent (honest a),Agent (dishonest i)))),f(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))))));
fp_45: iknows(scrypt(SymKey (absK(pair(Agent (honest a),Agent (dishonest i)))),f(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))))));
fp_46: iknows(scrypt(SymKey (absK(pair(Agent (honest a),Agent (honest a)))),f(Nonce (absNA(pair(Agent (honest a),Agent (honest a)))))));
fp_47: iknows(crypt(pk(Agent (honest a)),pair(f(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i))))),pair(Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),SymKey (absK(pair(Agent (honest a),Agent (honest a)))))))));
fp_48: iknows(crypt(pk(Agent (honest a)),pair(f(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i))))),pair(Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),SymKey (absK(pair(Agent (honest a),Agent (honest a)))))))));
fp_49: iknows(crypt(pk(Agent (dishonest i)),pair(f(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i))))),pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),SymKey (absK(pair(Agent (honest a),Agent (dishonest i)))))))));
fp_50: iknows(crypt(pk(Agent (dishonest i)),pair(f(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i))))),pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),SymKey (absK(pair(Agent (honest a),Agent (dishonest i)))))))));
fp_51: iknows(pair(Agent (honest a),crypt(pk(Agent (honest a)),pair(Nonce (absNB(pair(Agent (honest a),Agent (honest a)))),Agent (honest a)))));
fp_52: iknows(pair(Agent (honest a),crypt(pk(Agent (dishonest i)),pair(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),Agent (honest a)))));
fp_53: iknows(pair(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),Agent (honest a)));
fp_54: iknows(pair(Agent (honest a),SymKey (absK(pair(Agent (honest a),Agent (dishonest i))))));
fp_55: iknows(pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),SymKey (absK(pair(Agent (honest a),Agent (dishonest i)))))));
fp_56: iknows(pair(f(Nonce (ni)),pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),SymKey (absK(pair(Agent (honest a),Agent (dishonest i))))))));
fp_57: iknows(pair(f(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i))))),pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),SymKey (absK(pair(Agent (honest a),Agent (dishonest i))))))));
fp_58: iknows(pair(f(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i))))),pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),SymKey (absK(pair(Agent (honest a),Agent (dishonest i))))))));
fp_59: State (rA,[Agent (honest a),Step 2,inv(pk(Agent (honest a))),pk(Agent (dishonest i)),pk(Agent (honest a)),Agent (dishonest i),Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),crypt(pk(Agent (honest a)),pair(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),Agent (dishonest i))),pair(Agent (dishonest i),crypt(pk(Agent (honest a)),pair(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),Agent (dishonest i)))),Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),SymKey (absK(pair(Agent (honest a),Agent (dishonest i)))),crypt(pk(Agent (dishonest i)),pair(f(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i))))),pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),SymKey (absK(pair(Agent (honest a),Agent (dishonest i)))))))),scrypt(SymKey (absK(pair(Agent (honest a),Agent (dishonest i)))),f(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))))),(SID sid)]);
fp_60: State (rA,[Agent (honest a),Step 2,inv(pk(Agent (honest a))),pk(Agent (dishonest i)),pk(Agent (honest a)),Agent (dishonest i),Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),crypt(pk(Agent (honest a)),pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),Agent (dishonest i))),pair(Agent (dishonest i),crypt(pk(Agent (honest a)),pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),Agent (dishonest i)))),Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),SymKey (absK(pair(Agent (honest a),Agent (dishonest i)))),crypt(pk(Agent (dishonest i)),pair(f(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i))))),pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),SymKey (absK(pair(Agent (honest a),Agent (dishonest i)))))))),scrypt(SymKey (absK(pair(Agent (honest a),Agent (dishonest i)))),f(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))))),(SID sid)]);
fp_61: State (rA,[Agent (honest a),Step 2,inv(pk(Agent (honest a))),pk(Agent (honest a)),pk(Agent (honest a)),Agent (honest a),Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),crypt(pk(Agent (honest a)),pair(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),Agent (honest a))),pair(Agent (honest a),crypt(pk(Agent (honest a)),pair(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),Agent (honest a)))),Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),SymKey (absK(pair(Agent (honest a),Agent (honest a)))),crypt(pk(Agent (honest a)),pair(f(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i))))),pair(Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),SymKey (absK(pair(Agent (honest a),Agent (honest a)))))))),scrypt(SymKey (absK(pair(Agent (honest a),Agent (honest a)))),f(Nonce (absNA(pair(Agent (honest a),Agent (honest a)))))),(SID sid)]);
fp_62: State (rA,[Agent (honest a),Step 2,inv(pk(Agent (honest a))),pk(Agent (honest a)),pk(Agent (honest a)),Agent (honest a),Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),crypt(pk(Agent (honest a)),pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),Agent (honest a))),pair(Agent (honest a),crypt(pk(Agent (honest a)),pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),Agent (honest a)))),Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),SymKey (absK(pair(Agent (honest a),Agent (honest a)))),crypt(pk(Agent (honest a)),pair(f(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i))))),pair(Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),SymKey (absK(pair(Agent (honest a),Agent (honest a)))))))),scrypt(SymKey (absK(pair(Agent (honest a),Agent (honest a)))),f(Nonce (absNA(pair(Agent (honest a),Agent (honest a)))))),(SID sid)]);
fp_63: State (rA,[Agent (honest a),Step 2,inv(pk(Agent (honest a))),pk(Agent (honest a)),pk(Agent (honest a)),Agent (honest a),Nonce (absNB(pair(Agent (honest a),Agent (honest a)))),crypt(pk(Agent (honest a)),pair(Nonce (absNB(pair(Agent (honest a),Agent (honest a)))),Agent (honest a))),pair(Agent (honest a),crypt(pk(Agent (honest a)),pair(Nonce (absNB(pair(Agent (honest a),Agent (honest a)))),Agent (honest a)))),Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),SymKey (absK(pair(Agent (honest a),Agent (honest a)))),crypt(pk(Agent (honest a)),pair(f(Nonce (absNB(pair(Agent (honest a),Agent (honest a))))),pair(Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),SymKey (absK(pair(Agent (honest a),Agent (honest a)))))))),scrypt(SymKey (absK(pair(Agent (honest a),Agent (honest a)))),f(Nonce (absNA(pair(Agent (honest a),Agent (honest a)))))),(SID sid)]);
fp_64: State (rA,[Agent (honest a),Step 2,inv(pk(Agent (honest a))),pk(Agent (honest a)),pk(Agent (honest a)),Agent (honest a),Nonce (ni),crypt(pk(Agent (honest a)),pair(Nonce (ni),Agent (honest a))),pair(Agent (honest a),crypt(pk(Agent (honest a)),pair(Nonce (ni),Agent (honest a)))),Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),SymKey (absK(pair(Agent (honest a),Agent (honest a)))),crypt(pk(Agent (honest a)),pair(f(Nonce (ni)),pair(Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),SymKey (absK(pair(Agent (honest a),Agent (honest a)))))))),scrypt(SymKey (absK(pair(Agent (honest a),Agent (honest a)))),f(Nonce (absNA(pair(Agent (honest a),Agent (honest a)))))),(SID sid)]);
fp_65: iknows(f(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i))))));
fp_66: iknows(f(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i))))));
fp_67: iknows(pair(Agent (honest a),crypt(pk(Agent (honest a)),pair(Nonce (absNB(pair(Agent (honest a),Agent (honest a)))),Agent (honest a)))));
fp_68: iknows(pair(Agent (honest a),crypt(pk(Agent (dishonest i)),pair(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),Agent (honest a)))));
fp_69: iknows(pair(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),Agent (honest a)));
fp_70: iknows(pair(Agent (honest a),SymKey (absK(pair(Agent (honest a),Agent (dishonest i))))));
fp_71: iknows(pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),SymKey (absK(pair(Agent (honest a),Agent (dishonest i)))))));
fp_72: iknows(pair(f(Nonce (ni)),pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),SymKey (absK(pair(Agent (honest a),Agent (dishonest i))))))));
fp_73: iknows(pair(f(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i))))),pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),SymKey (absK(pair(Agent (honest a),Agent (dishonest i))))))));
fp_74: iknows(pair(f(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i))))),pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),SymKey (absK(pair(Agent (honest a),Agent (dishonest i))))))));

section abstraction:
NB->Nonce (absNB(pair(B,A)));
NA->Nonce (absNA(pair(A,B)));
K->SymKey (absK(pair(A,B)))


+ 24
- 0
examples/AnB/Denning-Sacco.AnB View File

@@ -0,0 +1,24 @@
Protocol: DenningSacco
Types: Agent A,B,s;
Number T,timestamp,Payload;
Symmetric_key KAB;
Function sk
Knowledge: A: A,B,sk(A,s),timestamp;
B: B,A,sk(B,s),timestamp;
s: A,B,sk(A,s),sk(B,s)
Actions:
A->s: A,B
s->A: {|B,KAB,T,{|A,KAB,T|}sk(B,s)|}sk(A,s)
A->B: {|A,KAB,T|}sk(B,s)
B->A: {|Payload|}KAB
Goals:
B *->* A: Payload
Abstraction:
T -> timestamp;
Payload -> payload(B,A);
KAB -> sk(A,B)

+ 213
- 0
examples/AnB/Denning-Sacco.fp View File

@@ -0,0 +1,213 @@
Backend: Open-Source Fixedpoint Model-Checker version 2009c
Protocol: DenningSacco
Types:
[(Purpose,["purposePayload"]),(Agent False False,["A","B","s"]),(Number,["T","timestamp","Payload"]),(SymmetricKey,["KAB"]),(Function,["sk"])]
section rules:
step rule_0:
iknows(crypt(K,M));
iknows(inv(K))

=>
iknows(M)

step rule_1:
iknows(crypt(inv(K),M));
iknows(K)

=>
iknows(M)

step rule_2:
iknows(scrypt(K,M));
iknows(K)

=>
iknows(M)

step rule_3:
iknows(pair(M1,M2))

=>
iknows(M1);
iknows(M2)

step rule_4:
secret(M,Agent (honest a));
iknows(M)

=>
attack(pair(secrecy,M))

step rule_5:
request(A,B,Purpose (purposePayload),M,(SID sid))
| B/=Agent (dishonest i);
M/=Nonce (payload(pair(B,A)))
=>
attack(pair(authentication,pair(A,pair(B,M))))

step rule_6:
request(A,B,Purpose (purposeKAB),M,(SID sid))
| B/=Agent (dishonest i);
M/=SymKey (sk(pair(B,A)))
=>
attack(pair(authentication,pair(A,pair(B,M))))

step rule_7:
State (rA,[Agent (A),Step 0,Nonce (timestamp),SymKey (sk(pair(Agent (A),Agent (honest a)))),Agent (B),(SID sid)])

=>
State (rA,[Agent (A),Step 1,Nonce (timestamp),SymKey (sk(pair(Agent (A),Agent (honest a)))),Agent (B),pair(Agent (A),Agent (B)),(SID sid)]);
iknows(pair(Agent (A),Agent (B)))

step rule_8:
State (rs,[Agent (honest a),Step 0,SymKey (sk(pair(Agent (B),Agent (honest a)))),SymKey (sk(pair(Agent (A),Agent (honest a)))),Agent (B),Agent (A),(SID sid)]);
iknows(Agent (A));
iknows(Agent (B))

=>
State (rs,[Agent (honest a),Step 1,SymKey (sk(pair(Agent (B),Agent (honest a)))),SymKey (sk(pair(Agent (A),Agent (honest a)))),Agent (B),Agent (A),pair(Agent (A),Agent (B)),SymKey (sk(pair(Agent (A),Agent (B)))),Nonce (timestamp),scrypt(SymKey (sk(pair(Agent (A),Agent (honest a)))),pair(Agent (B),pair(SymKey (sk(pair(Agent (A),Agent (B)))),pair(Nonce (timestamp),scrypt(SymKey (sk(pair(Agent (B),Agent (honest a)))),pair(Agent (A),pair(SymKey (sk(pair(Agent (A),Agent (B)))),Nonce (timestamp)))))))),(SID sid)]);
iknows(scrypt(SymKey (sk(pair(Agent (A),Agent (honest a)))),pair(Agent (B),pair(SymKey (sk(pair(Agent (A),Agent (B)))),pair(Nonce (timestamp),scrypt(SymKey (sk(pair(Agent (B),Agent (honest a)))),pair(Agent (A),pair(SymKey (sk(pair(Agent (A),Agent (B)))),Nonce (timestamp)))))))))

step rule_9:
State (rA,[Agent (A),Step 1,Nonce (timestamp),SymKey (sk(pair(Agent (A),Agent (honest a)))),Agent (B),pair(Agent (A),Agent (B)),(SID sid)]);
iknows(scrypt(SymKey (sk(pair(Agent (A),Agent (honest a)))),pair(Agent (B),pair(SymKey (KAB),pair(Nonce (T),Agent (dishonest i))))))

=>
State (rA,[Agent (A),Step 2,Nonce (timestamp),SymKey (sk(pair(Agent (A),Agent (honest a)))),Agent (B),pair(Agent (A),Agent (B)),Agent (dishonest i),Nonce (T),SymKey (KAB),scrypt(SymKey (sk(pair(Agent (A),Agent (honest a)))),pair(Agent (B),pair(SymKey (KAB),pair(Nonce (T),Agent (dishonest i))))),(SID sid)]);
iknows(Agent (dishonest i))

step rule_10:
State (rA,[Agent (A),Step 1,Nonce (timestamp),SymKey (sk(pair(Agent (A),Agent (honest a)))),Agent (B),pair(Agent (A),Agent (B)),(SID sid)]);
iknows(SymKey (sk(pair(Agent (A),Agent (honest a)))));
iknows(Agent (B));
iknows(SymKey (KAB));
iknows(Nonce (T));
iknows(Agent (dishonest i))

=>
State (rA,[Agent (A),Step 2,Nonce (timestamp),SymKey (sk(pair(Agent (A),Agent (honest a)))),Agent (B),pair(Agent (A),Agent (B)),Agent (dishonest i),Nonce (T),SymKey (KAB),scrypt(SymKey (sk(pair(Agent (A),Agent (honest a)))),pair(Agent (B),pair(SymKey (KAB),pair(Nonce (T),Agent (dishonest i))))),(SID sid)]);
iknows(Agent (dishonest i))

step rule_11:
State (rB,[Agent (B),Step 0,Nonce (timestamp),SymKey (sk(pair(Agent (B),Agent (honest a)))),Agent (A),(SID sid)]);
iknows(scrypt(SymKey (sk(pair(Agent (B),Agent (honest a)))),pair(Agent (A),pair(SymKey (KAB),Nonce (T)))))

=>
secret(Nonce (payload(pair(Agent (B),Agent (A)))),Agent (A));
witness(Agent (B),Agent (A),Purpose (purposePayload),Nonce (payload(pair(Agent (B),Agent (A)))));
State (rB,[Agent (B),Step 1,Nonce (timestamp),SymKey (sk(pair(Agent (B),Agent (honest a)))),Agent (A),Nonce (T),SymKey (KAB),scrypt(SymKey (sk(pair(Agent (B),Agent (honest a)))),pair(Agent (A),pair(SymKey (KAB),Nonce (T)))),Nonce (payload(pair(Agent (B),Agent (A)))),scrypt(SymKey (KAB),Nonce (payload(pair(Agent (B),Agent (A))))),(SID sid)]);
iknows(scrypt(SymKey (KAB),Nonce (payload(pair(Agent (B),Agent (A))))))

step rule_12:
State (rB,[Agent (B),Step 0,Nonce (timestamp),SymKey (sk(pair(Agent (B),Agent (honest a)))),Agent (A),(SID sid)]);
iknows(SymKey (sk(pair(Agent (B),Agent (honest a)))));
iknows(Agent (A));
iknows(SymKey (KAB));
iknows(Nonce (T))

=>
secret(Nonce (payload(pair(Agent (B),Agent (A)))),Agent (A));
witness(Agent (B),Agent (A),Purpose (purposePayload),Nonce (payload(pair(Agent (B),Agent (A)))));
State (rB,[Agent (B),Step 1,Nonce (timestamp),SymKey (sk(pair(Agent (B),Agent (honest a)))),Agent (A),Nonce (T),SymKey (KAB),scrypt(SymKey (sk(pair(Agent (B),Agent (honest a)))),pair(Agent (A),pair(SymKey (KAB),Nonce (T)))),Nonce (payload(pair(Agent (B),Agent (A)))),scrypt(SymKey (KAB),Nonce (payload(pair(Agent (B),Agent (A))))),(SID sid)]);
iknows(scrypt(SymKey (KAB),Nonce (payload(pair(Agent (B),Agent (A))))))

step rule_13:
State (rA,[Agent (A),Step 2,Nonce (timestamp),SymKey (sk(pair(Agent (A),Agent (honest a)))),Agent (B),pair(Agent (A),Agent (B)),Agent (dishonest i),Nonce (T),SymKey (KAB),scrypt(SymKey (sk(pair(Agent (A),Agent (honest a)))),pair(Agent (B),pair(SymKey (KAB),pair(Nonce (T),Agent (dishonest i))))),(SID sid)]);
iknows(scrypt(SymKey (KAB),Nonce (Payload)))

=>
request(Agent (A),Agent (B),Purpose (purposePayload),Nonce (Payload),(SID sid));
State (rA,[Agent (A),Step 3,Nonce (timestamp),SymKey (sk(pair(Agent (A),Agent (honest a)))),Agent (B),pair(Agent (A),Agent (B)),Agent (dishonest i),Nonce (T),SymKey (KAB),scrypt(SymKey (sk(pair(Agent (A),Agent (honest a)))),pair(Agent (B),pair(SymKey (KAB),pair(Nonce (T),Agent (dishonest i))))),Nonce (Payload),scrypt(SymKey (KAB),Nonce (Payload)),(SID sid)])

step rule_14:
State (rA,[Agent (A),Step 2,Nonce (timestamp),SymKey (sk(pair(Agent (A),Agent (honest a)))),Agent (B),pair(Agent (A),Agent (B)),Agent (dishonest i),Nonce (T),SymKey (KAB),scrypt(SymKey (sk(pair(Agent (A),Agent (honest a)))),pair(Agent (B),pair(SymKey (KAB),pair(Nonce (T),Agent (dishonest i))))),(SID sid)]);
iknows(SymKey (KAB));
iknows(Nonce (Payload))

=>
request(Agent (A),Agent (B),Purpose (purposePayload),Nonce (Payload),(SID sid));
State (rA,[Agent (A),Step 3,Nonce (timestamp),SymKey (sk(pair(Agent (A),Agent (honest a)))),Agent (B),pair(Agent (A),Agent (B)),Agent (dishonest i),Nonce (T),SymKey (KAB),scrypt(SymKey (sk(pair(Agent (A),Agent (honest a)))),pair(Agent (B),pair(SymKey (KAB),pair(Nonce (T),Agent (dishonest i))))),Nonce (Payload),scrypt(SymKey (KAB),Nonce (Payload)),(SID sid)])


section initial state:
init_0: iknows(Nonce (ni));
init_1: iknows(Agent (dishonest i));
init_2: State (rA,[Agent (honest a),Step 0,Nonce (timestamp),SymKey (sk(pair(Agent (honest a),Agent (honest a)))),Agent (dishonest i),(SID sid)]);
init_3: State (rA,[Agent (honest a),Step 0,Nonce (timestamp),SymKey (sk(pair(Agent (honest a),Agent (honest a)))),Agent (honest a),(SID sid)]);
init_4: iknows(Step 0);
init_5: iknows(Nonce (timestamp));
init_6: iknows(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))));
init_7: iknows((SID sid));
init_8: iknows(Agent (honest a));
init_9: State (rB,[Agent (honest a),Step 0,Nonce (timestamp),SymKey (sk(pair(Agent (honest a),Agent (honest a)))),Agent (dishonest i),(SID sid)]);
init_10: State (rB,[Agent (honest a),Step 0,Nonce (timestamp),SymKey (sk(pair(Agent (honest a),Agent (honest a)))),Agent (honest a),(SID sid)]);
init_11: State (rs,[Agent (honest a),Step 0,SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Agent (dishonest i),Agent (dishonest i),(SID sid)]);
init_12: State (rs,[Agent (honest a),Step 0,SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),SymKey (sk(pair(Agent (honest a),Agent (honest a)))),Agent (dishonest i),Agent (honest a),(SID sid)]);
init_13: State (rs,[Agent (honest a),Step 0,SymKey (sk(pair(Agent (honest a),Agent (honest a)))),SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Agent (honest a),Agent (dishonest i),(SID sid)]);
init_14: State (rs,[Agent (honest a),Step 0,SymKey (sk(pair(Agent (honest a),Agent (honest a)))),SymKey (sk(pair(Agent (honest a),Agent (honest a)))),Agent (honest a),Agent (honest a),(SID sid)]);

section fixedpoint:
fp_0: iknows(pair(Agent (honest a),Agent (honest a)));
fp_1: iknows(pair(Agent (honest a),Agent (dishonest i)));
fp_2: State (rA,[Agent (honest a),Step 1,Nonce (timestamp),SymKey (sk(pair(Agent (honest a),Agent (honest a)))),Agent (dishonest i),pair(Agent (honest a),Agent (dishonest i)),(SID sid)]);
fp_3: State (rA,[Agent (honest a),Step 1,Nonce (timestamp),SymKey (sk(pair(Agent (honest a),Agent (honest a)))),Agent (honest a),pair(Agent (honest a),Agent (honest a)),(SID sid)]);
fp_4: State (rs,[Agent (honest a),Step 1,SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Agent (dishonest i),Agent (dishonest i),pair(Agent (dishonest i),Agent (dishonest i)),SymKey (sk(pair(Agent (dishonest i),Agent (dishonest i)))),Nonce (timestamp),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Agent (dishonest i),pair(SymKey (sk(pair(Agent (dishonest i),Agent (dishonest i)))),pair(Nonce (timestamp),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Agent (dishonest i),pair(SymKey (sk(pair(Agent (dishonest i),Agent (dishonest i)))),Nonce (timestamp)))))))),(SID sid)]);
fp_5: State (rs,[Agent (honest a),Step 1,SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),SymKey (sk(pair(Agent (honest a),Agent (honest a)))),Agent (dishonest i),Agent (honest a),pair(Agent (honest a),Agent (dishonest i)),SymKey (sk(pair(Agent (honest a),Agent (dishonest i)))),Nonce (timestamp),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Agent (dishonest i),pair(SymKey (sk(pair(Agent (honest a),Agent (dishonest i)))),pair(Nonce (timestamp),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Agent (honest a),pair(SymKey (sk(pair(Agent (honest a),Agent (dishonest i)))),Nonce (timestamp)))))))),(SID sid)]);
fp_6: State (rs,[Agent (honest a),Step 1,SymKey (sk(pair(Agent (honest a),Agent (honest a)))),SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Agent (honest a),Agent (dishonest i),pair(Agent (dishonest i),Agent (honest a)),SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Nonce (timestamp),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Agent (honest a),pair(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (timestamp),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Agent (dishonest i),pair(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Nonce (timestamp)))))))),(SID sid)]);
fp_7: State (rs,[Agent (honest a),Step 1,SymKey (sk(pair(Agent (honest a),Agent (honest a)))),SymKey (sk(pair(Agent (honest a),Agent (honest a)))),Agent (honest a),Agent (honest a),pair(Agent (honest a),Agent (honest a)),SymKey (sk(pair(Agent (honest a),Agent (honest a)))),Nonce (timestamp),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),pair(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (timestamp),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),pair(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),Nonce (timestamp)))))))),(SID sid)]);
fp_8: iknows(scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),pair(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (timestamp),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),pair(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),Nonce (timestamp)))))))));
fp_9: iknows(scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Agent (honest a),pair(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (timestamp),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Agent (dishonest i),pair(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Nonce (timestamp)))))))));
fp_10: iknows(scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Agent (dishonest i),pair(SymKey (sk(pair(Agent (honest a),Agent (dishonest i)))),pair(Nonce (timestamp),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Agent (honest a),pair(SymKey (sk(pair(Agent (honest a),Agent (dishonest i)))),Nonce (timestamp)))))))));
fp_11: iknows(scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Agent (dishonest i),pair(SymKey (sk(pair(Agent (dishonest i),Agent (dishonest i)))),pair(Nonce (timestamp),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Agent (dishonest i),pair(SymKey (sk(pair(Agent (dishonest i),Agent (dishonest i)))),Nonce (timestamp)))))))));
fp_12: iknows(pair(Agent (honest a),Agent (honest a)));
fp_13: iknows(pair(Agent (honest a),Agent (dishonest i)));
fp_14: iknows(pair(Nonce (timestamp),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Agent (dishonest i),pair(SymKey (sk(pair(Agent (dishonest i),Agent (dishonest i)))),Nonce (timestamp))))));
fp_15: iknows(pair(SymKey (sk(pair(Agent (dishonest i),Agent (dishonest i)))),pair(Nonce (timestamp),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Agent (dishonest i),pair(SymKey (sk(pair(Agent (dishonest i),Agent (dishonest i)))),Nonce (timestamp)))))));
fp_16: iknows(pair(Agent (dishonest i),pair(SymKey (sk(pair(Agent (dishonest i),Agent (dishonest i)))),pair(Nonce (timestamp),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Agent (dishonest i),pair(SymKey (sk(pair(Agent (dishonest i),Agent (dishonest i)))),Nonce (timestamp))))))));
fp_17: iknows(pair(Nonce (timestamp),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Agent (dishonest i),pair(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Nonce (timestamp))))));
fp_18: iknows(pair(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (timestamp),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Agent (dishonest i),pair(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Nonce (timestamp)))))));
fp_19: iknows(pair(Agent (honest a),pair(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (timestamp),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Agent (dishonest i),pair(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Nonce (timestamp))))))));
fp_20: iknows(scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Agent (dishonest i),pair(SymKey (sk(pair(Agent (dishonest i),Agent (dishonest i)))),Nonce (timestamp)))));
fp_21: iknows(SymKey (sk(pair(Agent (dishonest i),Agent (dishonest i)))));
fp_22: iknows(scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Agent (dishonest i),pair(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Nonce (timestamp)))));
fp_23: iknows(pair(Agent (honest a),Agent (honest a)));
fp_24: iknows(pair(Agent (honest a),Agent (dishonest i)));
fp_25: iknows(pair(Nonce (timestamp),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Agent (dishonest i),pair(SymKey (sk(pair(Agent (dishonest i),Agent (dishonest i)))),Nonce (timestamp))))));
fp_26: iknows(pair(SymKey (sk(pair(Agent (dishonest i),Agent (dishonest i)))),pair(Nonce (timestamp),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Agent (dishonest i),pair(SymKey (sk(pair(Agent (dishonest i),Agent (dishonest i)))),Nonce (timestamp)))))));
fp_27: iknows(pair(Agent (dishonest i),pair(SymKey (sk(pair(Agent (dishonest i),Agent (dishonest i)))),pair(Nonce (timestamp),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Agent (dishonest i),pair(SymKey (sk(pair(Agent (dishonest i),Agent (dishonest i)))),Nonce (timestamp))))))));
fp_28: iknows(pair(Nonce (timestamp),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Agent (dishonest i),pair(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Nonce (timestamp))))));
fp_29: iknows(pair(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (timestamp),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Agent (dishonest i),pair(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Nonce (timestamp)))))));
fp_30: iknows(pair(Agent (honest a),pair(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (timestamp),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Agent (dishonest i),pair(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Nonce (timestamp))))))));
fp_31: iknows(pair(SymKey (sk(pair(Agent (dishonest i),Agent (dishonest i)))),Nonce (timestamp)));
fp_32: iknows(pair(Agent (dishonest i),pair(SymKey (sk(pair(Agent (dishonest i),Agent (dishonest i)))),Nonce (timestamp))));
fp_33: secret(Nonce (payload(pair(Agent (honest a),Agent (dishonest i)))),Agent (dishonest i));
fp_34: witness(Agent (honest a),Agent (dishonest i),Purpose (purposePayload),Nonce (payload(pair(Agent (honest a),Agent (dishonest i)))));
fp_35: State (rB,[Agent (honest a),Step 1,Nonce (timestamp),SymKey (sk(pair(Agent (honest a),Agent (honest a)))),Agent (dishonest i),Nonce (timestamp),SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Agent (dishonest i),pair(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Nonce (timestamp)))),Nonce (payload(pair(Agent (honest a),Agent (dishonest i)))),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Nonce (payload(pair(Agent (honest a),Agent (dishonest i))))),(SID sid)]);
fp_36: iknows(scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Nonce (payload(pair(Agent (honest a),Agent (dishonest i))))));
fp_37: iknows(pair(Agent (honest a),Agent (honest a)));
fp_38: iknows(pair(Agent (honest a),Agent (dishonest i)));
fp_39: iknows(pair(Nonce (timestamp),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Agent (dishonest i),pair(SymKey (sk(pair(Agent (dishonest i),Agent (dishonest i)))),Nonce (timestamp))))));
fp_40: iknows(pair(SymKey (sk(pair(Agent (dishonest i),Agent (dishonest i)))),pair(Nonce (timestamp),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Agent (dishonest i),pair(SymKey (sk(pair(Agent (dishonest i),Agent (dishonest i)))),Nonce (timestamp)))))));
fp_41: iknows(pair(Agent (dishonest i),pair(SymKey (sk(pair(Agent (dishonest i),Agent (dishonest i)))),pair(Nonce (timestamp),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Agent (dishonest i),pair(SymKey (sk(pair(Agent (dishonest i),Agent (dishonest i)))),Nonce (timestamp))))))));
fp_42: iknows(pair(Nonce (timestamp),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Agent (dishonest i),pair(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Nonce (timestamp))))));
fp_43: iknows(pair(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (timestamp),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Agent (dishonest i),pair(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Nonce (timestamp)))))));
fp_44: iknows(pair(Agent (honest a),pair(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (timestamp),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Agent (dishonest i),pair(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Nonce (timestamp))))))));
fp_45: iknows(pair(SymKey (sk(pair(Agent (dishonest i),Agent (dishonest i)))),Nonce (timestamp)));
fp_46: iknows(pair(Agent (dishonest i),pair(SymKey (sk(pair(Agent (dishonest i),Agent (dishonest i)))),Nonce (timestamp))));
fp_47: iknows(Nonce (payload(pair(Agent (honest a),Agent (dishonest i)))));
fp_48: iknows(pair(Agent (honest a),Agent (honest a)));
fp_49: iknows(pair(Agent (honest a),Agent (dishonest i)));
fp_50: iknows(pair(Nonce (timestamp),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Agent (dishonest i),pair(SymKey (sk(pair(Agent (dishonest i),Agent (dishonest i)))),Nonce (timestamp))))));
fp_51: iknows(pair(SymKey (sk(pair(Agent (dishonest i),Agent (dishonest i)))),pair(Nonce (timestamp),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Agent (dishonest i),pair(SymKey (sk(pair(Agent (dishonest i),Agent (dishonest i)))),Nonce (timestamp)))))));
fp_52: iknows(pair(Agent (dishonest i),pair(SymKey (sk(pair(Agent (dishonest i),Agent (dishonest i)))),pair(Nonce (timestamp),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Agent (dishonest i),pair(SymKey (sk(pair(Agent (dishonest i),Agent (dishonest i)))),Nonce (timestamp))))))));
fp_53: iknows(pair(Nonce (timestamp),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Agent (dishonest i),pair(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Nonce (timestamp))))));
fp_54: iknows(pair(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (timestamp),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Agent (dishonest i),pair(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Nonce (timestamp)))))));
fp_55: iknows(pair(Agent (honest a),pair(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (timestamp),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Agent (dishonest i),pair(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Nonce (timestamp))))))));
fp_56: iknows(pair(SymKey (sk(pair(Agent (dishonest i),Agent (dishonest i)))),Nonce (timestamp)));
fp_57: iknows(pair(Agent (dishonest i),pair(SymKey (sk(pair(Agent (dishonest i),Agent (dishonest i)))),Nonce (timestamp))));

section abstraction:
T->timestamp;
Payload->Nonce (payload(pair(B,A)));
KAB->SymKey (sk(pair(A,B)))


+ 18
- 0
examples/AnB/ISOpubKeyOnePassUnilateralAuthProt.AnB View File

@@ -0,0 +1,18 @@
Protocol: ISO_onepass_pk
# should be fine (replay is not considered here!)
Types: Agent A,B,s;
Number NA,Text1;
Function pk
Knowledge: A: A,B,{A,pk(A)}inv(pk(s)),pk(A),inv(pk(A));
B: B,pk(s)
Actions:
A->B: {A,pk(A)}inv(pk(s)),
{NA,B,Text1}inv(pk(A))
Goals:
A *-> B: Text1

+ 222
- 0
examples/AnB/ISOpubKeyOnePassUnilateralAuthProt.fp View File

@@ -0,0 +1,222 @@
Backend: Open-Source Fixedpoint Model-Checker version 2009c
Protocol: ISO_onepass_pk
Types:
[(Purpose,["purposeText1"]),(Agent False False,["A","B","s"]),(Number,["NA","Text1"]),(Function,["pk"])]
section rules:
step rule_0:
iknows(crypt(K,M));
iknows(inv(K))

=>
iknows(M)

step rule_1:
iknows(crypt(inv(K),M));
iknows(K)

=>
iknows(M)

step rule_2:
iknows(scrypt(K,M));
iknows(K)

=>
iknows(M)

step rule_3:
iknows(pair(M1,M2))

=>
iknows(M1);
iknows(M2)

step rule_4:
secret(M,Agent (honest a));
iknows(M)

=>
attack(pair(secrecy,M))

step rule_5:
request(A,B,Purpose (purposeNA),M,(SID sid))
| B/=Agent (dishonest i);
M/=Nonce (absNA(pair(B,A)))
=>
attack(pair(authentication,pair(A,pair(B,M))))

step rule_6:
request(A,B,Purpose (purposeText1),M,(SID sid))
| B/=Agent (dishonest i);
M/=Nonce (absText1(pair(B,A)))
=>
attack(pair(authentication,pair(A,pair(B,M))))

step rule_7:
State (rA,[Agent (A),Step 0,inv(pk(Agent (A))),pk(Agent (A)),crypt(inv(pk(Agent (honest a))),pair(Agent (A),pk(Agent (A)))),Agent (B),(SID sid)])

=>
witness(Agent (A),Agent (B),Purpose (purposeText1),Nonce (absText1(pair(Agent (A),Agent (B)))));
State (rA,[Agent (A),Step 1,inv(pk(Agent (A))),pk(Agent (A)),crypt(inv(pk(Agent (honest a))),pair(Agent (A),pk(Agent (A)))),Agent (B),Nonce (absNA(pair(Agent (A),Agent (B)))),Nonce (absText1(pair(Agent (A),Agent (B)))),pair(crypt(inv(pk(Agent (honest a))),pair(Agent (A),pk(Agent (A)))),crypt(inv(pk(Agent (A))),pair(Nonce (absNA(pair(Agent (A),Agent (B)))),pair(Agent (B),Nonce (absText1(pair(Agent (A),Agent (B)))))))),(SID sid)]);
iknows(pair(crypt(inv(pk(Agent (honest a))),pair(Agent (A),pk(Agent (A)))),crypt(inv(pk(Agent (A))),pair(Nonce (absNA(pair(Agent (A),Agent (B)))),pair(Agent (B),Nonce (absText1(pair(Agent (A),Agent (B)))))))))

step rule_8:
State (rB,[Agent (B),Step 0,pk(Agent (honest a)),(SID sid)]);
iknows(crypt(inv(pk(Agent (honest a))),pair(Agent (A),pk(Agent (A)))));
iknows(crypt(inv(pk(Agent (A))),pair(Nonce (NA),pair(Agent (B),Nonce (Text1)))))

=>
request(Agent (B),Agent (A),Purpose (purposeText1),Nonce (Text1),(SID sid));
State (rB,[Agent (B),Step 1,pk(Agent (honest a)),Nonce (Text1),Nonce (NA),crypt(inv(pk(Agent (A))),pair(Nonce (NA),pair(Agent (B),Nonce (Text1)))),pk(Agent (A)),Agent (A),crypt(inv(pk(Agent (honest a))),pair(Agent (A),pk(Agent (A)))),pair(crypt(inv(pk(Agent (honest a))),pair(Agent (A),pk(Agent (A)))),crypt(inv(pk(Agent (A))),pair(Nonce (NA),pair(Agent (B),Nonce (Text1))))),(SID sid)])

step rule_9:
State (rB,[Agent (B),Step 0,pk(Agent (honest a)),(SID sid)]);
iknows(crypt(inv(pk(Agent (honest a))),pair(Agent (A),pk(Agent (A)))));
iknows(inv(pk(Agent (A))));
iknows(Nonce (NA));
iknows(Agent (B));
iknows(Nonce (Text1))

=>
request(Agent (B),Agent (A),Purpose (purposeText1),Nonce (Text1),(SID sid));
State (rB,[Agent (B),Step 1,pk(Agent (honest a)),Nonce (Text1),Nonce (NA),crypt(inv(pk(Agent (A))),pair(Nonce (NA),pair(Agent (B),Nonce (Text1)))),pk(Agent (A)),Agent (A),crypt(inv(pk(Agent (honest a))),pair(Agent (A),pk(Agent (A)))),pair(crypt(inv(pk(Agent (honest a))),pair(Agent (A),pk(Agent (A)))),crypt(inv(pk(Agent (A))),pair(Nonce (NA),pair(Agent (B),Nonce (Text1))))),(SID sid)])

step rule_10:
State (rB,[Agent (B),Step 0,pk(Agent (honest a)),(SID sid)]);
iknows(inv(pk(Agent (honest a))));
iknows(Agent (A));
iknows(pk(Agent (A)));
iknows(crypt(inv(pk(Agent (A))),pair(Nonce (NA),pair(Agent (B),Nonce (Text1)))))

=>
request(Agent (B),Agent (A),Purpose (purposeText1),Nonce (Text1),(SID sid));
State (rB,[Agent (B),Step 1,pk(Agent (honest a)),Nonce (Text1),Nonce (NA),crypt(inv(pk(Agent (A))),pair(Nonce (NA),pair(Agent (B),Nonce (Text1)))),pk(Agent (A)),Agent (A),crypt(inv(pk(Agent (honest a))),pair(Agent (A),pk(Agent (A)))),pair(crypt(inv(pk(Agent (honest a))),pair(Agent (A),pk(Agent (A)))),crypt(inv(pk(Agent (A))),pair(Nonce (NA),pair(Agent (B),Nonce (Text1))))),(SID sid)])

step rule_11:
State (rB,[Agent (B),Step 0,pk(Agent (honest a)),(SID sid)]);
iknows(inv(pk(Agent (honest a))));
iknows(Agent (A));
iknows(pk(Agent (A)));
iknows(inv(pk(Agent (A))));
iknows(Nonce (NA));
iknows(Agent (B));
iknows(Nonce (Text1))

=>
request(Agent (B),Agent (A),Purpose (purposeText1),Nonce (Text1),(SID sid));
State (rB,[Agent (B),Step 1,pk(Agent (honest a)),Nonce (Text1),Nonce (NA),crypt(inv(pk(Agent (A))),pair(Nonce (NA),pair(Agent (B),Nonce (Text1)))),pk(Agent (A)),Agent (A),crypt(inv(pk(Agent (honest a))),pair(Agent (A),pk(Agent (A)))),pair(crypt(inv(pk(Agent (honest a))),pair(Agent (A),pk(Agent (A)))),crypt(inv(pk(Agent (A))),pair(Nonce (NA),pair(Agent (B),Nonce (Text1))))),(SID sid)])

step rule_12:
State (rB,[Agent (B),Step 0,pk(Agent (honest a)),(SID sid)]);
iknows(inv(pk(Agent (honest a))));
iknows(Agent (A));
iknows(crypt(inv(pk(Agent (A))),pair(Nonce (NA),pair(Agent (B),Nonce (Text1)))))

=>
request(Agent (B),Agent (A),Purpose (purposeText1),Nonce (Text1),(SID sid));
State (rB,[Agent (B),Step 1,pk(Agent (honest a)),Nonce (Text1),Nonce (NA),crypt(inv(pk(Agent (A))),pair(Nonce (NA),pair(Agent (B),Nonce (Text1)))),pk(Agent (A)),Agent (A),crypt(inv(pk(Agent (honest a))),pair(Agent (A),pk(Agent (A)))),pair(crypt(inv(pk(Agent (honest a))),pair(Agent (A),pk(Agent (A)))),crypt(inv(pk(Agent (A))),pair(Nonce (NA),pair(Agent (B),Nonce (Text1))))),(SID sid)])

step rule_13:
State (rB,[Agent (B),Step 0,pk(Agent (honest a)),(SID sid)]);
iknows(inv(pk(Agent (honest a))));
iknows(Agent (A));
iknows(inv(pk(Agent (A))));
iknows(Nonce (NA));
iknows(Agent (B));
iknows(Nonce (Text1))

=>
request(Agent (B),Agent (A),Purpose (purposeText1),Nonce (Text1),(SID sid));
State (rB,[Agent (B),Step 1,pk(Agent (honest a)),Nonce (Text1),Nonce (NA),crypt(inv(pk(Agent (A))),pair(Nonce (NA),pair(Agent (B),Nonce (Text1)))),pk(Agent (A)),Agent (A),crypt(inv(pk(Agent (honest a))),pair(Agent (A),pk(Agent (A)))),pair(crypt(inv(pk(Agent (honest a))),pair(Agent (A),pk(Agent (A)))),crypt(inv(pk(Agent (A))),pair(Nonce (NA),pair(Agent (B),Nonce (Text1))))),(SID sid)])


section initial state:
init_0: iknows(Nonce (ni));
init_1: iknows(Agent (dishonest i));
init_2: State (rA,[Agent (honest a),Step 0,inv(pk(Agent (honest a))),pk(Agent (honest a)),crypt(inv(pk(Agent (honest a))),pair(Agent (honest a),pk(Agent (honest a)))),Agent (dishonest i),(SID sid)]);
init_3: State (rA,[Agent (honest a),Step 0,inv(pk(Agent (honest a))),pk(Agent (honest a)),crypt(inv(pk(Agent (honest a))),pair(Agent (honest a),pk(Agent (honest a)))),Agent (honest a),(SID sid)]);
init_4: iknows(Step 0);
init_5: iknows(inv(pk(Agent (dishonest i))));
init_6: iknows(pk(Agent (dishonest i)));
init_7: iknows(crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))));
init_8: iknows((SID sid));
init_9: iknows(Agent (honest a));
init_10: State (rB,[Agent (honest a),Step 0,pk(Agent (honest a)),(SID sid)]);
init_11: iknows(pk(Agent (honest a)));

section fixedpoint:
fp_0: iknows(pair(crypt(inv(pk(Agent (honest a))),pair(Agent (honest a),pk(Agent (honest a)))),crypt(inv(pk(Agent (honest a))),pair(Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),Nonce (absText1(pair(Agent (honest a),Agent (honest a)))))))));
fp_1: iknows(pair(crypt(inv(pk(Agent (honest a))),pair(Agent (honest a),pk(Agent (honest a)))),crypt(inv(pk(Agent (honest a))),pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (dishonest i),Nonce (absText1(pair(Agent (honest a),Agent (dishonest i)))))))));
fp_2: iknows(pair(Agent (dishonest i),pk(Agent (dishonest i))));
fp_3: witness(Agent (honest a),Agent (dishonest i),Purpose (purposeText1),Nonce (absText1(pair(Agent (honest a),Agent (dishonest i)))));
fp_4: State (rA,[Agent (honest a),Step 1,inv(pk(Agent (honest a))),pk(Agent (honest a)),crypt(inv(pk(Agent (honest a))),pair(Agent (honest a),pk(Agent (honest a)))),Agent (dishonest i),Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),Nonce (absText1(pair(Agent (honest a),Agent (dishonest i)))),pair(crypt(inv(pk(Agent (honest a))),pair(Agent (honest a),pk(Agent (honest a)))),crypt(inv(pk(Agent (honest a))),pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (dishonest i),Nonce (absText1(pair(Agent (honest a),Agent (dishonest i)))))))),(SID sid)]);
fp_5: witness(Agent (honest a),Agent (honest a),Purpose (purposeText1),Nonce (absText1(pair(Agent (honest a),Agent (honest a)))));
fp_6: State (rA,[Agent (honest a),Step 1,inv(pk(Agent (honest a))),pk(Agent (honest a)),crypt(inv(pk(Agent (honest a))),pair(Agent (honest a),pk(Agent (honest a)))),Agent (honest a),Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),Nonce (absText1(pair(Agent (honest a),Agent (honest a)))),pair(crypt(inv(pk(Agent (honest a))),pair(Agent (honest a),pk(Agent (honest a)))),crypt(inv(pk(Agent (honest a))),pair(Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),Nonce (absText1(pair(Agent (honest a),Agent (honest a)))))))),(SID sid)]);
fp_7: request(Agent (honest a),Agent (dishonest i),Purpose (purposeText1),Nonce (ni),(SID sid));
fp_8: State (rB,[Agent (honest a),Step 1,pk(Agent (honest a)),Nonce (ni),Nonce (ni),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (ni),pair(Agent (honest a),Nonce (ni)))),pk(Agent (dishonest i)),Agent (dishonest i),crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),pair(crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (ni),pair(Agent (honest a),Nonce (ni))))),(SID sid)]);
fp_9: iknows(crypt(inv(pk(Agent (honest a))),pair(Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),Nonce (absText1(pair(Agent (honest a),Agent (honest a))))))));
fp_10: iknows(crypt(inv(pk(Agent (honest a))),pair(Agent (honest a),pk(Agent (honest a)))));
fp_11: iknows(crypt(inv(pk(Agent (honest a))),pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (dishonest i),Nonce (absText1(pair(Agent (honest a),Agent (dishonest i))))))));
fp_12: iknows(pair(crypt(inv(pk(Agent (honest a))),pair(Agent (honest a),pk(Agent (honest a)))),crypt(inv(pk(Agent (honest a))),pair(Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),Nonce (absText1(pair(Agent (honest a),Agent (honest a)))))))));
fp_13: iknows(pair(crypt(inv(pk(Agent (honest a))),pair(Agent (honest a),pk(Agent (honest a)))),crypt(inv(pk(Agent (honest a))),pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (dishonest i),Nonce (absText1(pair(Agent (honest a),Agent (dishonest i)))))))));
fp_14: iknows(pair(Agent (dishonest i),pk(Agent (dishonest i))));
fp_15: iknows(pair(Agent (dishonest i),Nonce (absText1(pair(Agent (honest a),Agent (dishonest i))))));
fp_16: iknows(pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (dishonest i),Nonce (absText1(pair(Agent (honest a),Agent (dishonest i)))))));
fp_17: iknows(pair(Agent (honest a),pk(Agent (honest a))));
fp_18: iknows(pair(Agent (honest a),Nonce (absText1(pair(Agent (honest a),Agent (honest a))))));
fp_19: iknows(pair(Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),Nonce (absText1(pair(Agent (honest a),Agent (honest a)))))));
fp_20: request(Agent (honest a),Agent (honest a),Purpose (purposeText1),Nonce (absText1(pair(Agent (honest a),Agent (honest a)))),(SID sid));
fp_21: State (rB,[Agent (honest a),Step 1,pk(Agent (honest a)),Nonce (absText1(pair(Agent (honest a),Agent (honest a)))),Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),crypt(inv(pk(Agent (honest a))),pair(Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),Nonce (absText1(pair(Agent (honest a),Agent (honest a))))))),pk(Agent (honest a)),Agent (honest a),crypt(inv(pk(Agent (honest a))),pair(Agent (honest a),pk(Agent (honest a)))),pair(crypt(inv(pk(Agent (honest a))),pair(Agent (honest a),pk(Agent (honest a)))),crypt(inv(pk(Agent (honest a))),pair(Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),Nonce (absText1(pair(Agent (honest a),Agent (honest a)))))))),(SID sid)]);
fp_22: iknows(Nonce (absText1(pair(Agent (honest a),Agent (dishonest i)))));
fp_23: iknows(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))));
fp_24: iknows(Nonce (absText1(pair(Agent (honest a),Agent (honest a)))));
fp_25: iknows(Nonce (absNA(pair(Agent (honest a),Agent (honest a)))));
fp_26: iknows(pair(crypt(inv(pk(Agent (honest a))),pair(Agent (honest a),pk(Agent (honest a)))),crypt(inv(pk(Agent (honest a))),pair(Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),Nonce (absText1(pair(Agent (honest a),Agent (honest a)))))))));
fp_27: iknows(pair(crypt(inv(pk(Agent (honest a))),pair(Agent (honest a),pk(Agent (honest a)))),crypt(inv(pk(Agent (honest a))),pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (dishonest i),Nonce (absText1(pair(Agent (honest a),Agent (dishonest i)))))))));
fp_28: iknows(pair(Agent (dishonest i),pk(Agent (dishonest i))));
fp_29: iknows(pair(Agent (dishonest i),Nonce (absText1(pair(Agent (honest a),Agent (dishonest i))))));
fp_30: iknows(pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (dishonest i),Nonce (absText1(pair(Agent (honest a),Agent (dishonest i)))))));
fp_31: iknows(pair(Agent (honest a),pk(Agent (honest a))));
fp_32: iknows(pair(Agent (honest a),Nonce (absText1(pair(Agent (honest a),Agent (honest a))))));
fp_33: iknows(pair(Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),Nonce (absText1(pair(Agent (honest a),Agent (honest a)))))));
fp_34: request(Agent (honest a),Agent (dishonest i),Purpose (purposeText1),Nonce (absText1(pair(Agent (honest a),Agent (dishonest i)))),(SID sid));
fp_35: State (rB,[Agent (honest a),Step 1,pk(Agent (honest a)),Nonce (absText1(pair(Agent (honest a),Agent (dishonest i)))),Nonce (absText1(pair(Agent (honest a),Agent (dishonest i)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (absText1(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),Nonce (absText1(pair(Agent (honest a),Agent (dishonest i))))))),pk(Agent (dishonest i)),Agent (dishonest i),crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),pair(crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (absText1(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),Nonce (absText1(pair(Agent (honest a),Agent (dishonest i)))))))),(SID sid)]);
fp_36: request(Agent (honest a),Agent (dishonest i),Purpose (purposeText1),Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),(SID sid));
fp_37: State (rB,[Agent (honest a),Step 1,pk(Agent (honest a)),Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),Nonce (absText1(pair(Agent (honest a),Agent (dishonest i)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (absText1(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),Nonce (absNA(pair(Agent (honest a),Agent (dishonest i))))))),pk(Agent (dishonest i)),Agent (dishonest i),crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),pair(crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (absText1(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))))))),(SID sid)]);
fp_38: request(Agent (honest a),Agent (dishonest i),Purpose (purposeText1),Nonce (absText1(pair(Agent (honest a),Agent (honest a)))),(SID sid));
fp_39: State (rB,[Agent (honest a),Step 1,pk(Agent (honest a)),Nonce (absText1(pair(Agent (honest a),Agent (honest a)))),Nonce (absText1(pair(Agent (honest a),Agent (dishonest i)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (absText1(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),Nonce (absText1(pair(Agent (honest a),Agent (honest a))))))),pk(Agent (dishonest i)),Agent (dishonest i),crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),pair(crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (absText1(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),Nonce (absText1(pair(Agent (honest a),Agent (honest a)))))))),(SID sid)]);
fp_40: request(Agent (honest a),Agent (dishonest i),Purpose (purposeText1),Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),(SID sid));
fp_41: State (rB,[Agent (honest a),Step 1,pk(Agent (honest a)),Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),Nonce (absText1(pair(Agent (honest a),Agent (dishonest i)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (absText1(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),Nonce (absNA(pair(Agent (honest a),Agent (honest a))))))),pk(Agent (dishonest i)),Agent (dishonest i),crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),pair(crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (absText1(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),Nonce (absNA(pair(Agent (honest a),Agent (honest a)))))))),(SID sid)]);
fp_42: State (rB,[Agent (honest a),Step 1,pk(Agent (honest a)),Nonce (ni),Nonce (absText1(pair(Agent (honest a),Agent (dishonest i)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (absText1(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),Nonce (ni)))),pk(Agent (dishonest i)),Agent (dishonest i),crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),pair(crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (absText1(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),Nonce (ni))))),(SID sid)]);
fp_43: State (rB,[Agent (honest a),Step 1,pk(Agent (honest a)),Nonce (absText1(pair(Agent (honest a),Agent (dishonest i)))),Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),Nonce (absText1(pair(Agent (honest a),Agent (dishonest i))))))),pk(Agent (dishonest i)),Agent (dishonest i),crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),pair(crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),Nonce (absText1(pair(Agent (honest a),Agent (dishonest i)))))))),(SID sid)]);
fp_44: State (rB,[Agent (honest a),Step 1,pk(Agent (honest a)),Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),Nonce (absNA(pair(Agent (honest a),Agent (dishonest i))))))),pk(Agent (dishonest i)),Agent (dishonest i),crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),pair(crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))))))),(SID sid)]);
fp_45: State (rB,[Agent (honest a),Step 1,pk(Agent (honest a)),Nonce (absText1(pair(Agent (honest a),Agent (honest a)))),Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),Nonce (absText1(pair(Agent (honest a),Agent (honest a))))))),pk(Agent (dishonest i)),Agent (dishonest i),crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),pair(crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),Nonce (absText1(pair(Agent (honest a),Agent (honest a)))))))),(SID sid)]);
fp_46: State (rB,[Agent (honest a),Step 1,pk(Agent (honest a)),Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),Nonce (absNA(pair(Agent (honest a),Agent (honest a))))))),pk(Agent (dishonest i)),Agent (dishonest i),crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),pair(crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),Nonce (absNA(pair(Agent (honest a),Agent (honest a)))))))),(SID sid)]);
fp_47: State (rB,[Agent (honest a),Step 1,pk(Agent (honest a)),Nonce (ni),Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),Nonce (ni)))),pk(Agent (dishonest i)),Agent (dishonest i),crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),pair(crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),Nonce (ni))))),(SID sid)]);
fp_48: State (rB,[Agent (honest a),Step 1,pk(Agent (honest a)),Nonce (absText1(pair(Agent (honest a),Agent (dishonest i)))),Nonce (absText1(pair(Agent (honest a),Agent (honest a)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (absText1(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),Nonce (absText1(pair(Agent (honest a),Agent (dishonest i))))))),pk(Agent (dishonest i)),Agent (dishonest i),crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),pair(crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (absText1(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),Nonce (absText1(pair(Agent (honest a),Agent (dishonest i)))))))),(SID sid)]);
fp_49: State (rB,[Agent (honest a),Step 1,pk(Agent (honest a)),Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),Nonce (absText1(pair(Agent (honest a),Agent (honest a)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (absText1(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),Nonce (absNA(pair(Agent (honest a),Agent (dishonest i))))))),pk(Agent (dishonest i)),Agent (dishonest i),crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),pair(crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (absText1(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))))))),(SID sid)]);
fp_50: State (rB,[Agent (honest a),Step 1,pk(Agent (honest a)),Nonce (absText1(pair(Agent (honest a),Agent (honest a)))),Nonce (absText1(pair(Agent (honest a),Agent (honest a)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (absText1(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),Nonce (absText1(pair(Agent (honest a),Agent (honest a))))))),pk(Agent (dishonest i)),Agent (dishonest i),crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),pair(crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (absText1(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),Nonce (absText1(pair(Agent (honest a),Agent (honest a)))))))),(SID sid)]);
fp_51: State (rB,[Agent (honest a),Step 1,pk(Agent (honest a)),Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),Nonce (absText1(pair(Agent (honest a),Agent (honest a)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (absText1(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),Nonce (absNA(pair(Agent (honest a),Agent (honest a))))))),pk(Agent (dishonest i)),Agent (dishonest i),crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),pair(crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (absText1(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),Nonce (absNA(pair(Agent (honest a),Agent (honest a)))))))),(SID sid)]);
fp_52: State (rB,[Agent (honest a),Step 1,pk(Agent (honest a)),Nonce (ni),Nonce (absText1(pair(Agent (honest a),Agent (honest a)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (absText1(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),Nonce (ni)))),pk(Agent (dishonest i)),Agent (dishonest i),crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),pair(crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (absText1(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),Nonce (ni))))),(SID sid)]);
fp_53: State (rB,[Agent (honest a),Step 1,pk(Agent (honest a)),Nonce (absText1(pair(Agent (honest a),Agent (dishonest i)))),Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),Nonce (absText1(pair(Agent (honest a),Agent (dishonest i))))))),pk(Agent (dishonest i)),Agent (dishonest i),crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),pair(crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),Nonce (absText1(pair(Agent (honest a),Agent (dishonest i)))))))),(SID sid)]);
fp_54: State (rB,[Agent (honest a),Step 1,pk(Agent (honest a)),Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),Nonce (absNA(pair(Agent (honest a),Agent (dishonest i))))))),pk(Agent (dishonest i)),Agent (dishonest i),crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),pair(crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))))))),(SID sid)]);
fp_55: State (rB,[Agent (honest a),Step 1,pk(Agent (honest a)),Nonce (absText1(pair(Agent (honest a),Agent (honest a)))),Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),Nonce (absText1(pair(Agent (honest a),Agent (honest a))))))),pk(Agent (dishonest i)),Agent (dishonest i),crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),pair(crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),Nonce (absText1(pair(Agent (honest a),Agent (honest a)))))))),(SID sid)]);
fp_56: State (rB,[Agent (honest a),Step 1,pk(Agent (honest a)),Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),Nonce (absNA(pair(Agent (honest a),Agent (honest a))))))),pk(Agent (dishonest i)),Agent (dishonest i),crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),pair(crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),Nonce (absNA(pair(Agent (honest a),Agent (honest a)))))))),(SID sid)]);
fp_57: State (rB,[Agent (honest a),Step 1,pk(Agent (honest a)),Nonce (ni),Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),Nonce (ni)))),pk(Agent (dishonest i)),Agent (dishonest i),crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),pair(crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),Nonce (ni))))),(SID sid)]);
fp_58: State (rB,[Agent (honest a),Step 1,pk(Agent (honest a)),Nonce (absText1(pair(Agent (honest a),Agent (dishonest i)))),Nonce (ni),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (ni),pair(Agent (honest a),Nonce (absText1(pair(Agent (honest a),Agent (dishonest i))))))),pk(Agent (dishonest i)),Agent (dishonest i),crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),pair(crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (ni),pair(Agent (honest a),Nonce (absText1(pair(Agent (honest a),Agent (dishonest i)))))))),(SID sid)]);
fp_59: State (rB,[Agent (honest a),Step 1,pk(Agent (honest a)),Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),Nonce (ni),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (ni),pair(Agent (honest a),Nonce (absNA(pair(Agent (honest a),Agent (dishonest i))))))),pk(Agent (dishonest i)),Agent (dishonest i),crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),pair(crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (ni),pair(Agent (honest a),Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))))))),(SID sid)]);
fp_60: State (rB,[Agent (honest a),Step 1,pk(Agent (honest a)),Nonce (absText1(pair(Agent (honest a),Agent (honest a)))),Nonce (ni),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (ni),pair(Agent (honest a),Nonce (absText1(pair(Agent (honest a),Agent (honest a))))))),pk(Agent (dishonest i)),Agent (dishonest i),crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),pair(crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (ni),pair(Agent (honest a),Nonce (absText1(pair(Agent (honest a),Agent (honest a)))))))),(SID sid)]);
fp_61: State (rB,[Agent (honest a),Step 1,pk(Agent (honest a)),Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),Nonce (ni),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (ni),pair(Agent (honest a),Nonce (absNA(pair(Agent (honest a),Agent (honest a))))))),pk(Agent (dishonest i)),Agent (dishonest i),crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),pair(crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),crypt(inv(pk(Agent (dishonest i))),pair(Nonce (ni),pair(Agent (honest a),Nonce (absNA(pair(Agent (honest a),Agent (honest a)))))))),(SID sid)]);
fp_62: iknows(pair(crypt(inv(pk(Agent (honest a))),pair(Agent (honest a),pk(Agent (honest a)))),crypt(inv(pk(Agent (honest a))),pair(Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),Nonce (absText1(pair(Agent (honest a),Agent (honest a)))))))));
fp_63: iknows(pair(crypt(inv(pk(Agent (honest a))),pair(Agent (honest a),pk(Agent (honest a)))),crypt(inv(pk(Agent (honest a))),pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (dishonest i),Nonce (absText1(pair(Agent (honest a),Agent (dishonest i)))))))));
fp_64: iknows(pair(Agent (dishonest i),pk(Agent (dishonest i))));
fp_65: iknows(pair(Agent (dishonest i),Nonce (absText1(pair(Agent (honest a),Agent (dishonest i))))));
fp_66: iknows(pair(Nonce (absNA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (dishonest i),Nonce (absText1(pair(Agent (honest a),Agent (dishonest i)))))));
fp_67: iknows(pair(Agent (honest a),pk(Agent (honest a))));
fp_68: iknows(pair(Agent (honest a),Nonce (absText1(pair(Agent (honest a),Agent (honest a))))));
fp_69: iknows(pair(Nonce (absNA(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),Nonce (absText1(pair(Agent (honest a),Agent (honest a)))))));

section abstraction:
NA->Nonce (absNA(pair(A,B)));
Text1->Nonce (absText1(pair(A,B)))


+ 15
- 0
examples/AnB/ISOsymKeyTwoPassUnilateralAuthProt.AnB View File

@@ -0,0 +1,15 @@
Protocol: ISO_twopass_symm # Verified & Certified
Types: Agent A,B;
Number NB,Text1,Text2,Text3;
Function sk
Knowledge: A: A,B,sk(A,B);
B: B,A,sk(A,B)
Actions:
B->A: NB
A->B: {|NB,B,Text2|}sk(A,B)
Goals:
A *-> B: Text2

+ 154
- 0
examples/AnB/ISOsymKeyTwoPassUnilateralAuthProt.fp View File

@@ -0,0 +1,154 @@
Backend: Open-Source Fixedpoint Model-Checker version 2009c
Protocol: ISO_twopass_symm
Types:
[(Purpose,["purposeText2"]),(Agent False False,["A","B"]),(Number,["NB","Text1","Text2","Text3"]),(Function,["sk"])]
section rules:
step rule_0:
iknows(crypt(K,M));
iknows(inv(K))

=>
iknows(M)

step rule_1:
iknows(crypt(inv(K),M));
iknows(K)

=>
iknows(M)

step rule_2:
iknows(scrypt(K,M));
iknows(K)

=>
iknows(M)

step rule_3:
iknows(pair(M1,M2))

=>
iknows(M1);
iknows(M2)

step rule_4:
secret(M,Agent (honest a));
iknows(M)

=>
attack(pair(secrecy,M))

step rule_5:
request(A,B,Purpose (purposeNB),M,(SID sid))
| B/=Agent (dishonest i);
M/=Nonce (absNB(pair(B,A)))
=>
attack(pair(authentication,pair(A,pair(B,M))))

step rule_6:
request(A,B,Purpose (purposeText2),M,(SID sid))
| B/=Agent (dishonest i);
M/=Nonce (absText2(pair(B,A)))
=>
attack(pair(authentication,pair(A,pair(B,M))))

step rule_7:
State (rB,[Agent (B),Step 0,SymKey (sk(pair(Agent (A),Agent (B)))),Agent (A),(SID sid)])

=>
State (rB,[Agent (B),Step 1,SymKey (sk(pair(Agent (A),Agent (B)))),Agent (A),Nonce (absNB(pair(Agent (B),Agent (A)))),(SID sid)]);
iknows(Nonce (absNB(pair(Agent (B),Agent (A)))))

step rule_8:
State (rA,[Agent (A),Step 0,SymKey (sk(pair(Agent (A),Agent (B)))),Agent (B),(SID sid)]);
iknows(Nonce (NB))

=>
witness(Agent (A),Agent (B),Purpose (purposeText2),Nonce (absText2(pair(Agent (A),Agent (B)))));
State (rA,[Agent (A),Step 1,SymKey (sk(pair(Agent (A),Agent (B)))),Agent (B),Nonce (NB),Nonce (absText2(pair(Agent (A),Agent (B)))),scrypt(SymKey (sk(pair(Agent (A),Agent (B)))),pair(Nonce (NB),pair(Agent (B),Nonce (absText2(pair(Agent (A),Agent (B))))))),(SID sid)]);
iknows(scrypt(SymKey (sk(pair(Agent (A),Agent (B)))),pair(Nonce (NB),pair(Agent (B),Nonce (absText2(pair(Agent (A),Agent (B))))))))

step rule_9:
State (rB,[Agent (B),Step 1,SymKey (sk(pair(Agent (A),Agent (B)))),Agent (A),Nonce (NB),(SID sid)]);
iknows(scrypt(SymKey (sk(pair(Agent (A),Agent (B)))),pair(Nonce (NB),pair(Agent (B),Nonce (Text2)))))

=>
request(Agent (B),Agent (A),Purpose (purposeText2),Nonce (Text2),(SID sid));
State (rB,[Agent (B),Step 2,SymKey (sk(pair(Agent (A),Agent (B)))),Agent (A),Nonce (NB),Nonce (Text2),scrypt(SymKey (sk(pair(Agent (A),Agent (B)))),pair(Nonce (NB),pair(Agent (B),Nonce (Text2)))),(SID sid)])

step rule_10:
State (rB,[Agent (B),Step 1,SymKey (sk(pair(Agent (A),Agent (B)))),Agent (A),Nonce (NB),(SID sid)]);
iknows(SymKey (sk(pair(Agent (A),Agent (B)))));
iknows(Nonce (NB));
iknows(Agent (B));
iknows(Nonce (Text2))

=>
request(Agent (B),Agent (A),Purpose (purposeText2),Nonce (Text2),(SID sid));
State (rB,[Agent (B),Step 2,SymKey (sk(pair(Agent (A),Agent (B)))),Agent (A),Nonce (NB),Nonce (Text2),scrypt(SymKey (sk(pair(Agent (A),Agent (B)))),pair(Nonce (NB),pair(Agent (B),Nonce (Text2)))),(SID sid)])


section initial state:
init_0: iknows(Nonce (ni));
init_1: iknows(Agent (dishonest i));
init_2: State (rA,[Agent (honest a),Step 0,SymKey (sk(pair(Agent (honest a),Agent (dishonest i)))),Agent (dishonest i),(SID sid)]);
init_3: State (rA,[Agent (honest a),Step 0,SymKey (sk(pair(Agent (honest a),Agent (honest a)))),Agent (honest a),(SID sid)]);
init_4: iknows(Step 0);
init_5: iknows(SymKey (sk(pair(Agent (dishonest i),Agent (dishonest i)))));
init_6: iknows((SID sid));
init_7: iknows(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))));
init_8: iknows(Agent (honest a));
init_9: State (rB,[Agent (honest a),Step 0,SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Agent (dishonest i),(SID sid)]);
init_10: State (rB,[Agent (honest a),Step 0,SymKey (sk(pair(Agent (honest a),Agent (honest a)))),Agent (honest a),(SID sid)]);
init_11: iknows(SymKey (sk(pair(Agent (honest a),Agent (dishonest i)))));

section fixedpoint:
fp_0: State (rB,[Agent (honest a),Step 1,SymKey (sk(pair(Agent (honest a),Agent (honest a)))),Agent (honest a),Nonce (absNB(pair(Agent (honest a),Agent (honest a)))),(SID sid)]);
fp_1: State (rB,[Agent (honest a),Step 1,SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Agent (dishonest i),Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),(SID sid)]);
fp_2: witness(Agent (honest a),Agent (dishonest i),Purpose (purposeText2),Nonce (absText2(pair(Agent (honest a),Agent (dishonest i)))));
fp_3: State (rA,[Agent (honest a),Step 1,SymKey (sk(pair(Agent (honest a),Agent (dishonest i)))),Agent (dishonest i),Nonce (ni),Nonce (absText2(pair(Agent (honest a),Agent (dishonest i)))),scrypt(SymKey (sk(pair(Agent (honest a),Agent (dishonest i)))),pair(Nonce (ni),pair(Agent (dishonest i),Nonce (absText2(pair(Agent (honest a),Agent (dishonest i))))))),(SID sid)]);
fp_4: witness(Agent (honest a),Agent (honest a),Purpose (purposeText2),Nonce (absText2(pair(Agent (honest a),Agent (honest a)))));
fp_5: State (rA,[Agent (honest a),Step 1,SymKey (sk(pair(Agent (honest a),Agent (honest a)))),Agent (honest a),Nonce (ni),Nonce (absText2(pair(Agent (honest a),Agent (honest a)))),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (ni),pair(Agent (honest a),Nonce (absText2(pair(Agent (honest a),Agent (honest a))))))),(SID sid)]);
fp_6: iknows(scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (ni),pair(Agent (honest a),Nonce (absText2(pair(Agent (honest a),Agent (honest a))))))));
fp_7: iknows(scrypt(SymKey (sk(pair(Agent (honest a),Agent (dishonest i)))),pair(Nonce (ni),pair(Agent (dishonest i),Nonce (absText2(pair(Agent (honest a),Agent (dishonest i))))))));
fp_8: iknows(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))));
fp_9: iknows(Nonce (absNB(pair(Agent (honest a),Agent (honest a)))));
fp_10: iknows(pair(Agent (dishonest i),Nonce (absText2(pair(Agent (honest a),Agent (dishonest i))))));
fp_11: iknows(pair(Nonce (ni),pair(Agent (dishonest i),Nonce (absText2(pair(Agent (honest a),Agent (dishonest i)))))));
fp_12: State (rA,[Agent (honest a),Step 1,SymKey (sk(pair(Agent (honest a),Agent (dishonest i)))),Agent (dishonest i),Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),Nonce (absText2(pair(Agent (honest a),Agent (dishonest i)))),scrypt(SymKey (sk(pair(Agent (honest a),Agent (dishonest i)))),pair(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (dishonest i),Nonce (absText2(pair(Agent (honest a),Agent (dishonest i))))))),(SID sid)]);
fp_13: State (rA,[Agent (honest a),Step 1,SymKey (sk(pair(Agent (honest a),Agent (dishonest i)))),Agent (dishonest i),Nonce (absNB(pair(Agent (honest a),Agent (honest a)))),Nonce (absText2(pair(Agent (honest a),Agent (dishonest i)))),scrypt(SymKey (sk(pair(Agent (honest a),Agent (dishonest i)))),pair(Nonce (absNB(pair(Agent (honest a),Agent (honest a)))),pair(Agent (dishonest i),Nonce (absText2(pair(Agent (honest a),Agent (dishonest i))))))),(SID sid)]);
fp_14: State (rA,[Agent (honest a),Step 1,SymKey (sk(pair(Agent (honest a),Agent (honest a)))),Agent (honest a),Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),Nonce (absText2(pair(Agent (honest a),Agent (honest a)))),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),Nonce (absText2(pair(Agent (honest a),Agent (honest a))))))),(SID sid)]);
fp_15: State (rA,[Agent (honest a),Step 1,SymKey (sk(pair(Agent (honest a),Agent (honest a)))),Agent (honest a),Nonce (absNB(pair(Agent (honest a),Agent (honest a)))),Nonce (absText2(pair(Agent (honest a),Agent (honest a)))),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absNB(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),Nonce (absText2(pair(Agent (honest a),Agent (honest a))))))),(SID sid)]);
fp_16: request(Agent (honest a),Agent (dishonest i),Purpose (purposeText2),Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),(SID sid));
fp_17: State (rB,[Agent (honest a),Step 2,SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Agent (dishonest i),Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),Nonce (absNB(pair(Agent (honest a),Agent (dishonest i))))))),(SID sid)]);
fp_18: request(Agent (honest a),Agent (dishonest i),Purpose (purposeText2),Nonce (absNB(pair(Agent (honest a),Agent (honest a)))),(SID sid));
fp_19: State (rB,[Agent (honest a),Step 2,SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Agent (dishonest i),Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),Nonce (absNB(pair(Agent (honest a),Agent (honest a)))),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),Nonce (absNB(pair(Agent (honest a),Agent (honest a))))))),(SID sid)]);
fp_20: request(Agent (honest a),Agent (dishonest i),Purpose (purposeText2),Nonce (ni),(SID sid));
fp_21: State (rB,[Agent (honest a),Step 2,SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Agent (dishonest i),Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),Nonce (ni),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),Nonce (ni)))),(SID sid)]);
fp_22: iknows(scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absNB(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),Nonce (absText2(pair(Agent (honest a),Agent (honest a))))))));
fp_23: iknows(scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),Nonce (absText2(pair(Agent (honest a),Agent (honest a))))))));
fp_24: iknows(scrypt(SymKey (sk(pair(Agent (honest a),Agent (dishonest i)))),pair(Nonce (absNB(pair(Agent (honest a),Agent (honest a)))),pair(Agent (dishonest i),Nonce (absText2(pair(Agent (honest a),Agent (dishonest i))))))));
fp_25: iknows(scrypt(SymKey (sk(pair(Agent (honest a),Agent (dishonest i)))),pair(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (dishonest i),Nonce (absText2(pair(Agent (honest a),Agent (dishonest i))))))));
fp_26: iknows(Nonce (absText2(pair(Agent (honest a),Agent (dishonest i)))));
fp_27: iknows(pair(Agent (dishonest i),Nonce (absText2(pair(Agent (honest a),Agent (dishonest i))))));
fp_28: iknows(pair(Nonce (ni),pair(Agent (dishonest i),Nonce (absText2(pair(Agent (honest a),Agent (dishonest i)))))));
fp_29: iknows(pair(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (dishonest i),Nonce (absText2(pair(Agent (honest a),Agent (dishonest i)))))));
fp_30: iknows(pair(Nonce (absNB(pair(Agent (honest a),Agent (honest a)))),pair(Agent (dishonest i),Nonce (absText2(pair(Agent (honest a),Agent (dishonest i)))))));
fp_31: State (rA,[Agent (honest a),Step 1,SymKey (sk(pair(Agent (honest a),Agent (dishonest i)))),Agent (dishonest i),Nonce (absText2(pair(Agent (honest a),Agent (dishonest i)))),Nonce (absText2(pair(Agent (honest a),Agent (dishonest i)))),scrypt(SymKey (sk(pair(Agent (honest a),Agent (dishonest i)))),pair(Nonce (absText2(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (dishonest i),Nonce (absText2(pair(Agent (honest a),Agent (dishonest i))))))),(SID sid)]);
fp_32: State (rA,[Agent (honest a),Step 1,SymKey (sk(pair(Agent (honest a),Agent (honest a)))),Agent (honest a),Nonce (absText2(pair(Agent (honest a),Agent (dishonest i)))),Nonce (absText2(pair(Agent (honest a),Agent (honest a)))),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absText2(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),Nonce (absText2(pair(Agent (honest a),Agent (honest a))))))),(SID sid)]);
fp_33: request(Agent (honest a),Agent (honest a),Purpose (purposeText2),Nonce (absText2(pair(Agent (honest a),Agent (honest a)))),(SID sid));
fp_34: State (rB,[Agent (honest a),Step 2,SymKey (sk(pair(Agent (honest a),Agent (honest a)))),Agent (honest a),Nonce (absNB(pair(Agent (honest a),Agent (honest a)))),Nonce (absText2(pair(Agent (honest a),Agent (honest a)))),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absNB(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),Nonce (absText2(pair(Agent (honest a),Agent (honest a))))))),(SID sid)]);
fp_35: request(Agent (honest a),Agent (dishonest i),Purpose (purposeText2),Nonce (absText2(pair(Agent (honest a),Agent (dishonest i)))),(SID sid));
fp_36: State (rB,[Agent (honest a),Step 2,SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Agent (dishonest i),Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),Nonce (absText2(pair(Agent (honest a),Agent (dishonest i)))),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),Nonce (absText2(pair(Agent (honest a),Agent (dishonest i))))))),(SID sid)]);
fp_37: iknows(scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absText2(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),Nonce (absText2(pair(Agent (honest a),Agent (honest a))))))));
fp_38: iknows(scrypt(SymKey (sk(pair(Agent (honest a),Agent (dishonest i)))),pair(Nonce (absText2(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (dishonest i),Nonce (absText2(pair(Agent (honest a),Agent (dishonest i))))))));
fp_39: iknows(pair(Agent (dishonest i),Nonce (absText2(pair(Agent (honest a),Agent (dishonest i))))));
fp_40: iknows(pair(Nonce (ni),pair(Agent (dishonest i),Nonce (absText2(pair(Agent (honest a),Agent (dishonest i)))))));
fp_41: iknows(pair(Nonce (absNB(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (dishonest i),Nonce (absText2(pair(Agent (honest a),Agent (dishonest i)))))));
fp_42: iknows(pair(Nonce (absNB(pair(Agent (honest a),Agent (honest a)))),pair(Agent (dishonest i),Nonce (absText2(pair(Agent (honest a),Agent (dishonest i)))))));
fp_43: iknows(pair(Nonce (absText2(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (dishonest i),Nonce (absText2(pair(Agent (honest a),Agent (dishonest i)))))));

section abstraction:
NB->Nonce (absNB(pair(B,A)));
Text2->Nonce (absText2(pair(A,B)))


+ 19
- 0
examples/AnB/WideMouthFrog.AnB View File

@@ -0,0 +1,19 @@
Protocol: WideMouthFrog
## Problem with abstract authentication
Types: Agent A,B,s;
Number TA,TS; # actually timestamps
Symmetric_key KAB;
Function sk
Knowledge: A: A,B,sk(A,s);
B: B,A,sk(B,s);
s: A,B,sk(A,s),sk(B,s)
Actions:
A->s: A,{|TA,B,KAB|}sk(A,s)
s->B: {|TS,A,KAB|}sk(B,s)
Goals:
A *->* B: KAB

+ 209
- 0
examples/AnB/WideMouthFrog.fp View File

@@ -0,0 +1,209 @@
Backend: Open-Source Fixedpoint Model-Checker version 2009c
Protocol: WideMouthFrog
Types:
[(Purpose,["purposeKAB"]),(Agent False False,["A","B","s"]),(Number,["TA","TS"]),(SymmetricKey,["KAB"]),(Function,["sk"])]
section rules:
step rule_0:
iknows(crypt(K,M));
iknows(inv(K))

=>
iknows(M)

step rule_1:
iknows(crypt(inv(K),M));
iknows(K)

=>
iknows(M)

step rule_2:
iknows(scrypt(K,M));
iknows(K)

=>
iknows(M)

step rule_3:
iknows(pair(M1,M2))

=>
iknows(M1);
iknows(M2)

step rule_4:
secret(M,Agent (honest a));
iknows(M)

=>
attack(pair(secrecy,M))

step rule_5:
request(A,B,Purpose (purposeTA),M,(SID sid))
| B/=Agent (dishonest i);
M/=Nonce (absTA(pair(B,A)))
=>
attack(pair(authentication,pair(A,pair(B,M))))

step rule_6:
request(A,B,Purpose (purposeKAB),M,(SID sid))
| B/=Agent (dishonest i);
M/=SymKey (absKAB(pair(B,A)))
=>
attack(pair(authentication,pair(A,pair(B,M))))

step rule_7:
request(A,B,Purpose (purposeTS),M,(SID sid))
| B/=Agent (dishonest i);
M/=Nonce (absTS(pair(B,A)))
=>
attack(pair(authentication,pair(A,pair(B,M))))

step rule_8:
State (rA,[Agent (A),Step 0,SymKey (sk(pair(Agent (A),Agent (honest a)))),Agent (B),(SID sid)])

=>
secret(SymKey (absKAB(pair(Agent (A),Agent (B)))),Agent (B));
witness(Agent (A),Agent (B),Purpose (purposeKAB),SymKey (absKAB(pair(Agent (A),Agent (B)))));
State (rA,[Agent (A),Step 1,SymKey (sk(pair(Agent (A),Agent (honest a)))),Agent (B),Nonce (absTA(pair(Agent (A),Agent (B)))),SymKey (absKAB(pair(Agent (A),Agent (B)))),pair(Agent (A),scrypt(SymKey (sk(pair(Agent (A),Agent (honest a)))),pair(Nonce (absTA(pair(Agent (A),Agent (B)))),pair(Agent (B),SymKey (absKAB(pair(Agent (A),Agent (B)))))))),(SID sid)]);
iknows(pair(Agent (A),scrypt(SymKey (sk(pair(Agent (A),Agent (honest a)))),pair(Nonce (absTA(pair(Agent (A),Agent (B)))),pair(Agent (B),SymKey (absKAB(pair(Agent (A),Agent (B)))))))))

step rule_9:
State (rs,[Agent (honest a),Step 0,SymKey (sk(pair(Agent (B),Agent (honest a)))),SymKey (sk(pair(Agent (A),Agent (honest a)))),Agent (B),Agent (A),(SID sid)]);
iknows(Agent (A));
iknows(scrypt(SymKey (sk(pair(Agent (A),Agent (honest a)))),pair(Nonce (TA),pair(Agent (B),SymKey (KAB)))))

=>
State (rs,[Agent (honest a),Step 1,SymKey (sk(pair(Agent (B),Agent (honest a)))),SymKey (sk(pair(Agent (A),Agent (honest a)))),Agent (B),Agent (A),SymKey (KAB),Nonce (TA),scrypt(SymKey (sk(pair(Agent (A),Agent (honest a)))),pair(Nonce (TA),pair(Agent (B),SymKey (KAB)))),pair(Agent (A),scrypt(SymKey (sk(pair(Agent (A),Agent (honest a)))),pair(Nonce (TA),pair(Agent (B),SymKey (KAB))))),Nonce (absTS(pair(Agent (B),Agent (A)))),scrypt(SymKey (sk(pair(Agent (B),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (B),Agent (A)))),pair(Agent (A),SymKey (KAB)))),(SID sid)]);
iknows(scrypt(SymKey (sk(pair(Agent (B),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (B),Agent (A)))),pair(Agent (A),SymKey (KAB)))))

step rule_10:
State (rs,[Agent (honest a),Step 0,SymKey (sk(pair(Agent (B),Agent (honest a)))),SymKey (sk(pair(Agent (A),Agent (honest a)))),Agent (B),Agent (A),(SID sid)]);
iknows(Agent (A));
iknows(SymKey (sk(pair(Agent (A),Agent (honest a)))));
iknows(Nonce (TA));
iknows(Agent (B));
iknows(SymKey (KAB))

=>
State (rs,[Agent (honest a),Step 1,SymKey (sk(pair(Agent (B),Agent (honest a)))),SymKey (sk(pair(Agent (A),Agent (honest a)))),Agent (B),Agent (A),SymKey (KAB),Nonce (TA),scrypt(SymKey (sk(pair(Agent (A),Agent (honest a)))),pair(Nonce (TA),pair(Agent (B),SymKey (KAB)))),pair(Agent (A),scrypt(SymKey (sk(pair(Agent (A),Agent (honest a)))),pair(Nonce (TA),pair(Agent (B),SymKey (KAB))))),Nonce (absTS(pair(Agent (B),Agent (A)))),scrypt(SymKey (sk(pair(Agent (B),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (B),Agent (A)))),pair(Agent (A),SymKey (KAB)))),(SID sid)]);
iknows(scrypt(SymKey (sk(pair(Agent (B),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (B),Agent (A)))),pair(Agent (A),SymKey (KAB)))))

step rule_11:
State (rB,[Agent (B),Step 0,SymKey (sk(pair(Agent (B),Agent (honest a)))),Agent (A),(SID sid)]);
iknows(scrypt(SymKey (sk(pair(Agent (B),Agent (honest a)))),pair(Nonce (TS),pair(Agent (A),SymKey (KAB)))))

=>
request(Agent (B),Agent (A),Purpose (purposeKAB),SymKey (KAB),(SID sid));
State (rB,[Agent (B),Step 1,SymKey (sk(pair(Agent (B),Agent (honest a)))),Agent (A),SymKey (KAB),Nonce (TS),scrypt(SymKey (sk(pair(Agent (B),Agent (honest a)))),pair(Nonce (TS),pair(Agent (A),SymKey (KAB)))),(SID sid)])

step rule_12:
State (rB,[Agent (B),Step 0,SymKey (sk(pair(Agent (B),Agent (honest a)))),Agent (A),(SID sid)]);
iknows(SymKey (sk(pair(Agent (B),Agent (honest a)))));
iknows(Nonce (TS));
iknows(Agent (A));
iknows(SymKey (KAB))

=>
request(Agent (B),Agent (A),Purpose (purposeKAB),SymKey (KAB),(SID sid));
State (rB,[Agent (B),Step 1,SymKey (sk(pair(Agent (B),Agent (honest a)))),Agent (A),SymKey (KAB),Nonce (TS),scrypt(SymKey (sk(pair(Agent (B),Agent (honest a)))),pair(Nonce (TS),pair(Agent (A),SymKey (KAB)))),(SID sid)])


section initial state:
init_0: iknows(Nonce (ni));
init_1: iknows(Agent (dishonest i));
init_2: State (rA,[Agent (honest a),Step 0,SymKey (sk(pair(Agent (honest a),Agent (honest a)))),Agent (dishonest i),(SID sid)]);
init_3: State (rA,[Agent (honest a),Step 0,SymKey (sk(pair(Agent (honest a),Agent (honest a)))),Agent (honest a),(SID sid)]);
init_4: iknows(Step 0);
init_5: iknows(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))));
init_6: iknows((SID sid));
init_7: iknows(Agent (honest a));
init_8: State (rB,[Agent (honest a),Step 0,SymKey (sk(pair(Agent (honest a),Agent (honest a)))),Agent (dishonest i),(SID sid)]);
init_9: State (rB,[Agent (honest a),Step 0,SymKey (sk(pair(Agent (honest a),Agent (honest a)))),Agent (honest a),(SID sid)]);
init_10: State (rs,[Agent (honest a),Step 0,SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Agent (dishonest i),Agent (dishonest i),(SID sid)]);
init_11: State (rs,[Agent (honest a),Step 0,SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),SymKey (sk(pair(Agent (honest a),Agent (honest a)))),Agent (dishonest i),Agent (honest a),(SID sid)]);
init_12: State (rs,[Agent (honest a),Step 0,SymKey (sk(pair(Agent (honest a),Agent (honest a)))),SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Agent (honest a),Agent (dishonest i),(SID sid)]);
init_13: State (rs,[Agent (honest a),Step 0,SymKey (sk(pair(Agent (honest a),Agent (honest a)))),SymKey (sk(pair(Agent (honest a),Agent (honest a)))),Agent (honest a),Agent (honest a),(SID sid)]);

section fixedpoint:
fp_0: iknows(pair(Agent (honest a),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absTA(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),SymKey (absKAB(pair(Agent (honest a),Agent (honest a)))))))));
fp_1: iknows(pair(Agent (honest a),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absTA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (dishonest i),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i)))))))));
fp_2: secret(SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i)))),Agent (dishonest i));
fp_3: witness(Agent (honest a),Agent (dishonest i),Purpose (purposeKAB),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i)))));
fp_4: State (rA,[Agent (honest a),Step 1,SymKey (sk(pair(Agent (honest a),Agent (honest a)))),Agent (dishonest i),Nonce (absTA(pair(Agent (honest a),Agent (dishonest i)))),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (honest a),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absTA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (dishonest i),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i)))))))),(SID sid)]);
fp_5: secret(SymKey (absKAB(pair(Agent (honest a),Agent (honest a)))),Agent (honest a));
fp_6: witness(Agent (honest a),Agent (honest a),Purpose (purposeKAB),SymKey (absKAB(pair(Agent (honest a),Agent (honest a)))));
fp_7: State (rA,[Agent (honest a),Step 1,SymKey (sk(pair(Agent (honest a),Agent (honest a)))),Agent (honest a),Nonce (absTA(pair(Agent (honest a),Agent (honest a)))),SymKey (absKAB(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absTA(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),SymKey (absKAB(pair(Agent (honest a),Agent (honest a)))))))),(SID sid)]);
fp_8: State (rs,[Agent (honest a),Step 1,SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Agent (dishonest i),Agent (dishonest i),SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Nonce (ni),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (ni),pair(Agent (dishonest i),SymKey (sk(pair(Agent (dishonest i),Agent (honest a))))))),pair(Agent (dishonest i),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (ni),pair(Agent (dishonest i),SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))))))),Nonce (absTS(pair(Agent (dishonest i),Agent (dishonest i)))),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (dishonest i),Agent (dishonest i)))),pair(Agent (dishonest i),SymKey (sk(pair(Agent (dishonest i),Agent (honest a))))))),(SID sid)]);
fp_9: State (rs,[Agent (honest a),Step 1,SymKey (sk(pair(Agent (honest a),Agent (honest a)))),SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Agent (honest a),Agent (dishonest i),SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Nonce (ni),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (ni),pair(Agent (honest a),SymKey (sk(pair(Agent (dishonest i),Agent (honest a))))))),pair(Agent (dishonest i),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (ni),pair(Agent (honest a),SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))))))),Nonce (absTS(pair(Agent (honest a),Agent (dishonest i)))),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (dishonest i),SymKey (sk(pair(Agent (dishonest i),Agent (honest a))))))),(SID sid)]);
fp_10: iknows(scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (dishonest i),SymKey (sk(pair(Agent (dishonest i),Agent (honest a))))))));
fp_11: iknows(scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (dishonest i),Agent (dishonest i)))),pair(Agent (dishonest i),SymKey (sk(pair(Agent (dishonest i),Agent (honest a))))))));
fp_12: iknows(scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absTA(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),SymKey (absKAB(pair(Agent (honest a),Agent (honest a))))))));
fp_13: iknows(scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absTA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (dishonest i),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i))))))));
fp_14: iknows(pair(Agent (honest a),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absTA(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),SymKey (absKAB(pair(Agent (honest a),Agent (honest a)))))))));
fp_15: iknows(pair(Agent (honest a),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absTA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (dishonest i),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i)))))))));
fp_16: iknows(pair(Agent (dishonest i),SymKey (sk(pair(Agent (dishonest i),Agent (honest a))))));
fp_17: iknows(pair(Nonce (absTS(pair(Agent (dishonest i),Agent (dishonest i)))),pair(Agent (dishonest i),SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))))));
fp_18: State (rs,[Agent (honest a),Step 1,SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Agent (dishonest i),Agent (dishonest i),SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Nonce (absTS(pair(Agent (dishonest i),Agent (dishonest i)))),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (dishonest i),Agent (dishonest i)))),pair(Agent (dishonest i),SymKey (sk(pair(Agent (dishonest i),Agent (honest a))))))),pair(Agent (dishonest i),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (dishonest i),Agent (dishonest i)))),pair(Agent (dishonest i),SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))))))),Nonce (absTS(pair(Agent (dishonest i),Agent (dishonest i)))),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (dishonest i),Agent (dishonest i)))),pair(Agent (dishonest i),SymKey (sk(pair(Agent (dishonest i),Agent (honest a))))))),(SID sid)]);
fp_19: State (rs,[Agent (honest a),Step 1,SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),SymKey (sk(pair(Agent (honest a),Agent (honest a)))),Agent (dishonest i),Agent (honest a),SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Nonce (absTS(pair(Agent (honest a),Agent (dishonest i)))),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (dishonest i),SymKey (sk(pair(Agent (dishonest i),Agent (honest a))))))),pair(Agent (honest a),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (dishonest i),SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))))))),Nonce (absTS(pair(Agent (dishonest i),Agent (honest a)))),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (dishonest i),Agent (honest a)))),pair(Agent (honest a),SymKey (sk(pair(Agent (dishonest i),Agent (honest a))))))),(SID sid)]);
fp_20: State (rs,[Agent (honest a),Step 1,SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),SymKey (sk(pair(Agent (honest a),Agent (honest a)))),Agent (dishonest i),Agent (honest a),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i)))),Nonce (absTA(pair(Agent (honest a),Agent (dishonest i)))),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absTA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (dishonest i),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i))))))),pair(Agent (honest a),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absTA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (dishonest i),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i)))))))),Nonce (absTS(pair(Agent (dishonest i),Agent (honest a)))),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (dishonest i),Agent (honest a)))),pair(Agent (honest a),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i))))))),(SID sid)]);
fp_21: State (rs,[Agent (honest a),Step 1,SymKey (sk(pair(Agent (honest a),Agent (honest a)))),SymKey (sk(pair(Agent (honest a),Agent (honest a)))),Agent (honest a),Agent (honest a),SymKey (absKAB(pair(Agent (honest a),Agent (honest a)))),Nonce (absTA(pair(Agent (honest a),Agent (honest a)))),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absTA(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),SymKey (absKAB(pair(Agent (honest a),Agent (honest a))))))),pair(Agent (honest a),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absTA(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),SymKey (absKAB(pair(Agent (honest a),Agent (honest a)))))))),Nonce (absTS(pair(Agent (honest a),Agent (honest a)))),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),SymKey (absKAB(pair(Agent (honest a),Agent (honest a))))))),(SID sid)]);
fp_22: request(Agent (honest a),Agent (dishonest i),Purpose (purposeKAB),SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),(SID sid));
fp_23: State (rB,[Agent (honest a),Step 1,SymKey (sk(pair(Agent (honest a),Agent (honest a)))),Agent (dishonest i),SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Nonce (absTS(pair(Agent (honest a),Agent (dishonest i)))),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (dishonest i),SymKey (sk(pair(Agent (dishonest i),Agent (honest a))))))),(SID sid)]);
fp_24: request(Agent (honest a),Agent (dishonest i),Purpose (purposeKAB),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i)))),(SID sid));
fp_25: State (rB,[Agent (honest a),Step 1,SymKey (sk(pair(Agent (honest a),Agent (honest a)))),Agent (dishonest i),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i)))),Nonce (absTA(pair(Agent (honest a),Agent (dishonest i)))),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absTA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (dishonest i),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i))))))),(SID sid)]);
fp_26: request(Agent (honest a),Agent (honest a),Purpose (purposeKAB),SymKey (absKAB(pair(Agent (honest a),Agent (honest a)))),(SID sid));
fp_27: State (rB,[Agent (honest a),Step 1,SymKey (sk(pair(Agent (honest a),Agent (honest a)))),Agent (honest a),SymKey (absKAB(pair(Agent (honest a),Agent (honest a)))),Nonce (absTA(pair(Agent (honest a),Agent (honest a)))),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absTA(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),SymKey (absKAB(pair(Agent (honest a),Agent (honest a))))))),(SID sid)]);
fp_28: iknows(scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),SymKey (absKAB(pair(Agent (honest a),Agent (honest a))))))));
fp_29: iknows(scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (dishonest i),Agent (honest a)))),pair(Agent (honest a),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i))))))));
fp_30: iknows(scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (dishonest i),Agent (honest a)))),pair(Agent (honest a),SymKey (sk(pair(Agent (dishonest i),Agent (honest a))))))));
fp_31: iknows(Nonce (absTS(pair(Agent (dishonest i),Agent (dishonest i)))));
fp_32: iknows(pair(Agent (honest a),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absTA(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),SymKey (absKAB(pair(Agent (honest a),Agent (honest a)))))))));
fp_33: iknows(pair(Agent (honest a),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absTA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (dishonest i),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i)))))))));
fp_34: iknows(pair(Agent (dishonest i),SymKey (sk(pair(Agent (dishonest i),Agent (honest a))))));
fp_35: iknows(pair(Nonce (absTS(pair(Agent (dishonest i),Agent (dishonest i)))),pair(Agent (dishonest i),SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))))));
fp_36: iknows(pair(Agent (honest a),SymKey (sk(pair(Agent (dishonest i),Agent (honest a))))));
fp_37: iknows(pair(Nonce (absTS(pair(Agent (dishonest i),Agent (honest a)))),pair(Agent (honest a),SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))))));
fp_38: iknows(pair(Agent (honest a),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i))))));
fp_39: iknows(pair(Nonce (absTS(pair(Agent (dishonest i),Agent (honest a)))),pair(Agent (honest a),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i)))))));
fp_40: State (rs,[Agent (honest a),Step 1,SymKey (sk(pair(Agent (honest a),Agent (honest a)))),SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Agent (honest a),Agent (dishonest i),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i)))),Nonce (absTS(pair(Agent (dishonest i),Agent (honest a)))),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (dishonest i),Agent (honest a)))),pair(Agent (honest a),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i))))))),pair(Agent (dishonest i),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (dishonest i),Agent (honest a)))),pair(Agent (honest a),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i)))))))),Nonce (absTS(pair(Agent (honest a),Agent (dishonest i)))),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (dishonest i),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i))))))),(SID sid)]);
fp_41: State (rs,[Agent (honest a),Step 1,SymKey (sk(pair(Agent (honest a),Agent (honest a)))),SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Agent (honest a),Agent (dishonest i),SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Nonce (absTS(pair(Agent (dishonest i),Agent (honest a)))),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (dishonest i),Agent (honest a)))),pair(Agent (honest a),SymKey (sk(pair(Agent (dishonest i),Agent (honest a))))))),pair(Agent (dishonest i),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (dishonest i),Agent (honest a)))),pair(Agent (honest a),SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))))))),Nonce (absTS(pair(Agent (honest a),Agent (dishonest i)))),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (dishonest i),SymKey (sk(pair(Agent (dishonest i),Agent (honest a))))))),(SID sid)]);
fp_42: State (rs,[Agent (honest a),Step 1,SymKey (sk(pair(Agent (honest a),Agent (honest a)))),SymKey (sk(pair(Agent (honest a),Agent (honest a)))),Agent (honest a),Agent (honest a),SymKey (absKAB(pair(Agent (honest a),Agent (honest a)))),Nonce (absTS(pair(Agent (honest a),Agent (honest a)))),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),SymKey (absKAB(pair(Agent (honest a),Agent (honest a))))))),pair(Agent (honest a),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),SymKey (absKAB(pair(Agent (honest a),Agent (honest a)))))))),Nonce (absTS(pair(Agent (honest a),Agent (honest a)))),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),SymKey (absKAB(pair(Agent (honest a),Agent (honest a))))))),(SID sid)]);
fp_43: State (rs,[Agent (honest a),Step 1,SymKey (sk(pair(Agent (honest a),Agent (honest a)))),SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Agent (honest a),Agent (dishonest i),SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Nonce (absTS(pair(Agent (dishonest i),Agent (dishonest i)))),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (dishonest i),Agent (dishonest i)))),pair(Agent (honest a),SymKey (sk(pair(Agent (dishonest i),Agent (honest a))))))),pair(Agent (dishonest i),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (dishonest i),Agent (dishonest i)))),pair(Agent (honest a),SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))))))),Nonce (absTS(pair(Agent (honest a),Agent (dishonest i)))),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (dishonest i),SymKey (sk(pair(Agent (dishonest i),Agent (honest a))))))),(SID sid)]);
fp_44: State (rB,[Agent (honest a),Step 1,SymKey (sk(pair(Agent (honest a),Agent (honest a)))),Agent (honest a),SymKey (absKAB(pair(Agent (honest a),Agent (honest a)))),Nonce (absTS(pair(Agent (honest a),Agent (honest a)))),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),SymKey (absKAB(pair(Agent (honest a),Agent (honest a))))))),(SID sid)]);
fp_45: iknows(scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (dishonest i),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i))))))));
fp_46: iknows(Nonce (absTS(pair(Agent (dishonest i),Agent (honest a)))));
fp_47: iknows(SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i)))));
fp_48: iknows(pair(Agent (honest a),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absTA(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),SymKey (absKAB(pair(Agent (honest a),Agent (honest a)))))))));
fp_49: iknows(pair(Agent (honest a),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absTA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (dishonest i),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i)))))))));
fp_50: iknows(pair(Agent (dishonest i),SymKey (sk(pair(Agent (dishonest i),Agent (honest a))))));
fp_51: iknows(pair(Nonce (absTS(pair(Agent (dishonest i),Agent (dishonest i)))),pair(Agent (dishonest i),SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))))));
fp_52: iknows(pair(Agent (honest a),SymKey (sk(pair(Agent (dishonest i),Agent (honest a))))));
fp_53: iknows(pair(Nonce (absTS(pair(Agent (dishonest i),Agent (honest a)))),pair(Agent (honest a),SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))))));
fp_54: iknows(pair(Agent (honest a),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i))))));
fp_55: iknows(pair(Nonce (absTS(pair(Agent (dishonest i),Agent (honest a)))),pair(Agent (honest a),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i)))))));
fp_56: State (rs,[Agent (honest a),Step 1,SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),SymKey (sk(pair(Agent (honest a),Agent (honest a)))),Agent (dishonest i),Agent (honest a),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i)))),Nonce (absTS(pair(Agent (honest a),Agent (dishonest i)))),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (dishonest i),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i))))))),pair(Agent (honest a),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (dishonest i),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i)))))))),Nonce (absTS(pair(Agent (dishonest i),Agent (honest a)))),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (dishonest i),Agent (honest a)))),pair(Agent (honest a),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i))))))),(SID sid)]);
fp_57: State (rs,[Agent (honest a),Step 1,SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Agent (dishonest i),Agent (dishonest i),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i)))),Nonce (absTS(pair(Agent (dishonest i),Agent (honest a)))),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (dishonest i),Agent (honest a)))),pair(Agent (dishonest i),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i))))))),pair(Agent (dishonest i),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (dishonest i),Agent (honest a)))),pair(Agent (dishonest i),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i)))))))),Nonce (absTS(pair(Agent (dishonest i),Agent (dishonest i)))),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (dishonest i),Agent (dishonest i)))),pair(Agent (dishonest i),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i))))))),(SID sid)]);
fp_58: State (rs,[Agent (honest a),Step 1,SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Agent (dishonest i),Agent (dishonest i),SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Nonce (absTS(pair(Agent (dishonest i),Agent (honest a)))),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (dishonest i),Agent (honest a)))),pair(Agent (dishonest i),SymKey (sk(pair(Agent (dishonest i),Agent (honest a))))))),pair(Agent (dishonest i),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (dishonest i),Agent (honest a)))),pair(Agent (dishonest i),SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))))))),Nonce (absTS(pair(Agent (dishonest i),Agent (dishonest i)))),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (dishonest i),Agent (dishonest i)))),pair(Agent (dishonest i),SymKey (sk(pair(Agent (dishonest i),Agent (honest a))))))),(SID sid)]);
fp_59: State (rs,[Agent (honest a),Step 1,SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Agent (dishonest i),Agent (dishonest i),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i)))),Nonce (absTS(pair(Agent (dishonest i),Agent (dishonest i)))),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (dishonest i),Agent (dishonest i)))),pair(Agent (dishonest i),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i))))))),pair(Agent (dishonest i),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (dishonest i),Agent (dishonest i)))),pair(Agent (dishonest i),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i)))))))),Nonce (absTS(pair(Agent (dishonest i),Agent (dishonest i)))),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (dishonest i),Agent (dishonest i)))),pair(Agent (dishonest i),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i))))))),(SID sid)]);
fp_60: State (rs,[Agent (honest a),Step 1,SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Agent (dishonest i),Agent (dishonest i),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i)))),Nonce (ni),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (ni),pair(Agent (dishonest i),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i))))))),pair(Agent (dishonest i),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (ni),pair(Agent (dishonest i),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i)))))))),Nonce (absTS(pair(Agent (dishonest i),Agent (dishonest i)))),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (dishonest i),Agent (dishonest i)))),pair(Agent (dishonest i),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i))))))),(SID sid)]);
fp_61: State (rs,[Agent (honest a),Step 1,SymKey (sk(pair(Agent (honest a),Agent (honest a)))),SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Agent (honest a),Agent (dishonest i),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i)))),Nonce (absTS(pair(Agent (dishonest i),Agent (dishonest i)))),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (dishonest i),Agent (dishonest i)))),pair(Agent (honest a),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i))))))),pair(Agent (dishonest i),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (dishonest i),Agent (dishonest i)))),pair(Agent (honest a),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i)))))))),Nonce (absTS(pair(Agent (honest a),Agent (dishonest i)))),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (dishonest i),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i))))))),(SID sid)]);
fp_62: State (rs,[Agent (honest a),Step 1,SymKey (sk(pair(Agent (honest a),Agent (honest a)))),SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),Agent (honest a),Agent (dishonest i),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i)))),Nonce (ni),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (ni),pair(Agent (honest a),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i))))))),pair(Agent (dishonest i),scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (ni),pair(Agent (honest a),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i)))))))),Nonce (absTS(pair(Agent (honest a),Agent (dishonest i)))),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (dishonest i),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i))))))),(SID sid)]);
fp_63: State (rB,[Agent (honest a),Step 1,SymKey (sk(pair(Agent (honest a),Agent (honest a)))),Agent (dishonest i),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i)))),Nonce (absTS(pair(Agent (honest a),Agent (dishonest i)))),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (dishonest i),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i))))))),(SID sid)]);
fp_64: iknows(scrypt(SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))),pair(Nonce (absTS(pair(Agent (dishonest i),Agent (dishonest i)))),pair(Agent (dishonest i),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i))))))));
fp_65: iknows(pair(Agent (honest a),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absTA(pair(Agent (honest a),Agent (honest a)))),pair(Agent (honest a),SymKey (absKAB(pair(Agent (honest a),Agent (honest a)))))))));
fp_66: iknows(pair(Agent (honest a),scrypt(SymKey (sk(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (absTA(pair(Agent (honest a),Agent (dishonest i)))),pair(Agent (dishonest i),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i)))))))));
fp_67: iknows(pair(Agent (dishonest i),SymKey (sk(pair(Agent (dishonest i),Agent (honest a))))));
fp_68: iknows(pair(Nonce (absTS(pair(Agent (dishonest i),Agent (dishonest i)))),pair(Agent (dishonest i),SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))))));
fp_69: iknows(pair(Agent (honest a),SymKey (sk(pair(Agent (dishonest i),Agent (honest a))))));
fp_70: iknows(pair(Nonce (absTS(pair(Agent (dishonest i),Agent (honest a)))),pair(Agent (honest a),SymKey (sk(pair(Agent (dishonest i),Agent (honest a)))))));
fp_71: iknows(pair(Agent (honest a),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i))))));
fp_72: iknows(pair(Nonce (absTS(pair(Agent (dishonest i),Agent (honest a)))),pair(Agent (honest a),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i)))))));
fp_73: iknows(pair(Agent (dishonest i),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i))))));
fp_74: iknows(pair(Nonce (absTS(pair(Agent (dishonest i),Agent (dishonest i)))),pair(Agent (dishonest i),SymKey (absKAB(pair(Agent (honest a),Agent (dishonest i)))))));

section abstraction:
TA->Nonce (absTA(pair(A,B)));
KAB->SymKey (absKAB(pair(A,B)));
TS->Nonce (absTS(pair(B,A)))


+ 26
- 0
examples/AnB/nsl-ks.AnB View File

@@ -0,0 +1,26 @@
Protocol: NSL

Types: Agent A,B,s;
Number NA,NB;
Function pk

Knowledge: A: A,pk(A),inv(pk(A)),s,pk(s),B;
B: B,pk(B),inv(pk(B)),s,pk(s);
s: s,pk,inv(pk(s))

Actions:
A->s: A,B
s->A: {B,pk(B)}(inv(pk(s)))
A->B: {NA,A}(pk(B))
B->s: B,A
s->B: {A,pk(A)}(inv(pk(s)))
B->A: {NA,NB,B}(pk(A))
A->B: {NB}(pk(B))

Goals:
A *->* B: NA
B *->* A: NB

Abstraction:
NA -> na(A,B);
NB -> nb(B,A,equals(NA,na(A,B)))

+ 401
- 0
examples/AnB/nsl-ks.fp View File

@@ -0,0 +1,401 @@
Backend: Open-Source Fixedpoint Model-Checker version 2009c
Protocol: NSL
Types:
[(Purpose,["purposeNA","purposeNB"]),(Agent False False,["A","B","s"]),(Number,["NA","NB"]),(Function,["pk"])]
section rules:
step rule_0:
iknows(crypt(K,M));
iknows(inv(K))

=>
iknows(M)

step rule_1:
iknows(crypt(inv(K),M));
iknows(K)

=>
iknows(M)

step rule_2:
iknows(scrypt(K,M));
iknows(K)

=>
iknows(M)

step rule_3:
iknows(pair(M1,M2))

=>
iknows(M1);
iknows(M2)

step rule_4:
secret(M,Agent (honest a));
iknows(M)

=>
attack(pair(secrecy,M))

step rule_5:
request(A,B,Purpose (purposeNA),M,(SID sid))
| B/=Agent (dishonest i);
M/=Nonce (na(pair(B,A)))
=>
attack(pair(authentication,pair(A,pair(B,M))))

step rule_6:
request(A,B,Purpose (purposeNB),M,(SID sid))
| B/=Agent (dishonest i);
M/=Nonce (nb(pair(B,pair(A,Arg1))))
=>
attack(pair(authentication,pair(A,pair(B,M))))

step rule_7:
State (rA,[Agent (A),Step 0,Agent (B),pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (A))),pk(Agent (A)),(SID sid)])

=>
State (rA,[Agent (A),Step 1,Agent (B),pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (A))),pk(Agent (A)),pair(Agent (A),Agent (B)),(SID sid)]);
iknows(pair(Agent (A),Agent (B)))

step rule_8:
State (rs,[Agent (honest a),Step 0,inv(pk(Agent (honest a))),(SID sid)]);
iknows(Agent (A));
iknows(Agent (B))

=>
State (rs,[Agent (honest a),Step 1,inv(pk(Agent (honest a))),Agent (B),Agent (A),pair(Agent (A),Agent (B)),crypt(inv(pk(Agent (honest a))),pair(Agent (B),pk(Agent (B)))),(SID sid)]);
iknows(crypt(inv(pk(Agent (honest a))),pair(Agent (B),pk(Agent (B)))))

step rule_9:
State (rA,[Agent (A),Step 1,Agent (B),pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (A))),pk(Agent (A)),pair(Agent (A),Agent (B)),(SID sid)]);
iknows(crypt(inv(pk(Agent (honest a))),pair(Agent (B),pk(Agent (B)))))

=>
secret(Nonce (na(pair(Agent (A),Agent (B)))),Agent (B));
witness(Agent (A),Agent (B),Purpose (purposeNA),Nonce (na(pair(Agent (A),Agent (B)))));
State (rA,[Agent (A),Step 2,Agent (B),pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (A))),pk(Agent (A)),pair(Agent (A),Agent (B)),pk(Agent (B)),crypt(inv(pk(Agent (honest a))),pair(Agent (B),pk(Agent (B)))),Nonce (na(pair(Agent (A),Agent (B)))),crypt(pk(Agent (B)),pair(Nonce (na(pair(Agent (A),Agent (B)))),Agent (A))),(SID sid)]);
iknows(crypt(pk(Agent (B)),pair(Nonce (na(pair(Agent (A),Agent (B)))),Agent (A))))

step rule_10:
State (rA,[Agent (A),Step 1,Agent (B),pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (A))),pk(Agent (A)),pair(Agent (A),Agent (B)),(SID sid)]);
iknows(inv(pk(Agent (honest a))));
iknows(Agent (B));
iknows(pk(Agent (B)))

=>
secret(Nonce (na(pair(Agent (A),Agent (B)))),Agent (B));
witness(Agent (A),Agent (B),Purpose (purposeNA),Nonce (na(pair(Agent (A),Agent (B)))));
State (rA,[Agent (A),Step 2,Agent (B),pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (A))),pk(Agent (A)),pair(Agent (A),Agent (B)),pk(Agent (B)),crypt(inv(pk(Agent (honest a))),pair(Agent (B),pk(Agent (B)))),Nonce (na(pair(Agent (A),Agent (B)))),crypt(pk(Agent (B)),pair(Nonce (na(pair(Agent (A),Agent (B)))),Agent (A))),(SID sid)]);
iknows(crypt(pk(Agent (B)),pair(Nonce (na(pair(Agent (A),Agent (B)))),Agent (A))))

step rule_11:
State (rA,[Agent (A),Step 1,Agent (B),pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (A))),pk(Agent (A)),pair(Agent (A),Agent (B)),(SID sid)]);
iknows(inv(pk(Agent (honest a))));
iknows(Agent (B))

=>
secret(Nonce (na(pair(Agent (A),Agent (B)))),Agent (B));
witness(Agent (A),Agent (B),Purpose (purposeNA),Nonce (na(pair(Agent (A),Agent (B)))));
State (rA,[Agent (A),Step 2,Agent (B),pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (A))),pk(Agent (A)),pair(Agent (A),Agent (B)),pk(Agent (B)),crypt(inv(pk(Agent (honest a))),pair(Agent (B),pk(Agent (B)))),Nonce (na(pair(Agent (A),Agent (B)))),crypt(pk(Agent (B)),pair(Nonce (na(pair(Agent (A),Agent (B)))),Agent (A))),(SID sid)]);
iknows(crypt(pk(Agent (B)),pair(Nonce (na(pair(Agent (A),Agent (B)))),Agent (A))))

step rule_12:
State (rB,[Agent (B),Step 0,pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (B))),pk(Agent (B)),(SID sid)]);
iknows(crypt(pk(Agent (B)),pair(Nonce (NA),Agent (A))))

=>
State (rB,[Agent (B),Step 1,pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (B))),pk(Agent (B)),Agent (A),Nonce (NA),crypt(pk(Agent (B)),pair(Nonce (NA),Agent (A))),pair(Agent (B),Agent (A)),(SID sid)]);
iknows(pair(Agent (B),Agent (A)))

step rule_13:
State (rB,[Agent (B),Step 0,pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (B))),pk(Agent (B)),(SID sid)]);
iknows(pk(Agent (B)));
iknows(Nonce (NA));
iknows(Agent (A))

=>
State (rB,[Agent (B),Step 1,pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (B))),pk(Agent (B)),Agent (A),Nonce (NA),crypt(pk(Agent (B)),pair(Nonce (NA),Agent (A))),pair(Agent (B),Agent (A)),(SID sid)]);
iknows(pair(Agent (B),Agent (A)))

step rule_14:
State (rB,[Agent (B),Step 0,pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (B))),pk(Agent (B)),(SID sid)]);
iknows(Agent (B));
iknows(Nonce (NA));
iknows(Agent (A))

=>
State (rB,[Agent (B),Step 1,pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (B))),pk(Agent (B)),Agent (A),Nonce (NA),crypt(pk(Agent (B)),pair(Nonce (NA),Agent (A))),pair(Agent (B),Agent (A)),(SID sid)]);
iknows(pair(Agent (B),Agent (A)))

step rule_15:
State (rs,[Agent (honest a),Step 1,inv(pk(Agent (honest a))),Agent (B),Agent (A),pair(Agent (A),Agent (B)),crypt(inv(pk(Agent (honest a))),pair(Agent (B),pk(Agent (B)))),(SID sid)]);
iknows(Agent (B));
iknows(Agent (A))

=>
State (rs,[Agent (honest a),Step 2,inv(pk(Agent (honest a))),Agent (B),Agent (A),pair(Agent (A),Agent (B)),crypt(inv(pk(Agent (honest a))),pair(Agent (B),pk(Agent (B)))),pair(Agent (B),Agent (A)),crypt(inv(pk(Agent (honest a))),pair(Agent (A),pk(Agent (A)))),(SID sid)]);
iknows(crypt(inv(pk(Agent (honest a))),pair(Agent (A),pk(Agent (A)))))

step rule_16:
State (rB,[Agent (B),Step 1,pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (B))),pk(Agent (B)),Agent (A),Nonce (na(pair(Agent (A),Agent (B)))),crypt(pk(Agent (B)),pair(Nonce (na(pair(Agent (A),Agent (B)))),Agent (A))),pair(Agent (B),Agent (A)),(SID sid)]);
iknows(crypt(inv(pk(Agent (honest a))),pair(Agent (A),pk(Agent (A)))))

=>
secret(Nonce (nb(pair(Agent (B),pair(Agent (A),Step 1)))),Agent (A));
witness(Agent (B),Agent (A),Purpose (purposeNB),Nonce (nb(pair(Agent (B),pair(Agent (A),Step 1)))));
State (rB,[Agent (B),Step 2,pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (B))),pk(Agent (B)),Agent (A),Nonce (na(pair(Agent (A),Agent (B)))),crypt(pk(Agent (B)),pair(Nonce (na(pair(Agent (A),Agent (B)))),Agent (A))),pair(Agent (B),Agent (A)),pk(Agent (A)),crypt(inv(pk(Agent (honest a))),pair(Agent (A),pk(Agent (A)))),Nonce (nb(pair(Agent (B),pair(Agent (A),Step 1)))),crypt(pk(Agent (A)),pair(Nonce (na(pair(Agent (A),Agent (B)))),pair(Nonce (nb(pair(Agent (B),pair(Agent (A),Step 1)))),Agent (B)))),(SID sid)]);
iknows(crypt(pk(Agent (A)),pair(Nonce (na(pair(Agent (A),Agent (B)))),pair(Nonce (nb(pair(Agent (B),pair(Agent (A),Step 1)))),Agent (B)))))

step rule_17:
State (rB,[Agent (B),Step 1,pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (B))),pk(Agent (B)),Agent (A),Nonce (na(pair(Agent (A),Agent (B)))),crypt(pk(Agent (B)),pair(Nonce (na(pair(Agent (A),Agent (B)))),Agent (A))),pair(Agent (B),Agent (A)),(SID sid)]);
iknows(inv(pk(Agent (honest a))));
iknows(Agent (A));
iknows(pk(Agent (A)))

=>
secret(Nonce (nb(pair(Agent (B),pair(Agent (A),Step 1)))),Agent (A));
witness(Agent (B),Agent (A),Purpose (purposeNB),Nonce (nb(pair(Agent (B),pair(Agent (A),Step 1)))));
State (rB,[Agent (B),Step 2,pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (B))),pk(Agent (B)),Agent (A),Nonce (na(pair(Agent (A),Agent (B)))),crypt(pk(Agent (B)),pair(Nonce (na(pair(Agent (A),Agent (B)))),Agent (A))),pair(Agent (B),Agent (A)),pk(Agent (A)),crypt(inv(pk(Agent (honest a))),pair(Agent (A),pk(Agent (A)))),Nonce (nb(pair(Agent (B),pair(Agent (A),Step 1)))),crypt(pk(Agent (A)),pair(Nonce (na(pair(Agent (A),Agent (B)))),pair(Nonce (nb(pair(Agent (B),pair(Agent (A),Step 1)))),Agent (B)))),(SID sid)]);
iknows(crypt(pk(Agent (A)),pair(Nonce (na(pair(Agent (A),Agent (B)))),pair(Nonce (nb(pair(Agent (B),pair(Agent (A),Step 1)))),Agent (B)))))

step rule_18:
State (rB,[Agent (B),Step 1,pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (B))),pk(Agent (B)),Agent (A),Nonce (na(pair(Agent (A),Agent (B)))),crypt(pk(Agent (B)),pair(Nonce (na(pair(Agent (A),Agent (B)))),Agent (A))),pair(Agent (B),Agent (A)),(SID sid)]);
iknows(inv(pk(Agent (honest a))));
iknows(Agent (A))

=>
secret(Nonce (nb(pair(Agent (B),pair(Agent (A),Step 1)))),Agent (A));
witness(Agent (B),Agent (A),Purpose (purposeNB),Nonce (nb(pair(Agent (B),pair(Agent (A),Step 1)))));
State (rB,[Agent (B),Step 2,pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (B))),pk(Agent (B)),Agent (A),Nonce (na(pair(Agent (A),Agent (B)))),crypt(pk(Agent (B)),pair(Nonce (na(pair(Agent (A),Agent (B)))),Agent (A))),pair(Agent (B),Agent (A)),pk(Agent (A)),crypt(inv(pk(Agent (honest a))),pair(Agent (A),pk(Agent (A)))),Nonce (nb(pair(Agent (B),pair(Agent (A),Step 1)))),crypt(pk(Agent (A)),pair(Nonce (na(pair(Agent (A),Agent (B)))),pair(Nonce (nb(pair(Agent (B),pair(Agent (A),Step 1)))),Agent (B)))),(SID sid)]);
iknows(crypt(pk(Agent (A)),pair(Nonce (na(pair(Agent (A),Agent (B)))),pair(Nonce (nb(pair(Agent (B),pair(Agent (A),Step 1)))),Agent (B)))))

step rule_19:
State (rB,[Agent (B),Step 1,pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (B))),pk(Agent (B)),Agent (A),Nonce (NA),crypt(pk(Agent (B)),pair(Nonce (NA),Agent (A))),pair(Agent (B),Agent (A)),(SID sid)]);
iknows(crypt(inv(pk(Agent (honest a))),pair(Agent (A),pk(Agent (A)))))
| Nonce (NA)/=Nonce (na(pair(Agent (A),Agent (B))))
=>
secret(Nonce (nb(pair(Agent (B),pair(Agent (A),Step 0)))),Agent (A));
witness(Agent (B),Agent (A),Purpose (purposeNB),Nonce (nb(pair(Agent (B),pair(Agent (A),Step 0)))));
State (rB,[Agent (B),Step 2,pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (B))),pk(Agent (B)),Agent (A),Nonce (NA),crypt(pk(Agent (B)),pair(Nonce (NA),Agent (A))),pair(Agent (B),Agent (A)),pk(Agent (A)),crypt(inv(pk(Agent (honest a))),pair(Agent (A),pk(Agent (A)))),Nonce (nb(pair(Agent (B),pair(Agent (A),Step 0)))),crypt(pk(Agent (A)),pair(Nonce (NA),pair(Nonce (nb(pair(Agent (B),pair(Agent (A),Step 0)))),Agent (B)))),(SID sid)]);
iknows(crypt(pk(Agent (A)),pair(Nonce (NA),pair(Nonce (nb(pair(Agent (B),pair(Agent (A),Step 0)))),Agent (B)))))

step rule_20:
State (rB,[Agent (B),Step 1,pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (B))),pk(Agent (B)),Agent (A),Nonce (NA),crypt(pk(Agent (B)),pair(Nonce (NA),Agent (A))),pair(Agent (B),Agent (A)),(SID sid)]);
iknows(inv(pk(Agent (honest a))));
iknows(Agent (A));
iknows(pk(Agent (A)))
| Nonce (NA)/=Nonce (na(pair(Agent (A),Agent (B))))
=>
secret(Nonce (nb(pair(Agent (B),pair(Agent (A),Step 0)))),Agent (A));
witness(Agent (B),Agent (A),Purpose (purposeNB),Nonce (nb(pair(Agent (B),pair(Agent (A),Step 0)))));
State (rB,[Agent (B),Step 2,pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (B))),pk(Agent (B)),Agent (A),Nonce (NA),crypt(pk(Agent (B)),pair(Nonce (NA),Agent (A))),pair(Agent (B),Agent (A)),pk(Agent (A)),crypt(inv(pk(Agent (honest a))),pair(Agent (A),pk(Agent (A)))),Nonce (nb(pair(Agent (B),pair(Agent (A),Step 0)))),crypt(pk(Agent (A)),pair(Nonce (NA),pair(Nonce (nb(pair(Agent (B),pair(Agent (A),Step 0)))),Agent (B)))),(SID sid)]);
iknows(crypt(pk(Agent (A)),pair(Nonce (NA),pair(Nonce (nb(pair(Agent (B),pair(Agent (A),Step 0)))),Agent (B)))))

step rule_21:
State (rB,[Agent (B),Step 1,pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (B))),pk(Agent (B)),Agent (A),Nonce (NA),crypt(pk(Agent (B)),pair(Nonce (NA),Agent (A))),pair(Agent (B),Agent (A)),(SID sid)]);
iknows(inv(pk(Agent (honest a))));
iknows(Agent (A))
| Nonce (NA)/=Nonce (na(pair(Agent (A),Agent (B))))
=>
secret(Nonce (nb(pair(Agent (B),pair(Agent (A),Step 0)))),Agent (A));
witness(Agent (B),Agent (A),Purpose (purposeNB),Nonce (nb(pair(Agent (B),pair(Agent (A),Step 0)))));
State (rB,[Agent (B),Step 2,pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (B))),pk(Agent (B)),Agent (A),Nonce (NA),crypt(pk(Agent (B)),pair(Nonce (NA),Agent (A))),pair(Agent (B),Agent (A)),pk(Agent (A)),crypt(inv(pk(Agent (honest a))),pair(Agent (A),pk(Agent (A)))),Nonce (nb(pair(Agent (B),pair(Agent (A),Step 0)))),crypt(pk(Agent (A)),pair(Nonce (NA),pair(Nonce (nb(pair(Agent (B),pair(Agent (A),Step 0)))),Agent (B)))),(SID sid)]);
iknows(crypt(pk(Agent (A)),pair(Nonce (NA),pair(Nonce (nb(pair(Agent (B),pair(Agent (A),Step 0)))),Agent (B)))))

step rule_22:
State (rA,[Agent (A),Step 2,Agent (B),pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (A))),pk(Agent (A)),pair(Agent (A),Agent (B)),pk(Agent (B)),crypt(inv(pk(Agent (honest a))),pair(Agent (B),pk(Agent (B)))),Nonce (NA),crypt(pk(Agent (B)),pair(Nonce (NA),Agent (A))),(SID sid)]);
iknows(crypt(pk(Agent (A)),pair(Nonce (NA),pair(Nonce (NB),Agent (B)))))

=>
request(Agent (A),Agent (B),Purpose (purposeNB),Nonce (NB),(SID sid));
State (rA,[Agent (A),Step 3,Agent (B),pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (A))),pk(Agent (A)),pair(Agent (A),Agent (B)),pk(Agent (B)),crypt(inv(pk(Agent (honest a))),pair(Agent (B),pk(Agent (B)))),Nonce (NA),crypt(pk(Agent (B)),pair(Nonce (NA),Agent (A))),Nonce (NB),crypt(pk(Agent (A)),pair(Nonce (NA),pair(Nonce (NB),Agent (B)))),crypt(pk(Agent (B)),Nonce (NB)),(SID sid)]);
iknows(crypt(pk(Agent (B)),Nonce (NB)))

step rule_23:
State (rA,[Agent (A),Step 2,Agent (B),pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (A))),pk(Agent (A)),pair(Agent (A),Agent (B)),pk(Agent (B)),crypt(inv(pk(Agent (honest a))),pair(Agent (B),pk(Agent (B)))),Nonce (NA),crypt(pk(Agent (B)),pair(Nonce (NA),Agent (A))),(SID sid)]);
iknows(pk(Agent (A)));
iknows(Nonce (NA));
iknows(Nonce (NB));
iknows(Agent (B))

=>
request(Agent (A),Agent (B),Purpose (purposeNB),Nonce (NB),(SID sid));
State (rA,[Agent (A),Step 3,Agent (B),pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (A))),pk(Agent (A)),pair(Agent (A),Agent (B)),pk(Agent (B)),crypt(inv(pk(Agent (honest a))),pair(Agent (B),pk(Agent (B)))),Nonce (NA),crypt(pk(Agent (B)),pair(Nonce (NA),Agent (A))),Nonce (NB),crypt(pk(Agent (A)),pair(Nonce (NA),pair(Nonce (NB),Agent (B)))),crypt(pk(Agent (B)),Nonce (NB)),(SID sid)]);
iknows(crypt(pk(Agent (B)),Nonce (NB)))

step rule_24:
State (rA,[Agent (A),Step 2,Agent (B),pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (A))),pk(Agent (A)),pair(Agent (A),Agent (B)),pk(Agent (B)),crypt(inv(pk(Agent (honest a))),pair(Agent (B),pk(Agent (B)))),Nonce (NA),crypt(pk(Agent (B)),pair(Nonce (NA),Agent (A))),(SID sid)]);
iknows(Agent (A));
iknows(Nonce (NA));
iknows(Nonce (NB));
iknows(Agent (B))

=>
request(Agent (A),Agent (B),Purpose (purposeNB),Nonce (NB),(SID sid));
State (rA,[Agent (A),Step 3,Agent (B),pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (A))),pk(Agent (A)),pair(Agent (A),Agent (B)),pk(Agent (B)),crypt(inv(pk(Agent (honest a))),pair(Agent (B),pk(Agent (B)))),Nonce (NA),crypt(pk(Agent (B)),pair(Nonce (NA),Agent (A))),Nonce (NB),crypt(pk(Agent (A)),pair(Nonce (NA),pair(Nonce (NB),Agent (B)))),crypt(pk(Agent (B)),Nonce (NB)),(SID sid)]);
iknows(crypt(pk(Agent (B)),Nonce (NB)))

step rule_25:
State (rB,[Agent (B),Step 2,pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (B))),pk(Agent (B)),Agent (A),Nonce (NA),crypt(pk(Agent (B)),pair(Nonce (NA),Agent (A))),pair(Agent (B),Agent (A)),pk(Agent (A)),crypt(inv(pk(Agent (honest a))),pair(Agent (A),pk(Agent (A)))),Nonce (NB),crypt(pk(Agent (A)),pair(Nonce (NA),pair(Nonce (NB),Agent (B)))),(SID sid)]);
iknows(crypt(pk(Agent (B)),Nonce (NB)))

=>
request(Agent (B),Agent (A),Purpose (purposeNA),Nonce (NA),(SID sid));
State (rB,[Agent (B),Step 3,pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (B))),pk(Agent (B)),Agent (A),Nonce (NA),crypt(pk(Agent (B)),pair(Nonce (NA),Agent (A))),pair(Agent (B),Agent (A)),pk(Agent (A)),crypt(inv(pk(Agent (honest a))),pair(Agent (A),pk(Agent (A)))),Nonce (NB),crypt(pk(Agent (A)),pair(Nonce (NA),pair(Nonce (NB),Agent (B)))),crypt(pk(Agent (B)),Nonce (NB)),(SID sid)])

step rule_26:
State (rB,[Agent (B),Step 2,pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (B))),pk(Agent (B)),Agent (A),Nonce (NA),crypt(pk(Agent (B)),pair(Nonce (NA),Agent (A))),pair(Agent (B),Agent (A)),pk(Agent (A)),crypt(inv(pk(Agent (honest a))),pair(Agent (A),pk(Agent (A)))),Nonce (NB),crypt(pk(Agent (A)),pair(Nonce (NA),pair(Nonce (NB),Agent (B)))),(SID sid)]);
iknows(pk(Agent (B)));
iknows(Nonce (NB))

=>
request(Agent (B),Agent (A),Purpose (purposeNA),Nonce (NA),(SID sid));
State (rB,[Agent (B),Step 3,pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (B))),pk(Agent (B)),Agent (A),Nonce (NA),crypt(pk(Agent (B)),pair(Nonce (NA),Agent (A))),pair(Agent (B),Agent (A)),pk(Agent (A)),crypt(inv(pk(Agent (honest a))),pair(Agent (A),pk(Agent (A)))),Nonce (NB),crypt(pk(Agent (A)),pair(Nonce (NA),pair(Nonce (NB),Agent (B)))),crypt(pk(Agent (B)),Nonce (NB)),(SID sid)])

step rule_27:
State (rB,[Agent (B),Step 2,pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (B))),pk(Agent (B)),Agent (A),Nonce (NA),crypt(pk(Agent (B)),pair(Nonce (NA),Agent (A))),pair(Agent (B),Agent (A)),pk(Agent (A)),crypt(inv(pk(Agent (honest a))),pair(Agent (A),pk(Agent (A)))),Nonce (NB),crypt(pk(Agent (A)),pair(Nonce (NA),pair(Nonce (NB),Agent (B)))),(SID sid)]);
iknows(Agent (B));
iknows(Nonce (NB))

=>
request(Agent (B),Agent (A),Purpose (purposeNA),Nonce (NA),(SID sid));
State (rB,[Agent (B),Step 3,pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (B))),pk(Agent (B)),Agent (A),Nonce (NA),crypt(pk(Agent (B)),pair(Nonce (NA),Agent (A))),pair(Agent (B),Agent (A)),pk(Agent (A)),crypt(inv(pk(Agent (honest a))),pair(Agent (A),pk(Agent (A)))),Nonce (NB),crypt(pk(Agent (A)),pair(Nonce (NA),pair(Nonce (NB),Agent (B)))),crypt(pk(Agent (B)),Nonce (NB)),(SID sid)])


section initial state:
init_0: iknows(Nonce (ni));
init_1: iknows(Agent (dishonest i));
init_2: State (rA,[Agent (honest a),Step 0,Agent (dishonest i),pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (honest a))),pk(Agent (honest a)),(SID sid)]);
init_3: State (rA,[Agent (honest a),Step 0,Agent (honest a),pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (honest a))),pk(Agent (honest a)),(SID sid)]);
init_4: iknows(Step 0);
init_5: iknows(pk(Agent (honest a)));
init_6: iknows(Agent (honest a));
init_7: iknows(inv(pk(Agent (dishonest i))));
init_8: iknows(pk(Agent (dishonest i)));
init_9: iknows((SID sid));
init_10: iknows(Agent (honest a));
init_11: State (rB,[Agent (honest a),Step 0,pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (honest a))),pk(Agent (honest a)),(SID sid)]);
init_12: State (rs,[Agent (honest a),Step 0,inv(pk(Agent (honest a))),(SID sid)]);

section fixedpoint:
fp_0: iknows(pair(Agent (honest a),Agent (honest a)));
fp_1: iknows(pair(Agent (honest a),Agent (dishonest i)));
fp_2: State (rA,[Agent (honest a),Step 1,Agent (dishonest i),pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (honest a))),pk(Agent (honest a)),pair(Agent (honest a),Agent (dishonest i)),(SID sid)]);
fp_3: State (rA,[Agent (honest a),Step 1,Agent (honest a),pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (honest a))),pk(Agent (honest a)),pair(Agent (honest a),Agent (honest a)),(SID sid)]);
fp_4: State (rs,[Agent (honest a),Step 1,inv(pk(Agent (honest a))),Agent (dishonest i),Agent (dishonest i),pair(Agent (dishonest i),Agent (dishonest i)),crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),(SID sid)]);
fp_5: State (rs,[Agent (honest a),Step 1,inv(pk(Agent (honest a))),Agent (honest a),Agent (dishonest i),pair(Agent (dishonest i),Agent (honest a)),crypt(inv(pk(Agent (honest a))),pair(Agent (honest a),pk(Agent (honest a)))),(SID sid)]);
fp_6: State (rs,[Agent (honest a),Step 1,inv(pk(Agent (honest a))),Agent (dishonest i),Agent (honest a),pair(Agent (honest a),Agent (dishonest i)),crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),(SID sid)]);
fp_7: State (rs,[Agent (honest a),Step 1,inv(pk(Agent (honest a))),Agent (honest a),Agent (honest a),pair(Agent (honest a),Agent (honest a)),crypt(inv(pk(Agent (honest a))),pair(Agent (honest a),pk(Agent (honest a)))),(SID sid)]);
fp_8: State (rB,[Agent (honest a),Step 1,pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (honest a))),pk(Agent (honest a)),Agent (dishonest i),Nonce (ni),crypt(pk(Agent (honest a)),pair(Nonce (ni),Agent (dishonest i))),pair(Agent (honest a),Agent (dishonest i)),(SID sid)]);
fp_9: State (rB,[Agent (honest a),Step 1,pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (honest a))),pk(Agent (honest a)),Agent (honest a),Nonce (ni),crypt(pk(Agent (honest a)),pair(Nonce (ni),Agent (honest a))),pair(Agent (honest a),Agent (honest a)),(SID sid)]);
fp_10: iknows(crypt(inv(pk(Agent (honest a))),pair(Agent (honest a),pk(Agent (honest a)))));
fp_11: iknows(crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))));
fp_12: iknows(pair(Agent (honest a),Agent (honest a)));
fp_13: iknows(pair(Agent (honest a),Agent (dishonest i)));
fp_14: iknows(pair(Agent (dishonest i),pk(Agent (dishonest i))));
fp_15: iknows(pair(Agent (honest a),pk(Agent (honest a))));
fp_16: secret(Nonce (na(pair(Agent (honest a),Agent (dishonest i)))),Agent (dishonest i));
fp_17: witness(Agent (honest a),Agent (dishonest i),Purpose (purposeNA),Nonce (na(pair(Agent (honest a),Agent (dishonest i)))));
fp_18: State (rA,[Agent (honest a),Step 2,Agent (dishonest i),pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (honest a))),pk(Agent (honest a)),pair(Agent (honest a),Agent (dishonest i)),pk(Agent (dishonest i)),crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),Nonce (na(pair(Agent (honest a),Agent (dishonest i)))),crypt(pk(Agent (dishonest i)),pair(Nonce (na(pair(Agent (honest a),Agent (dishonest i)))),Agent (honest a))),(SID sid)]);
fp_19: secret(Nonce (na(pair(Agent (honest a),Agent (honest a)))),Agent (honest a));
fp_20: witness(Agent (honest a),Agent (honest a),Purpose (purposeNA),Nonce (na(pair(Agent (honest a),Agent (honest a)))));
fp_21: State (rA,[Agent (honest a),Step 2,Agent (honest a),pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (honest a))),pk(Agent (honest a)),pair(Agent (honest a),Agent (honest a)),pk(Agent (honest a)),crypt(inv(pk(Agent (honest a))),pair(Agent (honest a),pk(Agent (honest a)))),Nonce (na(pair(Agent (honest a),Agent (honest a)))),crypt(pk(Agent (honest a)),pair(Nonce (na(pair(Agent (honest a),Agent (honest a)))),Agent (honest a))),(SID sid)]);
fp_22: State (rs,[Agent (honest a),Step 2,inv(pk(Agent (honest a))),Agent (dishonest i),Agent (dishonest i),pair(Agent (dishonest i),Agent (dishonest i)),crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),pair(Agent (dishonest i),Agent (dishonest i)),crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),(SID sid)]);
fp_23: State (rs,[Agent (honest a),Step 2,inv(pk(Agent (honest a))),Agent (honest a),Agent (dishonest i),pair(Agent (dishonest i),Agent (honest a)),crypt(inv(pk(Agent (honest a))),pair(Agent (honest a),pk(Agent (honest a)))),pair(Agent (honest a),Agent (dishonest i)),crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),(SID sid)]);
fp_24: State (rs,[Agent (honest a),Step 2,inv(pk(Agent (honest a))),Agent (dishonest i),Agent (honest a),pair(Agent (honest a),Agent (dishonest i)),crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),pair(Agent (dishonest i),Agent (honest a)),crypt(inv(pk(Agent (honest a))),pair(Agent (honest a),pk(Agent (honest a)))),(SID sid)]);
fp_25: State (rs,[Agent (honest a),Step 2,inv(pk(Agent (honest a))),Agent (honest a),Agent (honest a),pair(Agent (honest a),Agent (honest a)),crypt(inv(pk(Agent (honest a))),pair(Agent (honest a),pk(Agent (honest a)))),pair(Agent (honest a),Agent (honest a)),crypt(inv(pk(Agent (honest a))),pair(Agent (honest a),pk(Agent (honest a)))),(SID sid)]);
fp_26: secret(Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),Agent (dishonest i));
fp_27: witness(Agent (honest a),Agent (dishonest i),Purpose (purposeNB),Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))));
fp_28: State (rB,[Agent (honest a),Step 2,pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (honest a))),pk(Agent (honest a)),Agent (dishonest i),Nonce (ni),crypt(pk(Agent (honest a)),pair(Nonce (ni),Agent (dishonest i))),pair(Agent (honest a),Agent (dishonest i)),pk(Agent (dishonest i)),crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),crypt(pk(Agent (dishonest i)),pair(Nonce (ni),pair(Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),Agent (honest a)))),(SID sid)]);
fp_29: secret(Nonce (nb(pair(Agent (honest a),pair(Agent (honest a),Step 0)))),Agent (honest a));
fp_30: witness(Agent (honest a),Agent (honest a),Purpose (purposeNB),Nonce (nb(pair(Agent (honest a),pair(Agent (honest a),Step 0)))));
fp_31: State (rB,[Agent (honest a),Step 2,pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (honest a))),pk(Agent (honest a)),Agent (honest a),Nonce (ni),crypt(pk(Agent (honest a)),pair(Nonce (ni),Agent (honest a))),pair(Agent (honest a),Agent (honest a)),pk(Agent (honest a)),crypt(inv(pk(Agent (honest a))),pair(Agent (honest a),pk(Agent (honest a)))),Nonce (nb(pair(Agent (honest a),pair(Agent (honest a),Step 0)))),crypt(pk(Agent (honest a)),pair(Nonce (ni),pair(Nonce (nb(pair(Agent (honest a),pair(Agent (honest a),Step 0)))),Agent (honest a)))),(SID sid)]);
fp_32: iknows(crypt(pk(Agent (honest a)),pair(Nonce (ni),pair(Nonce (nb(pair(Agent (honest a),pair(Agent (honest a),Step 0)))),Agent (honest a)))));
fp_33: iknows(crypt(pk(Agent (dishonest i)),pair(Nonce (ni),pair(Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),Agent (honest a)))));
fp_34: iknows(crypt(pk(Agent (honest a)),pair(Nonce (na(pair(Agent (honest a),Agent (honest a)))),Agent (honest a))));
fp_35: iknows(crypt(pk(Agent (dishonest i)),pair(Nonce (na(pair(Agent (honest a),Agent (dishonest i)))),Agent (honest a))));
fp_36: iknows(pair(Agent (honest a),Agent (honest a)));
fp_37: iknows(pair(Agent (honest a),Agent (dishonest i)));
fp_38: iknows(pair(Agent (dishonest i),pk(Agent (dishonest i))));
fp_39: iknows(pair(Agent (honest a),pk(Agent (honest a))));
fp_40: iknows(pair(Nonce (na(pair(Agent (honest a),Agent (dishonest i)))),Agent (honest a)));
fp_41: iknows(pair(Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),Agent (honest a)));
fp_42: iknows(pair(Nonce (ni),pair(Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),Agent (honest a))));
fp_43: State (rB,[Agent (honest a),Step 1,pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (honest a))),pk(Agent (honest a)),Agent (honest a),Nonce (na(pair(Agent (honest a),Agent (honest a)))),crypt(pk(Agent (honest a)),pair(Nonce (na(pair(Agent (honest a),Agent (honest a)))),Agent (honest a))),pair(Agent (honest a),Agent (honest a)),(SID sid)]);
fp_44: iknows(Nonce (na(pair(Agent (honest a),Agent (dishonest i)))));
fp_45: iknows(Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))));
fp_46: iknows(pair(Agent (honest a),Agent (honest a)));
fp_47: iknows(pair(Agent (honest a),Agent (dishonest i)));
fp_48: iknows(pair(Agent (dishonest i),pk(Agent (dishonest i))));
fp_49: iknows(pair(Agent (honest a),pk(Agent (honest a))));
fp_50: iknows(pair(Nonce (na(pair(Agent (honest a),Agent (dishonest i)))),Agent (honest a)));
fp_51: iknows(pair(Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),Agent (honest a)));
fp_52: iknows(pair(Nonce (ni),pair(Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),Agent (honest a))));
fp_53: State (rB,[Agent (honest a),Step 1,pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (honest a))),pk(Agent (honest a)),Agent (dishonest i),Nonce (na(pair(Agent (honest a),Agent (dishonest i)))),crypt(pk(Agent (honest a)),pair(Nonce (na(pair(Agent (honest a),Agent (dishonest i)))),Agent (dishonest i))),pair(Agent (honest a),Agent (dishonest i)),(SID sid)]);
fp_54: State (rB,[Agent (honest a),Step 1,pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (honest a))),pk(Agent (honest a)),Agent (honest a),Nonce (na(pair(Agent (honest a),Agent (dishonest i)))),crypt(pk(Agent (honest a)),pair(Nonce (na(pair(Agent (honest a),Agent (dishonest i)))),Agent (honest a))),pair(Agent (honest a),Agent (honest a)),(SID sid)]);
fp_55: State (rB,[Agent (honest a),Step 1,pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (honest a))),pk(Agent (honest a)),Agent (dishonest i),Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),crypt(pk(Agent (honest a)),pair(Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),Agent (dishonest i))),pair(Agent (honest a),Agent (dishonest i)),(SID sid)]);
fp_56: State (rB,[Agent (honest a),Step 1,pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (honest a))),pk(Agent (honest a)),Agent (honest a),Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),crypt(pk(Agent (honest a)),pair(Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),Agent (honest a))),pair(Agent (honest a),Agent (honest a)),(SID sid)]);
fp_57: secret(Nonce (nb(pair(Agent (honest a),pair(Agent (honest a),Step 1)))),Agent (honest a));
fp_58: witness(Agent (honest a),Agent (honest a),Purpose (purposeNB),Nonce (nb(pair(Agent (honest a),pair(Agent (honest a),Step 1)))));
fp_59: State (rB,[Agent (honest a),Step 2,pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (honest a))),pk(Agent (honest a)),Agent (honest a),Nonce (na(pair(Agent (honest a),Agent (honest a)))),crypt(pk(Agent (honest a)),pair(Nonce (na(pair(Agent (honest a),Agent (honest a)))),Agent (honest a))),pair(Agent (honest a),Agent (honest a)),pk(Agent (honest a)),crypt(inv(pk(Agent (honest a))),pair(Agent (honest a),pk(Agent (honest a)))),Nonce (nb(pair(Agent (honest a),pair(Agent (honest a),Step 1)))),crypt(pk(Agent (honest a)),pair(Nonce (na(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (nb(pair(Agent (honest a),pair(Agent (honest a),Step 1)))),Agent (honest a)))),(SID sid)]);
fp_60: request(Agent (honest a),Agent (dishonest i),Purpose (purposeNB),Nonce (na(pair(Agent (honest a),Agent (dishonest i)))),(SID sid));
fp_61: State (rA,[Agent (honest a),Step 3,Agent (dishonest i),pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (honest a))),pk(Agent (honest a)),pair(Agent (honest a),Agent (dishonest i)),pk(Agent (dishonest i)),crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),Nonce (na(pair(Agent (honest a),Agent (dishonest i)))),crypt(pk(Agent (dishonest i)),pair(Nonce (na(pair(Agent (honest a),Agent (dishonest i)))),Agent (honest a))),Nonce (na(pair(Agent (honest a),Agent (dishonest i)))),crypt(pk(Agent (honest a)),pair(Nonce (na(pair(Agent (honest a),Agent (dishonest i)))),pair(Nonce (na(pair(Agent (honest a),Agent (dishonest i)))),Agent (dishonest i)))),crypt(pk(Agent (dishonest i)),Nonce (na(pair(Agent (honest a),Agent (dishonest i))))),(SID sid)]);
fp_62: request(Agent (honest a),Agent (dishonest i),Purpose (purposeNB),Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),(SID sid));
fp_63: State (rA,[Agent (honest a),Step 3,Agent (dishonest i),pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (honest a))),pk(Agent (honest a)),pair(Agent (honest a),Agent (dishonest i)),pk(Agent (dishonest i)),crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),Nonce (na(pair(Agent (honest a),Agent (dishonest i)))),crypt(pk(Agent (dishonest i)),pair(Nonce (na(pair(Agent (honest a),Agent (dishonest i)))),Agent (honest a))),Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),crypt(pk(Agent (honest a)),pair(Nonce (na(pair(Agent (honest a),Agent (dishonest i)))),pair(Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),Agent (dishonest i)))),crypt(pk(Agent (dishonest i)),Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0))))),(SID sid)]);
fp_64: request(Agent (honest a),Agent (dishonest i),Purpose (purposeNB),Nonce (ni),(SID sid));
fp_65: State (rA,[Agent (honest a),Step 3,Agent (dishonest i),pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (honest a))),pk(Agent (honest a)),pair(Agent (honest a),Agent (dishonest i)),pk(Agent (dishonest i)),crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),Nonce (na(pair(Agent (honest a),Agent (dishonest i)))),crypt(pk(Agent (dishonest i)),pair(Nonce (na(pair(Agent (honest a),Agent (dishonest i)))),Agent (honest a))),Nonce (ni),crypt(pk(Agent (honest a)),pair(Nonce (na(pair(Agent (honest a),Agent (dishonest i)))),pair(Nonce (ni),Agent (dishonest i)))),crypt(pk(Agent (dishonest i)),Nonce (ni)),(SID sid)]);
fp_66: request(Agent (honest a),Agent (dishonest i),Purpose (purposeNA),Nonce (ni),(SID sid));
fp_67: State (rB,[Agent (honest a),Step 3,pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (honest a))),pk(Agent (honest a)),Agent (dishonest i),Nonce (ni),crypt(pk(Agent (honest a)),pair(Nonce (ni),Agent (dishonest i))),pair(Agent (honest a),Agent (dishonest i)),pk(Agent (dishonest i)),crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),crypt(pk(Agent (dishonest i)),pair(Nonce (ni),pair(Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),Agent (honest a)))),crypt(pk(Agent (honest a)),Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0))))),(SID sid)]);
fp_68: iknows(crypt(pk(Agent (dishonest i)),Nonce (ni)));
fp_69: iknows(crypt(pk(Agent (dishonest i)),Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0))))));
fp_70: iknows(crypt(pk(Agent (dishonest i)),Nonce (na(pair(Agent (honest a),Agent (dishonest i))))));
fp_71: iknows(crypt(pk(Agent (honest a)),pair(Nonce (na(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (nb(pair(Agent (honest a),pair(Agent (honest a),Step 1)))),Agent (honest a)))));
fp_72: iknows(pair(Agent (honest a),Agent (honest a)));
fp_73: iknows(pair(Agent (honest a),Agent (dishonest i)));
fp_74: iknows(pair(Agent (dishonest i),pk(Agent (dishonest i))));
fp_75: iknows(pair(Agent (honest a),pk(Agent (honest a))));
fp_76: iknows(pair(Nonce (na(pair(Agent (honest a),Agent (dishonest i)))),Agent (honest a)));
fp_77: iknows(pair(Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),Agent (honest a)));
fp_78: iknows(pair(Nonce (ni),pair(Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),Agent (honest a))));
fp_79: State (rB,[Agent (honest a),Step 2,pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (honest a))),pk(Agent (honest a)),Agent (dishonest i),Nonce (na(pair(Agent (honest a),Agent (dishonest i)))),crypt(pk(Agent (honest a)),pair(Nonce (na(pair(Agent (honest a),Agent (dishonest i)))),Agent (dishonest i))),pair(Agent (honest a),Agent (dishonest i)),pk(Agent (dishonest i)),crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),crypt(pk(Agent (dishonest i)),pair(Nonce (na(pair(Agent (honest a),Agent (dishonest i)))),pair(Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),Agent (honest a)))),(SID sid)]);
fp_80: State (rB,[Agent (honest a),Step 2,pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (honest a))),pk(Agent (honest a)),Agent (honest a),Nonce (na(pair(Agent (honest a),Agent (dishonest i)))),crypt(pk(Agent (honest a)),pair(Nonce (na(pair(Agent (honest a),Agent (dishonest i)))),Agent (honest a))),pair(Agent (honest a),Agent (honest a)),pk(Agent (honest a)),crypt(inv(pk(Agent (honest a))),pair(Agent (honest a),pk(Agent (honest a)))),Nonce (nb(pair(Agent (honest a),pair(Agent (honest a),Step 0)))),crypt(pk(Agent (honest a)),pair(Nonce (na(pair(Agent (honest a),Agent (dishonest i)))),pair(Nonce (nb(pair(Agent (honest a),pair(Agent (honest a),Step 0)))),Agent (honest a)))),(SID sid)]);
fp_81: State (rB,[Agent (honest a),Step 2,pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (honest a))),pk(Agent (honest a)),Agent (dishonest i),Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),crypt(pk(Agent (honest a)),pair(Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),Agent (dishonest i))),pair(Agent (honest a),Agent (dishonest i)),pk(Agent (dishonest i)),crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),crypt(pk(Agent (dishonest i)),pair(Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),pair(Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),Agent (honest a)))),(SID sid)]);
fp_82: State (rB,[Agent (honest a),Step 2,pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (honest a))),pk(Agent (honest a)),Agent (honest a),Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),crypt(pk(Agent (honest a)),pair(Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),Agent (honest a))),pair(Agent (honest a),Agent (honest a)),pk(Agent (honest a)),crypt(inv(pk(Agent (honest a))),pair(Agent (honest a),pk(Agent (honest a)))),Nonce (nb(pair(Agent (honest a),pair(Agent (honest a),Step 0)))),crypt(pk(Agent (honest a)),pair(Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),pair(Nonce (nb(pair(Agent (honest a),pair(Agent (honest a),Step 0)))),Agent (honest a)))),(SID sid)]);
fp_83: request(Agent (honest a),Agent (honest a),Purpose (purposeNB),Nonce (nb(pair(Agent (honest a),pair(Agent (honest a),Step 1)))),(SID sid));
fp_84: State (rA,[Agent (honest a),Step 3,Agent (honest a),pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (honest a))),pk(Agent (honest a)),pair(Agent (honest a),Agent (honest a)),pk(Agent (honest a)),crypt(inv(pk(Agent (honest a))),pair(Agent (honest a),pk(Agent (honest a)))),Nonce (na(pair(Agent (honest a),Agent (honest a)))),crypt(pk(Agent (honest a)),pair(Nonce (na(pair(Agent (honest a),Agent (honest a)))),Agent (honest a))),Nonce (nb(pair(Agent (honest a),pair(Agent (honest a),Step 1)))),crypt(pk(Agent (honest a)),pair(Nonce (na(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (nb(pair(Agent (honest a),pair(Agent (honest a),Step 1)))),Agent (honest a)))),crypt(pk(Agent (honest a)),Nonce (nb(pair(Agent (honest a),pair(Agent (honest a),Step 1))))),(SID sid)]);
fp_85: iknows(crypt(pk(Agent (honest a)),Nonce (nb(pair(Agent (honest a),pair(Agent (honest a),Step 1))))));
fp_86: iknows(crypt(pk(Agent (honest a)),pair(Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),pair(Nonce (nb(pair(Agent (honest a),pair(Agent (honest a),Step 0)))),Agent (honest a)))));
fp_87: iknows(crypt(pk(Agent (dishonest i)),pair(Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),pair(Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),Agent (honest a)))));
fp_88: iknows(crypt(pk(Agent (honest a)),pair(Nonce (na(pair(Agent (honest a),Agent (dishonest i)))),pair(Nonce (nb(pair(Agent (honest a),pair(Agent (honest a),Step 0)))),Agent (honest a)))));
fp_89: iknows(crypt(pk(Agent (dishonest i)),pair(Nonce (na(pair(Agent (honest a),Agent (dishonest i)))),pair(Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),Agent (honest a)))));
fp_90: iknows(pair(Agent (honest a),Agent (honest a)));
fp_91: iknows(pair(Agent (honest a),Agent (dishonest i)));
fp_92: iknows(pair(Agent (dishonest i),pk(Agent (dishonest i))));
fp_93: iknows(pair(Agent (honest a),pk(Agent (honest a))));
fp_94: iknows(pair(Nonce (na(pair(Agent (honest a),Agent (dishonest i)))),Agent (honest a)));
fp_95: iknows(pair(Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),Agent (honest a)));
fp_96: iknows(pair(Nonce (ni),pair(Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),Agent (honest a))));
fp_97: iknows(pair(Nonce (na(pair(Agent (honest a),Agent (dishonest i)))),pair(Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),Agent (honest a))));
fp_98: iknows(pair(Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),pair(Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),Agent (honest a))));
fp_99: request(Agent (honest a),Agent (honest a),Purpose (purposeNA),Nonce (na(pair(Agent (honest a),Agent (honest a)))),(SID sid));
fp_100: State (rB,[Agent (honest a),Step 3,pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (honest a))),pk(Agent (honest a)),Agent (honest a),Nonce (na(pair(Agent (honest a),Agent (honest a)))),crypt(pk(Agent (honest a)),pair(Nonce (na(pair(Agent (honest a),Agent (honest a)))),Agent (honest a))),pair(Agent (honest a),Agent (honest a)),pk(Agent (honest a)),crypt(inv(pk(Agent (honest a))),pair(Agent (honest a),pk(Agent (honest a)))),Nonce (nb(pair(Agent (honest a),pair(Agent (honest a),Step 1)))),crypt(pk(Agent (honest a)),pair(Nonce (na(pair(Agent (honest a),Agent (honest a)))),pair(Nonce (nb(pair(Agent (honest a),pair(Agent (honest a),Step 1)))),Agent (honest a)))),crypt(pk(Agent (honest a)),Nonce (nb(pair(Agent (honest a),pair(Agent (honest a),Step 1))))),(SID sid)]);
fp_101: request(Agent (honest a),Agent (dishonest i),Purpose (purposeNA),Nonce (na(pair(Agent (honest a),Agent (dishonest i)))),(SID sid));
fp_102: State (rB,[Agent (honest a),Step 3,pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (honest a))),pk(Agent (honest a)),Agent (dishonest i),Nonce (na(pair(Agent (honest a),Agent (dishonest i)))),crypt(pk(Agent (honest a)),pair(Nonce (na(pair(Agent (honest a),Agent (dishonest i)))),Agent (dishonest i))),pair(Agent (honest a),Agent (dishonest i)),pk(Agent (dishonest i)),crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),crypt(pk(Agent (dishonest i)),pair(Nonce (na(pair(Agent (honest a),Agent (dishonest i)))),pair(Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),Agent (honest a)))),crypt(pk(Agent (honest a)),Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0))))),(SID sid)]);
fp_103: request(Agent (honest a),Agent (dishonest i),Purpose (purposeNA),Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),(SID sid));
fp_104: State (rB,[Agent (honest a),Step 3,pk(Agent (honest a)),Agent (honest a),inv(pk(Agent (honest a))),pk(Agent (honest a)),Agent (dishonest i),Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),crypt(pk(Agent (honest a)),pair(Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),Agent (dishonest i))),pair(Agent (honest a),Agent (dishonest i)),pk(Agent (dishonest i)),crypt(inv(pk(Agent (honest a))),pair(Agent (dishonest i),pk(Agent (dishonest i)))),Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),crypt(pk(Agent (dishonest i)),pair(Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),pair(Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),Agent (honest a)))),crypt(pk(Agent (honest a)),Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0))))),(SID sid)]);
fp_105: iknows(pair(Agent (honest a),Agent (honest a)));
fp_106: iknows(pair(Agent (honest a),Agent (dishonest i)));
fp_107: iknows(pair(Agent (dishonest i),pk(Agent (dishonest i))));
fp_108: iknows(pair(Agent (honest a),pk(Agent (honest a))));
fp_109: iknows(pair(Nonce (na(pair(Agent (honest a),Agent (dishonest i)))),Agent (honest a)));
fp_110: iknows(pair(Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),Agent (honest a)));
fp_111: iknows(pair(Nonce (ni),pair(Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),Agent (honest a))));
fp_112: iknows(pair(Nonce (na(pair(Agent (honest a),Agent (dishonest i)))),pair(Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),Agent (honest a))));
fp_113: iknows(pair(Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),pair(Nonce (nb(pair(Agent (honest a),pair(Agent (dishonest i),Step 0)))),Agent (honest a))));

section abstraction:
NA->Nonce (na(pair(A,B)));
NB->Nonce (nb(pair(B,pair(A,equals(pair(NA,Nonce (na(pair(A,B)))))))))


+ 18
- 0
examples/AnB/nsl.AnB View File

@@ -0,0 +1,18 @@
Protocol: NSL # Verified

Types: Agent A,B;
Number NA,NB;
Function pk

Knowledge: A: A,pk,inv(pk(A)),B;
B: B,pk,inv(pk(B))

Actions:
A->B: {NA,A}(pk(B))
B->A: {NA,NB,B}(pk(A))
A->B: {NB}(pk(B))

Goals:
A *->* B: NA
B *->* A: NB


+ 275
- 0
examples/AnB/nsl.fp View File

@@ -0,0 +1,275 @@
Backend: Open-Source Fixedpoint Model-Checker version 2009c
(**** REFINING ABSTRACTION: ["NA","NB"] *****)
Protocol: NSL
Types:
[(Purpose,["purposeNA","purposeNB"]),(Agent False False,["A","B"]),(Number,["NA","NB"]),(Function,["pk"])]
section rules:
step rule_0:
iknows(crypt(K,M));
iknows(inv(K))

=>
iknows(M)

step rule_1:
iknows(crypt(inv(K),M));
iknows(K)

=>
iknows(M)

step rule_2:
iknows(scrypt(K,M));
iknows(K)

=>
iknows(M)

step rule_3:
iknows(pair(M1,M2))

=>
iknows(M1);
iknows(M2)

step rule_4:
secret(M,Agent (honest a));
iknows(M)

=>
attack(pair(secrecy,M))

step rule_5:
request(A,B,Purpose (purposeNA),M,(SID sid))
| B/=Agent (dishonest i);
M/=Nonce (absNA(pair(B,A)))
=>
attack(pair(authentication,pair(A,pair(B,M))))

step rule_6:
request(A,B,Purpose (purposeNB),M,(SID sid))
| B/=Agent (dishonest i);
M/=Nonce (absNB(pair(B,pair(A,Arg1))))
=>
attack(pair(authentication,pair(A,pair(B,M))))

step rule_7:
State (rA,[Agent (A),Step 0,Agent (B),inv(pk(Agent (A))),(SID sid)])

=>
secret(Nonce (absNA(pair(Agent (A),Agent (B)))),Agent (B));
witness(Agent (A),Agent (B),Purpose (purposeNA),Nonce (absNA(pair(Agent (A),Agent (B)))));
State (rA,[Agent (A),Step 1,Agent (B),inv(pk(Agent (A))),Nonce (absNA(pair(Agent (A),Agent (B)))),crypt(pk(Agent (B)),pair(Nonce (absNA(pair(Agent (A),Agent (B)))),Agent (A))),(SID sid)]);
iknows(crypt(pk(Agent (B)),pair(Nonce (absNA(pair(Agent (A),Agent (B)))),Agent (A))))

step rule_8:
State (rB,[Agent (B),Step 0,inv(pk(Agent (B))),(SID sid)]);
iknows(crypt(pk(Agent (B)),pair(Nonce (absNA(pair(Agent (A),Agent (B)))),Agent (A))))

=>
secret(Nonce (absNB(pair(Agent (B),pair(Agent (A),Step 1)))),Agent (A));
witness(Agent (B),Agent (A),Purpose (purposeNB),Nonce (absNB(pair(Agent (B),pair(Agent (A),Step 1)))));
State (rB,[Agent (B),Step 1,inv(pk(Agent (B))),Agent (A),Nonce (absNA(pair(Agent (A),Agent (B)))),crypt(pk(Agent (B)),pair(Nonce (absNA(pair(Agent (A),Agent (B)))),Agent (A))),Nonce (absNB(pair(Agent (B),pair(Agent (A),Step 1)))),crypt(pk(Agent (A)),pair(Nonce (absNA(pair(Agent (A),Agent (B)))),pair(Nonce (absNB(pair(Agent (B),pair(Agent (A),Step 1)))),Agent (B)))),(SID sid)]);
iknows(crypt(pk(Agent (A)),pair(Nonce (absNA(pair(Agent (A),Agent (B)))),pair(Nonce (absNB(pair(Agent (B),pair(Agent (A),Step 1)))),Agent (B)))))

step rule_9:
State (rB,[Agent (B),Step 0,inv(pk(Agent (B))),(SID sid)]);
iknows(pk(Agent (B)));
iknows(Nonce (absNA(pair(Agent (A),Agent (B)))));
iknows(Agent (A))

=>
secret(Nonce (absNB(pair(Agent (B),pair(Agent (A),Step 1)))),Agent (A));
witness(Agent (B),Agent (A),Purpose (purposeNB),Nonce (absNB(pair(Agent (B),pair(Agent (A),Step 1)))));
State (rB,[Agent (B),Step 1,inv(pk(Agent (B))),Agent (A),Nonce (absNA(pair(Agent (A),Agent (B)))),crypt(pk(Agent (B)),pair(Nonce (absNA(pair(Agent (A),Agent (B)))),Agent (A))),Nonce (absNB(pair(Agent (B),pair(Agent (A),Step 1)))),crypt(pk(Agent (A)),pair(Nonce (absNA(pair(Agent (A),Agent (B)))),pair(Nonce (absNB(pair(Agent (B),pair(Agent (A),Step 1)))),Agent (B)))),(SID sid)]);
iknows(crypt(pk(Agent (A)),pair(Nonce (absNA(pair(Agent (A),Agent (B)))),pair(Nonce (absNB(pair(Agent (B),pair(Agent (A),Step 1)))),Agent (B)))))

step rule_10:
State (rB,[Agent (B),Step 0,inv(pk(Agent (B))),(SID sid)]);
iknows(Agent (B));
iknows(Nonce (absNA(pair(Agent (A),Agent (B)))));
iknows(Agent (A))

=>
secret(Nonce (absNB(pair(Agent (B),pair(Agent (A),Step 1)))),Agent (A));
witness(Agent (B),Agent (A),Purpose (purposeNB),Nonce (absNB(pair(Agent (B),pair(Agent (A),Step 1)))));
State (rB,[Agent (B),Step 1,inv(pk(Agent (B))),Agent (A),Nonce (absNA(pair(Agent (A),Agent (B)))),crypt(pk(Agent (B)),pair(Nonce (absNA(pair(Agent (A),Agent (B)))),Agent (A))),Nonce (absNB(pair(Agent (B),pair(Agent (A),Step 1)))),crypt(pk(Agent (A)),pair(Nonce (absNA(pair(Agent (A),Agent (B)))),pair(Nonce (absNB(pair(Agent (B),pair(Agent (A),Step 1)))),Agent (B)))),(SID sid)]);
iknows(crypt(pk(Agent (A)),pair(Nonce (absNA(pair(Agent (A),Agent (B)))),pair(Nonce (absNB(pair(Agent (B),pair(Agent (A),Step 1)))),Agent (B)))))

step rule_11:
State (rB,[Agent (B),Step 0,inv(pk(Agent (B))),(SID sid)]);
iknows(crypt(pk(Agent (B)),pair(Nonce (NA),Agent (A))))
| Nonce (NA)/=Nonce (absNA(pair(Agent (A),Agent (B))))
=>
secret(Nonce (absNB(pair(Agent (B),pair(Agent (A),Step 0)))),Agent (A));
witness(Agent (B),Agent (A),Purpose (purposeNB),Nonce (absNB(pair(Agent (B),pair(Agent (A),Step 0)))));
State (rB,[Agent (B),Step 1,inv(pk(Agent (B))),Agent (A),Nonce (NA),crypt(pk(Agent (B)),pair(Nonce (NA),Agent (A))),Nonce (absNB(pair(Agent (B),pair(Agent (A),Step 0)))),crypt(pk(Agent (A)),pair(Nonce (NA),pair(Nonce (absNB(pair(Agent (B),pair(Agent (A),Step 0)))),Agent (B)))),(SID sid)]);
iknows(crypt(pk(Agent (A)),pair(Nonce (NA),pair(Nonce (absNB(pair(Agent (B),pair(Agent (A),Step 0)))),Agent (B)))))

step rule_12:
State (rB,[Agent (B),Step 0,inv(pk(Agent (B))),(SID sid)]);
iknows(pk(Agent (B)));
iknows(Nonce (NA));
iknows(Agent (A))
| Nonce (NA)/=Nonce (absNA(pair(Agent (A),Agent (B))))
=>
secret(Nonce (absNB(pair(Agent (B),pair(Agent (A),Step 0)))),Agent (A));
witness(Agent (B),Agent (A),Purpose (purposeNB),Nonce (absNB(pair(Agent (B),pair(Agent (A),Step 0)))));
State (rB,[Agent (B),Step 1,inv(pk(Agent (B))),Agent (A),Nonce (NA),crypt(pk(Agent (B)),pair(Nonce (NA),Agent (A))),Nonce (absNB(pair(Agent (B),pair(Agent (A),Step 0)))),crypt(pk(Agent (A)),pair(Nonce (NA),pair(Nonce (absNB(pair(Agent (B),pair(Agent (A),Step 0)))),Agent (B)))),(SID sid)]);
iknows(crypt(pk(Agent (A)),pair(Nonce (NA),pair(Nonce (absNB(pair(Agent (B),pair(Agent (A),Step 0)))),Agent (B)))))

step rule_13:
State (rB,[Agent (B),Step 0,inv(pk(Agent (B))),(SID sid)]);
iknows(Agent (B));