Change search
ReferencesLink to record
Permanent link

Direct link
Verification of security protocols with state in ProVerif: Avoiding false attacks when verifying freshness
KTH, School of Computer Science and Communication (CSC).
2015 (English)Independent thesis Advanced level (degree of Master (Two Years)), 20 credits / 30 HE creditsStudent thesisAlternative title
Verifiering av säkerhetsprotokoll med persistenta variabler i ProVerif : Att undvika falska attacker vid verifiering av att genererade nycklar är unika (Swedish)
Abstract [en]

One of the issues when attempting to verify security properties of a protocol is how to model the protocol. We introduce a method for verifying event freshness in tools which use the applied π-calculus and are able to verify secrecy. Event freshness can be used to prove that a protocol never generates the same key twice. In this work we encode state in the applied π-calculus and perform bounded verification of freshness for MiniDC by using the ProVerif tool. MiniDC is a trivial protocol that for each iteration of a loop generates a unique key and outputs it to a private channel. When verifying freshness, the abstractions of ProVerif cause false attacks. We describe methods which can be used to avoid false attacks that appear when verifying freshness. We show how to avoid some false attacks introduced by private channels, state and protocols that disclose their secret. We conclude that the method used to verify freshness in MiniDCis impractical to use in more complicated protocols with state.

Abstract [sv]

Ett av problemen som uppstår vid verifiering av säkerhetsprotokoll är hur protokoll ska modelleras. Vi introducerar en metod för att verifiera att skapde termer inte har använts förr. Denna metod kan användas i program som använder applicerad π-kalkyl som input och kan verifiera sekretess. I detta arbete visar vi hur protokoll med persistenta variabler kan modelleras i applicerad π-kalkyl. Vi verifierar även MiniDC för ett begränsat antal iterationer med hjälp av ProVerif. MiniDC är ett enkelt protokoll som för varje iteration av en loop skapar en nyckel och skickar den över en privat kanal. När man verifierar att skapade termer inte har använts förr så introducerar ProVerifs abstraktioner falska attacker. Vi beskriver metoder som kan användas för att undvika dessa falska attacker. Dessa metoder kan användas för falska attacker introducerade av privata kanaler, persistenta variabler eller protokoll som avslöjar sin krypteringsnyckel. Vår slutsats är att metoden som används för att verifiera MiniDC är opraktisk att använda i mer komplicerade protokoll med persistenta variabler.

Place, publisher, year, edition, pages
Keyword [en]
formal verification ProVerif state counter applied pi calculus freshness security protocols
National Category
Computer Science
URN: urn:nbn:se:kth:diva-172323OAI: diva2:846632
Educational program
Master of Science in Engineering - Computer Science and Technology
Available from: 2015-08-21 Created: 2015-08-17 Last updated: 2015-08-21Bibliographically approved

Open Access in DiVA

fulltext(893 kB)131 downloads
File information
File name FULLTEXT01.pdfFile size 893 kBChecksum SHA-512
Type fulltextMimetype application/pdf

By organisation
School of Computer Science and Communication (CSC)
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 131 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 109 hits
ReferencesLink to record
Permanent link

Direct link