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.

This is a Web interface for SpiCA2.

Syntax

  (Variables)
    x, y, z, ...

  (messages)
    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 */
       

  (processes)
    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 **/