Examples

Examples: SSL Handshake, SRP, Dolev-Yao Example, KEA, and Perrig-Song. These are some interesting protocols not in the Clark-Jacob collection.

C.1 SSL Handshake

The CAPSL text illustrates conditional selection of subprotocols and the DENOTES section. The sha operator is used wherever hashes are called for, and much of the detailed construction of hashes and key material has been simplified. The method for simplifying hashes is to include the contributing data but ignore ordering, constants, and other details that affect the cryptographic strength but not the logical structure of the protocol. The key agreeement operators are used instead of explicit exponentiation in the Diffie-Hellman exchange, so the base and modulus are not mentioned.

TYPESPEC SSLS;
TYPES CertServer: PKUser;
FUNCTIONS
    T(CertServer): Field; /* PK certificate */
VARIABLES
    Sv: CertServer;
CONSTANTS 
    CA: PKUser;    /* Certificate Authority */
AXIOMS
    T(Sv) = {Sv,pk(Sv)}sk(CA);
END;

PROTOCOL SSLHandshake;
IMPORTS SSLS;
TYPES CipherSpec;
VARIABLES
    C: PKUser;
    S: CertServer;
    Rc,Rs: Nonce, CRYPTO;       /* Client/ServerHello.random */
    CS: CipherSpec;   
    SID: Nonce;                 /* session id */
    PMS: Skey;                  /* pre-master-secret */
    MS: Skey;                   /* master secret */
    PKs: Pkey;                  /* Server public key pk(S) */
CONSTANTS 
    DH, RSA, DMS: CipherSpec;
    SSLDH, SSLRSA, SSLDMS: Pspec;
DENOTES
    MS = sha({PMS,Rc,Rs});
ASSUMPTIONS
    HOLDS C: S, CS;
MESSAGES
    ClientHello.       C -> S: C,Rc,CS;
    ServerHello.       S -> C: S,Rs,CS;
    ServerCertificate. S -> C: T(S)%{S,PKs}sk(CA); 
    IF      CS = DH  THEN INCLUDE SSLDH; 
    ELSE IF CS = RSA THEN INCLUDE SSLRSA; 
    ELSE IF CS = DMS THEN INCLUDE SSLDMS;   
/*  ELSE INCLUDE SSLERR; */ ENDIF; 
    ENDIF; ENDIF;
GOALS
    SECRET MS;
    PRECEDES C: S | MS,Rs,Rc; 
END;


PROTOCOL SSLDH;
IMPORTS SSLHandshake;
VARIABLES
    Yc,Ys: Pval;                /* key agreement public values */
    Xc,Xs: Skey, FRESH,CRYPTO;  /* key agreement secret values */
    D: Field;
MESSAGES
    ServerKeyExchange. S -> C: kap(Xs)%Ys,({sha(kap(Xs))}sk(S))%D; 
                       {D}PKs = sha(Ys);
/*  SeverHelloDone.    S -> C: { } */
    ClientKeyExchange. C -> S: kap(Xc)%Yc;
                       PMS = kas(Yc,Xs);/
                       PMS = kas(Ys,Xc);
    ClientFinished.    C -> S: sha({MS,C});
    ServerFinished.    S -> C: sha({MS,S});
END;

/* protocols SSLRSA, SSLDMS, and SSLERR would be needed */

1. There is no mention of the modulus N for finite field arithmetic. Arithmetic is done on Skeys.
2. The checks that B, u, and A are not zero are omitted.
3. Messages 3 and 4 to confirm reception of the key K are simpler than the suggested ones.

TYPESPEC User;
TYPES User, Host: Principal;
FUNCTIONS
	g: Skey;	/* generator */
	p(User): Field, PRIVATE;  /* password */
	s(Host,User): Field, PRIVATE;     /* salt */
	v(Host,User): Skey, PRIVATE;      /* password verifier */
AXIOMS 
	v(H1,U1) = g^sha({s(H1,U1),p(U1)}); 
END;


PROTOCOL SRP;
IMPORTS User;
VARIABLES
	U: User;
	H: Host;
	A, B: Skey;
	a, b, u: Skey, FRESH, CRYPTO;
	K,S,s,x: Skey;
DENOTES
	A = g^a;
	B = v(H,U) + g^b;
	x = sha({s,p(U)}); 
	v = g^x;   
ASSUMPTIONS
	HOLDS U: H;
MESSAGES
  1. U -> H: U, A;             /* U generates a */
	S = (A*v(H,U)^u)^b;    /* H generates b */
	K = sha(S);
  2. H -> U: s(H,U)%s, B, u;	
	S = (B - v)^(a + u*x);
	K = sha(S);
  3. U -> H: {A}K;             /* proves U holds K */
  4. H -> U: {B}K;             /* proves H holds K */
GOALS	
	SECRET K;
END;

PROTOCOL DY;
VARIABLES
    A, B: PKUser;
    M: Nonce;
ASSUMPTIONS
    HOLDS A: B;
MESSAGES
    A -> B: {{M}pk(B),A}pk(B);
    B -> A: {{M}pk(A),B}pk(A);
GOALS
    SECRET M;
END;

TYPESPEC KEAPK;
TYPES KEAUser: Principal;
FUNCTIONS
    Y(KEAUser): Skey;
    x(KEAUser): Skey, PRIVATE;
CONSTANTS
    g: Skey;
VARIABLES
    Ul: KEAUser;
AXIOMS
    g^x(Ul) = Y(Ul);
END;

PROTOCOL KEA;
VARIABLES
    A, B: KEAUser;
    ra, rb: Skey, FRESH, CRYPTO;
    K, t, u, Ra, Rb: Skey;
    M: Nonce, CRYPTO;
DENOTES
    t = Y(B)*ra: A;
    t = x(B)*Ra: B;
    u = x(A)*Rb: A;
    u = Y(A)*rb: B;
    K = sha(t + u);
ASSUMPTIONS
    HOLDS A: B;
MESSAGES
    A -> B: A,g^ra%Ra;
    B -> A: g^rb%Rb;
    A -> B: {M}K;
GOALS
    SECRET M;
END;

PROTOCOL PerrigSong;
VARIABLES
    A, B: Node;
    Na, Nb: Nonce;
    Kab: Skey;
DENOTES
    Kab = msk(A,B): A;
    Kab = msk(B,A): B;
ASSUMPTIONS
    HOLDS A: B;
MESSAGES
  A -> B: A,Na;
  B -> A: {Na, Nb, B}Kab;
  A -> B: Nb;  
GOALS
  PRECEDES B: A | Na, Nb;
  PRECEDES A: B | Na, Nb;
END;