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.

Examples

Protocols using symmetric keys

• A simple handshake using a symmetric key
• An aritificial protocol that requires a fractional capability
• Woo and Lam's authentication protocol using a symmetric key
• Otway and Ree's key exchange protocol using a symmetric key
• Flawed wide mouth frog protocol
• Fixed variant of wide mouth frog protocol

Protocols using asymmetric keys

• POSH (public out, secret home) protocol using an asymmetric key
• SOPH (secret out, public home) protocol using an asymmetric key
• SOSH (secret out, secret home) protocol using an asymmetric key
• A three-party protocol that cannot be typed in Gordon and Jeffrey's type system
• Cremers and Mauw's generalized Needham-Schroeder-Lowe protocol (Cremers and Mauw, "A Family of Multi-Party Authentication Protocols", WISSEC'06)
• ISO Public Key Two-Pass Unilateral Authentication Protocol
• Needham-Schroeder protocol (flawed version, which is untypable)
• Needham-Schroeder-Lowe protocol (Lowe's fix, 3-message version)
• Needham-Schroeder-Lowe protocol (Lowe's fix, 3-message version, with man-in-the-middle attacks taken into account)
• Needham-Schroeder-Lowe protocol (Lowe's fix, 7-message version)
• NSL protocol (optimized version)
• NSL protocol (optimized version, with man-in-the-middle attacks taken into account)
• NSL protocol (with secret)
• NSL protocol (with secret and optimization)

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 **/