SpiCA2: A type-based verifier for Spi-calculus protocols with Corresponding Assertions

SpiCA is a type-based automated verifier for authenticity in cryptographic protocols. See the following paper for the technical background:

  Daisuke Kikuchi and Naoki Kobayashi, "Type-Based Automated Verification of Authenticity in Cryptographic Protocols,"
  Proceedings of ESOP 2009, Springer LNCS 5502, 2009.

  Morten Dahl, Naoki Kobayashi, Yunde Sun, and Hans Huttel,
  "Type-Based Automated Verification of Authenticity in Asymmetric Cryptographic Protocols,"
  Proceedings of ATVA 2011, Springer LNCS 6996, pp.75-89, 2011.
Enter a protocol in the box below, and press the "submit" button. Examples are given below.


Some examples are found in the links below. The description of ISO Public Key Two-Pass Unilateral Authentication Protocol is based on Gordon and Jeffrey's paper "Types and effects for asymmetric cryptographic protocols", Journal of Computer Security, 2004. The last six examples on asymmetric cryptographic protocols are based on sample programs for Cryptyc, modified for SpiCA2.

Protocols using symmetric keys

Protocols using asymmetric keys


    x, y, z, ...

    M ::= x | () | (M1,M2) | inl(M) | inr(M) | (M)
        | {M}K    /* encryption of M with a symmetric key K */
        | {{M}}K    /* encryption of M with an asymmetric key K */

    P ::= O     /* nil */
        | M!N   /* output N along a public channel M */
        | M?y.P  /* input y along a public channel M, and behave like P */
        | P1|P2 | *P 
        | (new x)P  /* create a fresh name x and behave like P */
        | (newSym k)P /* create a symmetric key k and behave like P */
        | (newASym ek, dk)P /* create an asymmetric key pair (ek, dk) 
                              (where ek and dk are for encryption and decryption respectively) and behave like P */
        | check x is y in P /* compare x and y, and if x=y, behave like P; otherwise behave like O */
        | decrypt M is {x}K in P  /* decrypt M with symmetric key K */
        | decrypt M is {{x}}K in P  /* decrypt M with asymmetric key K */
        | case M is inl(x).P is inr(y).Q  /* if M is inl(v), behave like [v/x]P; if M is inr(v), behaves like [v/y]P */
        | split M is (x,y) in P 
        | match M is (x,y) in P
        | begin M.P | end M   /* correspondence assertions */
        | (P)
        | M!!N | M??x.P | (news x)P  /** primitives for communication on private channels **/