Christianhaack.eu

Pattern-matching Spi-calculus
Abstract. Cryptographic protocols often make use of nested cryptographic primitives, for example signed
message digests, or encrypted signed messages. Gordon and Jeffrey’s prior work on types for authenticity did
not allow for such nested cryptography. In this work, we present the pattern-matching spi-calculus, which is
an obvious extension of the spi-calculus to include pattern-matching as primitive. The novelty of the language
is in the accompanying type system, which uses the same language of patterns to describe complex data
dependencies which cannot be described using prior type systems. We show that any appropriately typed
process is guaranteed to satisfy a strong robust safety property.
Introduction
Background. Cryptographic protocols are prone to subtle errors, in spite of the fact that they are oftenrelatively small, and so are a suitable target for formal and automated verification methods. One lineof such research is the development of domain-specific languages and logics, such as BAN logic [6],strand spaces [22], CSP [20, 21] MSR [8] and the spi-calculus [3]. These languages are based on theDolev–Yao model of cryptography [10], and often use Woo and Lam’s correspondence assertions [23]to model authenticity. Techniques for proving correctness include rank functions [21, 16, 15], theoremprovers [5, 19, 9], model checkers [17, 18] and type systems [1, 2, 7, 12, 13, 11].
Towards more complete and realistic cryptographic type systems. Type systems for interesting lan-guages are incomplete, that is they fail to type-check some safe programs. Because of the subtletyof cryptographic protocols and their desired safety properties, this is especially true for cryptographictype systems. Such systems often cover some cryptographic primitives while neglecting others, for in-stance, [12, 11] does not include asymmetric cryptography, [2] treats public encryption keys but notsigning keys and [13] covers full symmetric and asymmetric cryptography but not hashing. Moreover,even if primitives are included, it is often the case that some safe and common programs that use theseprimitives do not type-check, for example [13] treats full asymmetric cryptography, but does not allowfor nested cryptography such as sign-then-encrypt. In this paper, we will use the techniques developedin [12, 13, 11] to reason about protocols making use of asymmetric cryptography, symmetric cryptog-raphy and hashing.
Small core language. While increasing the completeness of a cryptographic type system, it is alsoimportant to keep the system tractable, so that rigorous safety proofs are still feasible. For that reason,we chose to define a very small core language and obtain the full language through derived forms.
The core language is extremely parsimonious: its only constructs for messages are tupling, asymmetricencryption and those for asymmetric keys. We show that symmetric encryption, hashing, and messagetagging are all derived operators from this small core.
Authorization types. The language of types is small, too. It contains key types for key pairs, encryptionand decryption keys. Moreover, it contains parameterized authorization types of the forms Public(M)and Secret(M). Typically, the parameter M is a list of principal names. For instance, if principal Breceives from an untrusted channel a ciphertext {|M|}esA encrypted with A’s private signing key esA,then the plaintext M is of type Public(A, ()), because M is a public message that has been authorizedby A. On the other hand, if B receives a ciphertext {|M|}epB encrypted with B’s public encryption keyepB and it is clear from the context that this ciphertext comes from a trusted source, then the plaintextM has type Secret(B), because it is a secret message that has been authorized for B.
Patterns and nested cryptography. The process language combines the suite of separate message de-structor’s and equality checks from previous systems [12, 13, 11] into one patten matching construct.
Patterns at the process level are convenient, and are similar to the communication techniques used in other specification languages [22, 8, 4]. Notably, our system uses patterns not only in processes but alsoin types. This permits types for nested use of cryptographic primitives, which would otherwise not bepossible. For example, previous type systems [12, 13, 11] could express data dependencies such as (∃a : Princ, ∃m : Msg, ∃b : Princ,[!begun(a, b, m)]) where !begun(a, b, m) is an effect ensuring that principals a and b have agreed on message m. In thispaper, we extend these systems to deal with more complex data dependencies such as {|#(∃a : Princ, ∃m : Msg), ∃b : Princ|}dk−1[!begun(a,b,m)] where the effect !begun(a, b, m) makes use of variables a, b and m which are doubly nested in the scopeof a decryption {| · |}dk−1 and a hash function #(·): such data dependencies were not previously allowedbecause the occurrences of a, b and m in !begun(a, b, m) would be considered out of scope.
Reusable long-term keys. Another form of incompleteness is that previous systems have often beendesigned for verifying small (yet, subtle) protocol sketches in isolation, but not for verifying largercryptographic systems where the same key may be used for multiple protocols. For instance, in [13]when a signing key for A is generated, its type specification fixes a finite number of message typesthat this key may sign. A more realistic approach for larger, possibly extensible, cryptosystems wouldbe to generate a key for encrypting arbitrary data authorized by A. We show how the combination ofkey types, authorization types and message tagging allow keys to be generated independently of theprotocols for which they will be used.
Notational conventions. If the meta-variable x ranges over set S, then x ranges over finite sequencesover S, and ¯ x ranges over finite subsets of S.
An Introductory Example
Before the technical exposition, we want to convey a flavor of the type system by discussing a simpleexample. Consider the following simple sign-then-encrypt protocol: A begins! (M, A, B)A → B {|{|sec(M, B)|}esA|}epB B ends (M, A, B) Alice wants to send Bob a secret message M. To this end, she first tags M together with Bob’s namewith a message tag sec. Message tags are traditionally used so that receivers can identify which protocola message belongs to and which role it plays in the protocol. In our system, message tags communicateadditional important type information. Next, Alice encrypts the tagged message sec(M, B) with her se-cret signing key esA to authenticate herself. Because M is to be kept secret, Alice finally encrypts themessage with Bob’s public encryption key. The begin- and end-statements are Woo-Lam correspon-dence specifications [23]. They specify that Alice begins a protocol session (M, A, B), which Bob endsafter message reception.
Protocol specification in pattern-matching spi. Here are Alice’s and Bob’s side of this protocol ex-pressed in pattern-matching spi calculus: PA = begin!(B, M); out net {|{|sec(B, M)|}esA|}epB PB = inp net {|{|sec(B, ∃x)|}dsA−1|}dpB−1; end(B,x) The variable net represents an untrusted channel and dsA and dpB are the matching decryption keysfor esA and epB. An output statement of the form (out net N) sends a message N out on channel net.
A statement of the form (inp net X ; P) inputs a message from channel net and then attempts to matchthe message against pattern X . If the pattern match succeeds then P gets executed, otherwise executiongets stuck. Existentials in patterns indicate which variables get bound as part of the pattern match. Inthe input pattern above, the variable x gets bound, whereas B, dsA and dpB are constants that must bematched exactly.
Type annotations. For a type-checker to verify the protocol’s correctness (and also for us to betterunderstand and document it), it is necessary that we annotate the protocol with types. For our example,the types for the free variables are: M will not be revealed to the opponent epB is B’s public encryption key dpB is B’s matching decryption key esA is A’s private signing key dsA is A’s matching signature verification key No type annotations are necessary in PA, because PA does not have input statements. In PB we add twotype annotations. The input variable x is annotated with Secret. Moreover, we add a postcondition tothe input statement that indicates that a (x, A, B)-session can safely be ended after a successful patternmatch. Here is the annotated version of PB: PB = inp net {|{|sec(B, ∃x : Secret)|}dsA−1|}dpB−1[!begun(x,A,B)]; end(B,x) These type annotations, together with our Robust Safety Theorem are enough to ensure the safety ofthis protocol in the presence of an arbitrary opponent.
A Spi Calculus with Pattern Matching
Messages
As usual in spi calculi, messages are modeled as elements of an algebraic datatype. They may be builtfrom atomic names and variables by pairing and asymmetric-key encryption. Moreover, there are twospecial symbolic operators Enc and Dec with the following meanings: if message M represents a keypair, then Enc (M) represents its encryption and Dec (M) its decryption part. This language of messagesis extremely parsimonious; in Section 5 we show how to introduce derived forms for constructs such assymmetric key encryption and message tagging.
In th presentation of messages, we include asymmetric-key encryption {|M|}N which encrypts plain- text M with encryption key N. We also allow messages {|M|}N−1 which represents the encryption ofplaintext M with the encryption key which matches decryption key N. This is clearly not an imple-mentable operation: it is used in the next section when we discuss patterns.
Messages:
M encrypted under encryption key N M encrypted under inverse of decryption key N Syntactic restriction: No subterms of the form {|M|}(Dec(N))−1.
Define: A message M is implementable if it contains no subterms of the form {|M|}N−1.
Because of the restriction that we never build a message of the form {|M|}(Dec(N))−1, we have to becareful with our definition of substitution. This is standard, except for when we substitute into a termof the form {|M|}N−1.
Substitution into Messages:
We will often use the following abbreviation: (M1, . . . , Mn) = (M1, (. . . , (Mn, ()) . . .)) Patterns
Patterns are of the form {x . M | ¯ A}, where M is a pattern body and ¯ A an assertion set. Assertion sets are only used in type-checking, so we delay their discussion until Section 4.2. The variables x act asbinders. A message N matches a pattern {x . M | ¯ A} if it is of the form N = M{x←L}, in which case variables x will be bound to messages L. The pattern body M may have multiple occurrences of thesame variable and it may contain variables that are not mentioned in x: such variables are regardedas constants and must be matched exactly. For instance, the pattern {x . (x, {|x|}y) | ¯ messages of the form (M, {|M|}y), but not by messages (M, {|M|}z) or (M, {|N|}y).
Patterns:
pattern matching term M binding x Syntactic restrictions: x ⊆ fv(M) and x distinct.
Define: A pattern {x . M | ¯ A} is implementable if (fn(M), fv(M) − x, M Importantly, not all patterns are implementable. For instance, the patterns {x, dk . {|x|}dk−1 | ¯A} and {x .
{|x|}ek | ¯ A} are not implementable, because they would allow access to the plaintext without knowing the decryption key. On the other hand, {x . {|x|}dk−1 | ¯A}and {x.{|x|}Enc(k) | ¯A} are implementable patterns. Asyntactic restriction forbids non-implementable input patterns in processes. We formalize the notion ofimplementable pattern by making use of the Dolev–Yao ‘derivable message’ judgment ¯ Dolev–Yao Derivability, ¯
N:
(N, N ) M, (N, N ) We use some convenient syntactic abbreviations that treat patterns as if they were messages containingbinding existentials. These ‘derived forms’ for patterns are defined below. For example: {|{|sec(B, ∃x : Secret)|}dsA−1|}dpB−1[!begun(x,A,B)] {x . {|{|sec(B, x)|}dsA−1|}dpB−1 | x : Secret,!begun(x,A,B)} Derived Forms for Patterns:
T = {x . x | x : T } for fresh x; . . . = (∃x) for fresh x; {|X|}N = {x . {|M|}N | ¯ A}, if X = {x . M | ¯ {|X|}N−1 = {x . {|M|}N−1 | ¯A}, if X = {x . M | ¯A}; B}, if X = {x . M | ¯ (X1, . . ., Xn) = {x1, . . . , xn . (M1, . . . , Mn) | ¯ An}, if Xi = {xi . Mi | ¯ Processes
The spi-calculus with patterns is a variant of the spi-calculus, where we add pattern-matching as aprimitive capability (in the spi-calculus it is derived).
Processes:
O, P, Q, R ::= asynchronous output of M on N input from N against pattern X • In (out N M), both N and M are implementable messages.
• In (inp N X; P), N is an implementable message and X is an implementable pattern.
• The scope of x in (inp N {x . M | ¯ • The scope of n in new n:T ; P is P.
The interesting construct is input of the form (inp N X ; P). If a message L is received on channel N,then L is matched against pattern X . If this match succeeds, then it results in a binding and the processcontinuation P is executed under this binding. This is captured by the main reduction rule for pattern-matching spi: (out L M{x←N} | inp L {x . M | ¯ A}; P) → (P{x←N}) Specifying Authenticity by Correspondence Assertions
Following [12, 13, 11], we specify authenticity properties by inserting correspondence assertions intoprotocol specifications. In this paper, we only consider non-injective or many-to-one correspondences [11],where each begin-many assertion may match many end assertions. We do not believe that treating one-to-one correspondences should pose any technical difficulties, and postpone it for future work.
Correspondence Assertions:
O, P, Q, R ::= A process is safe whenever at run-time each end(M) is preceded by a begin!(M) (precise definitionscan be found in the appendix). For example, consider process P: P = PA | PB, where PA = (begin!(M, A, B); out net (M, B)) PB = (inp net (∃x, B)[!begun(x, A, B)]; end(x, A, B)) Process P is safe in isolation, but we are really interested in safety in the presence of an opponent. Anopponent process is an untyped process that does not contain correspondence assertions. A process Pis called robustly safe whenever (O | P) is safe for all opponent processes O. The example process P isnot robustly safe, because (out net N | P) is not safe, and we ensure robust safety by adding encryption: P = new k : SigningKP(A); ( out net (Dec (k)) | PA(Enc (k)) | PB(Dec (k)) ) PA(ek) = (begin!(M, A, B); out net {|M, B|}ek) PB(dk) = (inp net {|∃x : Public, B|}dk−1[!begun(x,A,B)]; end(x,A,B)) Here, SigningKP(A) is a type for principal A’s signing key pair and Public is a type for public, untainteddata. The crucial property of our system is that processes that only make use of public data are robustlysafe (we will return in Section 4.3 to the definition of a public type): Theorem (Robust Safety) If T are public types and (n : T
P), then P is robustly safe. Highlights of the Type System
Environments
As is usual in most type systems, we give our judgments relative to a typing environment. In our case,this typing environment is used to: – Track the names of bound variables, for example dk and x.
– Give types to messages, for example dk : SigningDK(A) and {|x, B|}dk−1 : Un.
– List the begun assertions which can be ended safely, for example !begun(x, A, B).
The environment containing these assertions would be: dk, x; dk : SigningDK(A), {|x, B|}dk−1 : Un, !begun(x,A,B) A significant difference to previous type systems for the spi-calculus [12, 13, 11] is that we are uni-
fying the notions of variable environment and process effect into a common language of environ-
ments. In these previous papers, the above environment would be split into the variable environment
dk : SigningDK(A), and the process effect trust ({|x, B|}dk−1 : Un), !begun(x,A,B).
Environments:
A, B,C, D ::= We now discuss the interesting aspects of this type system; see Appendix B for details.
Typed Pattern Matching
We can now explain the assertion component of a pattern {x . M | ¯ must be satisfied by any process that constructs a term matching the pattern. For example, the pattern(∃x : Public, B)[!begun(x, A, B)] is a derived form for {x . (x, B) | x : Public, !begun(x, A, B)}. For M tomatch this pattern in environment E, it must be the case that M is well-typed (i.e. M is of type Top), Mis of the form M = (N, B), message N is of type Public and !begun(M, A, B) is contained in E.
Typed Pattern Matching (where X = {x . N | ¯
A} ):
where M = N{x←N} J ∆= E, M : Top, ¯A{x←N} J where M = N{x←N} Kinds and Subkinding
A message is publishable if it may be sent to an untrusted target. For instance, ciphertext {|M|}ek ispublishable if the decryption key for ek is secret. If ek is a signing key, whose corresponding decryptionkey is public, then {|M|}ek is only publishable if M is already publishable.
A message is untainted if it has been received from a trusted source. For instance, if dk is a signature verification key whose matching signing key is secret, then M is untainted even if {|M|}dk−1 is tainted.
If dk is a key whose matching encryption key is public, then M is only untainted if {|M|}dk−1 is alreadyuntainted.
An important part of the type system is a kinding relation (T :: K) that assigns kinds K to types T .
The type system is designed so that the following statements hold: – If (T :: K) and Public ∈ K, then members of type T are publishable.
– If (T :: K) and Tainted ∈ K, then members of type T are untainted.
We say that type T is public (respectively tainted) if (T :: K Public) (respectively (T :: K Kinds and Subkinding:
(Public ∈ H) ⇒ (Public ∈ K) (Tainted ∈ K) ⇒ (Tainted ∈ H) K, H, J ⊆ {Public, Tainted} Types and Subtyping
We will now give the grammar of types, together with the definition of kinding and subtyping. Wediscuss each of the types in more detail below.
Kinding T :: K:
(K, H) KP(X) :: K ∩ H; (K, H) EK(X) :: K; (K, H) DK(X) :: H Kinds are used to define subtyping. The rule (Subty Public Tainted) states that any message of publictype also has any tainted type, as in [13]. The subtyping rules (Subty Top) and (Subty Auth) are newand have not been part of [13].
Subtyping, T ≤ U:
T :: K ∪ {Public} U :: H ∪ {Tainted} K Auth(L) ≤ H Auth(L) Top Types
Top types have the form K Top and are the most general types of kind K, by (Subty Top). Moreover,{Tainted} Top is the greatest type of the entire type hierarchy. We define the following derived forms: Derived Forms for Top Types:
Authorization Types
A novel feature of this type system is authorization types. A message M : K Auth(L) is a message ofkind K which requires authorization by or for L.
Derived Forms for Authorization Types:
Tainted(L) = {Tainted} Auth(L); Public(L) = {Public} Auth(L); Un(L) = {Public, Tainted} Auth(L) In meaningful authorization types, parameter L is either a list of principal names (possibly terminatedby the empty message) or a single principal name. For example, Public(A, B,C, ()) is the type of publicmessages M that require authorizations by principals A, B and C. These authorizations are acquired byA, B and C digitally signing M. On the other hand, Secret(A) is the type of secret messages M thatrequire authorization for A. This authorization is acquired by encrypting M with A’s public encryptionkey.
Key Types
In this system, key types are extremely general: in examples, we will often use specialized derived keytypes for applications such as signing, as discussed in Section 5.2.
The key type (K, H) KT(X ) contains a pattern X . These keys will be used to encrypt plaintext messages M to produce ciphertexts which have an authorization type J Auth(L). In order to form theciphertext, we require the pair (M, L) to match the pattern X . The key type (K, H) KT(X ) also containsa kind K, which is the kind of the encryption key, and a kind H, which is the kind of the decryption key.
For example, in Section 5.2 we define principal A’s signing key to be: SigningEK(A) = ( /0, {Public}) EK(∃x : Secret(A, y), ∃y) A key esA of type SigningEK(A) is a secret encryption key, whose matching decryption key is public.
Thus, it is a signing key. It is typically used to encrypt messages M of type Public(A, B) to produceciphertexts {|M|}esA of type Public(B): thus, by signing the message, A removes her name from the listof principals required to authorize it.
Output and Input
The interesting rules for the process judgment E P are for input and output. We assume that ev- ery channel is untrusted, that is of type Un. Untrusted channels may transmit messages of type Un.
Moreover, untrusted channel names are themselves of type Un, and may, thus, be sent and received onuntrusted channels: In the output rule, message M has to be of type Un in order to be sent out on the untrusted channel N.
Note that M may also be sent out if M’s type is any other public type, because each public type is asubtype of Un.
Encryption
There are two typing rules for encryption, which only differ in the kind attributes of the types. The firstrule applies to encryption with a trusted key: N : (K, H) EK(X ), (M, L) ∈ X The condition Tainted ∈ K ∪ H−1 expresses that the ciphertext is only publishable if the encryption keyis untainted and the corresponding decryption key is not public. Otherwise, the following rule is usedfor encryption: J = (J − {Tainted}) ∪ (K − {Public}) N : (K, H) EK(X ), (M, L) ∈ X , M : J Top {|M|}N : J Auth(L) Note that here the ciphertext type J Auth(L) is only public if the plaintext type J Top is public, and istainted if the encryption key is tainted.
Decryption
There are two typing rules for decryption, which only differ in how they treat kinds and authorizations.
The first rule applies if both the decryption key and the ciphertext are untainted, and is the inverse ofthe rule for encryption with a trusted key: N : (K, H) DK(X ) E, (M, L) ∈ X E, {|M|}N−1 : J Auth(L) B The second decryption rule applies if we cannot trust the ciphertext; in particular we do not know whohas authorized the ciphertext: N : (K, H) DK(X ) x, E, (M, x) ∈ X (Tainted ∈ H ∪ K−1) ⇒ (x, E, M : J Top, x : Top E, {|M|}N−1 : J Top B Note that when we apply this rule, the authorization is unknown, so we replace it by a fresh variable x,which acts as a placeholder for the ‘real’ authorization. If the decryption key is untrusted, then wehave an additional requirement: we can only add (M, x) to the assumption list if it is derivable from(x, E, M : J Top, x : Top); as a result, untrusted keys can only be used when the pattern X is quite‘weak’.
Summary of Technical Properties
Here is a brief outline of the crucial technical properties of the type system, as proved in a longerversion of this paper [14]. Firstly, the type system satisfies substitutivity in the following sense: Theorem (Substitutivity) If (E
J ) and dom(E) = dom(σ), then (E{σ} J {σ}) Note that there is no condition on the substitution σ, except that its domain must coincide with E’sdomain. The second important theorem is (Cut): Theorem (Cut) If E is nominal, (E
An environment E is nominal, if dom(E) = /0, each type assertion in E is of the form (n : T ), and thereare no duplicate type assertions n : T, n : U . The nominality condition is needed to ensure that E is‘key-unique’, that is, E does not assign two unrelated key types to the same name. Using substitutivityand (Cut), it is not so hard to prove that state reductions preserve well-typedness: Theorem (Type Preservation) If
Safety is a simple corollary of type preservation: Theorem (Safety) If (n : T
As usual, we model opponent processes as well-typed, too. An opponent process is a process with nocorrespondence assertions, where all type annotations on names are Un and all input patterns are of theform {x . M | M : Un} for some x, M.
Theorem (Dolev-Yao ⇒ Typability) If ( ¯
N) = ¯x, then ( ¯x; ¯ Theorem (Opponent Typability) If P is an opponent process, fn(P) = ¯n and fv(P) = ¯x, then ( ¯x; ¯n : Un, ¯x : Un
P).
Robust safety is a simple corollary of safety and opponent typability: Theorem (Robust Safety) If T are public types and (n : T
P), then P is robustly safe. Derived Forms and Examples
In previous type systems for cryptographic protocols [12, 13, 11], message tags were introduced usingtagged union types. These types are sound, and they allow a key to be used in more than one protocol,but unfortunately they require the protocol suite to be known before the key is generated, since theplaintext type of the key is given as the tagged union of all the messages in the protocol suite. In thispaper, we adopt a variant of dynamic types to allow a key to be generated with no knowledge of theprotocol suite it will be used for.
In our system, we give message tags a type of the form : X → Auth(Y ), which can be used to tag messages M of kind (J ∪ Tainted) to get tagged messages (M) : J Auth(L). For example, our previousprotocol becomes: P = new k : SigningKP(A); ( out net (Dec (k)) | PA(Enc (k)) | PB(Dec (k)) ) PA(ek) = begin!(M, A, B); out net {|snd(M, B)|}ek PB(dk) = inp net {|snd(∃x : Public, B)|}dk−1[!begun(x,A,B)]; end(x,A,B)snd : (∃x : Public, ∃b : Public) → Auth(∃a : Public, . . .)[!begun(x, a, b)] Tags are not primitive in the pattern-matching spi-calculus, instead we can encode tags as public keypairs, and message tagging as encryption. We treat message tags (X → Auth(Y )) = ({Public}, {Public}) KP(X,Y ) We obtain the following derived typing rules for tagging: : X → Auth(Y ), M : (J ∪ {Tainted}) Top, (M, L) ∈ (X ,Y ) E, (M, L) ∈ (X ,Y ) E, (M) : J Auth(L) Signing Keys
A goal of this type system is to allow principals to have just one signing key, which can be used forany protocol, rather than requiring different signing key types for different protocols. Message tags arethen used to ensure the correctness of each protocol.
The type for a signing key is designed to support nested signatures, for example {|{|M|}esA|}esB is a message M signed by A (using her signing key esA : SigningEK(A)) and B (using his signingkey esB : SigningEK(B)). This signed message can be given type {|{|M|}esA|}esB : Secret as long asM : Secret(A, B, y) for some y, and can be given type {|{|M|}esA|}esB : Public as long as M : Public(A, B, y)for some y. This form of nested signing was not supported by [12, 13, 11].
SigningKT(L) = ( /0, {Public}) KT(∃x : Secret(L, y), ∃y) N : SigningEK(L), M : J Auth(L, L ) {|M|}N : J Auth(L ) E, M : Secret(L, L ) E, {|M|}N−1 : J Auth(L ) B x, E, M : Secret(L, x) E, {|M|}N−1 : J Top B These type rules are enough to verify the protocol in Section 5.1. A long version of this paper [14]contains a proof that this protocol is well-typed.
Public Encryption Keys
Public encryption is dual to signing: the encryption key is public, and the decryption key is kept secret.
One crucial difference is that although our type system supports nested uses of signatures, it does notsupport similar nested uses of public-key encryption. As a result, although we can support sign-then-encrypt, we cannot support encrypt-then-sign, due to the well-known problems with encrypt-then-signapplications (see, for instance, the analysis of the CCITT X.509 protocol in [6]).
PublicCryptoKT(L) = ({Public}, /0) KT(∃x : Secret(L), . . .) N : PublicCryptoEK(L), M : Secret(L) E, {|M|}N−1 : Un B The following example was not typable in previous Cryptyc systems: A begins! (M, A, B)A → B {|{|sec(M, B)|}esA|}epB B ends (M, A, B) It can now be typechecked using the types: esA : SigningEK(A)epB : PublicCryptoEK(B)sec : (∃x : Secret(a, b), ∃b : Public) → Auth(∃a : Public, . . .)[!begun(x, a, b)] This is very similar to the example in Section 5.1 except that now the message is a secret shared betweenA and B. A long version of this paper [14] contains a proof that this protocol type-checks.
Symmetric Keys
Symmetric cryptography is not primitive in pattern-matching spi-calculus, instead we encode it usingasymmetric cryptography: {M}N = {|M|}Enc(N); {X}N = {|X|}Enc(N); SymK(X) = ( /0, /0) KP(X, . . .) N : SymK(X ), M ∈ X These are the obvious analogues of the rules for encryption given in [12].
We can encode hashing as encryption with a hashing key, where the matching decryption key has beendiscarded.
#(M) = hash({|M|}ekH) where ekH : ({Public}, /0) EK(. . .) and hash : {|∃x : Secret(y)|}ekH → Auth(∃y) From this point on, we assume that each environment E is implicitly extended by the above type asser-tions for the special global names ekH and hash. We can then adapt the example from Section 5.1 toallow A to sign the message digest of M rather than signing the entire message: A begins! (M, A, B)A → B M, {|#(snd(B, M))|}esA B ends (M, A, B) This example uses the types which were introduced in previous examples, a full version is given in along version of this paper [14].
Conclusions and Further Work
In this paper, we have shown how pattern-matching types can be used to express complex data depen-dencies, in particular how they can be used to provide authenticity typings for nested uses of cryptog-raphy. This work shows that such types can be used to prove many-to-one correspondences; we expectthe extension to one-to-one correspondences to be fairly straightforward, although it will require somenotion of linear environment. We also hope to extend the attacker model, for example to cope with keycompromise.
Operational Semantics
Structural Process Equivalence, P ≡ Q:
P ≡ Q ⇒ Q ≡ P P ≡ Q, Q ≡ R ⇒ P ≡ R P ≡ Q ⇒ P | Q ≡ P | R P | 0 ≡ P
P | Q ≡ Q | P (P | Q) | R ≡ P | (Q | R) State Transition, ( ¯
B ::: Q):
A ::: (new n:T ; P) | Q) → ( ¯ A, n:T ::: P | Q) A ::: (begin!(M); P) | Q) → ( ¯ A, !begun(M) ::: P | Q) A, !begun(M) ::: (end(M); P) | Q) → ( ¯ A, !begun(M) ::: P | Q) A ::: (out L M{x←N} | inp L {x . M | ¯ A}; P) | Q) → ( ¯ A ::: P{x←N} | Q) Type System
Good Environment, E
Valid Assertions, E
A:
M : K Top, N : K Top M : (K, H) KP(X ) M : (K, H) KP(X ) Enc (M) : (K, H) EK(X) Dec (M) : (K, H) DK(X) Tainted ∈ K ∪ H−1E N : (K, H) EK(X ), (M, L) ∈ X J = (J − {Tainted}) ∪ (K − {Public}) N : (K, H) EK(X ), (M, L) ∈ X , M : J Top {|M|}N : J Auth(L) Left Rules, E, ¯
B:
fv(T ) ⊆ dom(E)E, M : U E, M : K Top, N : K Top E, (M, N) : K Top N : (K, H) DK(X ) E, (M, L) ∈ X E, decrypt(M, N) : J Auth(L) N : (K, H) DK(X ) x, E, (M, x) ∈ X (Tainted ∈ H ∪ K−1) ⇒ (x, E, M : J Top, x : Top E, decrypt(M, N) : J Top where decrypt(M, N) = Well-typed Processes, E
P:
Well-typed Computation States,
A ::: P:
References
1. M. Abadi. Secrecy by typing in security protocols. Journal of the ACM, 46(5):749–786, September 1999.
2. M. Abadi and B. Blanchet. Secrecy types for asymmetric communication. In Foundations of Software Science and Computation Structures, volume 2030 of Lecture Notes in Computer Science, pages 25–41. Springer, 2001.
3. M. Abadi and A.D. Gordon. A calculus for cryptographic protocols: The spi calculus. Information and Computation, 4. C. Bodei, M. Buchholtz, P. Degano, F. Nielson, and H. Riis Nielson. Automatic validation of protocol narration. In Proc. CSFW03, pages 126–140. IEEE Press, 2003.
5. D. Bolignano. An approach to the formal verification of cryptographic protocols. In Third ACM Conference on Computer and Communications Security, pages 106–118, 1996.
6. M. Burrows, M. Abadi, and R.M. Needham. A logic of authentication. Proceedings of the Royal Society of London A, 7. I. Cervesato. Typed MSR: Syntax and examples. In First International Workshop on Mathematical Methods, Models and Architectures for Computer Network Security, volume 2052 of Lecture Notes in Computer Science, pages 159–177.
Springer, 2001.
8. I. Cervesato, N. A. Durgin, P. D. Lincoln, J. C. Mitchell, and A. Scedrov. A meta-notation for protocol analysis. In Proc. IEEE Computer Security Foundations Workshop, pages 55–69, 1999.
9. E. Cohen. TAPS: A first-order verifier for cryptographic protocols. In 13th IEEE Computer Security Foundations Workshop, pages 144–158. IEEE Computer Society Press, 2000.
10. D. Dolev and A.C. Yao. On the security of public key protocols. IEEE Transactions on Information Theory, IT– 11. A. D. Gordon and A. S. A. Jeffrey. Typing one-to-one and one-to-many correspondences in security protocols. In Proc. Int. Software Security Symp., volume 2609 of Lecture Notes in Computer Science, pages 263–282. Springer-Verlag, 2002.
12. A.D. Gordon and A. Jeffrey. Authenticity by typing for security protocols. In 14th IEEE Computer Security Foundations Workshop, pages 145–159. IEEE Computer Society Press, 2001.
13. A.D. Gordon and A. Jeffrey. Types and effects for asymmetric cryptographic protocols. In 15th IEEE Computer Security Foundations Workshop, pages 77–91. IEEE Computer Society Press, 2002.
http://fpl.cs.depaul.edu/ajeffrey/fast04Long.pdf, 2004.
15. J. Heather. ‘Oh! . . . Is it really you?’ Using rank functions to verify authentication protocols. PhD thesis, Royal Holloway, 16. J. Heather and S. Schneider. Towards automatic verification of authentication protocols on an unbounded network. In 13th IEEE Computer Security Foundations Workshop, pages 132–143. IEEE Computer Society Press, 2000.
17. G. Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using CSP and FDR. In Tools and Algorithms for the Construction and Analysis of Systems, volume 1055 of Lecture Notes in Computer Science, pages 147–166.
Springer, 1996.
18. W. Marrero, E.M. Clarke, and S. Jha. Model checking for security protocols. In DIMACS Workshop on Design and Formal Verification of Security Protocols, 1997. Preliminary version appears as Technical Report TR–CMU–CS–97–139, Carnegie Mellon University, May 1997.
19. L.C. Paulson. The inductive approach to verifying cryptographic protocols. Journal of Computer Security, 6:85–128, 20. A.W. Roscoe. Modelling and verifying key-exchange protocols using CSP and FDR. In 8th IEEE Computer Security Foundations Workshop, pages 98–107. IEEE Computer Society Press, 1995.
21. S.A. Schneider. Verifying authentication protocols in CSP. IEEE Transactions on Software Engineering, 24(9):741–758, 22. F.J. Thayer F´abrega, J.C. Herzog, and J.D. Guttman. Strand spaces: Why is a security protocol correct? In IEEE Computer Society Symposium on Research in Security and Privacy, pages 160–171, 1998.
23. T.Y.C. Woo and S.S. Lam. A semantic model for authentication protocols. In IEEE Computer Society Symposium on Research in Security and Privacy, pages 178–194, 1993.

Source: http://www.christianhaack.eu/papers/papers/pattern-matching-spi.pdf